Mercurial > hg > Gears > GearsAgda
changeset 931:16ecb05cc50d
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 11 Jun 2024 16:10:33 +0900 |
| parents | 65664560f055 |
| children | 0cf53f1e0055 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 82 insertions(+), 9 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Mon Jun 10 11:13:58 2024 +0900 +++ b/hoareBinaryTree1.agda Tue Jun 11 16:10:33 2024 +0900 @@ -1012,6 +1012,28 @@ suc (black-depth right) ∎ ) ⟫ where open ≡-Reasoning black-children-eq {n} {A} {tree} {left} {right} {key} {value} {Red} eq () rb +black-depth-cong : {n : Level} (A : Set n) {tree tree₁ : bt (Color ∧ A)} + → tree ≡ tree₁ → black-depth tree ≡ black-depth tree₁ +black-depth-cong {n} A {leaf} {leaf} refl = refl +black-depth-cong {n} A {node key ⟪ Red , value ⟫ left right} {node .key ⟪ Red , .value ⟫ .left .right} refl + = cong₂ (λ j k → j ⊔ k ) (black-depth-cong A {left} {left} refl) (black-depth-cong A {right} {right} refl) +black-depth-cong {n} A {node key ⟪ Black , value ⟫ left right} {node .key ⟪ Black , .value ⟫ .left .right} refl + = cong₂ (λ j k → suc (j ⊔ k) ) (black-depth-cong A {left} {left} refl) (black-depth-cong A {right} {right} refl) + +rbi-from-red-black : {n : Level } {A : Set n} → (n1 rp-left : bt (Color ∧ A)) → (kp : ℕ) → (vp : Color ∧ A) + → RBtreeInvariant n1 → RBtreeInvariant rp-left + → black-depth n1 ≡ black-depth rp-left + → color n1 ≡ Black → color rp-left ≡ Black → ⟪ Red , proj2 vp ⟫ ≡ vp + → RBtreeInvariant (node kp vp n1 rp-left) +rbi-from-red-black leaf leaf kp vp rb1 rbp deq ceq1 ceq2 ceq3 + = subst (λ k → RBtreeInvariant (node kp k leaf leaf)) ceq3 (rb-red kp (proj2 vp) refl refl refl rb-leaf rb-leaf) +rbi-from-red-black leaf (node key ⟪ .Black , proj3 ⟫ trpl trpl₁) kp vp rb1 rbp deq ceq1 refl ceq3 + = subst (λ k → RBtreeInvariant (node kp k _ _)) ceq3 (rb-red kp (proj2 vp) refl refl deq rb1 rbp) +rbi-from-red-black (node key ⟪ .Black , proj3 ⟫ tn1 tn2) leaf kp vp rb1 rbp deq refl ceq2 ceq3 + = subst (λ k → RBtreeInvariant (node kp k _ _)) ceq3 (rb-red kp (proj2 vp) refl refl deq rb1 rbp) +rbi-from-red-black (node key ⟪ .Black , proj3 ⟫ tn1 tn2) (node key₁ ⟪ .Black , proj4 ⟫ trpl trpl₁) kp vp rb1 rbp deq refl refl ceq3 + = subst (λ k → RBtreeInvariant (node kp k _ _)) ceq3 (rb-red kp (proj2 vp) refl refl deq rb1 rbp ) + ⊔-succ : {m n : ℕ} → suc (m ⊔ n) ≡ suc m ⊔ suc n ⊔-succ {m} {n} = refl @@ -2191,7 +2213,7 @@ ; origti = RBI.origti r ; origrb = RBI.origrb r ; treerb = rb02 - ; replrb = subst (λ k → RBtreeInvariant k) rb10 (rb-black _ _ rb18 (RBI.replrb r) (rb-red _ _ rb16 uncle-black rb19 rb06 rb05)) + ; replrb = rb10 ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) ; state = rebuild (trans (cong color x₁) (cong proj1 (sym rb14))) rb17 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) rb11 } rb15 where @@ -2224,20 +2246,71 @@ (node rkey ⟪ Black , proj2 vr ⟫ (node kp ⟪ Red , proj2 vp ⟫ n1 rp-left) (node kg ⟪ Red , proj2 vg ⟫ rp-right (PG.uncle pg))) rb03 = rbr-rotate-lr rp-left rp-right kg kp rkey rb20 rb04 rb21 (subst (λ k → replacedRBTree key value (RBI.tree r) k) (trans (sym eq) (cong (λ k → node rkey k rp-left rp-right) rb23 )) rot ) - rb10 : node rkey ⟪ Black , proj2 vr ⟫ (RBI.repl r) (node kg ⟪ Red , proj2 vg ⟫ n1 (PG.uncle pg)) ≡ rb01 - rb10 = ? + 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) ? ? rb03 + rb11 = subst₂ (λ j k → replacedRBTree key value j k) rb24 rb25 rb03 rb05 : RBtreeInvariant (PG.uncle pg) rb05 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb02) rb06 : RBtreeInvariant n1 rb06 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x rb09) - rb19 : black-depth n1 ≡ black-depth (PG.uncle pg) - rb19 = ? -- trans (sym ( proj2 (red-children-eq x (sym (cong proj1 rb13)) rb09) )) (RBtreeEQ (subst (λ k → RBtreeInvariant k) x₁ rb02)) - rb18 : black-depth (RBI.repl r) ≡ black-depth n1 ⊔ black-depth (PG.uncle pg) - rb18 = ? + 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)) + rb18 : black-depth rp-right ≡ black-depth (PG.uncle pg) + rb18 = begin + black-depth rp-right ≡⟨ sym (proj2 (red-children-eq (cong (λ k → node rkey k rp-left rp-right) rb23) + refl (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r)) )) ⟩ + black-depth (node rkey vr rp-left rp-right) ≡⟨ cong black-depth eq ⟩ + black-depth (RBI.repl r) ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ + black-depth (RBI.tree r) ≡⟨ sym (proj2 (red-children-eq refl refl + (subst (λ k → RBtreeInvariant k) (trans x (cong (λ k → node kp k n1 (RBI.tree r) ) (sym rb13) )) rb09))) ⟩ + black-depth (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r)) ≡⟨ black-depth-cong _ (cong (λ k → node kp k n1 (RBI.tree r)) rb13) ⟩ + black-depth (node kp vp n1 (RBI.tree r)) ≡⟨ black-depth-cong _ (sym x) ⟩ + black-depth (PG.parent pg) ≡⟨ 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) ≡⟨ ? ⟩ + black-depth (RBI.repl r) ≡⟨ cong black-depth (sym eq) ⟩ + black-depth (node rkey vr rp-left rp-right) ≡⟨ black-depth-cong _ (cong (λ k → node rkey k rp-left rp-right) rb23) ⟩ + black-depth (node rkey ⟪ Red , proj2 vr ⟫ rp-left rp-right) ≡⟨ ? ⟩ + 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 = begin + black-depth (node kp vp n1 rp-left) ≡⟨ ? ⟩ + black-depth (node kp ⟪ Red , proj2 vp ⟫ n1 rp-left) ≡⟨ ? ⟩ + black-depth n1 ⊔ black-depth rp-left ≡⟨ ? ⟩ + black-depth rp-left ⊔ black-depth rp-left ≡⟨ ? ⟩ + black-depth rp-left ≡⟨ ? ⟩ + black-depth rp-right ≡⟨ ? ⟩ + black-depth rp-right ⊔ black-depth rp-right ≡⟨ ? ⟩ + black-depth rp-right ⊔ black-depth (PG.uncle pg) ∎ + where open ≡-Reasoning + rb29 : color n1 ≡ Black + rb29 = proj1 (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)) + 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) 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 = ? + rb17 = begin + suc (black-depth (node kp vp n1 rp-left) ⊔ (black-depth rp-right ⊔ black-depth (PG.uncle pg))) ≡⟨ ? ⟩ + suc ((black-depth rp-right ⊔ black-depth (PG.uncle pg)) ⊔ (black-depth rp-right ⊔ black-depth (PG.uncle pg))) ≡⟨ ? ⟩ + suc (black-depth rp-right ⊔ black-depth (PG.uncle pg)) ≡⟨ ? ⟩ + suc (black-depth (PG.uncle pg) ⊔ black-depth (PG.uncle pg)) ≡⟨ ? ⟩ + suc (black-depth (PG.uncle pg)) ≡⟨ ? ⟩ + 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₁ = ? replaceRBP1 : t