Mercurial > hg > Gears > GearsAgda
changeset 909:15a47dd48d8e
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 01 Jun 2024 20:35:37 +0900 |
| parents | a1b7703f8551 |
| children | e587d7a1634f |
| files | hoareBinaryTree1.agda |
| diffstat | 1 files changed, 185 insertions(+), 137 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree1.agda Fri May 31 17:23:46 2024 +0900 +++ b/hoareBinaryTree1.agda Sat Jun 01 20:35:37 2024 +0900 @@ -183,14 +183,6 @@ si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ _ _ _ si ) with si-property1 si ... | refl = si-property-last key x t0 (x ∷ st) si -si-property-not-orig-leaf : {n : Level} {A : Set} {stack : List ( bt A)} {tree orig : bt A} {key : ℕ} → stackInvariant key tree orig stack → ¬ ( orig ≡ leaf ) -si-property-not-orig-leaf {n} {A} {stack} {tree} {orig} {key} (s-nil ) = ? -si-property-not-orig-leaf {n} {A} {stack} {tree} {orig} {key} (s-right _ _ _ _ si) = ? -si-property-not-orig-leaf {n} {A} {stack} {tree} {orig} {key} (s-left _ _ _ _ si) = ? - --- 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 - -- Diffkey : {n : Level} (A : Set n) (tree0 : bt A) → (key : ℕ) → (tree : bt A) → (stack : List (bt A)) → (si : stackInvariant key tree tree0 stack) → Set -- Diffkey A leaf key .leaf .(leaf ∷ []) s-nil = ? -- Diffkey A (node key₁ value tree0 tree1) key .(node key₁ value tree0 tree1) .(node key₁ value tree0 tree1 ∷ []) s-nil = ? @@ -796,6 +788,12 @@ 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 : ℕ} + → RBtreeInvariant (node key value left right) + → proj1 value ≡ Red + → (color left ≡ Black) ∧ (color right ≡ Black) +RBtreeChildrenColorBlack left right (rb-red _ _ x x₁ x₂ rbi rbi₁) refl = ⟪ x , x₁ ⟫ + -- -- findRBT exit with replaced node -- case-eq node value is replaced, just do replacedTree and rebuild rb-invariant @@ -937,14 +935,14 @@ -- data RBI-state {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree repl : bt (Color ∧ A) ) → (stak : List (bt (Color ∧ A))) → Set n where - rebuild : {tree repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → black-depth repl ≡ black-depth tree + rebuild : {tree repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → color tree ≡ color repl → black-depth repl ≡ black-depth tree → (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 → (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 ∷ [] - → (rotated : replacedRBTree key value (to-black tree) repl) + → (rotated : replacedRBTree key value tree repl ∨ replacedRBTree key value (to-black tree) repl) → RBI-state key value tree repl stack record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A))) : Set n where @@ -1806,31 +1804,56 @@ → stack1 ≡ (orig ∷ []) → RBI key value orig repl stack1 → t ) → t -replaceRBP {n} {m} {A} {t} key value orig repl stack r next exit with RBI.state r -... | rebuild bdepth-eq rot = ? where -- rebuildRBT key value orig repl stack r bdepth-eq next exit - rebuildCase : (tr0 : bt (Color ∧ A)) → tr0 ≡ orig → stackInvariant key (RBI.tree r) orig stack → t - rebuildCase tr0 eq1 si = ? -... | top-black eq rot = {!!} -... | rotate repl-red pdepth< 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 (RBI.si r) where - -- +replaceRBP {n} {m} {A} {t} key value orig repl stack r next exit = replaceRBP1 where -- 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 - rb01 : stackInvariant key (RBI.tree r) orig stack - rb01 = RBI.si r insertCase12 : (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 si = ⊥-elim (rb04 eq eq1 si) where -- can't happen + insertCase12 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 si with <-cmp key key₁ | child-replaced key (node key₁ value₁ left right) in creq - ... | tri< a ¬b ¬c | cr = exit (to-black (node key₁ value₁ repl right)) (orig ∷ []) refl record { + insertCase12 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 + rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl with si-property1 si + ... | refl = ⊥-elim ( nat-<> x a ) + rb06 : black-depth repl ≡ black-depth right + rb06 = begin + black-depth repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ + black-depth (RBI.tree r) ≡⟨ cong black-depth (sym (rb04 si eq refl)) ⟩ + black-depth left ≡⟨ (RBtreeEQ (RBI.origrb r)) ⟩ + black-depth right ∎ + 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) + (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) ) + (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 { + tree = orig + ; ¬leaf = λ () + ; origti = RBI.origti r + ; origrb = RBI.origrb r + ; treerb = RBI.origrb r + ; 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 = λ () ; origti = RBI.origti r @@ -1838,50 +1861,20 @@ ; treerb = RBI.origrb r ; replrb = rb-black _ _ rb06 (RBI.replrb r) (RBtreeRightDown _ _ (RBI.origrb r)) ; si = s-nil - ; state = top-black refl (rbr-black-left repl-red a (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) rot)) - } 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 - rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl with si-property1 si - ... | refl = ⊥-elim ( nat-<> x a ) - rb05 : child-replaced key (node key₁ value₁ left right) ≡ left - rb05 with <-cmp key key₁ - ... | tri< a ¬b ¬c = refl - ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a) - ... | tri> ¬a ¬b c = ⊥-elim (¬a a) - rb06 : black-depth repl ≡ black-depth right - rb06 = begin - black-depth repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ - black-depth (RBI.tree r) ≡⟨ cong black-depth (sym (rb04 si eq refl)) ⟩ - black-depth left ≡⟨ (RBtreeEQ (RBI.origrb r)) ⟩ - black-depth right ∎ - where open ≡-Reasoning - ... | tri≈ ¬a b ¬c | cr = ⊥-elim ( rb06 _ eq (RBI.si r) b ) where -- can't happen + ; 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 → key ≡ key₁ → ⊥ rb06 (.right ∷ node key₁ value₁ left right ∷ []) refl (s-right .right .(node key₁ value₁ left right) .left x s-nil) eq = ⊥-elim ( nat-≡< (sym eq) x) rb06 (.left ∷ node key₁ value₁ left right ∷ []) refl (s-left .left .(node key₁ value₁ left right) .right x s-nil) eq = ⊥-elim ( nat-≡< eq x) - ... | tri> ¬a ¬b c | cr = exit (to-black (node key₁ value₁ left repl)) (orig ∷ []) refl record { - tree = orig - ; ¬leaf = λ () - ; origti = RBI.origti r - ; origrb = RBI.origrb r - ; treerb = RBI.origrb r - ; replrb = rb-black _ _ (sym rb06) (RBtreeLeftDown _ _ (RBI.origrb r)) (RBI.replrb r) - ; si = s-nil - ; state = top-black refl (rbr-black-right repl-red c (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) rot)) - } where + ... | tri> ¬a ¬b c = rb07 col where rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → right ≡ RBI.tree r rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl = refl rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x si) refl refl with si-property1 si ... | refl = ⊥-elim ( nat-<> x c ) - rb05 : child-replaced key (node key₁ value₁ left right) ≡ right - rb05 with <-cmp key key₁ - ... | tri< a ¬b ¬c = ⊥-elim (¬c c) - ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c) - ... | tri> ¬a ¬b c = refl rb06 : black-depth repl ≡ black-depth left rb06 = begin black-depth repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ @@ -1889,87 +1882,142 @@ black-depth right ≡⟨ (sym (RBtreeEQ (RBI.origrb r))) ⟩ black-depth left ∎ where open ≡-Reasoning -... | case2 (case2 pg) with color (PG.parent pg) in pcolor -... | Black = ? -- rebuildRBT key value orig ? ? ? ? next exit where -- insertCase1 -- parent is Black -... | 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 -... | 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 - ; ¬leaf = subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ()) + 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) ) + (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) ) + (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 { + tree = orig + ; ¬leaf = λ () + ; origti = RBI.origti r + ; origrb = RBI.origrb r + ; treerb = RBI.origrb r + ; 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 = λ () ; 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-< (RBI.¬leaf r) 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-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₁ = {!!} + ; treerb = RBI.origrb r + ; 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))) + } + replaceRBP1 : t + replaceRBP1 with RBI.state r + ... | rebuild ceq bdepth-eq rot = rebuildCase orig refl where -- rebuildRBT key value orig repl stack r bdepth-eq next exit + rebuildCase : (tr0 : bt (Color ∧ A)) → tr0 ≡ orig → t + rebuildCase tr0 eq 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 (case2 pg) = next ? (PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) record { + tree = PG.parent pg + ; ¬leaf = ? + ; origti = RBI.origti r + ; origrb = RBI.origrb r + ; treerb = ? + ; replrb = ? + ; si = popStackInvariant _ _ _ _ _ rb00 + ; state = rebuild ? ? ? + } ? 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) + ... | top-black eq rot = {!!} + ... | rotate repl-red pdepth< 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 ? (RBI.si r) -- one level stack, orig is parent of repl + ... | case2 (case2 pg) with color (PG.parent pg) in pcolor + ... | Black = ? -- rebuildRBT key value orig ? ? ? ? next exit where -- insertCase1 -- parent is Black + ... | 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 + ... | 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 + ; ¬leaf = subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ()) + ; 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-< (RBI.¬leaf r) 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-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₁ = {!!}