Mercurial > hg > Gears > GearsAgda
changeset 913:f2b78b3a5fb2
case5 1/4 done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 03 Jun 2024 15:07:48 +0900 |
| parents | e4a185896b7e |
| children | e87dca1b4c21 |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 145 insertions(+), 104 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Sun Jun 02 13:44:30 2024 +0900 +++ b/hoareBinaryTree1.agda Mon Jun 03 15:07:48 2024 +0900 @@ -279,7 +279,7 @@ ... | tri≈ ¬a b ¬c = node key₁ value left right ... | tri> ¬a ¬b c = right -child-replaced-left : {n : Level} {A : Set n} {key key₁ : ℕ} {value : A} {left right : bt A} +child-replaced-left : {n : Level} {A : Set n} {key key₁ : ℕ} {value : A} {left right : bt A} → key < key₁ → child-replaced key (node key₁ value left right) ≡ left child-replaced-left {n} {A} {key} {key₁} {value} {left} {right} lt = ch00 (node key₁ value left right) refl lt where @@ -289,7 +289,7 @@ ... | tri≈ ¬a b ¬c = ⊥-elim (¬a lt1) ... | tri> ¬a ¬b c = ⊥-elim (¬a lt1) -child-replaced-right : {n : Level} {A : Set n} {key key₁ : ℕ} {value : A} {left right : bt A} +child-replaced-right : {n : Level} {A : Set n} {key key₁ : ℕ} {value : A} {left right : bt A} → key₁ < key → child-replaced key (node key₁ value left right) ≡ right child-replaced-right {n} {A} {key} {key₁} {value} {left} {right} lt = ch00 (node key₁ value left right) refl lt where @@ -299,7 +299,7 @@ ... | tri≈ ¬a b ¬c = ⊥-elim (¬c lt1) ... | tri> ¬a ¬b c = refl -child-replaced-eq : {n : Level} {A : Set n} {key key₁ : ℕ} {value : A} {left right : bt A} +child-replaced-eq : {n : Level} {A : Set n} {key key₁ : ℕ} {value : A} {left right : bt A} → key₁ ≡ key → child-replaced key (node key₁ value left right) ≡ node key₁ value left right child-replaced-eq {n} {A} {key} {key₁} {value} {left} {right} lt = ch00 (node key₁ value left right) refl lt where @@ -760,7 +760,7 @@ RBtreeEQ (rb-red _ _ x x₁ x₂ rb rb₁) = x₂ RBtreeEQ (rb-black _ _ x rb rb₁) = x -RBtreeToBlack : {n : Level} {A : Set n} +RBtreeToBlack : {n : Level} {A : Set n} → (tree : bt (Color ∧ A)) → RBtreeInvariant tree → RBtreeInvariant (to-black tree) @@ -768,7 +768,7 @@ RBtreeToBlack (node key ⟪ Red , value ⟫ left right) (rb-red _ _ x x₁ x₂ rb rb₁) = rb-black key value x₂ rb rb₁ RBtreeToBlack (node key ⟪ Black , value ⟫ left right) (rb-black _ _ x rb rb₁) = rb-black key value x rb rb₁ -RBtreeToBlackColor : {n : Level} {A : Set n} +RBtreeToBlackColor : {n : Level} {A : Set n} → (tree : bt (Color ∧ A)) → RBtreeInvariant tree → color (to-black tree) ≡ Black @@ -778,7 +778,7 @@ RBtreeParentColorBlack : {n : Level} {A : Set n} → (left right : bt (Color ∧ A)) { value : A} {key : ℕ} { c : Color} → RBtreeInvariant (node key ⟪ c , value ⟫ left right) - → (color left ≡ Red) ∨ (color right ≡ Red) + → (color left ≡ Red) ∨ (color right ≡ Red) → c ≡ Black RBtreeParentColorBlack leaf leaf (rb-red _ _ x₁ x₂ x₃ x₄ x₅) (case1 ()) RBtreeParentColorBlack leaf leaf (rb-red _ _ x₁ x₂ x₃ x₄ x₅) (case2 ()) @@ -788,10 +788,10 @@ RBtreeParentColorBlack left (node key ⟪ Black , proj4 ⟫ right right₁) (rb-red _ _ x x₁ x₂ rb rb₁) (case2 ()) RBtreeParentColorBlack left right (rb-black _ _ x rb rb₁) x₃ = refl -RBtreeChildrenColorBlack : {n : Level} {A : Set n} → (left right : bt (Color ∧ A)) { value : Color ∧ A} {key : ℕ} +RBtreeChildrenColorBlack : {n : Level} {A : Set n} → (left right : bt (Color ∧ A)) { value : Color ∧ A} {key : ℕ} → RBtreeInvariant (node key value left right) → proj1 value ≡ Red - → (color left ≡ Black) ∧ (color right ≡ Black) + → (color left ≡ Black) ∧ (color right ≡ Black) RBtreeChildrenColorBlack left right (rb-red _ _ x x₁ x₂ rbi rbi₁) refl = ⟪ x , x₁ ⟫ -- @@ -971,10 +971,10 @@ red-children-eq : {n : Level} {A : Set n} {tree left right : bt (Color ∧ A)} → {key : ℕ} → {value : A} → {c : Color} → tree ≡ node key ⟪ c , value ⟫ left right - → c ≡ Red + → c ≡ Red → RBtreeInvariant tree → (black-depth tree ≡ black-depth left ) ∧ (black-depth tree ≡ black-depth right) -red-children-eq {n} {A} {.(node key₁ ⟪ Red , value₁ ⟫ left right)} {left} {right} {.key₁} {.value₁} {Red} refl eq₁ rb2@(rb-red key₁ value₁ x x₁ x₂ rb rb₁) = +red-children-eq {n} {A} {.(node key₁ ⟪ Red , value₁ ⟫ left right)} {left} {right} {.key₁} {.value₁} {Red} refl eq₁ rb2@(rb-red key₁ value₁ x x₁ x₂ rb rb₁) = ⟪ ( begin black-depth left ⊔ black-depth right ≡⟨ cong (λ k → black-depth left ⊔ k) (sym (RBtreeEQ rb2)) ⟩ black-depth left ⊔ black-depth left ≡⟨ ⊔-idem _ ⟩ @@ -987,17 +987,17 @@ black-children-eq : {n : Level} {A : Set n} {tree left right : bt (Color ∧ A)} → {key : ℕ} → {value : A} → {c : Color} → tree ≡ node key ⟪ c , value ⟫ left right - → c ≡ Black + → c ≡ Black → RBtreeInvariant tree → (black-depth tree ≡ suc (black-depth left) ) ∧ (black-depth tree ≡ suc (black-depth right)) -black-children-eq {n} {A} {.(node key₁ ⟪ Black , value₁ ⟫ left right)} {left} {right} {.key₁} {.value₁} {Black} refl eq₁ rb2@(rb-black key₁ value₁ x rb rb₁) = +black-children-eq {n} {A} {.(node key₁ ⟪ Black , value₁ ⟫ left right)} {left} {right} {.key₁} {.value₁} {Black} refl eq₁ rb2@(rb-black key₁ value₁ x rb rb₁) = ⟪ ( begin suc (black-depth left ⊔ black-depth right) ≡⟨ cong (λ k → suc (black-depth left ⊔ k)) (sym (RBtreeEQ rb2)) ⟩ suc (black-depth left ⊔ black-depth left) ≡⟨ ⊔-idem _ ⟩ suc (black-depth left) ∎ ) , ( begin suc (black-depth left ⊔ black-depth right) ≡⟨ cong (λ k → suc (k ⊔ black-depth right)) (RBtreeEQ rb2) ⟩ - suc (black-depth right ⊔ black-depth right) ≡⟨ ⊔-idem _ ⟩ + suc (black-depth right ⊔ black-depth right) ≡⟨ ⊔-idem _ ⟩ suc (black-depth right) ∎ ) ⟫ where open ≡-Reasoning black-children-eq {n} {A} {tree} {left} {right} {key} {value} {Red} eq () rb @@ -1667,7 +1667,7 @@ → ( tree orig : bt (Color ∧ A)) → (key : ℕ) → treeInvariant orig → stackInvariant key tree orig ( tree ∷ rest ) - → treeInvariant tree + → treeInvariant tree siToTreeinvariant .[] tree .tree key ti s-nil = ti siToTreeinvariant .(node _ _ leaf leaf ∷ []) .leaf .(node _ _ leaf leaf) key (t-single _ _) (s-right .leaf .(node _ _ leaf leaf) .leaf x s-nil) = t-leaf siToTreeinvariant .(node _ _ leaf (node key₁ _ _ _) ∷ []) .(node key₁ _ _ _) .(node _ _ leaf (node key₁ _ _ _)) key (t-right _ key₁ x₁ x₂ x₃ ti) (s-right .(node key₁ _ _ _) .(node _ _ leaf (node key₁ _ _ _)) .leaf x s-nil) = ti @@ -1698,9 +1698,9 @@ ... | t-left key₁ _ x₂ x₃ x₄ t = t ... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ t t₁ = t -PGtoRBinvariant1 : {n : Level} {A : Set n} +PGtoRBinvariant1 : {n : Level} {A : Set n} → (tree orig : bt (Color ∧ A) ) - → {key : ℕ } + → {key : ℕ } → (rb : RBtreeInvariant orig) → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) → RBtreeInvariant tree @@ -1719,11 +1719,6 @@ ... | tri≈ ¬a b ¬c = rbi ... | tri> ¬a ¬b c = RBtreeRightDown _ _ rbi --- this is too complacted to extend all arguments at once --- --- RBTtoRBI : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A)) → (key : ℕ) → (value : A) → RBtreeInvariant tree --- → replacedRBTree key value tree repl → RBtreeInvariant repl --- RBTtoRBI {_} {A} tree repl key value rbi rlt = ? -- -- create RBT invariant after findRBT, continue to replaceRBT -- @@ -1737,61 +1732,9 @@ → (exit : (r : RBI key value tree0 tree1 stack ) → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )) → t replaceRBTNode key value tree0 rbi tree1 stack rbi-stack exit = {!!} -insertCase5 : {n m : Level} {A : Set n} {t : Set m} - → (key : ℕ) → (value : A) - → (orig tree : bt (Color ∧ A)) - → (stack : List (bt (Color ∧ A))) - → (r : RBI key value orig tree stack ) - → (pg : PG (Color ∧ A) tree stack) - → color (PG.uncle pg) ≡ Black → color (PG.parent pg) ≡ Red - → (next : (tree1 : (bt (Color ∧ A))) → (stack1 : List (bt (Color ∧ A))) - → (r : RBI key value orig tree1 stack1 ) - → length stack1 < length stack → t ) → t -insertCase5 {n} {m} {A} {t} key value orig tree stack r pg cu=b cp=r next = insertCase51 tree (PG.grand pg) refl refl where - -- check inner repl case - -- node-key parent < node-key repl < node-key grand → rotateLeft parent then insertCase6 - -- node-key grand < node-key repl < node-key parent → rotateRight parent then insertCase6 - -- else insertCase6 - insertCase51 : (tree1 grand : bt (Color ∧ A)) → tree1 ≡ tree → grand ≡ PG.grand pg → t - insertCase51 leaf grand teq geq = next {!!} {!!} {!!} {!!} - insertCase51 (node kr vr rleft rright) leaf teq geq = {!!} -- can't happen - insertCase51 (node kr vr rleft rright) (node kg vg grand grand₁) teq geq with <-cmp kr kg - ... | tri< a ¬b ¬c = insertCase511 (PG.parent pg) refl where - insertCase511 : (parent : bt (Color ∧ A)) → parent ≡ PG.parent pg → t - insertCase511 leaf peq = ⊥-elim (proj2 (pg-prop-1 _ tree orig stack pg) (sym peq) ) - insertCase511 (node key₂ ⟪ co , value ⟫ n1 n2) peq with <-cmp key key₂ - ... | tri< a ¬b ¬c = next {!!} {!!} {!!} {!!} - ... | tri≈ ¬a b ¬c = {!!} -- can't happen - ... | tri> ¬a ¬b c = next {!!} {!!} {!!} {!!} --- rotareRight → insertCase6 key value orig ? stack ? pg next exit - ... | tri≈ ¬a b ¬c = {!!} -- can't happen - ... | tri> ¬a ¬b c = {!!} where - insertCase511 : (parent : bt (Color ∧ A)) → parent ≡ PG.parent pg → t - insertCase511 leaf peq = ⊥-elim (proj2 (pg-prop-1 _ tree orig stack pg) (sym peq) ) - insertCase511 (node key₂ ⟪ co , value ⟫ n1 n2) peq with <-cmp key key₂ - ... | tri< a ¬b ¬c = next {!!} {!!} {!!} {!!} --- rotareLeft → insertCase6 key value orig ? stack ? pg next exit - ... | tri≈ ¬a b ¬c = {!!} -- can't happen - ... | tri> ¬a ¬b c = next {!!} {!!} {!!} {!!} - --- --- replaced node increase blackdepth, so we need tree rotate --- --- case2 tree is Red --- --- go upward until --- --- if root --- insert top --- if unkle is leaf or Black --- go insertCase5/6 --- --- make color tree ≡ Black , color unkle ≡ Black, color grand ≡ Red --- loop with grand as repl --- --- case5/case6 rotation -- -- rotate and rebuild replaceTree and rb-invariant - - +-- replaceRBP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (orig repl : bt (Color ∧ A)) @@ -1808,19 +1751,18 @@ -- we have no grand parent -- eq : stack₁ ≡ RBI.tree r ∷ orig ∷ [] -- change parent color ≡ Black and exit - -- -- one level stack, orig is parent of repl - insertCase12 : (tr0 : bt (Color ∧ A)) → tr0 ≡ orig + insertCase4 : (tr0 : bt (Color ∧ A)) → tr0 ≡ orig → (eq : stack ≡ RBI.tree r ∷ orig ∷ []) → (rot : replacedRBTree key value (RBI.tree r) repl) → ( color repl ≡ Red ) ∨ (color (RBI.tree r) ≡ color repl) → stackInvariant key (RBI.tree r) orig stack → t - insertCase12 leaf eq1 eq rot col si = ⊥-elim (rb04 eq eq1 si) where -- can't happen + insertCase4 leaf eq1 eq rot col si = ⊥-elim (rb04 eq eq1 si) where -- can't happen rb04 : {stack : List ( bt ( Color ∧ A))} → stack ≡ RBI.tree r ∷ orig ∷ [] → leaf ≡ orig → stackInvariant key (RBI.tree r) orig stack → ⊥ rb04 refl refl (s-right tree leaf tree₁ x si) = si-property2 _ (s-right tree leaf tree₁ x si) refl rb04 refl refl (s-left tree₁ leaf tree x si) = si-property2 _ (s-left tree₁ leaf tree x si) refl - insertCase12 tr0@(node key₁ value₁ left right) refl eq rot col si with <-cmp key key₁ + insertCase4 tr0@(node key₁ value₁ left right) refl eq rot col si with <-cmp key key₁ ... | tri< a ¬b ¬c = rb07 col where rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → left ≡ RBI.tree r rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x s-nil) refl refl = refl @@ -1835,12 +1777,12 @@ where open ≡-Reasoning rb08 : (color (RBI.tree r) ≡ color repl) → RBtreeInvariant (node key₁ value₁ repl right) rb08 ceq with proj1 value₁ in coeq - ... | Red = subst (λ k → RBtreeInvariant (node key₁ k repl right)) (cong (λ k → ⟪ k , _ ⟫) (sym coeq) ) - (rb-red _ (proj2 value₁) rb09 (proj2 (RBtreeChildrenColorBlack _ _ (RBI.origrb r) coeq)) rb06 (RBI.replrb r) + ... | Red = subst (λ k → RBtreeInvariant (node key₁ k repl right)) (cong (λ k → ⟪ k , _ ⟫) (sym coeq) ) + (rb-red _ (proj2 value₁) rb09 (proj2 (RBtreeChildrenColorBlack _ _ (RBI.origrb r) coeq)) rb06 (RBI.replrb r) (RBtreeRightDown _ _ (RBI.origrb r))) where rb09 : color repl ≡ Black rb09 = trans (trans (sym ceq) (sym (cong color (rb04 si eq refl) ))) (proj1 (RBtreeChildrenColorBlack _ _ (RBI.origrb r) coeq)) - ... | Black = subst (λ k → RBtreeInvariant (node key₁ k repl right)) (cong (λ k → ⟪ k , _ ⟫) (sym coeq) ) + ... | Black = subst (λ k → RBtreeInvariant (node key₁ k repl right)) (cong (λ k → ⟪ k , _ ⟫) (sym coeq) ) (rb-black _ (proj2 value₁) rb06 (RBI.replrb r) (RBtreeRightDown _ _ (RBI.origrb r))) rb07 : ( color repl ≡ Red ) ∨ (color (RBI.tree r) ≡ color repl) → t rb07 (case2 cc ) = exit (node key₁ value₁ repl right) (orig ∷ []) refl record { @@ -1852,7 +1794,7 @@ ; replrb = rb08 cc ; si = s-nil ; state = top-black refl (case1 (rbr-left (trans (cong color (rb04 si eq refl)) cc) a (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) rot))) - } + } rb07 (case1 repl-red) = exit (to-black (node key₁ value₁ repl right)) (orig ∷ []) refl record { tree = orig ; ¬leaf = λ () @@ -1862,7 +1804,7 @@ ; replrb = rb-black _ _ rb06 (RBI.replrb r) (RBtreeRightDown _ _ (RBI.origrb r)) ; si = s-nil ; state = top-black refl (case2 (rbr-black-left repl-red a (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) rot))) - } + } ... | tri≈ ¬a b ¬c = ⊥-elim ( rb06 _ eq (RBI.si r) b ) where -- can't happen rb06 : (stack : List (bt (Color ∧ A))) → stack ≡ RBI.tree r ∷ node key₁ value₁ left right ∷ [] → stackInvariant key (RBI.tree r) (node key₁ value₁ left right) stack @@ -1881,15 +1823,15 @@ black-depth (RBI.tree r) ≡⟨ cong black-depth (sym (rb04 si eq refl)) ⟩ black-depth right ≡⟨ (sym (RBtreeEQ (RBI.origrb r))) ⟩ black-depth left ∎ - where open ≡-Reasoning + where open ≡-Reasoning rb08 : (color (RBI.tree r) ≡ color repl) → RBtreeInvariant (node key₁ value₁ left repl ) - rb08 ceq with proj1 value₁ in coeq - ... | Red = subst (λ k → RBtreeInvariant (node key₁ k left repl )) (cong (λ k → ⟪ k , _ ⟫) (sym coeq) ) + rb08 ceq with proj1 value₁ in coeq + ... | Red = subst (λ k → RBtreeInvariant (node key₁ k left repl )) (cong (λ k → ⟪ k , _ ⟫) (sym coeq) ) (rb-red _ (proj2 value₁) (proj1 (RBtreeChildrenColorBlack _ _ (RBI.origrb r) coeq)) rb09 (sym rb06) (RBtreeLeftDown _ _ (RBI.origrb r))(RBI.replrb r)) where rb09 : color repl ≡ Black rb09 = trans (trans (sym ceq) (sym (cong color (rb04 si eq refl) ))) (proj2 (RBtreeChildrenColorBlack _ _ (RBI.origrb r) coeq)) - ... | Black = subst (λ k → RBtreeInvariant (node key₁ k left repl )) (cong (λ k → ⟪ k , _ ⟫) (sym coeq) ) + ... | Black = subst (λ k → RBtreeInvariant (node key₁ k left repl )) (cong (λ k → ⟪ k , _ ⟫) (sym coeq) ) (rb-black _ (proj2 value₁) (sym rb06) (RBtreeLeftDown _ _ (RBI.origrb r)) (RBI.replrb r)) rb07 : ( color repl ≡ Red ) ∨ (color (RBI.tree r) ≡ color repl) → t rb07 (case2 cc ) = exit (node key₁ value₁ left repl ) (orig ∷ []) refl record { @@ -1901,7 +1843,7 @@ ; replrb = rb08 cc ; si = s-nil ; state = top-black refl (case1 (rbr-right (trans (cong color (rb04 si eq refl)) cc) c (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) rot))) - } + } rb07 (case1 repl-red ) = exit (to-black (node key₁ value₁ left repl)) (orig ∷ []) refl record { tree = orig ; ¬leaf = λ () @@ -1911,16 +1853,15 @@ ; replrb = rb-black _ _ (sym rb06) (RBtreeLeftDown _ _ (RBI.origrb r)) (RBI.replrb r) ; si = s-nil ; state = top-black refl (case2 (rbr-black-right repl-red c (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) rot))) - } - rebuildCase : (tr0 : bt (Color ∧ A)) → tr0 ≡ orig - → (ceq : color (RBI.tree r) ≡ color repl) + } + rebuildCase : (ceq : color (RBI.tree r) ≡ color repl) → (bdepth-eq : black-depth repl ≡ black-depth (RBI.tree r)) → (rot : replacedRBTree key value (RBI.tree r) repl ) → t - rebuildCase tr0 eq ceq bdepth-eq rot with stackToPG (RBI.tree r) orig stack (RBI.si r) + rebuildCase ceq bdepth-eq rot with stackToPG (RBI.tree r) orig stack (RBI.si r) ... | case1 x = exit repl stack x r where -- single node case rb00 : stack ≡ orig ∷ [] → orig ≡ RBI.tree r rb00 refl = si-property1 (RBI.si r) - ... | case2 (case1 x) = insertCase12 orig refl x rot (case2 ceq) (RBI.si r) -- one level stack, orig is parent of repl + ... | case2 (case1 x) = insertCase4 orig refl x rot (case2 ceq) (RBI.si r) -- one level stack, orig is parent of repl ... | case2 (case2 pg) = rebuildCase1 pg where rb00 : (pg : PG (Color ∧ A) (RBI.tree r) stack) → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) rb00 pg = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r) @@ -1954,25 +1895,125 @@ rb05 : treeInvariant (node kp vp n1 (RBI.tree r)) rb05 = subst (λ k → treeInvariant k) x (rb08 pg) rb04 : kp < key - rb04 = si-property-> (RBI.¬leaf r) rb05 (subst (λ k → stackInvariant key (RBI.tree r) orig + rb04 = si-property-> (RBI.¬leaf r) 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 + -- + -- both parent and uncle are Red, rotate then goto rebuild + -- + insertCase5 : (repl1 : bt (Color ∧ A)) → repl1 ≡ repl + → (pg : PG (Color ∧ A) (RBI.tree r) stack) + → (rot : replacedRBTree key value (RBI.tree r) repl) + → color repl ≡ Red → color (PG.uncle pg) ≡ Black → color (PG.parent pg) ≡ Red → t + insertCase5 leaf eq pg rot repl-red uncle-black pcolor = ⊥-elim ( rb00 repl repl-red (cong color (sym eq))) where + rb00 : (repl : bt (Color ∧ A)) → color repl ≡ Red → color repl ≡ Black → ⊥ + rb00 (node key ⟪ Black , proj4 ⟫ repl repl₁) () eq1 + rb00 (node key ⟪ Red , proj4 ⟫ repl repl₁) eq () + insertCase5 (node rkey vr rp-left rp-right) eq pg rot repl-red uncle-black pcolor = insertCase51 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) + 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 + rb02 : RBtreeInvariant (PG.grand pg) + rb02 = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)) + rb09 : RBtreeInvariant (PG.parent pg) + rb09 = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ rb00) + rb08 : treeInvariant (PG.parent pg) + rb08 = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00) + + insertCase51 : t + insertCase51 with PG.pg pg + ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = next rb01 (PG.grand pg ∷ PG.rest pg) record { + tree = PG.grand pg + ; ¬leaf = subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ()) + ; 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)) + ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) + ; state = rebuild (trans (cong color x₁) (cong proj1 (sym rb14))) rb17 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 = si-property-< (RBI.¬leaf r) (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)) + rb16 : color n1 ≡ Black + rb16 = proj2 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) x rb09) (trans (cong color (sym x)) pcolor)) + rb13 : ⟪ Red , proj2 vp ⟫ ≡ vp + rb13 with subst (λ k → color k ≡ Red ) x pcolor + ... | refl = refl + rb14 : ⟪ Black , proj2 vg ⟫ ≡ vg + rb14 with RBtreeParentColorBlack _ _ (subst (λ k → RBtreeInvariant k) x₁ rb02) (case1 pcolor) + ... | refl = refl + rb03 : replacedRBTree key value (node kg _ (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) (PG.uncle pg)) + (node kp ⟪ Black , proj2 vp ⟫ repl (node kg ⟪ Red , proj2 vg ⟫ n1 (PG.uncle pg))) + rb03 = rbr-rotate-ll repl-red rb04 rot + rb10 : node kp ⟪ Black , proj2 vp ⟫ repl (node kg ⟪ Red , proj2 vg ⟫ n1 (PG.uncle pg)) ≡ rb01 + rb10 = begin + to-black (node kp vp repl (to-red (node kg vg n1 (PG.uncle pg)))) ≡⟨ cong (λ k → node _ _ k _) (sym eq) ⟩ + rb01 ∎ where open ≡-Reasoning + rb12 : node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) (PG.uncle pg) ≡ PG.grand pg + rb12 = begin + node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) (PG.uncle pg) + ≡⟨ cong₂ (λ j k → node kg j (node kp k (RBI.tree r) n1) (PG.uncle pg) ) rb14 rb13 ⟩ + node kg vg _ (PG.uncle pg) ≡⟨ cong (λ k → node _ _ k _) (sym x) ⟩ + node kg vg (PG.parent pg) (PG.uncle pg) ≡⟨ sym x₁ ⟩ + PG.grand pg ∎ where open ≡-Reasoning + rb11 : replacedRBTree key value (PG.grand pg) rb01 + rb11 = subst₂ (λ j k → replacedRBTree key value j k) rb12 rb10 rb03 + rb05 : RBtreeInvariant (PG.uncle pg) + rb05 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb02) + rb06 : RBtreeInvariant n1 + rb06 = RBtreeRightDown _ _ (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 repl ≡ black-depth n1 ⊔ black-depth (PG.uncle pg) + rb18 = begin + black-depth repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ + black-depth (RBI.tree r) ≡⟨ RBtreeEQ (subst (λ k → RBtreeInvariant k) x rb09) ⟩ + black-depth n1 ≡⟨ sym (⊔-idem (black-depth n1)) ⟩ + black-depth n1 ⊔ black-depth n1 ≡⟨ cong (λ k → black-depth n1 ⊔ k) rb19 ⟩ + black-depth n1 ⊔ black-depth (PG.uncle pg) ∎ where open ≡-Reasoning + rb17 : suc (black-depth (node rkey vr rp-left rp-right) ⊔ (black-depth n1 ⊔ black-depth (PG.uncle pg))) ≡ black-depth (PG.grand pg) + rb17 = begin + suc (black-depth (node rkey vr rp-left rp-right) ⊔ (black-depth n1 ⊔ black-depth (PG.uncle pg))) + ≡⟨ cong₂ (λ j k → suc (black-depth j ⊔ k)) eq (sym rb18) ⟩ + suc (black-depth repl ⊔ black-depth repl) ≡⟨ ⊔-idem _ ⟩ + suc (black-depth repl ) ≡⟨ cong suc (sym (RB-repl→eq _ _ (RBI.treerb r) rot)) ⟩ + suc (black-depth (RBI.tree r) ) ≡⟨ cong suc (sym (proj1 (red-children-eq x (cong proj1 (sym rb13)) rb09))) ⟩ + 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 + ... | 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₁ = ? + replaceRBP1 : t replaceRBP1 with RBI.state r - ... | rebuild ceq bdepth-eq rot = rebuildCase orig refl ceq bdepth-eq rot + ... | rebuild ceq bdepth-eq rot = rebuildCase ceq bdepth-eq rot ... | top-black eq rot = exit repl stack (trans eq (cong (λ k → k ∷ []) rb00)) r where 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 rot with stackToPG (RBI.tree r) orig stack (RBI.si r) ... | case1 eq = exit repl stack eq r -- no stack, replace top node - ... | case2 (case1 eq) = insertCase12 orig refl eq rot (case1 repl-red) (RBI.si r) -- one level stack, orig is parent of repl + ... | 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 ... | Black = insertCase1 where + -- Parent is Black, make color repl ≡ color tree then goto rebuildCase rb00 : (pg : PG (Color ∧ A) (RBI.tree r) stack) → stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) rb00 pg = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r) treerb : (pg : PG (Color ∧ A) (RBI.tree r) stack) → RBtreeInvariant (PG.parent pg) @@ -1987,15 +2028,15 @@ ; origti = RBI.origti r ; origrb = RBI.origrb r ; treerb = treerb pg - ; replrb = ? + ; replrb = rb06 ; si = popStackInvariant _ _ _ _ _ (rb00 pg) - ; state = rebuild (cong color x) (rb05 (trans (sym (cong color x)) pcolor)) + ; state = rebuild (cong color x) (rb05 (trans (sym (cong color x)) pcolor)) (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 = si-property-< (RBI.¬leaf r) (subst (λ k → treeInvariant k) x (rb08 pg)) (subst (λ k → stackInvariant key (RBI.tree r) orig + rb03 = si-property-< (RBI.¬leaf r) (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)) rb04 : ⟪ Black , proj2 vp ⟫ ≡ vp rb04 with subst (λ k → color k ≡ Black) x pcolor @@ -2003,7 +2044,7 @@ 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 + 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 ∎ @@ -2016,15 +2057,15 @@ black-depth (PG.parent pg) ∎ where open ≡-Reasoning rb06 : RBtreeInvariant rb01 - rb06 = subst (λ k → RBtreeInvariant (node kp k repl n1)) rb04 + 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₁ = ? ... | Red with PG.uncle pg in uneq - ... | leaf = {!!} -- insertCase5 - ... | node key₁ ⟪ Black , value₁ ⟫ t₁ t₂ = {!!} -- insertCase5 - ... | node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ with PG.pg pg -- uncle and parent are Red, flip color and go up by two level + ... | 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 -- inswertCse2 : uncle and parent are Red, flip color and go up by two level ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = next (to-red (node kg vg (to-black (node kp vp repl n1)) (to-black (PG.uncle pg)))) (PG.grand pg ∷ (PG.rest pg)) record { tree = PG.grand pg