Mercurial > hg > Gears > GearsAgda
changeset 941:aa28dc870715
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 15 Jun 2024 18:28:43 +0900 |
| parents | b2537fa14a75 |
| children | 49ac34a645ef |
| files | hoareBinaryTree2.agda |
| diffstat | 1 files changed, 133 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree2.agda Sat Jun 15 00:40:16 2024 +0900 +++ b/hoareBinaryTree2.agda Sat Jun 15 18:28:43 2024 +0900 @@ -1595,6 +1595,7 @@ suc (black-depth (PG.parent pg) ) ≡⟨ sym (proj1 (black-children-eq refl (cong proj1 (sym rb14)) (subst (λ k → RBtreeInvariant k) x₁ rb02))) ⟩ black-depth (node kg vg (PG.parent pg) (PG.uncle pg)) ≡⟨ cong black-depth (sym x₁) ⟩ black-depth (PG.grand pg) ∎ where open ≡-Reasoning + -- outer case, repl is not decomposed -- lt : key < kp -- x : PG.parent pg ≡ node kp vp (RBI.tree r) n1 -- x₁ : PG.grand pg ≡ node kg vg (PG.parent pg) (PG.uncle pg) @@ -1609,8 +1610,9 @@ ; treerb = rb02 ; replrb = rb10 ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) - ; state = rebuild (trans (cong color x₁) (cong proj1 (sym rb14))) rb17 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) rb11 + ; state = rebuild rb33 rb17 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) rb11 } rb15 where + -- inner case, repl is decomposed -- lt : kp < key -- x : PG.parent pg ≡ node kp vp n1 (RBI.tree r) -- x₁ : PG.grand pg ≡ node kg vg (PG.parent pg) (PG.uncle pg) @@ -1704,8 +1706,136 @@ suc (black-depth (PG.uncle pg)) ≡⟨ rb32 ⟩ black-depth (PG.grand pg) ∎ where open ≡-Reasoning - ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? - ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? + ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase52 where + insertCase52 : t + insertCase52 = next (PG.grand pg ∷ PG.rest pg) record { + tree = PG.grand pg + ; repl = rb01 + ; origti = RBI.origti r + ; origrb = RBI.origrb r + ; treerb = rb02 + ; replrb = ? + ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) + ; state = rebuild rb33 ? (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) ? + } rb15 where + -- inner case, repl is decomposed + -- lt : key < kp + -- x : PG.parent pg ≡ node kp vp (RBI.tree r) n1 + -- x₁ : PG.grand pg ≡ node kg vg (PG.uncle pg) (PG.parent pg) + -- eq : node rkey vr rp-left rp-right ≡ RBI.repl r + rb01 : bt (Color ∧ A) + rb01 = to-black (node rkey vr (to-red (node kg vg (PG.uncle pg) rp-left )) (node kp vp rp-right n1)) + rb04 : key < kp + rb04 = lt + rb21 : kg < key -- this can be a part of ParentGand relation + rb21 = si-property-> (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())) (subst (λ k → treeInvariant k ) x₁ (siToTreeinvariant _ _ _ _ (RBI.origti r) + (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)))) + (subst (λ k → stackInvariant key _ orig (PG.parent pg ∷ k ∷ PG.rest pg)) x₁ (popStackInvariant _ _ _ _ _ rb00)) + rb16 : color n1 ≡ Black + rb16 = proj2 (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)) + rb23 : vr ≡ ⟪ Red , proj2 vr ⟫ + rb23 with subst (λ k → color k ≡ Red ) (sym eq) repl-red + ... | refl = refl + rb20 : color rp-right ≡ Black + rb20 = proj2 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r) ) (cong proj1 rb23)) + rb03 : replacedRBTree key value (node kg _ (PG.uncle pg) (node kp _ (RBI.tree r) n1 )) + (node rkey ⟪ Black , proj2 vr ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) rp-left ) (node kp ⟪ Red , proj2 vp ⟫ rp-right n1 )) + rb03 = rbr-rotate-rl rp-left rp-right kg kp rkey rb20 ? ? + (subst (λ k → replacedRBTree key value (RBI.tree r) k) (trans (sym eq) (cong (λ k → node rkey k rp-left rp-right) rb23 )) rot ) + rb24 : ? -- node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r)) (PG.uncle pg) ≡ PG.grand pg + rb24 = ? -- trans (trans (cong₂ (λ j k → node kg j (node kp k n1 (RBI.tree r)) (PG.uncle pg)) rb14 rb13 ) (cong (λ k → node kg vg k (PG.uncle pg)) (sym x))) (sym x₁) + rb25 : ? -- node rkey ⟪ Black , proj2 vr ⟫ (node kp ⟪ Red , proj2 vp ⟫ n1 rp-left) (node kg ⟪ Red , proj2 vg ⟫ rp-right (PG.uncle pg)) ≡ rb01 + rb25 = ? -- begin + -- node rkey ⟪ Black , proj2 vr ⟫ (node kp ⟪ Red , proj2 vp ⟫ n1 rp-left) (node kg ⟪ Red , proj2 vg ⟫ rp-right (PG.uncle pg)) + -- ≡⟨ cong (λ k → node _ _ (node kp k n1 rp-left) _ ) rb13 ⟩ + -- node rkey ⟪ Black , proj2 vr ⟫ (node kp vp n1 rp-left) (node kg ⟪ Red , proj2 vg ⟫ rp-right (PG.uncle pg)) ≡⟨ refl ⟩ + -- rb01 ∎ where open ≡-Reasoning + rb11 : replacedRBTree key value (PG.grand pg) rb01 + rb11 = subst₂ (λ j k → replacedRBTree key value j k) rb24 rb25 rb03 + rb05 : RBtreeInvariant (PG.uncle pg) + rb05 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb02) + rb06 : RBtreeInvariant n1 + rb06 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x rb09) + rb26 : RBtreeInvariant rp-left + rb26 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r)) + rb28 : RBtreeInvariant rp-right + rb28 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r)) + rb31 : RBtreeInvariant (node rkey vr rp-left rp-right ) + rb31 = subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r) + rb18 : black-depth rp-right ≡ black-depth (PG.uncle pg) + rb18 = begin + black-depth rp-right ≡⟨ sym ( proj2 (red-children-eq1 (sym eq) repl-red (RBI.replrb r) )) ⟩ + black-depth (RBI.repl r) ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ + black-depth (RBI.tree r) ≡⟨ sym (proj1 (red-children-eq1 x pcolor rb09) ) ⟩ + black-depth (PG.parent pg) ≡⟨ sym (RBtreeEQ (subst (λ k → RBtreeInvariant k) x₁ rb02 )) ⟩ + black-depth (PG.uncle pg) ∎ where open ≡-Reasoning + rb27 : ? -- black-depth n1 ≡ black-depth rp-left + rb27 = ? -- begin + -- black-depth n1 ≡⟨ RBtreeEQ (subst (λ k → RBtreeInvariant k) x rb09) ⟩ + -- black-depth (RBI.tree r) ≡⟨ RB-repl→eq _ _ (RBI.treerb r) rot ⟩ + -- black-depth (RBI.repl r) ≡⟨ proj1 (red-children-eq1 (sym eq) repl-red (RBI.replrb r)) ⟩ + -- black-depth rp-left ∎ + -- where open ≡-Reasoning + -- rb19 : ? -- black-depth (node kp vp n1 rp-left) ≡ black-depth rp-right ⊔ black-depth (PG.uncle pg) + rb19 : black-depth (PG.uncle pg) ⊔ black-depth rp-left ≡ black-depth (node kp vp rp-right n1) + rb19 = ? -- begin + -- black-depth (node kp vp n1 rp-left) ≡⟨ black-depth-resp A (node kp vp n1 rp-left) (node kp vp rp-left rp-left) refl refl refl rb27 refl ⟩ + -- black-depth (node kp vp rp-left rp-left) ≡⟨ black-depth-resp A (node kp vp rp-left rp-left) (node rkey vr rp-left rp-right) + -- refl refl (trans (sym (cong proj1 rb13)) (sym (cong proj1 rb23))) refl (RBtreeEQ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r))) ⟩ + -- black-depth (node rkey vr rp-left rp-right) ≡⟨ black-depth-cong A eq ⟩ + -- black-depth (RBI.repl r) ≡⟨ proj2 (red-children-eq1 (sym eq) repl-red (RBI.replrb r)) ⟩ + -- black-depth rp-right ≡⟨ sym ( ⊔-idem _ ) ⟩ + -- black-depth rp-right ⊔ black-depth rp-right ≡⟨ cong (λ k → black-depth rp-right ⊔ k) rb18 ⟩ + -- black-depth rp-right ⊔ black-depth (PG.uncle pg) ∎ + -- where open ≡-Reasoning + rb29 : color n1 ≡ Black + rb29 = proj2 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) x rb09) (sym (cong proj1 rb13)) ) + rb30 : color rp-left ≡ Black + rb30 = proj1 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r)) (cong proj1 rb23)) + rb32 : suc (black-depth (PG.uncle pg)) ≡ black-depth (PG.grand pg) + rb32 = sym (proj1 ( black-children-eq1 x₁ rb33 rb02 )) + -- rb10 : RBtreeInvariant (node rkey ⟪ Black , proj2 vr ⟫ (node kp vp n1 rp-left) (node kg ⟪ Red , proj2 vg ⟫ rp-right (PG.uncle pg))) + -- rb10 = rb-black _ _ rb19 (rbi-from-red-black _ _ kp vp rb06 rb26 rb27 rb29 rb30 rb13) (rb-red _ _ rb20 uncle-black rb18 rb28 rb05) + 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 ? ? ? ) (rbi-from-red-black _ _ _ _ ? ? ? ? ? ? ) + 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 : ? -- suc (black-depth (node kp vp n1 rp-left) ⊔ (black-depth rp-right ⊔ black-depth (PG.uncle pg))) ≡ black-depth (PG.grand pg) + rb17 = ? -- begin + -- suc (black-depth (node kp vp n1 rp-left) ⊔ (black-depth rp-right ⊔ black-depth (PG.uncle pg))) ≡⟨ cong (λ k → suc (k ⊔ _)) rb19 ⟩ + -- suc ((black-depth rp-right ⊔ black-depth (PG.uncle pg)) ⊔ (black-depth rp-right ⊔ black-depth (PG.uncle pg))) ≡⟨ cong suc ( ⊔-idem _) ⟩ + -- suc (black-depth rp-right ⊔ black-depth (PG.uncle pg)) ≡⟨ cong (λ k → suc (k ⊔ _)) rb18 ⟩ + -- suc (black-depth (PG.uncle pg) ⊔ black-depth (PG.uncle pg)) ≡⟨ cong suc (⊔-idem _) ⟩ + -- suc (black-depth (PG.uncle pg)) ≡⟨ rb32 ⟩ + -- black-depth (PG.grand pg) ∎ + -- where open ≡-Reasoning + ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase52 where + insertCase52 : t + insertCase52 = next (PG.grand pg ∷ PG.rest pg) record { + tree = PG.grand pg + ; repl = rb01 + ; origti = RBI.origti r + ; origrb = RBI.origrb r + ; treerb = ? + ; replrb = ? + ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) + ; state = rebuild ? ? (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) ? + } rb15 where + -- outer case, repl is not decomposed + -- lt : kp < key + -- x : PG.parent pg ≡ node kp vp n1 (RBI.tree r) + -- x₁ : PG.grand pg ≡ node kg vg (PG.uncle pg) (PG.parent pg) + rb01 : bt (Color ∧ A) + 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 replaceRBP1 : t replaceRBP1 with RBI.state r ... | rebuild ceq bdepth-eq ¬leaf rot = rebuildCase ceq bdepth-eq ¬leaf rot