Mercurial > hg > Gears > GearsAgda
changeset 943:03857be39158
....
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 16 Jun 2024 09:22:40 +0900 |
| parents | 49ac34a645ef |
| children | 911900003d25 |
| files | hoareBinaryTree2.agda |
| diffstat | 1 files changed, 39 insertions(+), 43 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree2.agda Sat Jun 15 19:56:16 2024 +0900 +++ b/hoareBinaryTree2.agda Sun Jun 16 09:22:40 2024 +0900 @@ -1751,16 +1751,18 @@ rb03 = rbr-rotate-rl rp-left rp-right kg kp rkey rb20 rb21 rb04 (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 ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) ≡ PG.grand pg - 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₁) + rb24 = begin + node kg ⟪ Black , proj2 vg ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) + ≡⟨ cong₂ (λ j k → node kg j (PG.uncle pg) (node kp k (RBI.tree r) n1) ) rb14 rb13 ⟩ + node kg vg (PG.uncle pg) (node kp vp (RBI.tree r) n1) ≡⟨ cong (λ k → node kg vg (PG.uncle pg) k ) (sym x) ⟩ + node kg vg (PG.uncle pg) (PG.parent pg) ≡⟨ sym x₁ ⟩ + PG.grand pg ∎ where open ≡-Reasoning rb25 : node rkey ⟪ Black , proj2 vr ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) rp-left) (node kp ⟪ Red , proj2 vp ⟫ rp-right n1) ≡ rb01 - -- 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 + rb25 = begin + node rkey ⟪ Black , proj2 vr ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) rp-left) (node kp ⟪ Red , proj2 vp ⟫ rp-right n1) + ≡⟨ cong (λ k → node rkey ⟪ Black , proj2 vr ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) rp-left) (node kp k rp-right n1)) rb13 ⟩ + node rkey ⟪ Black , proj2 vr ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) rp-left) (node kp vp rp-right n1) ≡⟨ 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) @@ -1774,54 +1776,48 @@ rb31 : RBtreeInvariant (node rkey vr rp-left rp-right ) rb31 = subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r) rb18 : black-depth (PG.uncle pg) ≡ black-depth rp-left - rb18 = ? - 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) )) ⟩ + rb18 = sym ( begin + black-depth rp-left ≡⟨ sym ( proj1 (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 + black-depth (PG.uncle pg) ∎ ) where open ≡-Reasoning rb27 : black-depth rp-right ≡ black-depth n1 - -- 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) + rb27 = sym ( begin + black-depth n1 ≡⟨ sym (RBtreeEQ (subst (λ k → RBtreeInvariant k) x rb09)) ⟩ + black-depth (RBI.tree r) ≡⟨ RB-repl→eq _ _ (RBI.treerb r) rot ⟩ + black-depth (RBI.repl r) ≡⟨ proj2 (red-children-eq1 (sym eq) repl-red (RBI.replrb r)) ⟩ + black-depth rp-right ∎ ) + where open ≡-Reasoning 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 + rb19 = sym ( begin + black-depth (node kp vp rp-right n1) ≡⟨ black-depth-resp A (node kp vp rp-right n1) (node kp vp rp-right rp-right) refl refl refl refl (sym rb27) ⟩ + black-depth (node kp vp rp-right rp-right) ≡⟨ black-depth-resp A (node kp vp rp-right rp-right) (node rkey vr rp-left rp-right) + refl refl (trans (sym (cong proj1 rb13)) (sym (cong proj1 rb23))) (sym (RBtreeEQ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r)))) refl ⟩ + black-depth (node rkey vr rp-left rp-right) ≡⟨ black-depth-cong A eq ⟩ + black-depth (RBI.repl r) ≡⟨ proj1 (red-children-eq1 (sym eq) repl-red (RBI.replrb r)) ⟩ + black-depth rp-left ≡⟨ sym ( ⊔-idem _ ) ⟩ + black-depth rp-left ⊔ black-depth rp-left ≡⟨ cong (λ k → k ⊔ black-depth rp-left ) (sym rb18) ⟩ + black-depth (PG.uncle pg) ⊔ black-depth rp-left ∎ ) + 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 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 : ? -- 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 + 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) ⟩ + suc (black-depth (PG.uncle pg) ⊔ black-depth rp-left ⊔ (black-depth (PG.uncle pg) ⊔ black-depth rp-left)) ≡⟨ cong suc ( ⊔-idem _) ⟩ + suc (black-depth (PG.uncle pg) ⊔ black-depth rp-left ) ≡⟨ cong (λ k → suc (_ ⊔ k)) (sym 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 {