Mercurial > hg > Gears > GearsAgda

changeset 899:58954abea83e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 30 May 2024 08:06:22 +0900
parents e5ac221866c5
children 2fea300378ca
files hoareBinaryTree1.agda
diffstat 1 files changed, 45 insertions(+), 35 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Wed May 29 21:31:02 2024 +0900
+++ b/hoareBinaryTree1.agda	Thu May 30 08:06:22 2024 +0900
@@ -1566,47 +1566,54 @@
 ... | s2-s12p refl refl = ⟪ (λ () ) , ( λ () ) ⟫
 ... | s2-1s2p refl refl = ⟪ (λ () ) , ( λ () ) ⟫
 
-
-stackCase2 : {n : Level} {A : Set n} → (rest : List ( bt (Color ∧ A)))
-           → ( tree parent grand orig : bt (Color ∧ A)) →  (key : ℕ)
-           → stackInvariant key tree  orig ( tree ∷ parent ∷ grand ∷ rest )
-           → stackInvariant key grand orig (grand ∷ rest )
-stackCase2 rest tree parent grand orig key (s-right .tree .orig tree₁ x si) = sc01 sc00 where
-     sc00 : stackInvariant key parent orig (parent ∷ grand ∷ rest )
+popStackInvariant : {n : Level} {A : Set n} → (rest : List ( bt (Color ∧ A)))
+           → ( tree parent orig : bt (Color ∧ A)) →  (key : ℕ)
+           → stackInvariant key tree  orig ( tree ∷ parent ∷ rest )
+           → stackInvariant key parent orig (parent ∷ rest )
+popStackInvariant rest tree parent orig key (s-right .tree .orig tree₁ x si) = sc00 where
+     sc00 : stackInvariant key parent orig (parent ∷ rest )
      sc00 with si-property1 si
      ... | refl = si
-     sc01 : stackInvariant key parent orig (parent ∷ grand ∷ rest ) → stackInvariant key grand orig (grand ∷ rest )
-     sc01 (s-right .parent .orig tree₁ x si2) with si-property1 si2
-     ... | refl = si2
-     sc01 (s-left .parent .orig tree x si2) with si-property1 si2
-     ... | refl = si2
-stackCase2 rest tree parent grand orig key (s-left .tree .orig tree₁ x si) = sc01 sc00 where
-     sc00 : stackInvariant key parent orig (parent ∷ grand ∷ rest )
+popStackInvariant rest tree parent orig key (s-left .tree .orig tree₁ x si) = sc00 where
+     sc00 : stackInvariant key parent orig (parent ∷ rest )
      sc00 with si-property1 si
      ... | refl = si
-     sc01 : stackInvariant key parent orig (parent ∷ grand ∷ rest ) → stackInvariant key grand orig (grand ∷ rest )
-     sc01 (s-right .parent .orig tree₁ x si2) with si-property1 si2
-     ... | refl = si2
-     sc01 (s-left .parent .orig tree x si2) with si-property1 si2
-     ... | refl = si2
+
 
-stackCase3 : {n : Level} {A : Set n} → (rest : List ( bt (Color ∧ A)))
+siToTreeinvariant : {n : Level} {A : Set n} → (rest : List ( bt (Color ∧ A)))
            → ( tree orig : bt (Color ∧ A)) →  (key : ℕ)
            → treeInvariant orig
            → stackInvariant key tree  orig ( tree ∷ rest )
            → treeInvariant tree 
-stackCase3 .[] tree .tree key ti s-nil = ti
-stackCase3 .(node _ _ leaf leaf ∷ []) .leaf .(node _ _ leaf leaf) key (t-single _ _) (s-right .leaf .(node _ _ leaf leaf) .leaf x s-nil) = t-leaf
-stackCase3 .(node _ _ leaf (node key₁ _ _ _) ∷ []) .(node key₁ _ _ _) .(node _ _ leaf (node key₁ _ _ _)) key (t-right _ key₁ x₁ x₂ x₃ ti) (s-right .(node key₁ _ _ _) .(node _ _ leaf (node key₁ _ _ _)) .leaf x s-nil) = ti
-stackCase3 .(node _ _ (node key₁ _ _ _) leaf ∷ []) .leaf .(node _ _ (node key₁ _ _ _) leaf) key (t-left key₁ _ x₁ x₂ x₃ ti) (s-right .leaf .(node _ _ (node key₁ _ _ _) leaf) .(node key₁ _ _ _) x s-nil) = t-leaf
-stackCase3 .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _) ∷ []) .(node key₂ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) key (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node key₂ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) .(node key₁ _ _ _) x s-nil) = ti₁
-stackCase3 .(node _ _ tree₁ tree ∷ _) tree orig key ti (s-right .tree .orig tree₁ x si2@(s-right .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) with stackCase3 _ _ _ _ ti si2
+siToTreeinvariant .[] tree .tree key ti s-nil = ti
+siToTreeinvariant .(node _ _ leaf leaf ∷ []) .leaf .(node _ _ leaf leaf) key (t-single _ _) (s-right .leaf .(node _ _ leaf leaf) .leaf x s-nil) = t-leaf
+siToTreeinvariant .(node _ _ leaf (node key₁ _ _ _) ∷ []) .(node key₁ _ _ _) .(node _ _ leaf (node key₁ _ _ _)) key (t-right _ key₁ x₁ x₂ x₃ ti) (s-right .(node key₁ _ _ _) .(node _ _ leaf (node key₁ _ _ _)) .leaf x s-nil) = ti
+siToTreeinvariant .(node _ _ (node key₁ _ _ _) leaf ∷ []) .leaf .(node _ _ (node key₁ _ _ _) leaf) key (t-left key₁ _ x₁ x₂ x₃ ti) (s-right .leaf .(node _ _ (node key₁ _ _ _) leaf) .(node key₁ _ _ _) x s-nil) = t-leaf
+siToTreeinvariant .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _) ∷ []) .(node key₂ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) key (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node key₂ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) .(node key₁ _ _ _) x s-nil) = ti₁
+siToTreeinvariant .(node _ _ tree₁ tree ∷ _) tree orig key ti (s-right .tree .orig tree₁ x si2@(s-right .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2
+... | t-single _ _ = t-leaf
+... | t-right _ key₁ x₂ x₃ x₄ ti₁ = ti₁
+... | t-left key₁ _ x₂ x₃ x₄ ti₁ = t-leaf
+... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ ti₁ ti₂ = ti₂
+siToTreeinvariant .(node _ _ tree₁ tree ∷ _) tree orig key ti (s-right .tree .orig tree₁ x si2@(s-left .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2
 ... | t-single _ _ = t-leaf
 ... | t-right _ key₁ x₂ x₃ x₄ ti₁ = ti₁
 ... | t-left key₁ _ x₂ x₃ x₄ ti₁ = t-leaf
 ... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ ti₁ ti₂ = ti₂
-stackCase3 .(node _ _ tree₁ tree ∷ _) tree orig key ti (s-right .tree .orig tree₁ x si2@(s-left .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) = ?
-stackCase3 rest tree orig key ti (s-left .tree .orig tree₁ x si) = ?
+siToTreeinvariant .(node _ _ leaf leaf ∷ []) .leaf .(node _ _ leaf leaf) key (t-single _ _) (s-left .leaf .(node _ _ leaf leaf) .leaf x s-nil) = t-leaf
+siToTreeinvariant .(node _ _ leaf (node key₁ _ _ _) ∷ []) .leaf .(node _ _ leaf (node key₁ _ _ _)) key (t-right _ key₁ x₁ x₂ x₃ ti) (s-left .leaf .(node _ _ leaf (node key₁ _ _ _)) .(node key₁ _ _ _) x s-nil) = t-leaf
+siToTreeinvariant .(node _ _ (node key₁ _ _ _) leaf ∷ []) .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) leaf) key (t-left key₁ _ x₁ x₂ x₃ ti) (s-left .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) leaf) .leaf x s-nil) = ti
+siToTreeinvariant .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _) ∷ []) .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) key (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-left .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) .(node key₂ _ _ _) x s-nil) = ti
+siToTreeinvariant .(node _ _ tree tree₁ ∷ _) tree orig key ti (s-left .tree .orig tree₁ x si2@(s-right .(node _ _ tree tree₁) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2
+... | t-single _ _ = t-leaf
+... | t-right _ key₁ x₂ x₃ x₄ t = t-leaf
+... | t-left key₁ _ x₂ x₃ x₄ t = t
+... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ t t₁ = t
+siToTreeinvariant .(node _ _ tree tree₁ ∷ _) tree orig key ti (s-left .tree .orig tree₁ x si2@(s-left .(node _ _ tree tree₁) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2
+... | t-single _ _ = t-leaf
+... | t-right _ key₁ x₂ x₃ x₄ t = t-leaf
+... | t-left key₁ _ x₂ x₃ x₄ t = t
+... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ t t₁ = t
 
 PGtoRBinvariant1 : {n : Level} {A : Set n} 
            → (tree orig : bt (Color ∧ A) )
@@ -1811,10 +1818,9 @@
          black-depth right ≡⟨ (sym (RBtreeEQ (RBI.origrb r))) ⟩
          black-depth left ∎
             where open ≡-Reasoning  
-... | case2 (case2 pg) with (PG.parent pg) in preq
-... | leaf = {!!} -- can't happen
-... | node kp ⟪ Black , vp₁ ⟫ t₁ t₂ = ?  -- insertCase1 -- parent is Black 
-... | node kp ⟪ Red , vp₁ ⟫ t₁₁ t₁₂ with PG.uncle pg in uneq
+... | case2 (case2 pg) with color (PG.parent pg) in pcolor
+... | Black = ?  -- insertCase1 -- parent is Black 
+... | Red with PG.uncle pg in uneq
 ... | leaf = {!!} -- insertCase5
 ... | node key₁ ⟪ Black , value₁ ⟫ t₁ t₂ = {!!} -- insertCase5
 ... | node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ with PG.pg pg
@@ -1825,13 +1831,13 @@
          ; origrb = RBI.origrb r
          ; treerb = rb01
          ; replrb = rb-red _ _ refl (RBtreeToBlackColor _ rb02) ? (rb-black _ _ ? (RBI.replrb r) rb04) (RBtreeToBlack _ rb02)
-         ; si = stackCase2 (PG.rest pg) (RBI.tree r) (PG.parent pg) (PG.grand pg) orig _  rb00
+         ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
          ; state = rotate refl ? (subst₂ (λ j k → replacedRBTree key value j k ) (sym ?) refl  (rbr-flip-ll repl-red (rb05 refl uneq) ? rot))
      }  ? where
        rb00 : stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg)
        rb00 = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r)
        rb01 :  RBtreeInvariant (PG.grand pg)
-       rb01 = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (stackCase2 (PG.rest pg) (RBI.tree r) (PG.parent pg) (PG.grand pg) orig _  rb00)
+       rb01 = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00))
        rb02 : RBtreeInvariant (PG.uncle pg)
        rb02 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01)
        rb03 : RBtreeInvariant (PG.parent pg)
@@ -1840,8 +1846,12 @@
        rb04 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x rb03)
        rb05 : { tree : bt (Color ∧ A) } → tree ≡ PG.uncle pg → tree ≡ node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ → color (PG.uncle pg) ≡ Red
        rb05 refl refl = refl
+       rb08 : treeInvariant (PG.parent pg)
+       rb08 = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00)
+       rb07 : treeInvariant (node kp vp (RBI.tree r) n1)
+       rb07 = ?
        rb06 : key < kp
-       rb06 = si-property-< ? ? ?
+       rb06 = si-property-< ? rb07 (subst (λ k → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ k ∷ PG.grand pg ∷ PG.rest pg)) x rb00)
 ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
 ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
 ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}