Mercurial > hg > Gears > GearsAgda

changeset 912:e4a185896b7e

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 Sun, 02 Jun 2024 13:44:30 +0900
parents ce13b8ffc4dd
children f2b78b3a5fb2
files hoareBinaryTree1.agda
diffstat 1 files changed, 23 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Sun Jun 02 12:29:26 2024 +0900
+++ b/hoareBinaryTree1.agda	Sun Jun 02 13:44:30 2024 +0900
@@ -1989,18 +1989,35 @@
             ; treerb = treerb pg
             ; replrb = ?
             ; si = popStackInvariant _ _ _ _ _ (rb00 pg)
-            ; state = rebuild ? rb05 (subst (λ k → replacedRBTree key value k (node kp vp repl n1) ) (sym x) (rb02 rb04 ))
-           } ? where
+            ; state = rebuild (cong color x)  (rb05 (trans (sym (cong color x)) pcolor)) 
+                (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)
             rb01 = node kp vp repl n1
             rb03 : key < kp
-            rb03 = ?
+            rb03 = si-property-< (RBI.¬leaf r) (subst (λ k → treeInvariant k) x (rb08 pg)) (subst (λ k → stackInvariant key (RBI.tree r) orig 
+              (RBI.tree r ∷ k ∷ PG.grand pg ∷ PG.rest pg)) x (rb00 pg))
             rb04 :  ⟪ Black , proj2 vp ⟫ ≡ vp
-            rb04 = ?
+            rb04 with subst (λ k → color k ≡ Black) x pcolor
+            ... | refl = refl
             rb02 : ⟪ Black , proj2 vp ⟫ ≡ vp → replacedRBTree key value (node kp vp (RBI.tree r) n1) (node kp vp repl n1)
             rb02 eq = subst (λ k → replacedRBTree key value (node kp k (RBI.tree r) n1) (node kp k repl n1)) eq (rbr-black-left repl-red rb03 rot )
-            rb05 : black-depth rb01 ≡ black-depth (PG.parent pg)
-            rb05 = ?
+            rb07 : black-depth repl ≡ black-depth n1
+            rb07 = begin 
+               black-depth repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩
+               black-depth (RBI.tree r) ≡⟨ RBtreeEQ (subst (λ k → RBtreeInvariant k) x (treerb pg)) ⟩
+               black-depth n1 ∎
+                 where open ≡-Reasoning
+            rb05 : proj1 vp ≡ Black → black-depth rb01 ≡ black-depth (PG.parent pg)
+            rb05 refl = begin
+               suc (black-depth repl ⊔ black-depth n1) ≡⟨ cong suc (cong (λ k → k ⊔ black-depth n1) pdepth-eq) ⟩
+               suc (black-depth (RBI.tree r) ⊔ black-depth n1) ≡⟨ refl ⟩
+               black-depth (node kp vp (RBI.tree r) n1) ≡⟨ cong black-depth (sym x) ⟩
+               black-depth (PG.parent pg) ∎
+                 where open ≡-Reasoning
+            rb06 : RBtreeInvariant rb01
+            rb06 = subst (λ k → RBtreeInvariant (node kp k repl n1))  rb04 
+               ( rb-black _ _ rb07 (RBI.replrb r) (RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x (treerb pg))))
        ... | 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₁ = ?