Mercurial > hg > Gears > GearsAgda
changeset 922:5fb90d662aa4
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 06 Jun 2024 17:53:41 +0900 |
| parents | 46ec01e94947 |
| children | 62393055b0dd |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 145 insertions(+), 239 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Wed Jun 05 14:42:54 2024 +0900 +++ b/hoareBinaryTree1.agda Thu Jun 06 17:53:41 2024 +0900 @@ -938,7 +938,6 @@ → (rotated : replacedRBTree key value tree repl) → RBI-state key value tree repl stack -- one stage up rotate : {tree repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → color repl ≡ Red → black-depth repl ≡ black-depth tree - → ¬ (tree ≡ leaf) → (rotated : replacedRBTree key value tree repl) → RBI-state key value tree repl stack -- two stages up top-black : {tree repl : bt (Color ∧ A) } → {stack : List (bt (Color ∧ A))} → stack ≡ tree ∷ [] @@ -1731,131 +1730,26 @@ → stackInvariant key tree1 tree0 stack → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → (exit : (stack : List ( bt (Color ∧ A))) (r : RBI key value tree0 stack ) → t ) → t -replaceRBTNode {n} {m} {A} {t} key value orig rbi ti tree stack si P exit with stackToPG tree orig stack si -... | case1 x = ? -... | case2 (case1 x) = ? -... | case2 (case2 pg) = rp01 where - rb00 : stackInvariant key tree orig (tree ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) - rb00 = subst (λ k → stackInvariant key tree orig k) (PG.stack=gp pg) si - treerb : RBtreeInvariant (PG.parent pg) - treerb = PGtoRBinvariant1 _ orig rbi _ (popStackInvariant _ _ _ _ _ rb00) - pti : treeInvariant (PG.parent pg) - pti = siToTreeinvariant _ _ _ _ ti (popStackInvariant _ _ _ _ _ rb00) - rp01 : t - rp01 with PG.pg pg - ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ with <-cmp key kp | proj1 vp in pcolor - ... | tri< a ¬b ¬c | Red = buildCase1 tree refl P where - rb04 : proj1 vp ≡ Red → ⟪ Red , proj2 vp ⟫ ≡ vp - rb04 refl = refl - rb07 : key < kp - rb07 = a - buildCase1 : (tree1 : bt (Color ∧ A)) → tree1 ≡ tree → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) → t - buildCase1 leaf refl (case1 refl) = exit (PG.grand pg ∷ PG.rest pg) record { - tree = PG.grand pg - ; repl = to-red ( node kg vg (to-black (node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1)) n2 ) - ; origti = ti - ; origrb = rbi - ; treerb = PGtoRBinvariant1 _ orig rbi _ (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)) - ; replrb = rb-red _ ? ? ? ? ? ? - ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) - ; state = rotate ? ? ? ? } - buildCase1 (node key₁ ⟪ c₁ , value₁ ⟫ left right) refl (case2 refl) = exit (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record { - tree = PG.parent pg - ; repl = rb01 - ; origti = ti - ; origrb = rbi - ; treerb = PGtoRBinvariant1 _ orig rbi _ (popStackInvariant _ _ _ _ _ rb00) - ; replrb = subst (λ k → RBtreeInvariant k) (cong (λ k → node kp k _ n1) (rb04 pcolor)) rb11 - ; si = popStackInvariant _ _ _ _ _ rb00 - ; state = rebuild (cong color x) rb06 (subst (λ k → replacedRBTree key value k _) (sym x) (rbr-left refl rb07 rbr-node )) } where - rb01 : bt (Color ∧ A) - rb01 = node kp vp (node key ⟪ c₁ , value ⟫ left right) n1 - rb08 : black-depth (node key₁ ⟪ c₁ , value₁ ⟫ left right) ≡ black-depth n1 - rb08 = RBtreeEQ (subst (λ k → RBtreeInvariant k) x treerb) - rb09 : (c₁ : Color ) → black-depth (node key₁ ⟪ c₁ , value ⟫ left right) ≡ black-depth (node key₁ ⟪ c₁ , value₁ ⟫ left right) - rb09 Red = refl - rb09 Black = refl - rb03 : black-depth (node key₁ ⟪ c₁ , value ⟫ left right) ≡ black-depth n1 - rb03 = trans (rb09 c₁) rb08 - rb05 : RBtreeInvariant (node key ⟪ c₁ , value ⟫ left right) - rb05 with RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x treerb) - ... | rb-red _ _ x₁ x₂ x₃ t t₁ = rb-red _ value x₁ x₂ x₃ t t₁ - ... | rb-black _ _ x₁ t t₁ = rb-black _ value x₁ t t₁ - rb10 : (vp : Color ∧ A) → black-depth (node kp vp (node key₁ ⟪ c₁ , value ⟫ left right) n1) - ≡ black-depth (node kp vp (node key₁ ⟪ c₁ , value₁ ⟫ left right) n1) - rb10 ⟪ Red , _ ⟫ = cong (λ k → k ⊔ black-depth n1 ) (rb09 c₁) - rb10 ⟪ Black , _ ⟫ = cong (λ k → suc (k ⊔ black-depth n1 )) (rb09 c₁) - rb06 : black-depth rb01 ≡ black-depth (PG.parent pg) - rb06 = trans (rb10 vp) (cong black-depth (sym x)) - rb11 : RBtreeInvariant (node kp ⟪ Red , proj2 vp ⟫ (node key₁ ⟪ c₁ , value ⟫ left right) n1) - rb11 with subst (λ k → RBtreeInvariant k) x treerb - ... | rb-red .kp value₂ x x₁ x₂ t t₁ = rb-red kp value₂ x x₁ rb03 rb05 t₁ - ... | tri< a ¬b ¬c | Black = buildCase1 tree refl P where - rb04 : proj1 vp ≡ Black → ⟪ Black , proj2 vp ⟫ ≡ vp - rb04 refl = refl - rb07 : key < kp - rb07 = a - buildCase1 : (tree1 : bt (Color ∧ A)) → tree1 ≡ tree → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) → t - buildCase1 leaf refl (case1 refl) = exit (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record { - tree = PG.parent pg - ; repl = rb01 - ; origti = ti - ; origrb = rbi - ; treerb = PGtoRBinvariant1 _ orig rbi _ (popStackInvariant _ _ _ _ _ rb00) - ; replrb = subst (λ k → RBtreeInvariant k) (cong (λ k → node kp k (node key ⟪ Red , value ⟫ leaf leaf) n1) (rb04 pcolor)) rb02 - ; si = popStackInvariant _ _ _ _ _ rb00 - ; state = rebuild (cong color x) rb05 rb06 } where - rb01 : bt (Color ∧ A) - rb01 = node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1 - rb03 : 1 ≡ black-depth n1 - rb03 = RBtreeEQ (subst (λ k → RBtreeInvariant k) x treerb) - rb02 : RBtreeInvariant (node kp ⟪ Black , proj2 vp ⟫ (node key ⟪ Red , value ⟫ leaf leaf) n1) - rb02 = rb-black kp (proj2 vp) rb03 (rb-red _ _ refl refl refl rb-leaf rb-leaf) (RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x treerb)) - rb06 : replacedRBTree key value (PG.parent pg) (node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1) - rb06 = subst₂ (λ j k → replacedRBTree key value k (node kp j (node key ⟪ Red , value ⟫ leaf leaf) n1)) (rb04 pcolor) - (trans (cong (λ k → node kp k leaf n1) (rb04 pcolor)) (sym x)) ( rbr-black-left refl rb07 rbr-leaf ) - rb05 : black-depth rb01 ≡ black-depth (PG.parent pg) - rb05 = begin - black-depth (node kp vp (node key ⟪ Red , value ⟫ leaf leaf) n1) ≡⟨ cong (λ k → black-depth (node kp k _ n1)) (sym (rb04 pcolor)) ⟩ - black-depth (node kp ⟪ Black , proj2 vp ⟫ (node key ⟪ Red , value ⟫ leaf leaf) n1) ≡⟨ refl ⟩ - black-depth (node kp ⟪ Black , proj2 vp ⟫ leaf n1 ) ≡⟨ cong (λ k → black-depth (node kp k leaf n1)) (rb04 pcolor) ⟩ - black-depth (node kp vp leaf n1) ≡⟨ cong black-depth (sym x) ⟩ - black-depth (PG.parent pg) ∎ where - open ≡-Reasoning - buildCase1 (node key₁ ⟪ c₁ , value₁ ⟫ left right) refl (case2 refl) = exit (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record { - tree = PG.parent pg - ; repl = rb01 - ; origti = ti - ; origrb = rbi - ; treerb = PGtoRBinvariant1 _ orig rbi _ (popStackInvariant _ _ _ _ _ rb00) - ; replrb = subst (λ k → RBtreeInvariant k) (cong (λ k → node kp k _ n1) (rb04 pcolor)) (rb-black _ _ rb03 - rb05 (RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x treerb))) - ; si = popStackInvariant _ _ _ _ _ rb00 - ; state = rebuild (cong color x) rb06 (subst (λ k → replacedRBTree key value k _) (sym x) (rbr-left refl rb07 rbr-node )) } where - rb01 : bt (Color ∧ A) - rb01 = node kp vp (node key ⟪ c₁ , value ⟫ left right) n1 - rb08 : black-depth (node key₁ ⟪ c₁ , value₁ ⟫ left right) ≡ black-depth n1 - rb08 = RBtreeEQ (subst (λ k → RBtreeInvariant k) x treerb) - rb09 : (c₁ : Color ) → black-depth (node key₁ ⟪ c₁ , value ⟫ left right) ≡ black-depth (node key₁ ⟪ c₁ , value₁ ⟫ left right) - rb09 Red = refl - rb09 Black = refl - rb03 : black-depth (node key₁ ⟪ c₁ , value ⟫ left right) ≡ black-depth n1 - rb03 = trans (rb09 c₁) rb08 - rb05 : RBtreeInvariant (node key ⟪ c₁ , value ⟫ left right) - rb05 with RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x treerb) - ... | rb-red _ _ x₁ x₂ x₃ t t₁ = rb-red _ value x₁ x₂ x₃ t t₁ - ... | rb-black _ _ x₁ t t₁ = rb-black _ value x₁ t t₁ - rb06 : black-depth rb01 ≡ black-depth (PG.parent pg) - rb06 = trans (rb10 vp) (cong black-depth (sym x)) where - rb10 : (vp : Color ∧ A) → black-depth (node kp vp (node key₁ ⟪ c₁ , value ⟫ left right) n1) - ≡ black-depth (node kp vp (node key₁ ⟪ c₁ , value₁ ⟫ left right) n1) - rb10 ⟪ Red , _ ⟫ = cong (λ k → k ⊔ black-depth n1 ) (rb09 c₁) - rb10 ⟪ Black , _ ⟫ = cong (λ k → suc (k ⊔ black-depth n1 )) (rb09 c₁) - ... | tri≈ ¬a b ¬c | t = ⊥-elim ( si-property-pne _ _ stack (trans (PG.stack=gp pg) (cong (λ k → tree ∷ k ∷ _) x) ) si b ) - ... | tri> ¬a ¬b c | t = ? - rp01 | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!} - rp01 | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!} - rp01 | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!} +replaceRBTNode {n} {m} {A} {t} key value orig rbi ti leaf stack si (case1 refl) exit = exit ? record { + tree = ? + ; repl = ? + ; origti = ti + ; origrb = rbi + ; treerb = ? + ; replrb = ? + ; si = ? + ; state = rotate ? ? ? + } +replaceRBTNode {n} {m} {A} {t} key value orig rbi ti (node key₁ value₁ left right) stack si (case2 x) exit = exit ? record { + tree = ? + ; repl = ? + ; origti = ti + ; origrb = rbi + ; treerb = ? + ; replrb = ? + ; si = ? + ; state = rebuild ? ? ? + } -- -- rotate and rebuild replaceTree and rb-invariant @@ -1994,34 +1888,38 @@ ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? - ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} 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 = 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)) - } (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 = si-property-> ? rb05 (subst (λ k → stackInvariant key (RBI.tree r) orig - (RBI.tree r ∷ k ∷ PG.grand pg ∷ PG.rest pg)) x (rb00 pg)) - 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-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = rebuildCase2 where + rebuildCase2 : t + rebuildCase2 with <-cmp key kp + ... | tri< a ¬b ¬c = ? + ... | 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 = 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 → 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 = c + 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 -- -- both parent and uncle are Red, rotate then goto rebuild -- @@ -2051,7 +1949,10 @@ insertCase51 : t insertCase51 with PG.pg pg - ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = next (PG.grand pg ∷ PG.rest pg) record { + ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = insertCase52 where + insertCase52 : t + insertCase52 with <-cmp key kp + ... | tri< a ¬b ¬c = next (PG.grand pg ∷ PG.rest pg) record { tree = PG.grand pg ; repl = rb01 ; origti = RBI.origti r @@ -2068,8 +1969,7 @@ 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 = si-property-< ? (subst (λ k → treeInvariant k) x rb08) (subst (λ k → stackInvariant key (RBI.tree r) orig - (RBI.tree r ∷ k ∷ PG.grand pg ∷ PG.rest pg)) x (rb00)) + rb04 = a rb16 : color n1 ≡ Black rb16 = proj2 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) x rb09) (trans (cong color (sym x)) pcolor)) rb13 : ⟪ Red , proj2 vp ⟫ ≡ vp @@ -2117,6 +2017,8 @@ 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} x x₁ = ? ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? @@ -2128,7 +2030,7 @@ rb00 : RBI.tree r ≡ orig rb00 with si-property-last _ _ _ _ (subst (λ k → stackInvariant key (RBI.tree r) orig k) (eq) (RBI.si r)) ... | refl = refl - ... | rotate repl-red pdepth-eq ¬leaf rot with stackToPG (RBI.tree r) orig stack (RBI.si r) + ... | rotate repl-red pdepth-eq rot with stackToPG (RBI.tree r) orig stack (RBI.si r) ... | case1 eq = exit stack eq r -- no stack, replace top node ... | case2 (case1 eq) = insertCase4 orig refl eq rot (case1 repl-red) (RBI.si r) -- one level stack, orig is parent of repl ... | case2 (case2 pg) with color (PG.parent pg) in pcolor @@ -2142,7 +2044,8 @@ rb08 pg = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (rb00 pg)) insertCase1 : t insertCase1 with PG.pg pg - ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record { + ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ with <-cmp key kp + ... | tri< a ¬b ¬c = next (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record { tree = PG.parent pg ; repl = rb01 ; origti = RBI.origti r @@ -2156,8 +2059,7 @@ rb01 : bt (Color ∧ A) rb01 = node kp vp repl n1 rb03 : key < kp - rb03 = si-property-< ¬leaf (subst (λ k → treeInvariant k) x (rb08 pg)) (subst (λ k → stackInvariant key (RBI.tree r) orig - (RBI.tree r ∷ k ∷ PG.grand pg ∷ PG.rest pg)) x (rb00 pg)) + rb03 = a rb04 : ⟪ Black , proj2 vp ⟫ ≡ vp rb04 with subst (λ k → color k ≡ Black) x pcolor ... | refl = refl @@ -2179,89 +2081,93 @@ 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)))) - ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? - ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? - ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? + ... | 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 = ? + insertCase1 | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? + insertCase1 | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? + insertCase1 | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = ? ... | 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 ... | node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ with PG.pg pg -- insertCase2 : uncle and parent are Red, flip color and go up by two level - ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = next (PG.grand pg ∷ (PG.rest pg)) - record { - tree = PG.grand pg - ; repl = to-red (node kg vg (to-black (node kp vp repl n1)) (to-black (PG.uncle pg))) - ; origti = RBI.origti r - ; origrb = RBI.origrb r - ; treerb = rb01 - ; replrb = rb-red _ _ refl (RBtreeToBlackColor _ rb02) rb12 (rb-black _ _ rb13 (RBI.replrb r) rb04) (RBtreeToBlack _ rb02) - ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) - ; state = rotate refl rb17 ? (subst₂ (λ j k → replacedRBTree key value j k ) (sym rb09) refl (rbr-flip-ll 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 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01) - rb03 : RBtreeInvariant (PG.parent pg) - rb03 = RBtreeLeftDown _ _ (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 = si-property-< ¬leaf rb07 (subst (λ k → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ k ∷ PG.grand pg ∷ PG.rest pg)) x 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 : PG.grand pg ≡ node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) (PG.uncle pg) - rb09 = 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 (RBI.tree r) n1) (PG.uncle pg) ≡⟨ cong₂ (λ j k → node kg j (node kp k (RBI.tree r) n1) (PG.uncle pg)) rb10 rb11 ⟩ - node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) (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) ≡⟨ 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 = 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 (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 ⟩ - 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 )) ⟩ - black-depth (PG.grand 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-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = insertCase2 where + insertCase2 : t + insertCase2 with <-cmp key kp + ... | tri< a ¬b ¬c = next (PG.grand pg ∷ (PG.rest pg)) + record { + tree = PG.grand pg + ; repl = to-red (node kg vg (to-black (node kp vp repl n1)) (to-black (PG.uncle pg))) + ; origti = RBI.origti r + ; origrb = RBI.origrb r + ; treerb = rb01 + ; replrb = rb-red _ _ refl (RBtreeToBlackColor _ rb02) rb12 (rb-black _ _ rb13 (RBI.replrb r) rb04) (RBtreeToBlack _ rb02) + ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) + ; state = rotate refl rb17 (subst₂ (λ j k → replacedRBTree key value j k ) (sym rb09) refl (rbr-flip-ll 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 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01) + rb03 : RBtreeInvariant (PG.parent pg) + rb03 = RBtreeLeftDown _ _ (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 = a + 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 : PG.grand pg ≡ node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) (PG.uncle pg) + rb09 = 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 (RBI.tree r) n1) (PG.uncle pg) ≡⟨ cong₂ (λ j k → node kg j (node kp k (RBI.tree r) n1) (PG.uncle pg)) rb10 rb11 ⟩ + node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) (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) ≡⟨ 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 = 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 (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 ⟩ + 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 )) ⟩ + black-depth (PG.grand 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 + ... | 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} x x₁ = {!!} ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!} ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!} - - -