Mercurial > hg > Gears > GearsAgda
changeset 945:7310dc7f2437
insertCase done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 17 Jun 2024 08:24:11 +0900 |
| parents | 911900003d25 |
| children | cfe8f3917a71 |
| files | hoareBinaryTree2.agda |
| diffstat | 1 files changed, 333 insertions(+), 8 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree2.agda Sun Jun 16 12:08:48 2024 +0900 +++ b/hoareBinaryTree2.agda Mon Jun 17 08:24:11 2024 +0900 @@ -1942,9 +1942,118 @@ rb06 : RBtreeInvariant rb01 rb06 = subst (λ k → RBtreeInvariant (node kp k repl n1)) rb04 ( rb-black _ _ rb07 (RBI.replrb r) (RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x (treerb pg)))) - insertCase1 | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? - insertCase1 | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? - insertCase1 | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? + ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = 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 = rb06 + ; si = popStackInvariant _ _ _ _ _ (rb00 pg) + ; state = rebuild (cong color x) (rb05 (trans (sym (cong color x)) pcolor)) (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())) + (subst (λ k → replacedRBTree key value k (node kp vp n1 repl) ) (sym x) (rb02 rb04 )) + } (subst₂ (λ j k → j < length k ) refl (sym (PG.stack=gp pg)) ≤-refl) where + --- x : PG.parent pg ≡ node kp vp n1 (RBI.tree r) + --- x₁ : PG.grand pg ≡ node kg vg (PG.parent pg) (PG.uncle pg) + rb01 : bt (Color ∧ A) + rb01 = node kp vp n1 repl + rb03 : kp < key + rb03 = lt + rb04 : ⟪ Black , proj2 vp ⟫ ≡ vp + rb04 with subst (λ k → color k ≡ Black) x pcolor + ... | refl = refl + rb02 : ⟪ Black , proj2 vp ⟫ ≡ vp → replacedRBTree key value (node kp vp n1 (RBI.tree r) ) (node kp vp n1 repl ) + rb02 eq = subst (λ k → replacedRBTree key value (node kp k n1 (RBI.tree r) ) (node kp k n1 repl )) eq (rbr-black-right repl-red rb03 rot ) + rb07 : black-depth repl ≡ black-depth n1 + rb07 = begin + black-depth repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ + black-depth (RBI.tree r) ≡⟨ sym ( RBtreeEQ (subst (λ k → RBtreeInvariant k) x (treerb pg))) ⟩ + black-depth n1 ∎ + where open ≡-Reasoning + rb05 : proj1 vp ≡ Black → black-depth rb01 ≡ black-depth (PG.parent pg) + rb05 refl = begin + suc (black-depth n1 ⊔ black-depth repl) ≡⟨ cong suc (cong (λ k → black-depth n1 ⊔ k ) (sym (RB-repl→eq _ _ (RBI.treerb r) rot))) ⟩ + suc (black-depth n1 ⊔ black-depth (RBI.tree r)) ≡⟨ refl ⟩ + black-depth (node kp vp n1 (RBI.tree r) ) ≡⟨ cong black-depth (sym x) ⟩ + black-depth (PG.parent pg) ∎ + where open ≡-Reasoning + rb06 : RBtreeInvariant rb01 + rb06 = subst (λ k → RBtreeInvariant (node kp k n1 repl )) rb04 + ( rb-black _ _ (sym rb07) (RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x (treerb pg))) (RBI.replrb r) ) + insertCase1 | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = 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 = rb06 + ; si = popStackInvariant _ _ _ _ _ (rb00 pg) + ; state = rebuild (cong color x) (rb05 (trans (sym (cong color x)) pcolor)) (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())) + (subst (λ k → replacedRBTree key value k (node kp vp repl n1) ) (sym x) (rb02 rb04 )) + } (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 : key < kp + rb03 = lt + rb04 : ⟪ Black , proj2 vp ⟫ ≡ vp + rb04 with subst (λ k → color k ≡ Black) x pcolor + ... | refl = refl + rb02 : ⟪ Black , proj2 vp ⟫ ≡ vp → replacedRBTree key value (node kp vp (RBI.tree r) n1) (node kp vp repl n1) + rb02 eq = subst (λ k → replacedRBTree key value (node kp k (RBI.tree r) n1) (node kp k repl n1)) eq (rbr-black-left repl-red rb03 rot ) + rb07 : black-depth repl ≡ black-depth n1 + rb07 = begin + black-depth repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ + black-depth (RBI.tree r) ≡⟨ RBtreeEQ (subst (λ k → RBtreeInvariant k) x (treerb pg)) ⟩ + black-depth n1 ∎ + where open ≡-Reasoning + rb05 : proj1 vp ≡ Black → black-depth rb01 ≡ black-depth (PG.parent pg) + rb05 refl = begin + suc (black-depth repl ⊔ black-depth n1) ≡⟨ cong suc (cong (λ k → k ⊔ black-depth n1) (sym (RB-repl→eq _ _ (RBI.treerb r) rot))) ⟩ + suc (black-depth (RBI.tree r) ⊔ black-depth n1) ≡⟨ refl ⟩ + black-depth (node kp vp (RBI.tree r) n1) ≡⟨ cong black-depth (sym x) ⟩ + black-depth (PG.parent pg) ∎ + where open ≡-Reasoning + rb06 : RBtreeInvariant rb01 + rb06 = subst (λ k → RBtreeInvariant (node kp k repl n1)) rb04 + ( rb-black _ _ rb07 (RBI.replrb r) (RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x (treerb pg)))) + insertCase1 | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = 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 = rb06 + ; si = popStackInvariant _ _ _ _ _ (rb00 pg) + ; state = rebuild (cong color x) (rb05 (trans (sym (cong color x)) pcolor)) (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())) + (subst (λ k → replacedRBTree key value k (node kp vp n1 repl) ) (sym x) (rb02 rb04 )) + } (subst₂ (λ j k → j < length k ) refl (sym (PG.stack=gp pg)) ≤-refl) where + -- x : PG.parent pg ≡ node kp vp (RBI.tree r) n1 + -- x₁ : PG.grand pg ≡ node kg vg (PG.uncle pg) (PG.parent pg) + rb01 : bt (Color ∧ A) + rb01 = node kp vp n1 repl + rb03 : kp < key + rb03 = lt + rb04 : ⟪ Black , proj2 vp ⟫ ≡ vp + rb04 with subst (λ k → color k ≡ Black) x pcolor + ... | refl = refl + rb02 : ⟪ Black , proj2 vp ⟫ ≡ vp → replacedRBTree key value (node kp vp n1 (RBI.tree r) ) (node kp vp n1 repl ) + rb02 eq = subst (λ k → replacedRBTree key value (node kp k n1 (RBI.tree r) ) (node kp k n1 repl )) eq (rbr-black-right repl-red rb03 rot ) + rb07 : black-depth repl ≡ black-depth n1 + rb07 = begin + black-depth repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ + black-depth (RBI.tree r) ≡⟨ sym ( RBtreeEQ (subst (λ k → RBtreeInvariant k) x (treerb pg))) ⟩ + black-depth n1 ∎ + where open ≡-Reasoning + rb05 : proj1 vp ≡ Black → black-depth rb01 ≡ black-depth (PG.parent pg) + rb05 refl = begin + suc (black-depth n1 ⊔ black-depth repl) ≡⟨ cong suc (cong (λ k → black-depth n1 ⊔ k ) (sym (RB-repl→eq _ _ (RBI.treerb r) rot))) ⟩ + suc (black-depth n1 ⊔ black-depth (RBI.tree r)) ≡⟨ refl ⟩ + black-depth (node kp vp n1 (RBI.tree r) ) ≡⟨ cong black-depth (sym x) ⟩ + black-depth (PG.parent pg) ∎ + where open ≡-Reasoning + rb06 : RBtreeInvariant rb01 + rb06 = subst (λ k → RBtreeInvariant (node kp k n1 repl )) rb04 + ( rb-black _ _ (sym rb07) (RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x (treerb pg))) (RBI.replrb r) ) ... | Red with PG.uncle pg in uneq ... | leaf = insertCase5 repl refl pg rot repl-red (cong color uneq) pcolor ... | node key₁ ⟪ Black , value₁ ⟫ t₁ t₂ = insertCase5 repl refl pg rot repl-red (cong color uneq) pcolor @@ -2009,12 +2118,160 @@ suc (black-depth (PG.uncle pg)) ≡⟨ to-black-eq (PG.uncle pg) (cong color uneq ) ⟩ black-depth (to-black (PG.uncle pg)) ∎ where open ≡-Reasoning + rb15 : suc (length (PG.rest pg)) < length stack + rb15 = begin + suc (suc (length (PG.rest pg))) ≤⟨ <-trans (n<1+n _) (n<1+n _) ⟩ + length (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) ≡⟨ cong length (sym (PG.stack=gp pg)) ⟩ + length stack ∎ + where open ≤-Reasoning + ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase2 where + insertCase2 : t + insertCase2 = next (PG.grand pg ∷ (PG.rest pg)) + record { + tree = PG.grand pg + ; repl = to-red (node kg vg (to-black (node kp vp n1 repl)) (to-black (PG.uncle pg)) ) + ; origti = RBI.origti r + ; origrb = RBI.origrb r + ; treerb = rb01 + ; replrb = rb-red _ _ refl (RBtreeToBlackColor _ rb02) rb12 (rb-black _ _ (sym rb13) rb04 (RBI.replrb r)) (RBtreeToBlack _ rb02) + ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) + ; state = rotate _ refl (subst₂ (λ j k → replacedRBTree key value j k ) rb09 refl (rbr-flip-lr repl-red (rb05 refl uneq) rb06 rb21 rot)) + } rb15 where + -- + -- 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) + -- + rb00 : stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) + rb00 = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r) + rb01 : RBtreeInvariant (PG.grand pg) + rb01 = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)) + rb02 : RBtreeInvariant (PG.uncle pg) + rb02 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01) + rb03 : RBtreeInvariant (PG.parent pg) + rb03 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01) + rb04 : RBtreeInvariant n1 + rb04 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x rb03) + rb05 : { tree : bt (Color ∧ A) } → tree ≡ PG.uncle pg → tree ≡ node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ → color (PG.uncle pg) ≡ Red + rb05 refl refl = refl + rb08 : treeInvariant (PG.parent pg) + rb08 = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00) + rb07 : treeInvariant (node kp vp n1 (RBI.tree r) ) + rb07 = subst (λ k → treeInvariant k) x (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00)) + rb06 : kp < key + rb06 = lt + rb21 : key < kg -- 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)) + rb10 : vg ≡ ⟪ Black , proj2 vg ⟫ + rb10 with RBtreeParentColorBlack _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01) (case1 pcolor) + ... | refl = refl + rb11 : vp ≡ ⟪ Red , proj2 vp ⟫ + rb11 with subst (λ k → color k ≡ Red) x pcolor + ... | refl = refl + rb09 : node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r) ) (PG.uncle pg) ≡ PG.grand pg + rb09 = sym ( begin + PG.grand pg ≡⟨ x₁ ⟩ + node kg vg (PG.parent pg) (PG.uncle pg) ≡⟨ cong (λ k → node kg vg k (PG.uncle pg)) x ⟩ + node kg vg (node kp vp n1 (RBI.tree r) ) (PG.uncle pg) ≡⟨ cong₂ (λ j k → node kg j (node kp k n1 (RBI.tree r) ) (PG.uncle pg) ) rb10 rb11 ⟩ + node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r) ) (PG.uncle pg) ∎ ) + where open ≡-Reasoning + rb13 : black-depth repl ≡ black-depth n1 + rb13 = begin + black-depth repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ + black-depth (RBI.tree r) ≡⟨ sym (RBtreeEQ (subst (λ k → RBtreeInvariant k) x rb03)) ⟩ + black-depth n1 ∎ + where open ≡-Reasoning + rb12 : suc (black-depth n1 ⊔ black-depth repl) ≡ black-depth (to-black (PG.uncle pg)) + rb12 = begin + suc (black-depth n1 ⊔ black-depth repl) ≡⟨ cong (λ k → suc (black-depth n1 ⊔ k)) (sym (RB-repl→eq _ _ (RBI.treerb r) rot)) ⟩ + suc (black-depth n1 ⊔ black-depth (RBI.tree r)) ≡⟨ cong (λ k → suc (black-depth n1 ⊔ k)) (sym (RBtreeEQ (subst (λ k → RBtreeInvariant k) x rb03))) ⟩ + suc (black-depth n1 ⊔ black-depth n1) ≡⟨ ⊔-idem _ ⟩ + suc (black-depth n1 ) ≡⟨ cong suc (sym (proj1 (red-children-eq x (cong proj1 rb11) rb03 ))) ⟩ + suc (black-depth (PG.parent pg)) ≡⟨ cong suc (RBtreeEQ (subst (λ k → RBtreeInvariant k) x₁ rb01)) ⟩ + suc (black-depth (PG.uncle pg)) ≡⟨ to-black-eq (PG.uncle pg) (cong color uneq ) ⟩ + black-depth (to-black (PG.uncle pg)) ∎ + where open ≡-Reasoning + rb15 : suc (length (PG.rest pg)) < length stack + rb15 = begin + suc (suc (length (PG.rest pg))) ≤⟨ <-trans (n<1+n _) (n<1+n _) ⟩ + length (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) ≡⟨ cong length (sym (PG.stack=gp pg)) ⟩ + length stack ∎ + where open ≤-Reasoning + ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase2 where + insertCase2 : t + insertCase2 = next (PG.grand pg ∷ (PG.rest pg)) + record { + tree = PG.grand pg + ; repl = to-red (node kg vg (to-black (PG.uncle pg)) (to-black (node kp vp repl n1)) ) + ; origti = RBI.origti r + ; origrb = RBI.origrb r + ; treerb = rb01 + ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) + ; replrb = rb-red _ _ (RBtreeToBlackColor _ rb02) refl rb12 (RBtreeToBlack _ rb02) (rb-black _ _ rb13 (RBI.replrb r) rb04) + ; state = rotate _ refl (subst₂ (λ j k → replacedRBTree key value j k ) rb09 refl (rbr-flip-rl repl-red (rb05 refl uneq) rb21 rb06 rot)) + } rb15 where + -- x : PG.parent pg ≡ node kp vp (RBI.tree r) n1 + -- x₁ : PG.grand pg ≡ node kg vg (PG.uncle pg) (PG.parent pg) + rb00 : stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) + rb00 = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r) + rb01 : RBtreeInvariant (PG.grand pg) + rb01 = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)) + rb02 : RBtreeInvariant (PG.uncle pg) + rb02 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01) + rb03 : RBtreeInvariant (PG.parent pg) + rb03 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01) + rb04 : RBtreeInvariant n1 + rb04 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x rb03) + rb05 : { tree : bt (Color ∧ A) } → tree ≡ PG.uncle pg → tree ≡ node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ → color (PG.uncle pg) ≡ Red + rb05 refl refl = refl + rb08 : treeInvariant (PG.parent pg) + rb08 = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00) + rb07 : treeInvariant (node kp vp (RBI.tree r) n1) + rb07 = subst (λ k → treeInvariant k) x (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00)) + rb06 : key < kp + rb06 = 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)) + rb10 : vg ≡ ⟪ Black , proj2 vg ⟫ + rb10 with RBtreeParentColorBlack _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01) (case2 pcolor) + ... | refl = refl + rb11 : vp ≡ ⟪ Red , proj2 vp ⟫ + rb11 with subst (λ k → color k ≡ Red) x pcolor + ... | refl = refl + rb09 : node kg ⟪ Black , proj2 vg ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) ≡ PG.grand pg + rb09 = sym ( begin + PG.grand pg ≡⟨ x₁ ⟩ + node kg vg (PG.uncle pg) (PG.parent pg) ≡⟨ cong (λ k → node kg vg (PG.uncle pg) k) x ⟩ + node kg vg (PG.uncle pg) (node kp vp (RBI.tree r) n1) ≡⟨ cong₂ (λ j k → node kg j (PG.uncle pg) (node kp k (RBI.tree r) n1) ) rb10 rb11 ⟩ + node kg ⟪ Black , proj2 vg ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) ∎ ) + where open ≡-Reasoning + rb13 : black-depth repl ≡ black-depth n1 + rb13 = begin + black-depth repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ + black-depth (RBI.tree r) ≡⟨ RBtreeEQ (subst (λ k → RBtreeInvariant k) x rb03) ⟩ + black-depth n1 ∎ + where open ≡-Reasoning + -- rb12 : suc (black-depth repl ⊔ black-depth n1) ≡ black-depth (to-black (PG.uncle pg)) + rb12 : black-depth (to-black (PG.uncle pg)) ≡ suc (black-depth repl ⊔ black-depth n1) + rb12 = sym ( begin + suc (black-depth repl ⊔ black-depth n1) ≡⟨ cong (λ k → suc (k ⊔ black-depth n1)) (sym (RB-repl→eq _ _ (RBI.treerb r) rot)) ⟩ + suc (black-depth (RBI.tree r) ⊔ black-depth n1) ≡⟨ cong (λ k → suc (k ⊔ black-depth n1)) (RBtreeEQ (subst (λ k → RBtreeInvariant k) x rb03)) ⟩ + suc (black-depth n1 ⊔ black-depth n1) ≡⟨ ⊔-idem _ ⟩ + suc (black-depth n1 ) ≡⟨ cong suc (sym (proj2 (red-children-eq x (cong proj1 rb11) rb03 ))) ⟩ + suc (black-depth (PG.parent pg)) ≡⟨ cong suc (sym (RBtreeEQ (subst (λ k → RBtreeInvariant k) x₁ rb01))) ⟩ + suc (black-depth (PG.uncle pg)) ≡⟨ to-black-eq (PG.uncle pg) (cong color uneq ) ⟩ + black-depth (to-black (PG.uncle pg)) ∎ ) + where open ≡-Reasoning rb17 : suc (black-depth repl ⊔ black-depth n1) ⊔ black-depth (to-black (PG.uncle pg)) ≡ black-depth (PG.grand pg) rb17 = begin - suc (black-depth repl ⊔ black-depth n1) ⊔ black-depth (to-black (PG.uncle pg)) ≡⟨ cong (λ k → k ⊔ black-depth (to-black (PG.uncle pg))) rb12 ⟩ + suc (black-depth repl ⊔ black-depth n1) ⊔ black-depth (to-black (PG.uncle pg)) ≡⟨ cong (λ k → k ⊔ black-depth (to-black (PG.uncle pg))) (sym rb12) ⟩ black-depth (to-black (PG.uncle pg)) ⊔ black-depth (to-black (PG.uncle pg)) ≡⟨ ⊔-idem _ ⟩ black-depth (to-black (PG.uncle pg)) ≡⟨ sym (to-black-eq (PG.uncle pg) (cong color uneq )) ⟩ - suc (black-depth (PG.uncle pg)) ≡⟨ sym ( proj2 (black-children-eq x₁ (cong proj1 rb10) rb01 )) ⟩ + suc (black-depth (PG.uncle pg)) ≡⟨ sym ( proj1 (black-children-eq x₁ (cong proj1 rb10) rb01 )) ⟩ black-depth (PG.grand pg) ∎ where open ≡-Reasoning rb15 : suc (length (PG.rest pg)) < length stack @@ -2023,7 +2280,75 @@ length (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) ≡⟨ cong length (sym (PG.stack=gp pg)) ⟩ length stack ∎ where open ≤-Reasoning - ... | 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₁ = {!!} + ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase2 where + --- 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) + insertCase2 : t + insertCase2 = next (PG.grand pg ∷ (PG.rest pg)) + record { + tree = PG.grand pg + ; repl = to-red (node kg vg (to-black (PG.uncle pg)) (to-black (node kp vp n1 repl )) ) + ; origti = RBI.origti r + ; origrb = RBI.origrb r + ; treerb = rb01 + ; replrb = rb-red _ _ (RBtreeToBlackColor _ rb02) refl rb12 (RBtreeToBlack _ rb02) (rb-black _ _ (sym rb13) rb04 (RBI.replrb r) ) + ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) + ; state = rotate _ refl (subst₂ (λ j k → replacedRBTree key value j k ) (sym rb09) refl (rbr-flip-rr repl-red (rb05 refl uneq) rb06 rot)) + } rb15 where + rb00 : stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) + rb00 = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r) + rb01 : RBtreeInvariant (PG.grand pg) + rb01 = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)) + rb02 : RBtreeInvariant (PG.uncle pg) + rb02 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01) + rb03 : RBtreeInvariant (PG.parent pg) + rb03 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01) + rb04 : RBtreeInvariant n1 + rb04 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x rb03) + rb05 : { tree : bt (Color ∧ A) } → tree ≡ PG.uncle pg → tree ≡ node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ → color (PG.uncle pg) ≡ Red + rb05 refl refl = refl + rb08 : treeInvariant (PG.parent pg) + rb08 = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00) + rb07 : treeInvariant (node kp vp n1 (RBI.tree r) ) + rb07 = subst (λ k → treeInvariant k) x (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00)) + rb06 : kp < key + rb06 = lt + rb10 : vg ≡ ⟪ Black , proj2 vg ⟫ + rb10 with RBtreeParentColorBlack _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01) (case2 pcolor) + ... | refl = refl + rb11 : vp ≡ ⟪ Red , proj2 vp ⟫ + rb11 with subst (λ k → color k ≡ Red) x pcolor + ... | refl = refl + rb09 : PG.grand pg ≡ node kg ⟪ Black , proj2 vg ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r) ) + rb09 = begin + PG.grand pg ≡⟨ x₁ ⟩ + node kg vg (PG.uncle pg) (PG.parent pg) ≡⟨ cong (λ k → node kg vg (PG.uncle pg) k) x ⟩ + node kg vg (PG.uncle pg) (node kp vp n1 (RBI.tree r) ) ≡⟨ cong₂ (λ j k → node kg j (PG.uncle pg) (node kp k n1 (RBI.tree r) ) ) rb10 rb11 ⟩ + node kg ⟪ Black , proj2 vg ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r) ) ∎ + where open ≡-Reasoning + rb13 : black-depth repl ≡ black-depth n1 + rb13 = begin + black-depth repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ + black-depth (RBI.tree r) ≡⟨ sym (RBtreeEQ (subst (λ k → RBtreeInvariant k) x rb03)) ⟩ + black-depth n1 ∎ + where open ≡-Reasoning + rb12 : black-depth (to-black (PG.uncle pg)) ≡ suc (black-depth n1 ⊔ black-depth repl) + rb12 = sym ( begin + suc (black-depth n1 ⊔ black-depth repl) ≡⟨ cong suc (⊔-comm (black-depth n1) _) ⟩ + suc (black-depth repl ⊔ black-depth n1) ≡⟨ cong (λ k → suc (k ⊔ black-depth n1)) (sym (RB-repl→eq _ _ (RBI.treerb r) rot)) ⟩ + suc (black-depth (RBI.tree r) ⊔ black-depth n1) ≡⟨ cong (λ k → suc (k ⊔ black-depth n1)) (sym (RBtreeEQ (subst (λ k → RBtreeInvariant k) x rb03))) ⟩ + suc (black-depth n1 ⊔ black-depth n1) ≡⟨ ⊔-idem _ ⟩ + suc (black-depth n1 ) ≡⟨ cong suc (sym (proj1 (red-children-eq x (cong proj1 rb11) rb03 ))) ⟩ + suc (black-depth (PG.parent pg)) ≡⟨ cong suc (sym (RBtreeEQ (subst (λ k → RBtreeInvariant k) x₁ rb01))) ⟩ + suc (black-depth (PG.uncle pg)) ≡⟨ to-black-eq (PG.uncle pg) (cong color uneq ) ⟩ + black-depth (to-black (PG.uncle pg)) ∎ ) + where open ≡-Reasoning + rb15 : suc (length (PG.rest pg)) < length stack + rb15 = begin + suc (suc (length (PG.rest pg))) ≤⟨ <-trans (n<1+n _) (n<1+n _) ⟩ + length (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) ≡⟨ cong length (sym (PG.stack=gp pg)) ⟩ + length stack ∎ + where open ≤-Reasoning +