Mercurial > hg > Gears > GearsAgda
changeset 944:911900003d25
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 16 Jun 2024 12:08:48 +0900 |
| parents | 03857be39158 |
| children | 7310dc7f2437 |
| files | hoareBinaryTree2.agda |
| diffstat | 1 files changed, 51 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree2.agda Sun Jun 16 09:22:40 2024 +0900 +++ b/hoareBinaryTree2.agda Sun Jun 16 12:08:48 2024 +0900 @@ -1808,7 +1808,6 @@ rb32 = sym (proj1 ( black-children-eq1 x₁ rb33 rb02 )) rb10 : RBtreeInvariant (node rkey ⟪ Black , proj2 vr ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) rp-left ) (node kp vp rp-right n1) ) rb10 = rb-black _ _ rb19 (rb-red _ _ uncle-black rb30 rb18 rb05 rb26 ) (rbi-from-red-black _ _ _ _ rb28 rb06 rb27 rb20 rb16 rb13 ) - -- rb17 : ? -- suc (black-depth (node kp vp n1 rp-left) ⊔ (black-depth rp-right ⊔ black-depth (PG.uncle pg))) ≡ black-depth (PG.grand pg) rb17 : suc (black-depth (PG.uncle pg) ⊔ black-depth rp-left ⊔ black-depth (node kp vp rp-right n1)) ≡ black-depth (PG.grand pg) rb17 = begin suc (black-depth (PG.uncle pg) ⊔ black-depth rp-left ⊔ black-depth (node kp vp rp-right n1)) ≡⟨ cong (λ k → suc (_ ⊔ k)) (sym rb19) ⟩ @@ -1825,10 +1824,10 @@ ; repl = rb01 ; origti = RBI.origti r ; origrb = RBI.origrb r - ; treerb = ? - ; replrb = ? + ; treerb = rb02 + ; replrb = subst (λ k → RBtreeInvariant k) rb10 (rb-black _ _ rb18 (rb-red _ _ uncle-black rb16 rb19 rb05 rb06) (RBI.replrb r) ) ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) - ; state = rebuild ? ? (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) ? + ; state = rebuild rb33 rb17 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) rb11 } rb15 where -- outer case, repl is not decomposed -- lt : kp < key @@ -1838,6 +1837,54 @@ rb01 = to-black (node kp vp (to-red (node kg vg (PG.uncle pg) n1) )(node rkey vr rp-left rp-right)) rb04 : kp < key rb04 = lt + rb16 : color n1 ≡ Black + rb16 = proj1 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) x rb09) (trans (cong color (sym x)) pcolor)) + rb13 : ⟪ Red , proj2 vp ⟫ ≡ vp + rb13 with subst (λ k → color k ≡ Red ) x pcolor + ... | refl = refl + rb14 : ⟪ Black , proj2 vg ⟫ ≡ vg + rb14 with RBtreeParentColorBlack _ _ (subst (λ k → RBtreeInvariant k) x₁ rb02) (case2 pcolor) + ... | refl = refl + rb33 : color (PG.grand pg) ≡ Black + rb33 = subst (λ k → color k ≡ Black ) (sym x₁) (sym (cong proj1 rb14)) + rb03 : replacedRBTree key value (node kg _ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r) )) + (node kp ⟪ Black , proj2 vp ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) n1 ) repl ) + rb03 = rbr-rotate-rr repl-red rb04 rot + rb10 : node kp ⟪ Black , proj2 vp ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) n1 ) repl ≡ rb01 + rb10 = cong (λ k → node _ _ _ k ) (sym eq) + rb12 : node kg ⟪ Black , proj2 vg ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r)) ≡ PG.grand pg + rb12 = begin + node kg ⟪ Black , proj2 vg ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r)) + ≡⟨ cong₂ (λ j k → node kg j (PG.uncle pg) (node kp k n1 (RBI.tree r) ) ) rb14 rb13 ⟩ + node kg vg (PG.uncle pg) _ ≡⟨ cong (λ k → node _ _ _ k) (sym x) ⟩ + node kg vg (PG.uncle pg) (PG.parent pg) ≡⟨ sym x₁ ⟩ + PG.grand pg ∎ where open ≡-Reasoning + rb11 : replacedRBTree key value (PG.grand pg) rb01 + rb11 = subst₂ (λ j k → replacedRBTree key value j k) rb12 rb10 rb03 + rb05 : RBtreeInvariant (PG.uncle pg) + rb05 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb02) + rb06 : RBtreeInvariant n1 + rb06 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x rb09) + rb19 : black-depth (PG.uncle pg) ≡ black-depth n1 + rb19 = sym (trans (sym ( proj1 (red-children-eq x (sym (cong proj1 rb13)) rb09) )) (sym (RBtreeEQ (subst (λ k → RBtreeInvariant k) x₁ rb02)))) + rb18 : black-depth (PG.uncle pg) ⊔ black-depth n1 ≡ black-depth repl + rb18 = sym ( begin + black-depth repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ + black-depth (RBI.tree r) ≡⟨ sym ( RBtreeEQ (subst (λ k → RBtreeInvariant k) x rb09)) ⟩ + black-depth n1 ≡⟨ sym (⊔-idem (black-depth n1)) ⟩ + black-depth n1 ⊔ black-depth n1 ≡⟨ cong (λ k → k ⊔ _) (sym rb19) ⟩ + black-depth (PG.uncle pg) ⊔ black-depth n1 ∎ ) where open ≡-Reasoning + -- suc (black-depth (node rkey vr rp-left rp-right) ⊔ (black-depth n1 ⊔ black-depth (PG.uncle pg))) ≡ black-depth (PG.grand pg) + rb17 : suc (black-depth (PG.uncle pg) ⊔ black-depth n1 ⊔ black-depth (node rkey vr rp-left rp-right)) ≡ black-depth (PG.grand pg) + rb17 = begin + suc (black-depth (PG.uncle pg) ⊔ black-depth n1 ⊔ black-depth (node rkey vr rp-left rp-right)) + ≡⟨ cong₂ (λ j k → suc (j ⊔ black-depth k)) rb18 eq ⟩ + suc (black-depth repl ⊔ black-depth repl) ≡⟨ ⊔-idem _ ⟩ + suc (black-depth repl ) ≡⟨ cong suc (sym (RB-repl→eq _ _ (RBI.treerb r) rot)) ⟩ + suc (black-depth (RBI.tree r) ) ≡⟨ cong suc (sym (proj2 (red-children-eq x (cong proj1 (sym rb13)) rb09))) ⟩ + suc (black-depth (PG.parent pg) ) ≡⟨ sym (proj2 (black-children-eq refl (cong proj1 (sym rb14)) (subst (λ k → RBtreeInvariant k) x₁ rb02))) ⟩ + black-depth (node kg vg (PG.uncle pg) (PG.parent pg)) ≡⟨ cong black-depth (sym x₁) ⟩ + black-depth (PG.grand pg) ∎ where open ≡-Reasoning replaceRBP1 : t replaceRBP1 with RBI.state r ... | rebuild ceq bdepth-eq ¬leaf rot = rebuildCase ceq bdepth-eq ¬leaf rot