Mercurial > hg > Gears > GearsAgda

changeset 925:9a67eb8e71ac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reintroducing child-replaced
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 08 Jun 2024 07:46:23 +0900
parents 69aab3105ac4
children 9936101bc974
files hoareBinaryTree1.agda
diffstat 1 files changed, 43 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Fri Jun 07 17:36:01 2024 +0900
+++ b/hoareBinaryTree1.agda	Sat Jun 08 07:46:23 2024 +0900
@@ -947,6 +947,7 @@
 
 data RBI-state  {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree repl : bt (Color ∧ A) ) → (stak : List (bt (Color ∧ A))) → Set n where
    rebuild : {tree repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → color tree ≡ color repl → black-depth repl ≡ black-depth tree
+       → ¬ ( tree ≡ leaf) 
        → (rotated : replacedRBTree key value tree repl)
        → RBI-state key value tree repl stack  -- one stage up
    rotate  : {tree repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → color repl ≡ Red → black-depth repl ≡ black-depth tree
@@ -1768,7 +1769,7 @@
          ; treerb = rbi
          ; replrb = crbt03 value₁ rbi
          ; si = si
-         ; state = rebuild refl (crbt01 value₁ ) crbt04
+         ; state = rebuild refl (crbt01 value₁ ) (λ ()) crbt04
          }  where 
              crbt01 : (value₁ : Color ∧ A) → black-depth (node key₁ ⟪ proj1 value₁ , value ⟫ left right) ≡ black-depth (node key₁ value₁ left right)
              crbt01 ⟪ Red , proj4 ⟫ = refl
@@ -1803,7 +1804,7 @@
          ; treerb = treerb
          ; replrb = crbt03 value₁ treerb
          ; si = si
-         ; state = rebuild refl (crbt01 value₁ ) crbt04
+         ; state = rebuild refl (crbt01 value₁ ) (λ ()) crbt04
          }  where 
              crbt01 : (value₁ : Color ∧ A) → black-depth (node key₁ ⟪ proj1 value₁ , value ⟫ left right) ≡ black-depth (node key₁ value₁ left right)
              crbt01 ⟪ Red , proj4 ⟫ = refl
@@ -1937,8 +1938,9 @@
          }
     rebuildCase : (ceq : color (RBI.tree r) ≡ color repl)
        → (bdepth-eq : black-depth repl ≡ black-depth (RBI.tree r))
+       → (¬ RBI.tree r ≡ leaf)
        → (rot       : replacedRBTree key value (RBI.tree r) repl ) → t
-    rebuildCase ceq bdepth-eq rot with stackToPG (RBI.tree r) orig stack (RBI.si r)
+    rebuildCase ceq bdepth-eq ¬leaf rot with stackToPG (RBI.tree r) orig stack (RBI.si r)
     ... | case1 x = exit stack x r  where  -- single node case
         rb00 : stack ≡ orig ∷ [] → orig ≡ RBI.tree r
         rb00 refl = si-property1 (RBI.si r)
@@ -1952,15 +1954,9 @@
        rb08 pg = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (rb00 pg))
        rebuildCase1 : (PG (Color ∧ A) (RBI.tree r) stack) → t
        rebuildCase1 pg with PG.pg pg
-       ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ?
-       ... | 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₁ = rebuildCase2 where
+       ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = rebuildCase2 where
           rebuildCase2 : t
-          rebuildCase2 with <-cmp key kp
-          ... | tri< a ¬b ¬c = ?
-          ... | tri≈ ¬a b ¬c  = ⊥-elim ( si-property-pne _ _ stack (trans (PG.stack=gp pg) (cong (λ k → _ ∷ k ∷ _) x) ) (RBI.si r) b ) -- can't happen
-          ... | tri> ¬a ¬b c = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
+          rebuildCase2 = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
               tree = PG.parent pg
               ; repl = rb01
               ; origti = RBI.origti r
@@ -1968,7 +1964,38 @@
               ; treerb = treerb pg
               ; replrb = rb02
               ; si = popStackInvariant _ _ _ _ _ (rb00 pg)
-              ; state = rebuild (cong color x) rb06 (subst (λ k → replacedRBTree key value k rb01) (sym x) (rbr-right ceq rb04 rot))
+              ; state = rebuild (cong color x) rb06 ? ? -- (subst (λ k → replacedRBTree key value k rb01) (sym x) (rbr-right ceq rb04 rot))
+             } (subst₂ (λ j k → j < length k ) refl (sym (PG.stack=gp pg)) ≤-refl) where
+               rb01 : bt (Color ∧ A)
+               rb01 = node kp vp repl n1 
+               rb03 : black-depth n1 ≡ black-depth repl
+               rb03 = ? -- trans (RBtreeEQ (subst (λ k → RBtreeInvariant k) x (treerb pg))) ((RB-repl→eq _ _ (RBI.treerb r) rot))
+               rb02 : RBtreeInvariant rb01
+               rb02 with subst (λ k → RBtreeInvariant k) x (treerb pg)
+               ... | rb-red .kp value cx cx₁ ex₂ t t₁ = ? -- rb-red kp value cx (trans (sym ceq) cx₁) rb03 t (RBI.replrb r)
+               ... | rb-black .kp value ex t t₁ = ? -- rb-black kp value rb03 t (RBI.replrb r)
+               rb05 : treeInvariant (node kp vp (RBI.tree r) n1 )
+               rb05 = subst (λ k → treeInvariant k) x (rb08 pg)
+               rb10 : ¬ RBI.tree r ≡ leaf → key < kp
+               rb10 notl = si-property-< notl rb05 (subst (λ k → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ k ∷ PG.grand pg ∷ PG.rest pg)) x (rb00 pg))
+               rb06 : black-depth rb01 ≡ black-depth (PG.parent pg)
+               rb06 = ? where -- trans (rb07 vp) ( cong black-depth (sym x) ) where
+                   rb07 : (vp : Color ∧ A) → black-depth (node kp vp n1 repl) ≡ black-depth (node kp vp n1 (RBI.tree r))
+                   rb07 ⟪ Black  , proj4 ⟫ = cong (λ k → suc (black-depth n1 ⊔ k)) bdepth-eq
+                   rb07 ⟪ Red  , proj4 ⟫ = cong (λ k → (black-depth n1 ⊔ k)) bdepth-eq
+       ... | 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₁ = rebuildCase2 where
+          rebuildCase2 : t
+          rebuildCase2 = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record {
+              tree = PG.parent pg
+              ; repl = rb01
+              ; origti = RBI.origti r
+              ; origrb = RBI.origrb r
+              ; treerb = treerb pg
+              ; replrb = rb02
+              ; si = popStackInvariant _ _ _ _ _ (rb00 pg)
+              ; state = rebuild (cong color x) rb06 (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())) (subst (λ k → replacedRBTree key value k rb01) (sym x) (rbr-right ceq rb04 rot))
              } (subst₂ (λ j k → j < length k ) refl (sym (PG.stack=gp pg)) ≤-refl) where
                rb01 : bt (Color ∧ A)
                rb01 = node kp vp n1 repl
@@ -1981,7 +2008,7 @@
                rb05 : treeInvariant (node kp vp n1 (RBI.tree r))
                rb05 = subst (λ k → treeInvariant k) x (rb08 pg)
                rb04 : kp < key
-               rb04 = c
+               rb04 = si-property-> ¬leaf rb05 (subst (λ k → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ k ∷ PG.grand pg ∷ PG.rest pg)) x (rb00 pg))
                rb06 : black-depth rb01 ≡ black-depth (PG.parent pg)
                rb06 = trans (rb07 vp) ( cong black-depth (sym x) ) where
                    rb07 : (vp : Color ∧ A) → black-depth (node kp vp n1 repl) ≡ black-depth (node kp vp n1 (RBI.tree r))
@@ -2027,7 +2054,7 @@
             ; treerb = rb02
             ; replrb = subst (λ k → RBtreeInvariant k) rb10 (rb-black _ _ rb18 (RBI.replrb r) (rb-red _ _ rb16 uncle-black rb19 rb06 rb05))
             ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)
-            ; state = rebuild (trans (cong color x₁) (cong proj1 (sym rb14))) rb17 rb11
+            ; state = rebuild (trans (cong color x₁) (cong proj1 (sym rb14))) rb17 ? rb11
            } rb15 where
             -- x₁ : PG.grand pg ≡ node kg vg (PG.parent pg) (PG.uncle pg)
             -- x  : PG.parent pg ≡ node kp vp (RBI.tree r) n1
@@ -2092,7 +2119,7 @@
 
     replaceRBP1 : t
     replaceRBP1 with RBI.state r
-    ... | rebuild ceq bdepth-eq rot = rebuildCase ceq bdepth-eq rot
+    ... | rebuild ceq bdepth-eq ¬leaf rot = rebuildCase ceq bdepth-eq ¬leaf rot
     ... | top-black eq rot = exit stack (trans eq (cong (λ k → k ∷ []) rb00)) r where
         rb00 : RBI.tree r ≡ orig
         rb00 with si-property-last _ _ _ _ (subst (λ k → stackInvariant key (RBI.tree r) orig k) (eq) (RBI.si r))
@@ -2120,7 +2147,7 @@
             ; treerb = treerb pg
             ; replrb = rb06
             ; si = popStackInvariant _ _ _ _ _ (rb00 pg)
-            ; state = rebuild (cong color x)  (rb05 (trans (sym (cong color x)) pcolor))
+            ; state = rebuild (cong color x)  (rb05 (trans (sym (cong color x)) pcolor)) (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ()))
                 (subst (λ k → replacedRBTree key value k (node kp vp repl n1) ) (sym x) (rb02 rb04 ))
            } (subst₂ (λ j k → j < length k ) refl (sym (PG.stack=gp pg)) ≤-refl) where
             rb01 : bt (Color ∧ A)