Mercurial > hg > Gears > GearsAgda
changeset 910:e587d7a1634f
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 02 Jun 2024 03:36:07 +0900 |
| parents | 15a47dd48d8e |
| children | ce13b8ffc4dd |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 56 insertions(+), 23 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Sat Jun 01 20:35:37 2024 +0900 +++ b/hoareBinaryTree1.agda Sun Jun 02 03:36:07 2024 +0900 @@ -1912,33 +1912,66 @@ ; si = s-nil ; state = top-black refl (case2 (rbr-black-right repl-red c (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) rot))) } + rebuildCase : (tr0 : bt (Color ∧ A)) → tr0 ≡ orig + → (ceq : color (RBI.tree r) ≡ color repl) + → (bdepth-eq : black-depth repl ≡ black-depth (RBI.tree r)) + → (rot : replacedRBTree key value (RBI.tree r) repl ) → t + rebuildCase tr0 eq ceq bdepth-eq rot with stackToPG (RBI.tree r) orig stack (RBI.si r) + ... | case1 x = exit repl stack x r where -- single node case + rb00 : stack ≡ orig ∷ [] → orig ≡ RBI.tree r + rb00 refl = si-property1 (RBI.si r) + ... | case2 (case1 x) = insertCase12 orig refl x rot (case2 ceq) (RBI.si r) -- one level stack, orig is parent of repl + ... | case2 (case2 pg) = rebuildCase1 pg where + rb00 : (pg : PG (Color ∧ A) (RBI.tree r) stack) → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) + rb00 pg = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r) + treerb : (pg : PG (Color ∧ A) (RBI.tree r) stack) → RBtreeInvariant (PG.parent pg) + treerb pg = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (rb00 pg)) + rb08 : (pg : PG (Color ∧ A) (RBI.tree r) stack) → treeInvariant (PG.parent pg) + 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₁ = next rb01 (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record { + tree = PG.parent pg + ; ¬leaf = subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ()) + ; 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 → 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 + 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 n1 (RBI.tree r)) + rb05 = subst (λ k → treeInvariant k) x (rb08 pg) + rb04 : kp < key + rb04 = si-property-> (RBI.¬leaf r) 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)) + rb07 ⟪ Black , proj4 ⟫ = cong (λ k → suc (black-depth n1 ⊔ k)) bdepth-eq + rb07 ⟪ Red , proj4 ⟫ = cong (λ k → (black-depth n1 ⊔ k)) bdepth-eq replaceRBP1 : t replaceRBP1 with RBI.state r - ... | rebuild ceq bdepth-eq rot = rebuildCase orig refl where -- rebuildRBT key value orig repl stack r bdepth-eq next exit - rebuildCase : (tr0 : bt (Color ∧ A)) → tr0 ≡ orig → t - rebuildCase tr0 eq with stackToPG (RBI.tree r) orig stack (RBI.si r) - ... | case1 x = exit repl stack x r where -- single node case - rb00 : stack ≡ orig ∷ [] → orig ≡ RBI.tree r - rb00 refl = si-property1 (RBI.si r) - ... | case2 (case1 x) = insertCase12 orig refl x rot (case2 ceq) (RBI.si r) -- one level stack, orig is parent of repl - ... | case2 (case2 pg) = next ? (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record { - tree = PG.parent pg - ; ¬leaf = ? - ; origti = RBI.origti r - ; origrb = RBI.origrb r - ; treerb = ? - ; replrb = ? - ; si = popStackInvariant _ _ _ _ _ rb00 - ; state = rebuild ? ? ? - } ? 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) - ... | top-black eq rot = {!!} - ... | rotate repl-red pdepth< rot with stackToPG (RBI.tree r) orig stack (RBI.si r) + ... | rebuild ceq bdepth-eq rot = rebuildCase orig refl ceq bdepth-eq rot + ... | top-black eq rot = exit repl stack ? r + ... | rotate repl-red pdepth-eq rot with stackToPG (RBI.tree r) orig stack (RBI.si r) ... | case1 eq = exit repl stack eq r -- no stack, replace top node - ... | case2 (case1 eq) = insertCase12 orig refl eq rot ? (RBI.si r) -- one level stack, orig is parent of repl + ... | case2 (case1 eq) = insertCase12 orig refl eq rot (case1 repl-red) (RBI.si r) -- one level stack, orig is parent of repl ... | case2 (case2 pg) with color (PG.parent pg) in pcolor - ... | Black = ? -- rebuildRBT key value orig ? ? ? ? next exit where -- insertCase1 -- parent is Black + ... | Black = rebuildCase orig refl ? pdepth-eq rot where + rb00 : color (RBI.tree r) ≡ color repl -- we cannot prove this + rb00 = black-children-color (RBI.origrb r) rot ... | Red with PG.uncle pg in uneq ... | leaf = {!!} -- insertCase5 ... | node key₁ ⟪ Black , value₁ ⟫ t₁ t₂ = {!!} -- insertCase5