Mercurial > hg > Gears > GearsAgda
changeset 929:5ca6182c1029
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 08 Jun 2024 20:15:19 +0900 |
| parents | 79d7e2a87f08 |
| children | 65664560f055 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 67 insertions(+), 18 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Sat Jun 08 16:10:41 2024 +0900 +++ b/hoareBinaryTree1.agda Sat Jun 08 20:15:19 2024 +0900 @@ -1981,27 +1981,83 @@ ; 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 → ¬ (k ≡ leaf)) (sym x) (λ ())) (subst (λ k → replacedRBTree key value k rb01) (sym x) (rbr-left 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)) + rb03 = trans (sym (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) + ... | rb-red .kp value cx cx₁ ex₂ t t₁ = rb-red kp value (trans (sym ceq) cx) cx₁ (sym rb03) (RBI.replrb r) t₁ + ... | rb-black .kp value ex t t₁ = rb-black kp value (sym rb03) (RBI.replrb r) t₁ 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)) + rb04 : key < kp + rb04 = lt rb06 : black-depth rb01 ≡ black-depth (PG.parent pg) - rb06 = ? where -- trans (rb07 vp) ( cong black-depth (sym x) ) where + rb06 = trans (rb07 vp) ( cong black-depth (sym x) ) where + rb07 : (vp : Color ∧ A) → black-depth (node kp vp repl n1) ≡ black-depth (node kp vp (RBI.tree r) n1 ) + rb07 ⟪ Black , proj4 ⟫ = cong (λ k → suc (k ⊔ black-depth n1 )) bdepth-eq + rb07 ⟪ Red , proj4 ⟫ = cong (λ k → (k ⊔ black-depth n1 )) bdepth-eq + ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt 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 + 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 = lt + 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 - ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? - ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? + ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt 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-left 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 (sym (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 (trans (sym ceq) cx) cx₁ (sym rb03) (RBI.replrb r) t₁ + ... | rb-black .kp value ex t t₁ = rb-black kp value (sym rb03) (RBI.replrb r) t₁ + rb05 : treeInvariant (node kp vp (RBI.tree r) n1) + rb05 = subst (λ k → treeInvariant k) x (rb08 pg) + rb04 : key < kp + rb04 = lt + 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 repl n1) ≡ black-depth (node kp vp (RBI.tree r) n1) + rb07 ⟪ Black , proj4 ⟫ = cong (λ k → suc (k ⊔ black-depth n1 )) bdepth-eq + rb07 ⟪ Red , proj4 ⟫ = cong (λ k → (k ⊔ black-depth n1 )) bdepth-eq ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = rebuildCase2 where rebuildCase2 : t rebuildCase2 = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record { @@ -2062,8 +2118,7 @@ insertCase51 with PG.pg pg ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase52 where insertCase52 : t - insertCase52 with <-cmp key kp - ... | tri< a ¬b ¬c = next (PG.grand pg ∷ PG.rest pg) record { + insertCase52 = next (PG.grand pg ∷ PG.rest pg) record { tree = PG.grand pg ; repl = rb01 ; origti = RBI.origti r @@ -2073,14 +2128,10 @@ ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) ; state = rebuild (trans (cong color x₁) (cong proj1 (sym rb14))) rb17 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) 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 - -- repl : ode rkey value rp-reft rp-right - rb01 : bt (Color ∧ A) rb01 = to-black (node kp vp (node rkey vr rp-left rp-right) (to-red (node kg vg n1 (PG.uncle pg)))) rb04 : key < kp - rb04 = a + rb04 = lt rb16 : color n1 ≡ Black rb16 = proj2 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) x rb09) (trans (cong color (sym x)) pcolor)) rb13 : ⟪ Red , proj2 vp ⟫ ≡ vp @@ -2128,8 +2179,6 @@ 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 - ... | 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 = ? ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ?