Mercurial > hg > Gears > GearsAgda
changeset 948:e5288029f850
RBTree fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 20 Jul 2024 17:01:50 +0900 |
| parents | 91137bc52ddd |
| children | 057d3309ed9d |
| files | RBTree.agda RBTree0.agda logic.agda |
| diffstat | 3 files changed, 2389 insertions(+), 312 deletions(-) [+] |
line wrap: on
line diff
--- a/RBTree.agda Tue Jul 09 08:51:13 2024 +0900 +++ b/RBTree.agda Sat Jul 20 17:01:50 2024 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --allow-unsolved-metas #-} +-- {-# OPTIONS --cubical-compatible --allow-unsolved-metas #-} module RBTree where open import Level hiding (suc ; zero ; _⊔_ ) @@ -155,7 +157,7 @@ → treeInvariant (node kp value₂ tree tree₃ ) → stackInvariant key tree orig (tree ∷ node kp value₂ tree tree₃ ∷ stack) → key < kp -si-property-< ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x s-nil) = ⊥-elim (nat-<> x₁ x₂) +si-property-< ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right (node _ _ _ _) _ (node _ _ _ _) x s-nil) = ⊥-elim (nat-<> x₁ x₂) si-property-< ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x (s-right .(node _ _ (node _ _ _ _) (node _ _ _ _)) _ tree₁ x₇ si)) = ⊥-elim (nat-<> x₁ x₂) si-property-< ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x (s-left .(node _ _ (node _ _ _ _) (node _ _ _ _)) _ tree x₇ si)) = ⊥-elim (nat-<> x₁ x₂) si-property-< ne ti (s-left _ _ _ x (s-right .(node _ _ _ _) _ tree₁ x₁ si)) = x @@ -328,253 +330,6 @@ ... | tri≈ ¬a b ¬c = refl ... | tri> ¬a ¬b c = ⊥-elim (¬b (sym lt1)) -record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A ) (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where - field - tree0 : bt A - ti : treeInvariant tree0 - si : stackInvariant key tree tree0 stack - ri : replacedTree key value (child-replaced key tree ) repl - ci : C tree repl stack -- data continuation - -record replacePR' {n : Level} {A : Set n} (key : ℕ) (value : A) (orig : bt A ) (stack : List (bt A)) : Set n where - field - tree repl : bt A - ti : treeInvariant orig - si : stackInvariant key tree orig stack - ri : replacedTree key value (child-replaced key tree) repl - -- treeInvariant of tree and repl is inferred from ti, si and ri. - -replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A) - → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) - → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value (child-replaced key tree) tree1 → t) → t -replaceNodeP k v1 leaf C P next = next (node k v1 leaf leaf) (t-single k v1 ) r-leaf -replaceNodeP k v1 (node .k value t t₁) (case2 refl) P next = next (node k v1 t t₁) (replaceTree1 k value v1 P) - (subst (λ j → replacedTree k v1 j (node k v1 t t₁) ) repl00 r-node) where - repl00 : node k value t t₁ ≡ child-replaced k (node k value t t₁) - repl00 with <-cmp k k - ... | tri< a ¬b ¬c = ⊥-elim (¬b refl) - ... | tri≈ ¬a b ¬c = refl - ... | tri> ¬a ¬b c = ⊥-elim (¬b refl) - -replaceP : {n m : Level} {A : Set n} {t : Set m} - → (key : ℕ) → (value : A) → {tree : bt A} ( repl : bt A) - → (stack : List (bt A)) → replacePR key value tree repl stack (λ _ _ _ → Lift n ⊤) - → (next : ℕ → A → {tree1 : bt A } (repl : bt A) → (stack1 : List (bt A)) - → replacePR key value tree1 repl stack1 (λ _ _ _ → Lift n ⊤) → length stack1 < length stack → t) - → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t -replaceP key value {tree} repl [] Pre next exit = ⊥-elim ( si-property0 (replacePR.si Pre) refl ) -- can't happen -replaceP key value {tree} repl (leaf ∷ []) Pre next exit with si-property-last _ _ _ _ (replacePR.si Pre)-- tree0 ≡ leaf -... | refl = exit (replacePR.tree0 Pre) (node key value leaf leaf) ⟪ replacePR.ti Pre , r-leaf ⟫ -replaceP key value {tree} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁ -... | tri< a ¬b ¬c = exit (replacePR.tree0 Pre) (node key₁ value₁ repl right ) ⟪ replacePR.ti Pre , repl01 ⟫ where - repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ repl right ) - repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre) - repl01 | refl | refl = subst (λ k → replacedTree key value (node key₁ value₁ k right ) (node key₁ value₁ repl right )) repl02 (r-left a repl03) where - repl03 : replacedTree key value ( child-replaced key (node key₁ value₁ left right)) repl - repl03 = replacePR.ri Pre - repl02 : child-replaced key (node key₁ value₁ left right) ≡ left - repl02 with <-cmp key key₁ - ... | tri< a ¬b ¬c = refl - ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a a) - ... | tri> ¬a ¬b c = ⊥-elim ( ¬a a) -... | tri≈ ¬a b ¬c = exit (replacePR.tree0 Pre) repl ⟪ replacePR.ti Pre , repl01 ⟫ where - repl01 : replacedTree key value (replacePR.tree0 Pre) repl - repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre) - repl01 | refl | refl = subst (λ k → replacedTree key value k repl) repl02 (replacePR.ri Pre) where - repl02 : child-replaced key (node key₁ value₁ left right) ≡ node key₁ value₁ left right - repl02 with <-cmp key key₁ - ... | tri< a ¬b ¬c = ⊥-elim ( ¬b b) - ... | tri≈ ¬a b ¬c = refl - ... | tri> ¬a ¬b c = ⊥-elim ( ¬b b) -... | tri> ¬a ¬b c = exit (replacePR.tree0 Pre) (node key₁ value₁ left repl ) ⟪ replacePR.ti Pre , repl01 ⟫ where - repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ left repl ) - repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre) - repl01 | refl | refl = subst (λ k → replacedTree key value (node key₁ value₁ left k ) (node key₁ value₁ left repl )) repl02 (r-right c repl03) where - repl03 : replacedTree key value ( child-replaced key (node key₁ value₁ left right)) repl - repl03 = replacePR.ri Pre - repl02 : child-replaced key (node key₁ value₁ left right) ≡ right - repl02 with <-cmp key key₁ - ... | tri< a ¬b ¬c = ⊥-elim ( ¬c c) - ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c c) - ... | tri> ¬a ¬b c = refl -replaceP {n} {_} {A} key value {tree} repl (leaf ∷ st@(tree1 ∷ st1)) Pre next exit = next key value repl st Post ≤-refl where - Post : replacePR key value tree1 repl (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤) - Post with replacePR.si Pre - ... | s-right _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where - repl09 : tree1 ≡ node key₂ v1 tree₁ leaf - repl09 = si-property1 si - repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) - repl10 with si-property1 si - ... | refl = si - repl07 : child-replaced key (node key₂ v1 tree₁ leaf) ≡ leaf - repl07 with <-cmp key key₂ - ... | tri< a ¬b ¬c = ⊥-elim (¬c x) - ... | tri≈ ¬a b ¬c = ⊥-elim (¬c x) - ... | tri> ¬a ¬b c = refl - repl12 : replacedTree key value (child-replaced key tree1 ) repl - repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07 ) ) (sym (rt-property-leaf (replacePR.ri Pre))) r-leaf - ... | s-left _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where - repl09 : tree1 ≡ node key₂ v1 leaf tree₁ - repl09 = si-property1 si - repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) - repl10 with si-property1 si - ... | refl = si - repl07 : child-replaced key (node key₂ v1 leaf tree₁ ) ≡ leaf - repl07 with <-cmp key key₂ - ... | tri< a ¬b ¬c = refl - ... | tri≈ ¬a b ¬c = ⊥-elim (¬a x) - ... | tri> ¬a ¬b c = ⊥-elim (¬a x) - repl12 : replacedTree key value (child-replaced key tree1 ) repl - repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07) ) (sym (rt-property-leaf (replacePR.ri Pre ))) r-leaf - -- repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07 ) ) (sym (rt-property-leaf (replacePR.ri Pre))) r-leaf -replaceP {n} {_} {A} key value {tree} repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit with <-cmp key key₁ -... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st Post ≤-refl where - Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤) - Post with replacePR.si Pre - ... | s-right _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where - repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right) - repl09 = si-property1 si - repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) - repl10 with si-property1 si - ... | refl = si - repl03 : child-replaced key (node key₁ value₁ left right) ≡ left - repl03 with <-cmp key key₁ - ... | tri< a1 ¬b ¬c = refl - ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a) - ... | tri> ¬a ¬b c = ⊥-elim (¬a a) - repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right - repl02 with repl09 | <-cmp key key₂ - ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt) - ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt) - ... | refl | tri> ¬a ¬b c = refl - repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1 - repl04 = begin - node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03 ⟩ - node key₁ value₁ left right ≡⟨ sym repl02 ⟩ - child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ - child-replaced key tree1 ∎ where open ≡-Reasoning - repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ repl right) - repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right) ) repl04 (r-left a (replacePR.ri Pre)) - ... | s-left _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where - repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁ - repl09 = si-property1 si - repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) - repl10 with si-property1 si - ... | refl = si - repl03 : child-replaced key (node key₁ value₁ left right) ≡ left - repl03 with <-cmp key key₁ - ... | tri< a1 ¬b ¬c = refl - ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a) - ... | tri> ¬a ¬b c = ⊥-elim (¬a a) - repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right - repl02 with repl09 | <-cmp key key₂ - ... | refl | tri< a ¬b ¬c = refl - ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt) - ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt) - repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1 - repl04 = begin - node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03 ⟩ - node key₁ value₁ left right ≡⟨ sym repl02 ⟩ - child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ - child-replaced key tree1 ∎ where open ≡-Reasoning - repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ repl right) - repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right) ) repl04 (r-left a (replacePR.ri Pre)) -... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st Post ≤-refl where - Post : replacePR key value tree1 (node key₁ value left right ) (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤) - Post with replacePR.si Pre - ... | s-right _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 b ; ci = lift tt } where - repl09 : tree1 ≡ node key₂ v1 tree₁ tree -- (node key₁ value₁ left right) - repl09 = si-property1 si - repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) - repl10 with si-property1 si - ... | refl = si - repl07 : child-replaced key (node key₂ v1 tree₁ tree) ≡ tree - repl07 with <-cmp key key₂ - ... | tri< a ¬b ¬c = ⊥-elim (¬c x) - ... | tri≈ ¬a b ¬c = ⊥-elim (¬c x) - ... | tri> ¬a ¬b c = refl - repl12 : (key ≡ key₁) → replacedTree key value (child-replaced key tree1 ) (node key₁ value left right ) - repl12 refl with repl09 - ... | refl = subst (λ k → replacedTree key value k (node key₁ value left right )) (sym repl07) r-node - ... | s-left _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 b ; ci = lift tt } where - repl09 : tree1 ≡ node key₂ v1 tree tree₁ - repl09 = si-property1 si - repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) - repl10 with si-property1 si - ... | refl = si - repl07 : child-replaced key (node key₂ v1 tree tree₁ ) ≡ tree - repl07 with <-cmp key key₂ - ... | tri< a ¬b ¬c = refl - ... | tri≈ ¬a b ¬c = ⊥-elim (¬a x) - ... | tri> ¬a ¬b c = ⊥-elim (¬a x) - repl12 : (key ≡ key₁) → replacedTree key value (child-replaced key tree1 ) (node key₁ value left right ) - repl12 refl with repl09 - ... | refl = subst (λ k → replacedTree key value k (node key₁ value left right )) (sym repl07) r-node -... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st Post ≤-refl where - Post : replacePR key value tree1 (node key₁ value₁ left repl ) st (λ _ _ _ → Lift n ⊤) - Post with replacePR.si Pre - ... | s-right _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where - repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right) - repl09 = si-property1 si - repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) - repl10 with si-property1 si - ... | refl = si - repl03 : child-replaced key (node key₁ value₁ left right) ≡ right - repl03 with <-cmp key key₁ - ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c) - ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c) - ... | tri> ¬a ¬b c = refl - repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right - repl02 with repl09 | <-cmp key key₂ - ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt) - ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt) - ... | refl | tri> ¬a ¬b c = refl - repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1 - repl04 = begin - node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩ - node key₁ value₁ left right ≡⟨ sym repl02 ⟩ - child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ - child-replaced key tree1 ∎ where open ≡-Reasoning - repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ left repl) - repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ left repl) ) repl04 (r-right c (replacePR.ri Pre)) - ... | s-left _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where - repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁ - repl09 = si-property1 si - repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) - repl10 with si-property1 si - ... | refl = si - repl03 : child-replaced key (node key₁ value₁ left right) ≡ right - repl03 with <-cmp key key₁ - ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c) - ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c) - ... | tri> ¬a ¬b c = refl - repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right - repl02 with repl09 | <-cmp key key₂ - ... | refl | tri< a ¬b ¬c = refl - ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt) - ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt) - repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1 - repl04 = begin - node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩ - node key₁ value₁ left right ≡⟨ sym repl02 ⟩ - child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ - child-replaced key tree1 ∎ where open ≡-Reasoning - repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ left repl) - repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ left repl) ) repl04 (r-right c (replacePR.ri Pre)) - -TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) - → (r : Index) → (p : Invraiant r) - → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t -TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r) -... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) -... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (m≤n⇒m≤1+n lt1) p1 lt1 ) where - TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t - TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) - TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) - ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt - ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 ) - ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) - open _∧_ ri-tr> : {n : Level} {A : Set n} → (tree repl : bt A) → (key key₁ : ℕ) → (value : A) @@ -679,6 +434,337 @@ -- RTtoTI1 (node key₁ value₁ (node key₂ value₂ n n₁) _) (node key₁ _ _ _) key value (t-node _ _ _ x₁ x₂ a b c d ti ti₁) (r-left x ri) = -- t-node _ _ _ (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) x₂ ? ? c d (RTtoTI1 _ _ key value ti ri) ti₁ -- key₂ < key₁ +popStackInvariant : {n : Level} {A : Set n} → (rest : List ( bt A)) + → ( tree parent orig : bt A) → (key : ℕ) + → stackInvariant key tree orig ( tree ∷ parent ∷ rest ) + → stackInvariant key parent orig (parent ∷ rest ) +popStackInvariant rest tree parent orig key (s-right .tree .orig tree₁ x si) = sc00 where + sc00 : stackInvariant key parent orig (parent ∷ rest ) + sc00 with si-property1 si + ... | refl = si +popStackInvariant rest tree parent orig key (s-left .tree .orig tree₁ x si) = sc00 where + sc00 : stackInvariant key parent orig (parent ∷ rest ) + sc00 with si-property1 si + ... | refl = si + + +siToTreeinvariant : {n : Level} {A : Set n} → (rest : List ( bt A)) + → ( tree orig : bt A) → (key : ℕ) + → treeInvariant orig + → stackInvariant key tree orig ( tree ∷ rest ) + → 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 +siToTreeinvariant .(node _ _ (node key₁ _ _ _) leaf ∷ []) .leaf .(node _ _ (node key₁ _ _ _) leaf) key (t-left key₁ _ x₁ x₂ x₃ ti) (s-right .leaf .(node _ _ (node key₁ _ _ _) leaf) .(node key₁ _ _ _) x s-nil) = t-leaf +siToTreeinvariant .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _) ∷ []) .(node key₂ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) key (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node key₂ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) .(node key₁ _ _ _) x s-nil) = ti₁ +siToTreeinvariant .(node _ _ tree₁ tree ∷ _) tree orig key ti (s-right .tree .orig tree₁ x si2@(s-right .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2 +... | t-single _ _ = t-leaf +... | t-right _ key₁ x₂ x₃ x₄ ti₁ = ti₁ +... | t-left key₁ _ x₂ x₃ x₄ ti₁ = t-leaf +... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ ti₁ ti₂ = ti₂ +siToTreeinvariant .(node _ _ tree₁ tree ∷ _) tree orig key ti (s-right .tree .orig tree₁ x si2@(s-left .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2 +... | t-single _ _ = t-leaf +... | t-right _ key₁ x₂ x₃ x₄ ti₁ = ti₁ +... | t-left key₁ _ x₂ x₃ x₄ ti₁ = t-leaf +... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ ti₁ ti₂ = ti₂ +siToTreeinvariant .(node _ _ leaf leaf ∷ []) .leaf .(node _ _ leaf leaf) key (t-single _ _) (s-left .leaf .(node _ _ leaf leaf) .leaf x s-nil) = t-leaf +siToTreeinvariant .(node _ _ leaf (node key₁ _ _ _) ∷ []) .leaf .(node _ _ leaf (node key₁ _ _ _)) key (t-right _ key₁ x₁ x₂ x₃ ti) (s-left .leaf .(node _ _ leaf (node key₁ _ _ _)) .(node key₁ _ _ _) x s-nil) = t-leaf +siToTreeinvariant .(node _ _ (node key₁ _ _ _) leaf ∷ []) .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) leaf) key (t-left key₁ _ x₁ x₂ x₃ ti) (s-left .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) leaf) .leaf x s-nil) = ti +siToTreeinvariant .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _) ∷ []) .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) key (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-left .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) .(node key₂ _ _ _) x s-nil) = ti +siToTreeinvariant .(node _ _ tree tree₁ ∷ _) tree orig key ti (s-left .tree .orig tree₁ x si2@(s-right .(node _ _ tree tree₁) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2 +... | t-single _ _ = t-leaf +... | t-right _ key₁ x₂ x₃ x₄ t = t-leaf +... | t-left key₁ _ x₂ x₃ x₄ t = t +... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ t t₁ = t +siToTreeinvariant .(node _ _ tree tree₁ ∷ _) tree orig key ti (s-left .tree .orig tree₁ x si2@(s-left .(node _ _ tree tree₁) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2 +... | t-single _ _ = t-leaf +... | t-right _ key₁ x₂ x₃ x₄ t = t-leaf +... | t-left key₁ _ x₂ x₃ x₄ t = t +... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ t t₁ = t + +record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A ) (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where + field + tree0 : bt A + ti : treeInvariant tree0 + si : stackInvariant key tree tree0 stack + ri : replacedTree key value (child-replaced key tree ) repl + rti : treeInvariant repl + ci : C tree repl stack -- data continuation + +replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A) + → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) + → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value (child-replaced key tree) tree1 → t) → t +replaceNodeP k v1 leaf C P next = next (node k v1 leaf leaf) (t-single k v1 ) r-leaf +replaceNodeP k v1 (node .k value t t₁) (case2 refl) P next = next (node k v1 t t₁) (replaceTree1 k value v1 P) + (subst (λ j → replacedTree k v1 j (node k v1 t t₁) ) repl00 r-node) where + repl00 : node k value t t₁ ≡ child-replaced k (node k value t t₁) + repl00 with <-cmp k k + ... | tri< a ¬b ¬c = ⊥-elim (¬b refl) + ... | tri≈ ¬a b ¬c = refl + ... | tri> ¬a ¬b c = ⊥-elim (¬b refl) + + +replaceP : {n m : Level} {A : Set n} {t : Set m} + → (key : ℕ) → (value : A) → {tree : bt A} ( repl : bt A) + → (stack : List (bt A)) → replacePR key value tree repl stack (λ _ _ _ → Lift n ⊤) + → (next : ℕ → A → {tree1 : bt A } (repl : bt A) → (stack1 : List (bt A)) + → replacePR key value tree1 repl stack1 (λ _ _ _ → Lift n ⊤) → length stack1 < length stack → t) + → (exit : (tree1 repl : bt A) → treeInvariant repl ∧ replacedTree key value tree1 repl → t) → t +replaceP key value {tree} repl [] Pre next exit = ⊥-elim ( si-property0 (replacePR.si Pre) refl ) -- can't happen +replaceP key value {tree} repl (leaf ∷ []) Pre next exit with si-property-last _ _ _ _ (replacePR.si Pre)-- tree0 ≡ leaf +... | refl = exit (replacePR.tree0 Pre) (node key value leaf leaf) ⟪ t-single _ _ , r-leaf ⟫ +replaceP key value {tree} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁ +... | tri< a ¬b ¬c = exit (replacePR.tree0 Pre) (node key₁ value₁ repl right ) + ⟪ RTtoTI0 _ _ _ _ (replacePR.ti Pre) repl01 , repl01 ⟫ where + repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ repl right ) + repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre) + repl01 | refl | refl = subst (λ k → replacedTree key value (node key₁ value₁ k right ) (node key₁ value₁ repl right )) repl02 (r-left a repl03) where + repl03 : replacedTree key value ( child-replaced key (node key₁ value₁ left right)) repl + repl03 = replacePR.ri Pre + repl02 : child-replaced key (node key₁ value₁ left right) ≡ left + repl02 with <-cmp key key₁ + ... | tri< a ¬b ¬c = refl + ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a a) + ... | tri> ¬a ¬b c = ⊥-elim ( ¬a a) +... | tri≈ ¬a b ¬c = exit (replacePR.tree0 Pre) repl ⟪ RTtoTI0 _ _ _ _ (replacePR.ti Pre) repl01 , repl01 ⟫ where + repl01 : replacedTree key value (replacePR.tree0 Pre) repl + repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre) + repl01 | refl | refl = subst (λ k → replacedTree key value k repl) repl02 (replacePR.ri Pre) where + repl02 : child-replaced key (node key₁ value₁ left right) ≡ node key₁ value₁ left right + repl02 with <-cmp key key₁ + ... | tri< a ¬b ¬c = ⊥-elim ( ¬b b) + ... | tri≈ ¬a b ¬c = refl + ... | tri> ¬a ¬b c = ⊥-elim ( ¬b b) +... | tri> ¬a ¬b c = exit (replacePR.tree0 Pre) (node key₁ value₁ left repl ) ⟪ RTtoTI0 _ _ _ _ (replacePR.ti Pre) repl01 , repl01 ⟫ where + repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ left repl ) + repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre) + repl01 | refl | refl = subst (λ k → replacedTree key value (node key₁ value₁ left k ) (node key₁ value₁ left repl )) repl02 (r-right c repl03) where + repl03 : replacedTree key value ( child-replaced key (node key₁ value₁ left right)) repl + repl03 = replacePR.ri Pre + repl02 : child-replaced key (node key₁ value₁ left right) ≡ right + repl02 with <-cmp key key₁ + ... | tri< a ¬b ¬c = ⊥-elim ( ¬c c) + ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c c) + ... | tri> ¬a ¬b c = refl +replaceP {n} {_} {A} key value {tree} repl (leaf ∷ st@(tree1 ∷ st1)) Pre next exit = next key value repl st Post ≤-refl where + Post : replacePR key value tree1 repl (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤) + Post with replacePR.si Pre + ... | s-right _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; + rti = replacePR.rti Pre ; ci = lift tt } where + repl09 : tree1 ≡ node key₂ v1 tree₁ leaf + repl09 = si-property1 si + repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) + repl10 with si-property1 si + ... | refl = si + repl07 : child-replaced key (node key₂ v1 tree₁ leaf) ≡ leaf + repl07 with <-cmp key key₂ + ... | tri< a ¬b ¬c = ⊥-elim (¬c x) + ... | tri≈ ¬a b ¬c = ⊥-elim (¬c x) + ... | tri> ¬a ¬b c = refl + repl12 : replacedTree key value (child-replaced key tree1 ) repl + repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07 ) ) (sym (rt-property-leaf (replacePR.ri Pre))) r-leaf + ... | s-left _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; rti = replacePR.rti Pre ; ri = repl12 ; ci = lift tt } where + repl09 : tree1 ≡ node key₂ v1 leaf tree₁ + repl09 = si-property1 si + repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) + repl10 with si-property1 si + ... | refl = si + repl07 : child-replaced key (node key₂ v1 leaf tree₁ ) ≡ leaf + repl07 with <-cmp key key₂ + ... | tri< a ¬b ¬c = refl + ... | tri≈ ¬a b ¬c = ⊥-elim (¬a x) + ... | tri> ¬a ¬b c = ⊥-elim (¬a x) + repl12 : replacedTree key value (child-replaced key tree1 ) repl + repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07) ) (sym (rt-property-leaf (replacePR.ri Pre ))) r-leaf +replaceP {n} {_} {A} key value {tree} repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit with <-cmp key key₁ +... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st Post ≤-refl where + Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤) + Post with replacePR.si Pre + ... | s-right _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 + ; rti = repl13 + ; ri = repl12 ; ci = lift tt } where + repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right) + repl09 = si-property1 si + repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) + repl10 with si-property1 si + ... | refl = si + repl11 : stackInvariant key (node key₂ v1 tree₁ (node key₁ value₁ left right)) (replacePR.tree0 Pre) (node key₂ v1 tree₁ (node key₁ value₁ left right)∷ st1) + repl11 = subst (λ k → stackInvariant key k (replacePR.tree0 Pre) (k ∷ st1)) repl09 repl10 + repl03 : child-replaced key (node key₁ value₁ left right) ≡ left + repl03 with <-cmp key key₁ + ... | tri< a1 ¬b ¬c = refl + ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a) + ... | tri> ¬a ¬b c = ⊥-elim (¬a a) + repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right + repl02 with repl09 | <-cmp key key₂ + ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt) + ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt) + ... | refl | tri> ¬a ¬b c = refl + repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1 + repl04 = begin + node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03 ⟩ + node key₁ value₁ left right ≡⟨ sym repl02 ⟩ + child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ + child-replaced key tree1 ∎ where open ≡-Reasoning + repl05 : node key₁ value₁ left right ≡ child-replaced key tree1 + repl05 = begin + node key₁ value₁ left right ≡⟨ sym repl02 ⟩ + child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ + child-replaced key tree1 ∎ where open ≡-Reasoning + repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ repl right) + repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right) ) repl04 (r-left a (replacePR.ri Pre)) + repl13 : treeInvariant (node key₁ value₁ repl right) + repl13 = RTtoTI0 _ _ _ _ (subst (λ k → treeInvariant k) repl05 (treeRightDown _ _ (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) repl11 ) )) repl12 + ... | s-left _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; rti = repl13 ; ri = repl12 ; ci = lift tt } where + repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁ + repl09 = si-property1 si + repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) + repl10 with si-property1 si + ... | refl = si + repl03 : child-replaced key (node key₁ value₁ left right) ≡ left + repl03 with <-cmp key key₁ + ... | tri< a1 ¬b ¬c = refl + ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a) + ... | tri> ¬a ¬b c = ⊥-elim (¬a a) + repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right + repl02 with repl09 | <-cmp key key₂ + ... | refl | tri< a ¬b ¬c = refl + ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt) + ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt) + repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1 + repl04 = begin + node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03 ⟩ + node key₁ value₁ left right ≡⟨ sym repl02 ⟩ + child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ + child-replaced key tree1 ∎ where open ≡-Reasoning + repl05 : node key₁ value₁ left right ≡ child-replaced key tree1 + repl05 = begin + node key₁ value₁ left right ≡⟨ sym repl02 ⟩ + child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ + child-replaced key tree1 ∎ where open ≡-Reasoning + repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ repl right) + repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right) ) repl04 (r-left a (replacePR.ri Pre)) + repl11 = subst (λ k → stackInvariant key k (replacePR.tree0 Pre) (k ∷ st1)) repl09 repl10 + repl13 : treeInvariant (node key₁ value₁ repl right) + repl13 = RTtoTI0 _ _ _ _ (subst (λ k → treeInvariant k) repl05 (treeLeftDown _ _ (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) repl11 ) )) repl12 +... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st Post ≤-refl where + Post : replacePR key value tree1 (node key₁ value left right ) (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤) + Post with replacePR.si Pre + ... | s-right _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; rti = repl13 ; ri = repl12 b ; ci = lift tt } where + repl09 : tree1 ≡ node key₂ v1 tree₁ tree -- (node key₁ value₁ left right) + repl09 = si-property1 si + repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) + repl10 with si-property1 si + ... | refl = si + repl07 : child-replaced key (node key₂ v1 tree₁ tree) ≡ tree + repl07 with <-cmp key key₂ + ... | tri< a ¬b ¬c = ⊥-elim (¬c x) + ... | tri≈ ¬a b ¬c = ⊥-elim (¬c x) + ... | tri> ¬a ¬b c = refl + repl12 : (key ≡ key₁) → replacedTree key value (child-replaced key tree1 ) (node key₁ value left right ) + repl12 refl with repl09 + ... | refl = subst (λ k → replacedTree key value k (node key₁ value left right )) (sym repl07) r-node + repl13 : treeInvariant (node key₁ value left right) + repl13 = RTtoTI0 _ _ _ _ (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) (replacePR.si Pre)) r-node + ... | s-left _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; rti = repl13 ; ri = repl12 b ; ci = lift tt } where + repl09 : tree1 ≡ node key₂ v1 tree tree₁ + repl09 = si-property1 si + repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) + repl10 with si-property1 si + ... | refl = si + repl07 : child-replaced key (node key₂ v1 tree tree₁ ) ≡ tree + repl07 with <-cmp key key₂ + ... | tri< a ¬b ¬c = refl + ... | tri≈ ¬a b ¬c = ⊥-elim (¬a x) + ... | tri> ¬a ¬b c = ⊥-elim (¬a x) + repl12 : (key ≡ key₁) → replacedTree key value (child-replaced key tree1 ) (node key₁ value left right ) + repl12 refl with repl09 + ... | refl = subst (λ k → replacedTree key value k (node key₁ value left right )) (sym repl07) r-node + repl13 : treeInvariant (node key₁ value left right) + repl13 = RTtoTI0 _ _ _ _ (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) (replacePR.si Pre)) r-node +... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st Post ≤-refl where + Post : replacePR key value tree1 (node key₁ value₁ left repl ) st (λ _ _ _ → Lift n ⊤) + Post with replacePR.si Pre + ... | s-right _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; rti = repl13 ; ri = repl12 ; ci = lift tt } where + repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right) + repl09 = si-property1 si + repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) + repl10 with si-property1 si + ... | refl = si + repl03 : child-replaced key (node key₁ value₁ left right) ≡ right + repl03 with <-cmp key key₁ + ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c) + ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c) + ... | tri> ¬a ¬b c = refl + repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right + repl02 with repl09 | <-cmp key key₂ + ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt) + ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt) + ... | refl | tri> ¬a ¬b c = refl + repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1 + repl04 = begin + node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩ + node key₁ value₁ left right ≡⟨ sym repl02 ⟩ + child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ + child-replaced key tree1 ∎ where open ≡-Reasoning + repl05 : node key₁ value₁ left right ≡ child-replaced key tree1 + repl05 = begin + node key₁ value₁ left right ≡⟨ sym repl02 ⟩ + child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ + child-replaced key tree1 ∎ where open ≡-Reasoning + repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ left repl) + repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ left repl) ) repl04 (r-right c (replacePR.ri Pre)) + repl11 = subst (λ k → stackInvariant key k (replacePR.tree0 Pre) (k ∷ st1)) repl09 repl10 + repl13 : treeInvariant (node key₁ value₁ left repl) + repl13 = RTtoTI0 _ _ _ _ (subst (λ k → treeInvariant k) repl05 (treeRightDown _ _ (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) repl11 ) )) repl12 + ... | s-left _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; rti = repl13 ; ri = repl12 ; ci = lift tt } where + repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁ + repl09 = si-property1 si + repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) + repl10 with si-property1 si + ... | refl = si + repl03 : child-replaced key (node key₁ value₁ left right) ≡ right + repl03 with <-cmp key key₁ + ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c) + ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c) + ... | tri> ¬a ¬b c = refl + repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right + repl02 with repl09 | <-cmp key key₂ + ... | refl | tri< a ¬b ¬c = refl + ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt) + ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt) + repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1 + repl04 = begin + node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩ + node key₁ value₁ left right ≡⟨ sym repl02 ⟩ + child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ + child-replaced key tree1 ∎ where open ≡-Reasoning + repl05 : node key₁ value₁ left right ≡ child-replaced key tree1 + repl05 = begin + node key₁ value₁ left right ≡⟨ sym repl02 ⟩ + child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ + child-replaced key tree1 ∎ where open ≡-Reasoning + repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ left repl) + repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ left repl) ) repl04 (r-right c (replacePR.ri Pre)) + repl13 : treeInvariant (node key₁ value₁ left repl) + repl13 = RTtoTI0 _ _ _ _ (subst (λ k → treeInvariant k) repl05 (treeLeftDown _ _ + (siToTreeinvariant _ _ _ _ (replacePR.ti Pre) (subst (λ k → stackInvariant key k (replacePR.tree0 Pre) (k ∷ st1)) repl09 repl10)) )) repl12 + +TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) + → (r : Index) → (p : Invraiant r) + → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t +TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r) +... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) +... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (m≤n⇒m≤1+n lt1) p1 lt1 ) where + TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t + TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) + TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) + ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt + ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 ) + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) + + insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → (exit : (tree repl : bt A) → treeInvariant repl ∧ replacedTree key value tree repl → t ) → t insertTreeP {n} {m} {A} {t} tree key value P0 exit = @@ -687,16 +773,17 @@ $ λ t s P C → replaceNodeP key value t C (proj1 P) $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ bt A ∧ bt A ) {λ p → replacePR key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) (λ _ _ _ → Lift n ⊤ ) } - (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ record { tree0 = tree ; ti = P0 ; si = proj2 P ; ri = R ; ci = lift tt } + (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ record { tree0 = tree ; ti = P0 ; si = proj2 P ; rti = P1 ; ri = R ; ci = lift tt } $ λ p P1 loop → replaceP key value (proj2 (proj2 p)) (proj1 p) P1 (λ key value {tree1} repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ P2 lt ) - $ λ tree repl P → exit tree repl ⟪ RTtoTI0 _ _ _ _ (proj1 P) (proj2 P) , proj2 P ⟫ + $ λ tree repl P → exit tree repl P insertTestP1 = insertTreeP leaf 1 1 t-leaf $ λ _ x0 P0 → insertTreeP x0 2 1 (proj1 P0) $ λ _ x1 P1 → insertTreeP x1 3 2 (proj1 P1) $ λ _ x2 P2 → insertTreeP x2 2 2 (proj1 P2) (λ _ x P → x ) + top-value : {n : Level} {A : Set n} → (tree : bt A) → Maybe A top-value leaf = nothing top-value (node key value tree tree₁) = just value @@ -972,6 +1059,7 @@ origrb : RBtreeInvariant orig treerb : RBtreeInvariant tree -- tree node te be replaced replrb : RBtreeInvariant repl + replti : treeInvariant repl si : stackInvariant key tree orig stack state : RBI-state key value tree repl stack @@ -1774,54 +1862,6 @@ ... | s2-s12p _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫ ... | s2-1s2p _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫ -popStackInvariant : {n : Level} {A : Set n} → (rest : List ( bt (Color ∧ A))) - → ( tree parent orig : bt (Color ∧ A)) → (key : ℕ) - → stackInvariant key tree orig ( tree ∷ parent ∷ rest ) - → stackInvariant key parent orig (parent ∷ rest ) -popStackInvariant rest tree parent orig key (s-right .tree .orig tree₁ x si) = sc00 where - sc00 : stackInvariant key parent orig (parent ∷ rest ) - sc00 with si-property1 si - ... | refl = si -popStackInvariant rest tree parent orig key (s-left .tree .orig tree₁ x si) = sc00 where - sc00 : stackInvariant key parent orig (parent ∷ rest ) - sc00 with si-property1 si - ... | refl = si - - -siToTreeinvariant : {n : Level} {A : Set n} → (rest : List ( bt (Color ∧ A))) - → ( tree orig : bt (Color ∧ A)) → (key : ℕ) - → treeInvariant orig - → stackInvariant key tree orig ( tree ∷ rest ) - → 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 -siToTreeinvariant .(node _ _ (node key₁ _ _ _) leaf ∷ []) .leaf .(node _ _ (node key₁ _ _ _) leaf) key (t-left key₁ _ x₁ x₂ x₃ ti) (s-right .leaf .(node _ _ (node key₁ _ _ _) leaf) .(node key₁ _ _ _) x s-nil) = t-leaf -siToTreeinvariant .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _) ∷ []) .(node key₂ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) key (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node key₂ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) .(node key₁ _ _ _) x s-nil) = ti₁ -siToTreeinvariant .(node _ _ tree₁ tree ∷ _) tree orig key ti (s-right .tree .orig tree₁ x si2@(s-right .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2 -... | t-single _ _ = t-leaf -... | t-right _ key₁ x₂ x₃ x₄ ti₁ = ti₁ -... | t-left key₁ _ x₂ x₃ x₄ ti₁ = t-leaf -... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ ti₁ ti₂ = ti₂ -siToTreeinvariant .(node _ _ tree₁ tree ∷ _) tree orig key ti (s-right .tree .orig tree₁ x si2@(s-left .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2 -... | t-single _ _ = t-leaf -... | t-right _ key₁ x₂ x₃ x₄ ti₁ = ti₁ -... | t-left key₁ _ x₂ x₃ x₄ ti₁ = t-leaf -... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ ti₁ ti₂ = ti₂ -siToTreeinvariant .(node _ _ leaf leaf ∷ []) .leaf .(node _ _ leaf leaf) key (t-single _ _) (s-left .leaf .(node _ _ leaf leaf) .leaf x s-nil) = t-leaf -siToTreeinvariant .(node _ _ leaf (node key₁ _ _ _) ∷ []) .leaf .(node _ _ leaf (node key₁ _ _ _)) key (t-right _ key₁ x₁ x₂ x₃ ti) (s-left .leaf .(node _ _ leaf (node key₁ _ _ _)) .(node key₁ _ _ _) x s-nil) = t-leaf -siToTreeinvariant .(node _ _ (node key₁ _ _ _) leaf ∷ []) .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) leaf) key (t-left key₁ _ x₁ x₂ x₃ ti) (s-left .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) leaf) .leaf x s-nil) = ti -siToTreeinvariant .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _) ∷ []) .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) key (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-left .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) .(node key₂ _ _ _) x s-nil) = ti -siToTreeinvariant .(node _ _ tree tree₁ ∷ _) tree orig key ti (s-left .tree .orig tree₁ x si2@(s-right .(node _ _ tree tree₁) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2 -... | t-single _ _ = t-leaf -... | t-right _ key₁ x₂ x₃ x₄ t = t-leaf -... | t-left key₁ _ x₂ x₃ x₄ t = t -... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ t t₁ = t -siToTreeinvariant .(node _ _ tree tree₁ ∷ _) tree orig key ti (s-left .tree .orig tree₁ x si2@(s-left .(node _ _ tree tree₁) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2 -... | t-single _ _ = t-leaf -... | t-right _ key₁ x₂ x₃ x₄ t = t-leaf -... | 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} → (tree orig : bt (Color ∧ A) ) @@ -1866,6 +1906,7 @@ ; origrb = rbi ; treerb = rb-leaf ; replrb = rb-red key value refl refl refl rb-leaf rb-leaf + ; replti = t-single _ _ ; si = subst (λ k → stackInvariant key k leaf _ ) crbt01 si ; state = rotate leaf refl rbr-leaf } where @@ -1882,6 +1923,7 @@ ; origrb = rbi ; treerb = rbi ; replrb = crbt03 value₁ rbi + ; replti = RTtoTI0 _ _ _ _ (siToTreeinvariant _ _ _ _ ti si) r-node ; si = si ; state = rebuild refl (crbt01 value₁ ) (λ ()) crbt04 } where @@ -1905,6 +1947,7 @@ ; origrb = rbi ; treerb = rb-leaf ; replrb = rb-red key value refl refl refl rb-leaf rb-leaf + ; replti = t-single _ _ ; si = si ; state = rotate leaf refl rbr-leaf } @@ -1917,6 +1960,7 @@ ; origrb = rbi ; treerb = treerb ; replrb = crbt03 value₁ treerb + ; replti = RB-repl→ti _ _ _ _ (siToTreeinvariant _ _ _ _ ti (subst (λ k → stackInvariant _ _ orig (k ∷ _)) eq2 si )) crbt04 ; si = si ; state = rebuild refl (crbt01 value₁ ) (λ ()) crbt04 } where @@ -1933,6 +1977,14 @@ treerb : RBtreeInvariant (node key₁ value₁ left right) treerb = PGtoRBinvariant1 _ orig rbi _ si + +ti-to-black : {n : Level} {A : Set n} → {tree : bt (Color ∧ A)} → treeInvariant tree → treeInvariant (to-black tree) +ti-to-black {n} {A} {.leaf} t-leaf = t-leaf +ti-to-black {n} {A} {.(node key value leaf leaf)} (t-single key value) = t-single key ⟪ Black , proj2 value ⟫ +ti-to-black {n} {A} {.(node key _ leaf (node key₁ _ _ _))} (t-right key key₁ x x₁ x₂ ti) = t-right key key₁ x x₁ x₂ ti +ti-to-black {n} {A} {.(node key₁ _ (node key _ _ _) leaf)} (t-left key key₁ x x₁ x₂ ti) = t-left key key₁ x x₁ x₂ ti +ti-to-black {n} {A} {.(node key₁ _ (node key _ _ _) (node key₂ _ _ _))} (t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁) = t-node key key₁ key₂ x x₁ x₂ x₃ x₄ x₅ ti ti₁ + -- -- rotate and rebuild replaceTree and rb-invariant -- @@ -1994,9 +2046,12 @@ ; origrb = RBI.origrb r ; treerb = RBI.origrb r ; replrb = rb08 cc + ; replti = RB-repl→ti _ _ _ _ (RBI.origti r) rb10 ; 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))) - } + ; state = top-black refl (case1 rb10 ) + } where + rb10 : replacedRBTree key value (node key₁ value₁ left right) (node key₁ value₁ repl right) + rb10 = 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 (orig ∷ []) refl record { tree = orig ; repl = to-black (node key₁ value₁ repl right) @@ -2004,9 +2059,13 @@ ; origrb = RBI.origrb r ; treerb = RBI.origrb r ; replrb = rb-black _ _ rb06 (RBI.replrb r) (RBtreeRightDown _ _ (RBI.origrb r)) + ; replti = RB-repl→ti _ _ _ _ (ti-to-black (RBI.origti r)) rb10 ; 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))) - } + ; state = top-black refl (case2 rb10 ) + } where + rb10 : replacedRBTree key value (node key₁ ⟪ Black , proj2 value₁ ⟫ left right) (node key₁ ⟪ Black , proj2 value₁ ⟫ repl right) + rb10 = rbr-black-left repl-red a (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) rot) + ... | tri≈ ¬a b ¬c = ⊥-elim ( si-property-pne _ _ stack eq si b ) -- can't happen ... | 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 @@ -2037,9 +2096,11 @@ ; origrb = RBI.origrb r ; treerb = RBI.origrb r ; replrb = rb08 cc + ; replti = RB-repl→ti _ _ _ _ (RBI.origti r) rb10 ; 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))) - } + ; state = top-black refl (case1 rb10) + } where + rb10 = 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 (orig ∷ []) refl record { tree = orig ; repl = to-black (node key₁ value₁ left repl) @@ -2047,9 +2108,11 @@ ; origrb = RBI.origrb r ; treerb = RBI.origrb r ; replrb = rb-black _ _ (sym rb06) (RBtreeLeftDown _ _ (RBI.origrb r)) (RBI.replrb r) + ; replti = RB-repl→ti _ _ _ _ (ti-to-black (RBI.origti r)) rb10 ; 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))) - } + ; state = top-black refl (case2 rb10 ) + } where + rb10 = rbr-black-right repl-red c (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) rot) rebuildCase : (ceq : color (RBI.tree r) ≡ color repl) → (bdepth-eq : black-depth repl ≡ black-depth (RBI.tree r)) → (¬ RBI.tree r ≡ leaf) @@ -2077,6 +2140,7 @@ ; origrb = RBI.origrb r ; treerb = treerb pg ; replrb = rb02 + ; replti = RB-repl→ti _ _ _ _ (rb08 pg) (subst (λ k → replacedRBTree key value k rb01) (sym x) (rbr-left ceq rb04 rot)) ; si = popStackInvariant _ _ _ _ _ (rb00 pg) ; state = rebuild (cong color x) rb06 (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())) (subst (λ k → replacedRBTree key value k rb01) (sym x) (rbr-left ceq rb04 rot)) } (subst₂ (λ j k → j < length k ) refl (sym (PG.stack=gp pg)) ≤-refl) where @@ -2106,6 +2170,7 @@ ; origrb = RBI.origrb r ; treerb = treerb pg ; replrb = rb02 + ; replti = RB-repl→ti _ _ _ _ (rb08 pg) (subst (λ k → replacedRBTree key value k rb01) (sym x) (rbr-right ceq rb04 rot)) ; si = popStackInvariant _ _ _ _ _ (rb00 pg) ; state = rebuild (cong color x) rb06 (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())) (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 @@ -2135,6 +2200,7 @@ ; origrb = RBI.origrb r ; treerb = treerb pg ; replrb = rb02 + ; replti = RB-repl→ti _ _ _ _ (rb08 pg) (subst (λ k → replacedRBTree key value k rb01) (sym x) (rbr-left ceq rb04 rot)) ; si = popStackInvariant _ _ _ _ _ (rb00 pg) ; state = rebuild (cong color x) rb06 (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())) (subst (λ k → replacedRBTree key value k rb01) (sym x) (rbr-left ceq rb04 rot)) } (subst₂ (λ j k → j < length k ) refl (sym (PG.stack=gp pg)) ≤-refl) where @@ -2164,6 +2230,7 @@ ; origrb = RBI.origrb r ; treerb = treerb pg ; replrb = rb02 + ; replti = RB-repl→ti _ _ _ _ (rb08 pg) (subst (λ k → replacedRBTree key value k rb01) (sym x) (rbr-right ceq rb04 rot)) ; si = popStackInvariant _ _ _ _ _ (rb00 pg) ; state = rebuild (cong color x) rb06 (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())) (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 @@ -2222,6 +2289,7 @@ ; 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)) + ; replti = RB-repl→ti _ _ _ _ (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00))) rb11 ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) ; state = rebuild (trans (cong color x₁) (cong proj1 (sym rb14))) rb17 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) rb11 } rb15 where @@ -2290,6 +2358,7 @@ ; origrb = RBI.origrb r ; treerb = rb02 ; replrb = rb10 + ; replti = RB-repl→ti _ _ _ _ (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00))) rb11 ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) ; state = rebuild rb33 rb17 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) rb11 } rb15 where @@ -2396,6 +2465,7 @@ ; origrb = RBI.origrb r ; treerb = rb02 ; replrb = rb10 + ; replti = RB-repl→ti _ _ _ _ (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00))) rb11 ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) ; state = rebuild rb33 rb17 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) rb11 } rb15 where @@ -2507,6 +2577,7 @@ ; origrb = RBI.origrb r ; treerb = rb02 ; replrb = subst (λ k → RBtreeInvariant k) rb10 (rb-black _ _ rb18 (rb-red _ _ uncle-black rb16 rb19 rb05 rb06) (RBI.replrb r) ) + ; replti = RB-repl→ti _ _ _ _ (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00))) rb11 ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) ; state = rebuild rb33 rb17 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) rb11 } rb15 where @@ -2594,9 +2665,9 @@ ; origrb = RBI.origrb r ; treerb = treerb pg ; replrb = rb06 + ; replti = RB-repl→ti _ _ _ _ (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (rb00 pg))) rb11 ; 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 )) + ; state = rebuild (cong color x) (rb05 (trans (sym (cong color x)) pcolor)) (subst (λ k → ¬ (k ≡ leaf)) (sym x) (λ ())) rb11 } (subst₂ (λ j k → j < length k ) refl (sym (PG.stack=gp pg)) ≤-refl) where rb01 : bt (Color ∧ A) rb01 = node kp vp repl n1 @@ -2623,6 +2694,7 @@ 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)))) + rb11 = subst (λ k → replacedRBTree key value k (node kp vp repl n1) ) (sym x) (rb02 rb04 ) ... | 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 @@ -2630,6 +2702,7 @@ ; origrb = RBI.origrb r ; treerb = treerb pg ; replrb = rb06 + ; replti = RB-repl→ti _ _ _ _ (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (rb00 pg))) rb11 ; 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 )) @@ -2661,6 +2734,7 @@ 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) ) + rb11 = subst (λ k → replacedRBTree key value k (node kp vp n1 repl) ) (sym x) (rb02 rb04 ) 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 @@ -2668,9 +2742,10 @@ ; origrb = RBI.origrb r ; treerb = treerb pg ; replrb = rb06 + ; replti = RB-repl→ti _ _ _ _ (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (rb00 pg))) rb11 ; 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 )) + rb11 } (subst₂ (λ j k → j < length k ) refl (sym (PG.stack=gp pg)) ≤-refl) where rb01 : bt (Color ∧ A) rb01 = node kp vp repl n1 @@ -2697,6 +2772,7 @@ 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)))) + rb11 = (subst (λ k → replacedRBTree key value k (node kp vp repl n1) ) (sym x) (rb02 rb04 )) 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 @@ -2704,9 +2780,10 @@ ; origrb = RBI.origrb r ; treerb = treerb pg ; replrb = rb06 + ; replti = RB-repl→ti _ _ _ _ (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (rb00 pg))) rb11 ; 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 )) + rb11 } (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) @@ -2735,6 +2812,7 @@ 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) ) + rb11 = (subst (λ k → replacedRBTree key value k (node kp vp n1 repl) ) (sym x) (rb02 rb04 )) ... | 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 @@ -2749,8 +2827,9 @@ ; origrb = RBI.origrb r ; treerb = rb01 ; replrb = rb-red _ _ refl (RBtreeToBlackColor _ rb02) rb12 (rb-black _ _ rb13 (RBI.replrb r) rb04) (RBtreeToBlack _ rb02) + ; replti = RB-repl→ti _ _ _ _ (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00))) rb20 ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) - ; state = rotate _ refl (subst₂ (λ j k → replacedRBTree key value j k ) (sym rb09) refl (rbr-flip-ll repl-red (rb05 refl uneq) rb06 rot)) + ; state = rotate _ refl rb20 } 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) @@ -2805,6 +2884,7 @@ 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 + rb20 = (subst₂ (λ j k → replacedRBTree key value j k ) (sym rb09) refl (rbr-flip-ll repl-red (rb05 refl uneq) rb06 rot)) ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase2 where insertCase2 : t insertCase2 = next (PG.grand pg ∷ (PG.rest pg)) @@ -2815,7 +2895,8 @@ ; 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) + ; replti = RB-repl→ti _ _ _ _ (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00))) rb20 + ; 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 -- @@ -2880,6 +2961,7 @@ 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 + rb20 = subst₂ (λ j k → replacedRBTree key value j k ) rb09 refl (rbr-flip-lr repl-red (rb05 refl uneq) rb06 rb21 rot) ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase2 where insertCase2 : t insertCase2 = next (PG.grand pg ∷ (PG.rest pg)) @@ -2891,6 +2973,7 @@ ; treerb = rb01 ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) ; replrb = rb-red _ _ (RBtreeToBlackColor _ rb02) refl rb12 (RBtreeToBlack _ rb02) (rb-black _ _ rb13 (RBI.replrb r) rb04) + ; replti = RB-repl→ti _ _ _ _ (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00))) rb20 ; 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 @@ -2961,6 +3044,7 @@ 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 + rb20 = subst₂ (λ j k → replacedRBTree key value j k ) rb09 refl (rbr-flip-rl repl-red (rb05 refl uneq) rb21 rb06 rot) ... | 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) @@ -2974,6 +3058,7 @@ ; origrb = RBI.origrb r ; treerb = rb01 ; replrb = rb-red _ _ (RBtreeToBlackColor _ rb02) refl rb12 (RBtreeToBlack _ rb02) (rb-black _ _ (sym rb13) rb04 (RBI.replrb r) ) + ; replti = RB-repl→ti _ _ _ _ (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00))) rb20 ; 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 @@ -3031,6 +3116,8 @@ 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 + rb20 = subst₂ (λ j k → replacedRBTree key value j k ) (sym rb09) refl (rbr-flip-rr repl-red (rb05 refl uneq) rb06 rot) + insertRBTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt (Color ∧ A)) → (key : ℕ) → (value : A) @@ -3044,3 +3131,11 @@ (λ stack → length stack ) st rbi $ λ stack rbi replaceLoop → replaceRBP key value orig stack rbi (λ stack1 rbi1 lt → replaceLoop stack1 rbi1 lt ) $ λ stack eq r → exit stack eq r + + +insertRBTestP1 = insertRBTreeP leaf 1 1 t-leaf rb-leaf + $ λ _ x0 P0 → insertRBTreeP (RBI.repl P0) 2 1 (RBI.replti P0) (RBI.replrb P0) + $ λ _ x0 P0 → insertRBTreeP (RBI.repl P0) 3 2 (RBI.replti P0) (RBI.replrb P0) + $ λ _ x0 P0 → insertRBTreeP (RBI.repl P0) 2 2 (RBI.replti P0) (RBI.replrb P0) + $ λ _ x P → RBI.repl P0 +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/RBTree0.agda Sat Jul 20 17:01:50 2024 +0900 @@ -0,0 +1,1981 @@ +module RBTree0 where + +open import Level hiding (suc ; zero ; _⊔_ ) + +open import Data.Nat hiding (compare) +open import Data.Nat.Properties as NatProp +open import Data.Maybe +-- open import Data.Maybe.Properties +open import Data.Empty +open import Data.List +open import Data.Product + +open import Function as F hiding (const) + +open import Relation.Binary +open import Relation.Binary.PropositionalEquality +open import Relation.Nullary +open import logic + + +-- +-- +-- no children , having left node , having right node , having both +-- +data bt {n : Level} (A : Set n) : Set n where + leaf : bt A + node : (key : ℕ) → (value : A) → + (left : bt A ) → (right : bt A ) → bt A + +node-key : {n : Level} {A : Set n} → bt A → Maybe ℕ +node-key (node key _ _ _) = just key +node-key _ = nothing + +node-value : {n : Level} {A : Set n} → bt A → Maybe A +node-value (node _ value _ _) = just value +node-value _ = nothing + +bt-depth : {n : Level} {A : Set n} → (tree : bt A ) → ℕ +bt-depth leaf = 0 +bt-depth (node key value t t₁) = suc (bt-depth t ⊔ bt-depth t₁ ) + +bt-ne : {n : Level} {A : Set n} {key : ℕ} {value : A} {t t₁ : bt A} → ¬ ( leaf ≡ node key value t t₁ ) +bt-ne {n} {A} {key} {value} {t} {t₁} () + +open import Data.Unit hiding ( _≟_ ) -- ; _≤?_ ; _≤_) + +tr< : {n : Level} {A : Set n} → (key : ℕ) → bt A → Set +tr< {_} {A} key leaf = ⊤ +tr< {_} {A} key (node key₁ value tr tr₁) = (key₁ < key ) ∧ tr< key tr ∧ tr< key tr₁ + +tr> : {n : Level} {A : Set n} → (key : ℕ) → bt A → Set +tr> {_} {A} key leaf = ⊤ +tr> {_} {A} key (node key₁ value tr tr₁) = (key < key₁ ) ∧ tr> key tr ∧ tr> key tr₁ + +-- +-- +data treeInvariant {n : Level} {A : Set n} : (tree : bt A) → Set n where + t-leaf : treeInvariant leaf + t-single : (key : ℕ) → (value : A) → treeInvariant (node key value leaf leaf) + t-right : (key key₁ : ℕ) → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁ + → tr> key t₁ + → tr> key t₂ + → treeInvariant (node key₁ value₁ t₁ t₂) + → treeInvariant (node key value leaf (node key₁ value₁ t₁ t₂)) + t-left : (key key₁ : ℕ) → {value value₁ : A} → {t₁ t₂ : bt A} → key < key₁ + → tr< key₁ t₁ + → tr< key₁ t₂ + → treeInvariant (node key value t₁ t₂) + → treeInvariant (node key₁ value₁ (node key value t₁ t₂) leaf ) + t-node : (key key₁ key₂ : ℕ) → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt A} → key < key₁ → key₁ < key₂ + → tr< key₁ t₁ + → tr< key₁ t₂ + → tr> key₁ t₃ + → tr> key₁ t₄ + → treeInvariant (node key value t₁ t₂) + → treeInvariant (node key₂ value₂ t₃ t₄) + → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) + +-- +-- stack always contains original top at end (path of the tree) +-- +data stackInvariant {n : Level} {A : Set n} (key : ℕ) : (top orig : bt A) → (stack : List (bt A)) → Set n where + s-nil : {tree0 : bt A} → stackInvariant key tree0 tree0 (tree0 ∷ []) + s-right : (tree tree0 tree₁ : bt A) → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} + → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree tree0 (tree ∷ st) + s-left : (tree₁ tree0 tree : bt A) → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} + → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree₁ tree0 (tree₁ ∷ st) + +add< : { i : ℕ } (j : ℕ ) → i < suc i + j +add< {i} j = begin + suc i ≤⟨ m≤m+n (suc i) j ⟩ + suc i + j ∎ where open ≤-Reasoning + +nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ +nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x +nat-<> : { x y : ℕ } → x < y → y < x → ⊥ +nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x + +nat-<≡ : { x : ℕ } → x < x → ⊥ +nat-<≡ (s≤s lt) = nat-<≡ lt + +nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥ +nat-≡< refl lt = nat-<≡ lt + +treeTest1 : bt ℕ +treeTest1 = node 0 0 leaf (node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf)) +treeTest2 : bt ℕ +treeTest2 = node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf) + +treeInvariantTest1 : treeInvariant treeTest1 +treeInvariantTest1 = t-right _ _ (m≤m+n _ 2) + ⟪ add< _ , ⟪ ⟪ add< _ , _ ⟫ , _ ⟫ ⟫ + ⟪ add< _ , ⟪ _ , _ ⟫ ⟫ (t-node _ _ _ (add< 0) (add< 1) ⟪ add< _ , ⟪ _ , _ ⟫ ⟫ _ _ _ (t-left _ _ (add< 0) _ _ (t-single 1 7)) (t-single 5 5) ) + +stack-top : {n : Level} {A : Set n} (stack : List (bt A)) → Maybe (bt A) +stack-top [] = nothing +stack-top (x ∷ s) = just x + +stack-last : {n : Level} {A : Set n} (stack : List (bt A)) → Maybe (bt A) +stack-last [] = nothing +stack-last (x ∷ []) = just x +stack-last (x ∷ s) = stack-last s + +stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] ) +stackInvariantTest1 = s-right _ _ _ (add< 3) (s-nil ) + +si-property0 : {n : Level} {A : Set n} {key : ℕ} {tree tree0 : bt A} → {stack : List (bt A)} → stackInvariant key tree tree0 stack → ¬ ( stack ≡ [] ) +si-property0 (s-nil ) () +si-property0 (s-right _ _ _ x si) () +si-property0 (s-left _ _ _ x si) () + +si-property1 : {n : Level} {A : Set n} {key : ℕ} {tree tree0 tree1 : bt A} → {stack : List (bt A)} → stackInvariant key tree tree0 (tree1 ∷ stack) + → tree1 ≡ tree +si-property1 (s-nil ) = refl +si-property1 (s-right _ _ _ _ si) = refl +si-property1 (s-left _ _ _ _ si) = refl + +si-property2 : {n : Level} {A : Set n} {key : ℕ} {tree tree0 tree1 : bt A} → (stack : List (bt A)) → stackInvariant key tree tree0 (tree1 ∷ stack) + → ¬ ( just leaf ≡ stack-last stack ) +si-property2 (.leaf ∷ []) (s-right _ _ tree₁ x ()) refl +si-property2 (x₁ ∷ x₂ ∷ stack) (s-right _ _ tree₁ x si) eq = si-property2 (x₂ ∷ stack) si eq +si-property2 (.leaf ∷ []) (s-left _ _ tree₁ x ()) refl +si-property2 (x₁ ∷ x₂ ∷ stack) (s-left _ _ tree₁ x si) eq = si-property2 (x₂ ∷ stack) si eq + +si-property-< : {n : Level} {A : Set n} {key kp : ℕ} {value₂ : A} {tree orig tree₃ : bt A} → {stack : List (bt A)} + → ¬ ( tree ≡ leaf ) + → treeInvariant (node kp value₂ tree tree₃ ) + → stackInvariant key tree orig (tree ∷ node kp value₂ tree tree₃ ∷ stack) + → key < kp +si-property-< ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x s-nil) = ⊥-elim (nat-<> x₁ x₂) +si-property-< ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x (s-right .(node _ _ (node _ _ _ _) (node _ _ _ _)) _ tree₁ x₇ si)) = ⊥-elim (nat-<> x₁ x₂) +si-property-< ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node _ _ _ _) _ .(node _ _ _ _) x (s-left .(node _ _ (node _ _ _ _) (node _ _ _ _)) _ tree x₇ si)) = ⊥-elim (nat-<> x₁ x₂) +si-property-< ne ti (s-left _ _ _ x (s-right .(node _ _ _ _) _ tree₁ x₁ si)) = x +si-property-< ne ti (s-left _ _ _ x (s-left .(node _ _ _ _) _ tree₁ x₁ si)) = x +si-property-< ne ti (s-left _ _ _ x s-nil) = x +si-property-< ne (t-single _ _) (s-right _ _ tree₁ x si) = ⊥-elim ( ne refl ) + +si-property-> : {n : Level} {A : Set n} {key kp : ℕ} {value₂ : A} {tree orig tree₃ : bt A} → {stack : List (bt A)} + → ¬ ( tree ≡ leaf ) + → treeInvariant (node kp value₂ tree₃ tree ) + → stackInvariant key tree orig (tree ∷ node kp value₂ tree₃ tree ∷ stack) + → kp < key +si-property-> ne ti (s-right _ _ tree₁ x s-nil) = x +si-property-> ne ti (s-right _ _ tree₁ x (s-right .(node _ _ tree₁ _) _ tree₂ x₁ si)) = x +si-property-> ne ti (s-right _ _ tree₁ x (s-left .(node _ _ tree₁ _) _ tree x₁ si)) = x +si-property-> ne (t-node _ _ _ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-left _ _ _ x s-nil) = ⊥-elim (nat-<> x₁ x₂) +si-property-> ne (t-node _ _ _ x₂ x₃ x₄ x₅ x₆ x₇ ti ti₁) (s-left _ _ _ x (s-right .(node _ _ _ _) _ tree₁ x₁ si)) = ⊥-elim (nat-<> x₂ x₃) +si-property-> ne (t-node _ _ _ x₂ x₃ x₄ x₅ x₆ x₇ ti ti₁) (s-left _ _ _ x (s-left .(node _ _ _ _) _ tree x₁ si)) = ⊥-elim (nat-<> x₂ x₃) +si-property-> ne (t-single _ _) (s-left _ _ _ x s-nil) = ⊥-elim ( ne refl ) +si-property-> ne (t-single _ _) (s-left _ _ _ x (s-right .(node _ _ leaf leaf) _ tree₁ x₁ si)) = ⊥-elim ( ne refl ) +si-property-> ne (t-single _ _) (s-left _ _ _ x (s-left .(node _ _ leaf leaf) _ tree x₁ si)) = ⊥-elim ( ne refl ) + +si-property-last : {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack : List (bt A)) → stackInvariant key tree tree0 stack + → stack-last stack ≡ just tree0 +si-property-last key t t0 (t ∷ []) (s-nil ) = refl +si-property-last key t t0 (.t ∷ x ∷ st) (s-right _ _ _ _ si ) with si-property1 si +... | refl = si-property-last key x t0 (x ∷ st) si +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-pne : {n : Level} {A : Set n} {key key₁ : ℕ} {value₁ : A} (tree orig : bt A) → {left right x : bt A} → (stack : List (bt A)) {rest : List (bt A)} + → stack ≡ x ∷ node key₁ value₁ left right ∷ rest + → stackInvariant key tree orig stack + → ¬ ( key ≡ key₁ ) +si-property-pne tree orig .(tree ∷ node _ _ _ _ ∷ _) refl (s-right .tree .orig tree₁ x si) eq with si-property1 si +... | refl = ⊥-elim ( nat-≡< (sym eq) x) +si-property-pne tree orig .(tree ∷ node _ _ _ _ ∷ _) refl (s-left .tree .orig tree₁ x si) eq with si-property1 si +... | refl = ⊥-elim ( nat-≡< eq x) + +si-property-parent-node : {n : Level} {A : Set n} {key : ℕ} (tree orig : bt A) {x : bt A} + → (stack : List (bt A)) {rest : List (bt A)} + → stackInvariant key tree orig stack + → ¬ ( stack ≡ x ∷ leaf ∷ rest ) +si-property-parent-node {n} {A} tree orig .(tree ∷ leaf ∷ _) (s-right .tree .orig tree₁ x si) refl with si-property1 si +... | () +si-property-parent-node {n} {A} tree orig .(tree ∷ leaf ∷ _) (s-left .tree .orig tree₁ x si) refl with si-property1 si +... | () + + + +open _∧_ + + +depth-1< : {i j : ℕ} → suc i ≤ suc (i Data.Nat.⊔ j ) +depth-1< {i} {j} = s≤s (m≤m⊔n _ j) + +depth-2< : {i j : ℕ} → suc i ≤ suc (j Data.Nat.⊔ i ) +depth-2< {i} {j} = s≤s (m≤n⊔m j i) + +depth-3< : {i : ℕ } → suc i ≤ suc (suc i) +depth-3< {zero} = s≤s ( z≤n ) +depth-3< {suc i} = s≤s (depth-3< {i} ) + + +treeLeftDown : {n : Level} {A : Set n} {k : ℕ} {v1 : A} → (tree tree₁ : bt A ) + → treeInvariant (node k v1 tree tree₁) + → treeInvariant tree +treeLeftDown {n} {A} {_} {v1} leaf leaf (t-single k1 v1) = t-leaf +treeLeftDown {n} {A} {_} {v1} .leaf .(node _ _ _ _) (t-right _ _ x _ _ ti) = t-leaf +treeLeftDown {n} {A} {_} {v1} .(node _ _ _ _) .leaf (t-left _ _ x _ _ ti) = ti +treeLeftDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node _ _ _ x x₁ _ _ _ _ ti ti₁) = ti + +treeRightDown : {n : Level} {A : Set n} {k : ℕ} {v1 : A} → (tree tree₁ : bt A ) + → treeInvariant (node k v1 tree tree₁) + → treeInvariant tree₁ +treeRightDown {n} {A} {_} {v1} .leaf .leaf (t-single _ .v1) = t-leaf +treeRightDown {n} {A} {_} {v1} .leaf .(node _ _ _ _) (t-right _ _ x _ _ ti) = ti +treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .leaf (t-left _ _ x _ _ ti) = t-leaf +treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node _ _ _ x x₁ _ _ _ _ ti ti₁) = ti₁ + +ti-property1 : {n : Level} {A : Set n} {key₁ : ℕ} {value₂ : A} {left right : bt A} → treeInvariant (node key₁ value₂ left right ) → tr< key₁ left ∧ tr> key₁ right +ti-property1 {n} {A} {key₁} {value₂} {.leaf} {.leaf} (t-single .key₁ .value₂) = ⟪ tt , tt ⟫ +ti-property1 {n} {A} {key₁} {value₂} {.leaf} {.(node key₂ _ _ _)} (t-right .key₁ key₂ x x₁ x₂ t) = ⟪ tt , ⟪ x , ⟪ x₁ , x₂ ⟫ ⟫ ⟫ +ti-property1 {n} {A} {key₁} {value₂} {.(node key _ _ _)} {.leaf} (t-left key .key₁ x x₁ x₂ t) = ⟪ ⟪ x , ⟪ x₁ , x₂ ⟫ ⟫ , tt ⟫ +ti-property1 {n} {A} {key₁} {value₂} {.(node key _ _ _)} {.(node key₂ _ _ _)} (t-node key .key₁ key₂ x x₁ x₂ x₃ x₄ x₅ t t₁) + = ⟪ ⟪ x , ⟪ x₂ , x₃ ⟫ ⟫ , ⟪ x₁ , ⟪ x₄ , x₅ ⟫ ⟫ ⟫ + + +findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A)) + → treeInvariant tree ∧ stackInvariant key tree tree0 stack + → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t ) + → (exit : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack + → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t +findP key leaf tree0 st Pre _ exit = exit leaf st Pre (case1 refl) +findP key (node key₁ v1 tree tree₁) tree0 st Pre next exit with <-cmp key key₁ +findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n st Pre (case2 refl) +findP {n} {_} {A} key (node key₁ v1 tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree (tree ∷ st) + ⟪ treeLeftDown tree tree₁ (proj1 Pre) , findP1 a st (proj2 Pre) ⟫ depth-1< where + findP1 : key < key₁ → (st : List (bt A)) → stackInvariant key (node key₁ v1 tree tree₁) tree0 st → stackInvariant key tree tree0 (tree ∷ st) + findP1 a (x ∷ st) si = s-left _ _ _ a si +findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st) ⟪ treeRightDown tree tree₁ (proj1 Pre) , s-right _ _ _ c (proj2 Pre) ⟫ depth-2< + +replaceTree1 : {n : Level} {A : Set n} {t t₁ : bt A } → ( k : ℕ ) → (v1 value : A ) → treeInvariant (node k v1 t t₁) → treeInvariant (node k value t t₁) +replaceTree1 k v1 value (t-single .k .v1) = t-single k value +replaceTree1 k v1 value (t-right _ _ x a b t) = t-right _ _ x a b t +replaceTree1 k v1 value (t-left _ _ x a b t) = t-left _ _ x a b t +replaceTree1 k v1 value (t-node _ _ _ x x₁ a b c d t t₁) = t-node _ _ _ x x₁ a b c d t t₁ + +open import Relation.Binary.Definitions + +lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥ +lemma3 refl () +lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥ +lemma5 (s≤s z≤n) () +¬x<x : {x : ℕ} → ¬ (x < x) +¬x<x (s≤s lt) = ¬x<x lt + +child-replaced : {n : Level} {A : Set n} (key : ℕ) (tree : bt A) → bt A +child-replaced key leaf = leaf +child-replaced key (node key₁ value left right) with <-cmp key key₁ +... | tri< a ¬b ¬c = left +... | 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} + → 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 + ch00 : (tree : bt A) → tree ≡ node key₁ value left right → key < key₁ → child-replaced key tree ≡ left + ch00 (node key₁ value tree tree₁) refl lt1 with <-cmp key key₁ + ... | tri< a ¬b ¬c = refl + ... | 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} + → 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 + ch00 : (tree : bt A) → tree ≡ node key₁ value left right → key₁ < key → child-replaced key tree ≡ right + ch00 (node key₁ value tree tree₁) refl lt1 with <-cmp key key₁ + ... | tri< a ¬b ¬c = ⊥-elim (¬c lt1) + ... | 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} + → 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 + ch00 : (tree : bt A) → tree ≡ node key₁ value left right → key₁ ≡ key → child-replaced key tree ≡ node key₁ value left right + ch00 (node key₁ value tree tree₁) refl lt1 with <-cmp key key₁ + ... | tri< a ¬b ¬c = ⊥-elim (¬b (sym lt1)) + ... | tri≈ ¬a b ¬c = refl + ... | tri> ¬a ¬b c = ⊥-elim (¬b (sym lt1)) + +record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A ) (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where + field + tree0 : bt A + ti : treeInvariant tree0 + si : stackInvariant key tree tree0 stack + ci : C tree repl stack -- data continuation + +record replacePR' {n : Level} {A : Set n} (key : ℕ) (value : A) (orig : bt A ) (stack : List (bt A)) : Set n where + field + tree repl : bt A + ti : treeInvariant orig + si : stackInvariant key tree orig stack + -- treeInvariant of tree and repl is inferred from ti, si and ri. + +replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A) + → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) + → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 → t) → t +replaceNodeP k v1 leaf C P next = next (node k v1 leaf leaf) (t-single k v1 ) +replaceNodeP k v1 (node .k value t t₁) (case2 refl) P next = next (node k v1 t t₁) (replaceTree1 k value v1 P) where + repl00 : node k value t t₁ ≡ child-replaced k (node k value t t₁) + repl00 with <-cmp k k + ... | tri< a ¬b ¬c = ⊥-elim (¬b refl) + ... | tri≈ ¬a b ¬c = refl + ... | tri> ¬a ¬b c = ⊥-elim (¬b refl) + +replaceP : {n m : Level} {A : Set n} {t : Set m} + → (key : ℕ) → (value : A) → {tree : bt A} ( repl : bt A) + → (stack : List (bt A)) → replacePR key value tree repl stack (λ _ _ _ → Lift n ⊤) + → (next : ℕ → A → {tree1 : bt A } (repl : bt A) → (stack1 : List (bt A)) + → replacePR key value tree1 repl stack1 (λ _ _ _ → Lift n ⊤) → length stack1 < length stack → t) + → (exit : (tree1 repl : bt A) → t) → t +replaceP key value {tree} repl [] Pre next exit = ⊥-elim ( si-property0 (replacePR.si Pre) refl ) -- can't happen +replaceP key value {tree} repl (leaf ∷ []) Pre next exit with si-property-last _ _ _ _ (replacePR.si Pre)-- tree0 ≡ leaf +... | refl = exit (replacePR.tree0 Pre) (node key value leaf leaf) +replaceP key value {tree} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁ +... | tri< a ¬b ¬c = exit (replacePR.tree0 Pre) (node key₁ value₁ repl right ) +... | tri≈ ¬a b ¬c = exit (replacePR.tree0 Pre) repl +... | tri> ¬a ¬b c = exit (replacePR.tree0 Pre) (node key₁ value₁ left repl ) +replaceP {n} {_} {A} key value {tree} repl (leaf ∷ st@(tree1 ∷ st1)) Pre next exit = next key value repl st Post ≤-refl where + Post : replacePR key value tree1 repl (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤) + Post with replacePR.si Pre + ... | s-right _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ci = lift tt } where + repl09 : tree1 ≡ node key₂ v1 tree₁ leaf + repl09 = si-property1 si + repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) + repl10 with si-property1 si + ... | refl = si + repl07 : child-replaced key (node key₂ v1 tree₁ leaf) ≡ leaf + repl07 with <-cmp key key₂ + ... | tri< a ¬b ¬c = ⊥-elim (¬c x) + ... | tri≈ ¬a b ¬c = ⊥-elim (¬c x) + ... | tri> ¬a ¬b c = refl + ... | s-left _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ci = lift tt } where + repl09 : tree1 ≡ node key₂ v1 leaf tree₁ + repl09 = si-property1 si + repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) + repl10 with si-property1 si + ... | refl = si + repl07 : child-replaced key (node key₂ v1 leaf tree₁ ) ≡ leaf + repl07 with <-cmp key key₂ + ... | tri< a ¬b ¬c = refl + ... | tri≈ ¬a b ¬c = ⊥-elim (¬a x) + ... | tri> ¬a ¬b c = ⊥-elim (¬a x) +replaceP {n} {_} {A} key value {tree} repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit with <-cmp key key₁ +... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st Post ≤-refl where + Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤) + Post with replacePR.si Pre + ... | s-right _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ci = lift tt } where + repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right) + repl09 = si-property1 si + repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) + repl10 with si-property1 si + ... | refl = si + repl03 : child-replaced key (node key₁ value₁ left right) ≡ left + repl03 with <-cmp key key₁ + ... | tri< a1 ¬b ¬c = refl + ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a) + ... | tri> ¬a ¬b c = ⊥-elim (¬a a) + repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right + repl02 with repl09 | <-cmp key key₂ + ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt) + ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt) + ... | refl | tri> ¬a ¬b c = refl + repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1 + repl04 = begin + node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03 ⟩ + node key₁ value₁ left right ≡⟨ sym repl02 ⟩ + child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ + child-replaced key tree1 ∎ where open ≡-Reasoning + ... | s-left _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ci = lift tt } where + repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁ + repl09 = si-property1 si + repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) + repl10 with si-property1 si + ... | refl = si + repl03 : child-replaced key (node key₁ value₁ left right) ≡ left + repl03 with <-cmp key key₁ + ... | tri< a1 ¬b ¬c = refl + ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a) + ... | tri> ¬a ¬b c = ⊥-elim (¬a a) + repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right + repl02 with repl09 | <-cmp key key₂ + ... | refl | tri< a ¬b ¬c = refl + ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt) + ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt) + repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1 + repl04 = begin + node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03 ⟩ + node key₁ value₁ left right ≡⟨ sym repl02 ⟩ + child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ + child-replaced key tree1 ∎ where open ≡-Reasoning +... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st Post ≤-refl where + Post : replacePR key value tree1 (node key₁ value left right ) (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤) + Post with replacePR.si Pre + ... | s-right _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ci = lift tt } where + repl09 : tree1 ≡ node key₂ v1 tree₁ tree -- (node key₁ value₁ left right) + repl09 = si-property1 si + repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) + repl10 with si-property1 si + ... | refl = si + repl07 : child-replaced key (node key₂ v1 tree₁ tree) ≡ tree + repl07 with <-cmp key key₂ + ... | tri< a ¬b ¬c = ⊥-elim (¬c x) + ... | tri≈ ¬a b ¬c = ⊥-elim (¬c x) + ... | tri> ¬a ¬b c = refl + ... | s-left _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ci = lift tt } where + repl09 : tree1 ≡ node key₂ v1 tree tree₁ + repl09 = si-property1 si + repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) + repl10 with si-property1 si + ... | refl = si + repl07 : child-replaced key (node key₂ v1 tree tree₁ ) ≡ tree + repl07 with <-cmp key key₂ + ... | tri< a ¬b ¬c = refl + ... | tri≈ ¬a b ¬c = ⊥-elim (¬a x) + ... | tri> ¬a ¬b c = ⊥-elim (¬a x) +... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st Post ≤-refl where + Post : replacePR key value tree1 (node key₁ value₁ left repl ) st (λ _ _ _ → Lift n ⊤) + Post with replacePR.si Pre + ... | s-right _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ci = lift tt } where + repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right) + repl09 = si-property1 si + repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) + repl10 with si-property1 si + ... | refl = si + repl03 : child-replaced key (node key₁ value₁ left right) ≡ right + repl03 with <-cmp key key₁ + ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c) + ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c) + ... | tri> ¬a ¬b c = refl + repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right + repl02 with repl09 | <-cmp key key₂ + ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt) + ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt) + ... | refl | tri> ¬a ¬b c = refl + repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1 + repl04 = begin + node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩ + node key₁ value₁ left right ≡⟨ sym repl02 ⟩ + child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ + child-replaced key tree1 ∎ where open ≡-Reasoning + ... | s-left _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ci = lift tt } where + repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁ + repl09 = si-property1 si + repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) + repl10 with si-property1 si + ... | refl = si + repl03 : child-replaced key (node key₁ value₁ left right) ≡ right + repl03 with <-cmp key key₁ + ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c) + ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c) + ... | tri> ¬a ¬b c = refl + repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right + repl02 with repl09 | <-cmp key key₂ + ... | refl | tri< a ¬b ¬c = refl + ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt) + ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt) + repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1 + repl04 = begin + node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩ + node key₁ value₁ left right ≡⟨ sym repl02 ⟩ + child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ + child-replaced key tree1 ∎ where open ≡-Reasoning + +TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) + → (r : Index) → (p : Invraiant r) + → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t +TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r) +... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) +... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (m≤n⇒m≤1+n lt1) p1 lt1 ) where + TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t + TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) + TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) + ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt + ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 ) + ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) + +open _∧_ + + +insertTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree + → (exit : (tree repl : bt A) → treeInvariant repl → t ) → t +insertTreeP {n} {m} {A} {t} tree key value ti exit = ? +-- TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant key (proj1 p) tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , tree ∷ [] ⟫ ⟪ ? , s-nil ⟫ +-- $ λ p P loop → findP key (proj1 p) tree (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt ) +-- $ λ t s P C → replaceNodeP key value t C (proj1 P) +-- $ λ t1 P1 R → TerminatingLoopS (List (bt A) ∧ bt A ∧ bt A ) +-- {λ p → replacePR key value (proj1 (proj2 p)) (proj2 (proj2 p)) (proj1 p) (λ _ _ _ → Lift n ⊤ ) } +-- (λ p → length (proj1 p)) ⟪ s , ⟪ t , t1 ⟫ ⟫ record { tree0 = tree ; ti = ? ; si = proj2 P ; ri = R ; ci = lift tt } +-- $ λ p P1 loop → replaceP key value (proj2 (proj2 p)) (proj1 p) P1 +-- (λ key value {tree1} repl1 stack P2 lt → loop ⟪ stack , ⟪ tree1 , repl1 ⟫ ⟫ P2 lt ) +-- $ λ tree repl P → exit tree repl ? +-- +insertTestP1 = insertTreeP leaf 1 1 t-leaf + $ λ _ x0 P0 → insertTreeP x0 2 1 ? + $ λ _ x1 P1 → insertTreeP x1 3 2 ? + $ λ _ x2 P2 → insertTreeP x2 2 2 ? (λ _ x P → x ) + +top-value : {n : Level} {A : Set n} → (tree : bt A) → Maybe A +top-value leaf = nothing +top-value (node key value tree tree₁) = just value + +-- is realy inserted? + +-- other element is preserved? + +-- deletion? + + +data Color : Set where + Red : Color + Black : Color + +RB→bt : {n : Level} (A : Set n) → (bt (Color ∧ A)) → bt A +RB→bt {n} A leaf = leaf +RB→bt {n} A (node key ⟪ C , value ⟫ tr t1) = (node key value (RB→bt A tr) (RB→bt A t1)) + +color : {n : Level} {A : Set n} → (bt (Color ∧ A)) → Color +color leaf = Black +color (node key ⟪ C , value ⟫ rb rb₁) = C + +to-red : {n : Level} {A : Set n} → (tree : bt (Color ∧ A)) → bt (Color ∧ A) +to-red leaf = leaf +to-red (node key ⟪ _ , value ⟫ t t₁) = (node key ⟪ Red , value ⟫ t t₁) + +to-black : {n : Level} {A : Set n} → (tree : bt (Color ∧ A)) → bt (Color ∧ A) +to-black leaf = leaf +to-black (node key ⟪ _ , value ⟫ t t₁) = (node key ⟪ Black , value ⟫ t t₁) + +black-depth : {n : Level} {A : Set n} → (tree : bt (Color ∧ A) ) → ℕ +black-depth leaf = 1 +black-depth (node key ⟪ Red , value ⟫ t t₁) = black-depth t ⊔ black-depth t₁ +black-depth (node key ⟪ Black , value ⟫ t t₁) = suc (black-depth t ⊔ black-depth t₁ ) + +zero≢suc : { m : ℕ } → zero ≡ suc m → ⊥ +zero≢suc () +suc≢zero : {m : ℕ } → suc m ≡ zero → ⊥ +suc≢zero () + +data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where + rb-leaf : RBtreeInvariant leaf + rb-red : (key : ℕ) → (value : A) → {left right : bt (Color ∧ A)} + → color left ≡ Black → color right ≡ Black + → black-depth left ≡ black-depth right + → RBtreeInvariant left → RBtreeInvariant right + → RBtreeInvariant (node key ⟪ Red , value ⟫ left right) + rb-black : (key : ℕ) → (value : A) → {left right : bt (Color ∧ A)} + → black-depth left ≡ black-depth right + → RBtreeInvariant left → RBtreeInvariant right + → RBtreeInvariant (node key ⟪ Black , value ⟫ left right) + +RightDown : {n : Level} {A : Set n} → bt (Color ∧ A) → bt (Color ∧ A) +RightDown leaf = leaf +RightDown (node key ⟪ c , value ⟫ t1 t2) = t2 +LeftDown : {n : Level} {A : Set n} → bt (Color ∧ A) → bt (Color ∧ A) +LeftDown leaf = leaf +LeftDown (node key ⟪ c , value ⟫ t1 t2 ) = t1 + +RBtreeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color} + → (left right : bt (Color ∧ A)) + → RBtreeInvariant (node key ⟪ c , value ⟫ left right) + → RBtreeInvariant left +RBtreeLeftDown left right (rb-red _ _ x x₁ x₂ rb rb₁) = rb +RBtreeLeftDown left right (rb-black _ _ x rb rb₁) = rb + + +RBtreeRightDown : {n : Level} {A : Set n} { key : ℕ} {value : A} {c : Color} + → (left right : bt (Color ∧ A)) + → RBtreeInvariant (node key ⟪ c , value ⟫ left right) + → RBtreeInvariant right +RBtreeRightDown left right (rb-red _ _ x x₁ x₂ rb rb₁) = rb₁ +RBtreeRightDown left right (rb-black _ _ x rb rb₁) = rb₁ + +RBtreeEQ : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color} + → {left right : bt (Color ∧ A)} + → RBtreeInvariant (node key ⟪ c , value ⟫ left right) + → black-depth left ≡ black-depth right +RBtreeEQ (rb-red _ _ x x₁ x₂ rb rb₁) = x₂ +RBtreeEQ (rb-black _ _ x rb rb₁) = x + +RBtreeToBlack : {n : Level} {A : Set n} + → (tree : bt (Color ∧ A)) + → RBtreeInvariant tree + → RBtreeInvariant (to-black tree) +RBtreeToBlack leaf rb-leaf = rb-leaf +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} + → (tree : bt (Color ∧ A)) + → RBtreeInvariant tree + → color (to-black tree) ≡ Black +RBtreeToBlackColor leaf rb-leaf = refl +RBtreeToBlackColor (node key ⟪ Red , value ⟫ left right) (rb-red _ _ x x₁ x₂ rb rb₁) = refl +RBtreeToBlackColor (node key ⟪ Black , value ⟫ left right) (rb-black _ _ x rb rb₁) = refl + +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) + → c ≡ Black +RBtreeParentColorBlack leaf leaf (rb-red _ _ x₁ x₂ x₃ x₄ x₅) (case1 ()) +RBtreeParentColorBlack leaf leaf (rb-red _ _ x₁ x₂ x₃ x₄ x₅) (case2 ()) +RBtreeParentColorBlack (node key ⟪ Red , proj4 ⟫ left left₁) right (rb-red _ _ () x₁ x₂ rb rb₁) (case1 x₃) +RBtreeParentColorBlack (node key ⟪ Black , proj4 ⟫ left left₁) right (rb-red _ _ x x₁ x₂ rb rb₁) (case1 ()) +RBtreeParentColorBlack left (node key ⟪ Red , proj4 ⟫ right right₁) (rb-red _ _ x () x₂ rb rb₁) (case2 x₃) +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 +-- case-leaf insert new single node +-- case1 if parent node is black, just do replacedTree and rebuild rb-invariant +-- case2 if parent node is red, increase blackdepth, do rotatation +-- + +findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) ) + → (stack : List (bt (Color ∧ A))) + → RBtreeInvariant tree ∧ stackInvariant key tree tree0 stack + → (next : (tree1 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A))) + → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack + → bt-depth tree1 < bt-depth tree → t ) + → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) + → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack + → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t +findRBT key leaf tree0 stack rb0 next exit = exit leaf stack rb0 (case1 refl) +findRBT key (node key₁ value left right) tree0 stack rb0 next exit with <-cmp key key₁ +findRBT key (node key₁ value left right) tree0 stack rb0 next exit | tri< a ¬b ¬c + = next left (left ∷ stack) ⟪ RBtreeLeftDown left right (_∧_.proj1 rb0) , s-left _ _ _ a (_∧_.proj2 rb0) ⟫ depth-1< +findRBT key n tree0 stack rb0 _ exit | tri≈ ¬a refl ¬c = exit n stack rb0 (case2 refl) +findRBT key (node key₁ value left right) tree0 stack rb0 next exit | tri> ¬a ¬b c + = next right (right ∷ stack) ⟪ RBtreeRightDown left right (_∧_.proj1 rb0), s-right _ _ _ c (_∧_.proj2 rb0) ⟫ depth-2< + + + +findTest : {n m : Level} {A : Set n } {t : Set m } + → (key : ℕ) + → (tree0 : bt (Color ∧ A)) + → RBtreeInvariant tree0 + → (exit : (tree1 : bt (Color ∧ A)) + → (stack : List (bt (Color ∧ A))) + → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack + → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t +findTest {n} {m} {A} {t} k tr0 rb0 exit = TerminatingLoopS (bt (Color ∧ A) ∧ List (bt (Color ∧ A))) + {λ p → RBtreeInvariant (proj1 p) ∧ stackInvariant k (proj1 p) tr0 (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tr0 , tr0 ∷ [] ⟫ ⟪ rb0 , s-nil ⟫ + $ λ p RBP loop → findRBT k (proj1 p) tr0 (proj2 p) RBP (λ t1 s1 P2 lt1 → loop ⟪ t1 , s1 ⟫ P2 lt1 ) + $ λ tr1 st P2 O → exit tr1 st P2 O + + +testRBTree0 : bt (Color ∧ ℕ) +testRBTree0 = node 8 ⟪ Black , 800 ⟫ (node 5 ⟪ Red , 500 ⟫ (node 2 ⟪ Black , 200 ⟫ leaf leaf) (node 6 ⟪ Black , 600 ⟫ leaf leaf)) (node 10 ⟪ Red , 1000 ⟫ (leaf) (node 15 ⟪ Black , 1500 ⟫ (node 14 ⟪ Red , 1400 ⟫ leaf leaf) leaf)) + +-- testRBI0 : RBtreeInvariant testRBTree0 +-- testRBI0 = rb-node-black (add< 2) (add< 1) refl (rb-node-red (add< 2) (add< 0) refl (rb-single 2 200) (rb-single 6 600)) (rb-right-red (add< 4) refl (rb-left-black (add< 0) refl (rb-single 14 1400) )) + +-- findRBTreeTest : result +-- findRBTreeTest = findTest 14 testRBTree0 testRBI0 +-- $ λ tr s P O → (record {tree = tr ; stack = s ; ti = (proj1 P) ; si = (proj2 P)}) + +-- create replaceRBTree with rotate + + +-- +-- Parent Grand Relation +-- should we require stack-invariant? +-- + +data ParentGrand {n : Level} {A : Set n} (key : ℕ) (self : bt A) : (parent uncle grand : bt A) → Set n where + s2-s1p2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } + → key < kp → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand key self parent n2 grand + s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } + → kp < key → parent ≡ node kp vp n1 self → grand ≡ node kg vg parent n2 → ParentGrand key self parent n2 grand + s2-s12p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } + → key < kp → parent ≡ node kp vp self n1 → grand ≡ node kg vg n2 parent → ParentGrand key self parent n2 grand + s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } + → kp < key → parent ≡ node kp vp n1 self → grand ≡ node kg vg n2 parent → ParentGrand key self parent n2 grand + +record PG {n : Level } (A : Set n) (key : ℕ) (self : bt A) (stack : List (bt A)) : Set n where + field + parent grand uncle : bt A + pg : ParentGrand key self parent uncle grand + rest : List (bt A) + stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest ) + +-- +-- RBI : Invariant on InsertCase2 +-- color repl ≡ Red ∧ black-depth repl ≡ suc (black-depth tree) +-- + +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))} → color tree ≡ color repl → black-depth repl ≡ black-depth tree + → ¬ ( tree ≡ leaf) + → RBI-state key value tree repl stack -- one stage up + rotate : (tree : bt (Color ∧ A)) → {repl : bt (Color ∧ A) } {stack : List (bt (Color ∧ A))} → color repl ≡ Red + → RBI-state key value tree repl stack -- two stages up + top-black : {tree repl : bt (Color ∧ A) } → {stack : List (bt (Color ∧ A))} → stack ≡ tree ∷ [] + → RBI-state key value tree repl stack + +record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A))) : Set n where + field + tree repl : bt (Color ∧ A) + origti : treeInvariant orig + origrb : RBtreeInvariant orig + treerb : RBtreeInvariant tree -- tree node te be replaced + replrb : RBtreeInvariant repl + si : stackInvariant key tree orig stack + state : RBI-state key value tree repl stack + +tr>-to-black : {n : Level} {A : Set n} {key : ℕ} {tree : bt (Color ∧ A)} → tr> key tree → tr> key (to-black tree) +tr>-to-black {n} {A} {key} {leaf} tr = tt +tr>-to-black {n} {A} {key} {node key₁ value tree tree₁} tr = tr + +tr<-to-black : {n : Level} {A : Set n} {key : ℕ} {tree : bt (Color ∧ A)} → tr< key tree → tr< key (to-black tree) +tr<-to-black {n} {A} {key} {leaf} tr = tt +tr<-to-black {n} {A} {key} {node key₁ value tree tree₁} tr = tr + +to-black-eq : {n : Level} {A : Set n} (tree : bt (Color ∧ A)) → color tree ≡ Red → suc (black-depth tree) ≡ black-depth (to-black tree) +to-black-eq {n} {A} (leaf) () +to-black-eq {n} {A} (node key₁ ⟪ Red , proj4 ⟫ tree tree₁) eq = refl +to-black-eq {n} {A} (node key₁ ⟪ Black , proj4 ⟫ tree tree₁) () + +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 + → 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₁) = + ⟪ ( begin + black-depth left ⊔ black-depth right ≡⟨ cong (λ k → black-depth left ⊔ k) (sym (RBtreeEQ rb2)) ⟩ + black-depth left ⊔ black-depth left ≡⟨ ⊔-idem _ ⟩ + black-depth left ∎ ) , ( + begin + black-depth left ⊔ black-depth right ≡⟨ cong (λ k → k ⊔ black-depth right ) (RBtreeEQ rb2) ⟩ + black-depth right ⊔ black-depth right ≡⟨ ⊔-idem _ ⟩ + black-depth right ∎ ) ⟫ where open ≡-Reasoning +red-children-eq {n} {A} {tree} {left} {right} {key} {value} {Black} eq () rb + +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 + → 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₁) = + ⟪ ( 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) ∎ ) ⟫ where open ≡-Reasoning +black-children-eq {n} {A} {tree} {left} {right} {key} {value} {Red} eq () rb + +black-depth-cong : {n : Level} (A : Set n) {tree tree₁ : bt (Color ∧ A)} + → tree ≡ tree₁ → black-depth tree ≡ black-depth tree₁ +black-depth-cong {n} A {leaf} {leaf} refl = refl +black-depth-cong {n} A {node key ⟪ Red , value ⟫ left right} {node .key ⟪ Red , .value ⟫ .left .right} refl + = cong₂ (λ j k → j ⊔ k ) (black-depth-cong A {left} {left} refl) (black-depth-cong A {right} {right} refl) +black-depth-cong {n} A {node key ⟪ Black , value ⟫ left right} {node .key ⟪ Black , .value ⟫ .left .right} refl + = cong₂ (λ j k → suc (j ⊔ k) ) (black-depth-cong A {left} {left} refl) (black-depth-cong A {right} {right} refl) + +black-depth-resp : {n : Level} (A : Set n) (tree tree₁ : bt (Color ∧ A)) → {c1 c2 : Color} { l1 l2 r1 r2 : bt (Color ∧ A)} {key1 key2 : ℕ} {value1 value2 : A} + → tree ≡ node key1 ⟪ c1 , value1 ⟫ l1 r1 → tree₁ ≡ node key2 ⟪ c2 , value2 ⟫ l2 r2 + → color tree ≡ color tree₁ + → black-depth l1 ≡ black-depth l2 → black-depth r1 ≡ black-depth r2 + → black-depth tree ≡ black-depth tree₁ +black-depth-resp A _ _ {Black} {Black} refl refl refl eql eqr = cong₂ (λ j k → suc (j ⊔ k) ) eql eqr +black-depth-resp A _ _ {Red} {Red} refl refl refl eql eqr = cong₂ (λ j k → j ⊔ k ) eql eqr + +red-children-eq1 : {n : Level} {A : Set n} {tree left right : bt (Color ∧ A)} → {key : ℕ} → {value : A} → {c : Color} + → tree ≡ node key ⟪ c , value ⟫ left right + → color tree ≡ Red + → RBtreeInvariant tree + → (black-depth tree ≡ black-depth left ) ∧ (black-depth tree ≡ black-depth right) +red-children-eq1 {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 _ ⟩ + black-depth left ∎ ) , ( + begin + black-depth left ⊔ black-depth right ≡⟨ cong (λ k → k ⊔ black-depth right ) (RBtreeEQ rb2) ⟩ + black-depth right ⊔ black-depth right ≡⟨ ⊔-idem _ ⟩ + black-depth right ∎ ) ⟫ where open ≡-Reasoning +red-children-eq1 {n} {A} {.(node key ⟪ Black , value ⟫ left right)} {left} {right} {key} {value} {Black} refl () rb + +black-children-eq1 : {n : Level} {A : Set n} {tree left right : bt (Color ∧ A)} → {key : ℕ} → {value : A} → {c : Color} + → tree ≡ node key ⟪ c , value ⟫ left right + → color tree ≡ Black + → RBtreeInvariant tree + → (black-depth tree ≡ suc (black-depth left) ) ∧ (black-depth tree ≡ suc (black-depth right)) +black-children-eq1 {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) ∎ ) ⟫ where open ≡-Reasoning +black-children-eq1 {n} {A} {.(node key ⟪ Red , value ⟫ left right)} {left} {right} {key} {value} {Red} refl () rb + + +rbi-from-red-black : {n : Level } {A : Set n} → (n1 rp-left : bt (Color ∧ A)) → (kp : ℕ) → (vp : Color ∧ A) + → RBtreeInvariant n1 → RBtreeInvariant rp-left + → black-depth n1 ≡ black-depth rp-left + → color n1 ≡ Black → color rp-left ≡ Black → ⟪ Red , proj2 vp ⟫ ≡ vp + → RBtreeInvariant (node kp vp n1 rp-left) +rbi-from-red-black leaf leaf kp vp rb1 rbp deq ceq1 ceq2 ceq3 + = subst (λ k → RBtreeInvariant (node kp k leaf leaf)) ceq3 (rb-red kp (proj2 vp) refl refl refl rb-leaf rb-leaf) +rbi-from-red-black leaf (node key ⟪ .Black , proj3 ⟫ trpl trpl₁) kp vp rb1 rbp deq ceq1 refl ceq3 + = subst (λ k → RBtreeInvariant (node kp k _ _)) ceq3 (rb-red kp (proj2 vp) refl refl deq rb1 rbp) +rbi-from-red-black (node key ⟪ .Black , proj3 ⟫ tn1 tn2) leaf kp vp rb1 rbp deq refl ceq2 ceq3 + = subst (λ k → RBtreeInvariant (node kp k _ _)) ceq3 (rb-red kp (proj2 vp) refl refl deq rb1 rbp) +rbi-from-red-black (node key ⟪ .Black , proj3 ⟫ tn1 tn2) (node key₁ ⟪ .Black , proj4 ⟫ trpl trpl₁) kp vp rb1 rbp deq refl refl ceq3 + = subst (λ k → RBtreeInvariant (node kp k _ _)) ceq3 (rb-red kp (proj2 vp) refl refl deq rb1 rbp ) + +⊔-succ : {m n : ℕ} → suc (m ⊔ n) ≡ suc m ⊔ suc n +⊔-succ {m} {n} = refl + + +-- +-- if we consider tree invariant, this may be much simpler and faster +-- +stackToPG : {n : Level} {A : Set n} → {key : ℕ } → (tree orig : bt A ) + → (stack : List (bt A)) → stackInvariant key tree orig stack + → ( stack ≡ orig ∷ [] ) ∨ ( stack ≡ tree ∷ orig ∷ [] ) ∨ PG A key tree stack +stackToPG {n} {A} {key} tree .tree .(tree ∷ []) s-nil = case1 refl +stackToPG {n} {A} {key} tree .(node _ _ _ tree) .(tree ∷ node _ _ _ tree ∷ []) (s-right _ _ _ x s-nil) = case2 (case1 refl) +stackToPG {n} {A} {key} tree .(node k2 v2 t5 (node k1 v1 t2 tree)) (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ [])) (s-right tree (node k2 v2 t5 (node k1 v1 t2 tree)) t2 {k1} {v1} x (s-right (node k1 v1 t2 tree) (node k2 v2 t5 (node k1 v1 t2 tree)) t5 {k2} {v2} x₁ s-nil)) = case2 (case2 + record { parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p x refl refl ; rest = _ ; stack=gp = refl } ) +stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ _)) (s-right tree orig t2 {k1} {v1} x (s-right (node k1 v1 t2 tree) orig t5 {k2} {v2} x₁ (s-right _ _ _ x₂ si))) = case2 (case2 + record { parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p x refl refl ; rest = _ ; stack=gp = refl } ) +stackToPG {n} {A} {key} tree orig (tree ∷ node _ _ _ tree ∷ .(node k2 v2 t5 (node k1 v1 t2 tree) ∷ _)) (s-right tree orig t2 {k1} {v1} x (s-right (node k1 v1 t2 tree) orig t5 {k2} {v2} x₁ (s-left _ _ _ x₂ si))) = case2 (case2 + record { parent = node k1 v1 t2 tree ; grand = _ ; pg = s2-1s2p x refl refl ; rest = _ ; stack=gp = refl } ) +stackToPG {n} {A} {key} tree .(node k2 v2 (node k1 v1 t1 tree) t2) .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ []) (s-right _ _ t1 {k1} {v1} x (s-left _ _ t2 {k2} {v2} x₁ s-nil)) = case2 (case2 + record { parent = node k1 v1 t1 tree ; grand = _ ; pg = s2-1sp2 x refl refl ; rest = _ ; stack=gp = refl } ) +stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ _) (s-right _ _ t1 {k1} {v1} x (s-left _ _ t2 {k2} {v2} x₁ (s-right _ _ _ x₂ si))) = case2 (case2 + record { parent = node k1 v1 t1 tree ; grand = _ ; pg = s2-1sp2 x refl refl ; rest = _ ; stack=gp = refl } ) +stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 t1 tree ∷ node k2 v2 (node k1 v1 t1 tree) t2 ∷ _) (s-right _ _ t1 {k1} {v1} x (s-left _ _ t2 {k2} {v2} x₁ (s-left _ _ _ x₂ si))) = case2 (case2 + record { parent = node k1 v1 t1 tree ; grand = _ ; pg = s2-1sp2 x refl refl ; rest = _ ; stack=gp = refl } ) +stackToPG {n} {A} {key} tree .(node _ _ tree _) .(tree ∷ node _ _ tree _ ∷ []) (s-left _ _ t1 {k1} {v1} x s-nil) = case2 (case1 refl) +stackToPG {n} {A} {key} tree .(node _ _ _ (node k1 v1 tree t1)) .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ []) (s-left _ _ t1 {k1} {v1} x (s-right _ _ _ x₁ s-nil)) = case2 (case2 + record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s12p x refl refl ; rest = _ ; stack=gp = refl } ) +stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ _) (s-left _ _ t1 {k1} {v1} x (s-right _ _ _ x₁ (s-right _ _ _ x₂ si))) = case2 (case2 + record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s12p x refl refl ; rest = _ ; stack=gp = refl } ) +stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ _ (node k1 v1 tree t1) ∷ _) (s-left _ _ t1 {k1} {v1} x (s-right _ _ _ x₁ (s-left _ _ _ x₂ si))) = case2 (case2 + record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s12p x refl refl ; rest = _ ; stack=gp = refl } ) +stackToPG {n} {A} {key} tree .(node _ _ (node k1 v1 tree t1) _) .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ []) (s-left _ _ t1 {k1} {v1} x (s-left _ _ _ x₁ s-nil)) = case2 (case2 + record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 x refl refl ; rest = _ ; stack=gp = refl } ) +stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left _ _ t1 {k1} {v1} x (s-left _ _ _ x₁ (s-right _ _ _ x₂ si))) = case2 (case2 + record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 x refl refl ; rest = _ ; stack=gp = refl } ) +stackToPG {n} {A} {key} tree orig .(tree ∷ node k1 v1 tree t1 ∷ node _ _ (node k1 v1 tree t1) _ ∷ _) (s-left _ _ t1 {k1} {v1} x (s-left _ _ _ x₁ (s-left _ _ _ x₂ si))) = case2 (case2 + record { parent = node k1 v1 tree t1 ; grand = _ ; pg = s2-s1p2 x refl refl ; rest = _ ; stack=gp = refl } ) + +stackCase1 : {n : Level} {A : Set n} → {key : ℕ } → {tree orig : bt A } + → {stack : List (bt A)} → stackInvariant key tree orig stack + → stack ≡ orig ∷ [] → tree ≡ orig +stackCase1 s-nil refl = refl + +pg-prop-1 : {n : Level} (A : Set n) → (key : ℕ) → (tree orig : bt A ) + → (stack : List (bt A)) → (pg : PG A key tree stack) + → (¬ PG.grand pg ≡ leaf ) ∧ (¬ PG.parent pg ≡ leaf) +pg-prop-1 {_} A _ tree orig stack pg with PG.pg pg +... | s2-s1p2 _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫ +... | s2-1sp2 _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫ +... | s2-s12p _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫ +... | s2-1s2p _ refl refl = ⟪ (λ () ) , ( λ () ) ⟫ + +popStackInvariant : {n : Level} {A : Set n} → (rest : List ( bt (Color ∧ A))) + → ( tree parent orig : bt (Color ∧ A)) → (key : ℕ) + → stackInvariant key tree orig ( tree ∷ parent ∷ rest ) + → stackInvariant key parent orig (parent ∷ rest ) +popStackInvariant rest tree parent orig key (s-right .tree .orig tree₁ x si) = sc00 where + sc00 : stackInvariant key parent orig (parent ∷ rest ) + sc00 with si-property1 si + ... | refl = si +popStackInvariant rest tree parent orig key (s-left .tree .orig tree₁ x si) = sc00 where + sc00 : stackInvariant key parent orig (parent ∷ rest ) + sc00 with si-property1 si + ... | refl = si + + +siToTreeinvariant : {n : Level} {A : Set n} → (rest : List ( bt (Color ∧ A))) + → ( tree orig : bt (Color ∧ A)) → (key : ℕ) + → treeInvariant orig + → stackInvariant key tree orig ( tree ∷ rest ) + → 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 +siToTreeinvariant .(node _ _ (node key₁ _ _ _) leaf ∷ []) .leaf .(node _ _ (node key₁ _ _ _) leaf) key (t-left key₁ _ x₁ x₂ x₃ ti) (s-right .leaf .(node _ _ (node key₁ _ _ _) leaf) .(node key₁ _ _ _) x s-nil) = t-leaf +siToTreeinvariant .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _) ∷ []) .(node key₂ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) key (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-right .(node key₂ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) .(node key₁ _ _ _) x s-nil) = ti₁ +siToTreeinvariant .(node _ _ tree₁ tree ∷ _) tree orig key ti (s-right .tree .orig tree₁ x si2@(s-right .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2 +... | t-single _ _ = t-leaf +... | t-right _ key₁ x₂ x₃ x₄ ti₁ = ti₁ +... | t-left key₁ _ x₂ x₃ x₄ ti₁ = t-leaf +... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ ti₁ ti₂ = ti₂ +siToTreeinvariant .(node _ _ tree₁ tree ∷ _) tree orig key ti (s-right .tree .orig tree₁ x si2@(s-left .(node _ _ tree₁ tree) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2 +... | t-single _ _ = t-leaf +... | t-right _ key₁ x₂ x₃ x₄ ti₁ = ti₁ +... | t-left key₁ _ x₂ x₃ x₄ ti₁ = t-leaf +... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ ti₁ ti₂ = ti₂ +siToTreeinvariant .(node _ _ leaf leaf ∷ []) .leaf .(node _ _ leaf leaf) key (t-single _ _) (s-left .leaf .(node _ _ leaf leaf) .leaf x s-nil) = t-leaf +siToTreeinvariant .(node _ _ leaf (node key₁ _ _ _) ∷ []) .leaf .(node _ _ leaf (node key₁ _ _ _)) key (t-right _ key₁ x₁ x₂ x₃ ti) (s-left .leaf .(node _ _ leaf (node key₁ _ _ _)) .(node key₁ _ _ _) x s-nil) = t-leaf +siToTreeinvariant .(node _ _ (node key₁ _ _ _) leaf ∷ []) .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) leaf) key (t-left key₁ _ x₁ x₂ x₃ ti) (s-left .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) leaf) .leaf x s-nil) = ti +siToTreeinvariant .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _) ∷ []) .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) key (t-node key₁ _ key₂ x₁ x₂ x₃ x₄ x₅ x₆ ti ti₁) (s-left .(node key₁ _ _ _) .(node _ _ (node key₁ _ _ _) (node key₂ _ _ _)) .(node key₂ _ _ _) x s-nil) = ti +siToTreeinvariant .(node _ _ tree tree₁ ∷ _) tree orig key ti (s-left .tree .orig tree₁ x si2@(s-right .(node _ _ tree tree₁) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2 +... | t-single _ _ = t-leaf +... | t-right _ key₁ x₂ x₃ x₄ t = t-leaf +... | t-left key₁ _ x₂ x₃ x₄ t = t +... | t-node key₁ _ key₂ x₂ x₃ x₄ x₅ x₆ x₇ t t₁ = t +siToTreeinvariant .(node _ _ tree tree₁ ∷ _) tree orig key ti (s-left .tree .orig tree₁ x si2@(s-left .(node _ _ tree tree₁) .orig tree₂ x₁ si)) with siToTreeinvariant _ _ _ _ ti si2 +... | t-single _ _ = t-leaf +... | t-right _ key₁ x₂ x₃ x₄ t = t-leaf +... | 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} + → (tree orig : bt (Color ∧ A) ) + → {key : ℕ } + → (rb : RBtreeInvariant orig) + → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) + → RBtreeInvariant tree +PGtoRBinvariant1 tree .tree rb .(tree ∷ []) s-nil = rb +PGtoRBinvariant1 tree orig rb (tree ∷ rest) (s-right .tree .orig tree₁ x si) with PGtoRBinvariant1 _ orig rb _ si +... | rb-red _ value x₁ x₂ x₃ t t₁ = t₁ +... | rb-black _ value x₁ t t₁ = t₁ +PGtoRBinvariant1 tree orig rb (tree ∷ rest) (s-left .tree .orig tree₁ x si) with PGtoRBinvariant1 _ orig rb _ si +... | rb-red _ value x₁ x₂ x₃ t t₁ = t +... | rb-black _ value x₁ t t₁ = t + +RBI-child-replaced : {n : Level} {A : Set n} (tr : bt (Color ∧ A)) (key : ℕ) → RBtreeInvariant tr → RBtreeInvariant (child-replaced key tr) +RBI-child-replaced {n} {A} leaf key rbi = rbi +RBI-child-replaced {n} {A} (node key₁ value tr tr₁) key rbi with <-cmp key key₁ +... | tri< a ¬b ¬c = RBtreeLeftDown _ _ rbi +... | tri≈ ¬a b ¬c = rbi +... | tri> ¬a ¬b c = RBtreeRightDown _ _ rbi + +-- +-- create RBT invariant after findRBT, continue to replaceRBT +-- +createRBT : {n m : Level} {A : Set n } {t : Set m } + → (key : ℕ) (value : A) + → (tree0 : bt (Color ∧ A)) + → RBtreeInvariant tree0 + → treeInvariant tree0 + → (tree1 : bt (Color ∧ A)) + → (stack : List (bt (Color ∧ A))) + → 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 +createRBT {n} {m} {A} {t} key value orig rbi ti tree (x ∷ []) si P exit = crbt00 orig P refl where + crbt00 : (tree1 : bt (Color ∧ A)) → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) → tree1 ≡ orig → t + crbt00 leaf P refl = exit (x ∷ []) record { + tree = leaf + ; repl = node key ⟪ Red , value ⟫ leaf leaf + ; origti = ti + ; origrb = rbi + ; treerb = rb-leaf + ; replrb = rb-red key value refl refl refl rb-leaf rb-leaf + ; si = subst (λ k → stackInvariant key k leaf _ ) crbt01 si + ; state = rotate leaf refl + } where + crbt01 : tree ≡ leaf + crbt01 with si-property-last _ _ _ _ si | si-property1 si + ... | refl | refl = refl + crbt00 (node key₁ value₁ left right ) (case1 eq) refl with si-property-last _ _ _ _ si | si-property1 si + ... | refl | refl = ⊥-elim (bt-ne (sym eq)) + crbt00 (node key₁ value₁ left right ) (case2 eq) refl with si-property-last _ _ _ _ si | si-property1 si + ... | refl | refl = exit (x ∷ []) record { + tree = node key₁ value₁ left right + ; repl = node key₁ ⟪ proj1 value₁ , value ⟫ left right + ; origti = ti + ; origrb = rbi + ; treerb = rbi + ; replrb = crbt03 value₁ rbi + ; si = si + ; state = rebuild refl (crbt01 value₁ ) (λ ()) + } where + crbt01 : (value₁ : Color ∧ A) → black-depth (node key₁ ⟪ proj1 value₁ , value ⟫ left right) ≡ black-depth (node key₁ value₁ left right) + crbt01 ⟪ Red , proj4 ⟫ = refl + crbt01 ⟪ Black , proj4 ⟫ = refl + crbt03 : (value₁ : Color ∧ A) → RBtreeInvariant (node key₁ value₁ left right) → RBtreeInvariant (node key₁ ⟪ proj1 value₁ , value ⟫ left right) + crbt03 ⟪ Red , proj4 ⟫ (rb-red .key₁ .proj4 x x₁ x₂ rbi rbi₁) = rb-red key₁ _ x x₁ x₂ rbi rbi₁ + crbt03 ⟪ Black , proj4 ⟫ (rb-black .key₁ .proj4 x rbi rbi₁) = rb-black key₁ _ x rbi rbi₁ + keq : ( just key₁ ≡ just key ) → key₁ ≡ key + keq refl = refl +createRBT {n} {m} {A} {t} key value orig rbi ti tree (x ∷ leaf ∷ stack) si P exit = ⊥-elim (si-property-parent-node _ _ _ si refl) +createRBT {n} {m} {A} {t} key value orig rbi ti tree sp@(x ∷ node kp vp pleft pright ∷ stack) si P exit = crbt00 tree P refl where + crbt00 : (tree1 : bt (Color ∧ A)) → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) → tree1 ≡ tree → t + crbt00 leaf P refl = exit sp record { + tree = leaf + ; repl = node key ⟪ Red , value ⟫ leaf leaf + ; origti = ti + ; origrb = rbi + ; treerb = rb-leaf + ; replrb = rb-red key value refl refl refl rb-leaf rb-leaf + ; si = si + ; state = rotate leaf refl + } + crbt00 (node key₁ value₁ left right ) (case1 eq) refl = ⊥-elim (bt-ne (sym eq)) + crbt00 (node key₁ value₁ left right ) (case2 eq) refl with si-property-last _ _ _ _ si | si-property1 si + ... | eq1 | eq2 = exit sp record { + tree = node key₁ value₁ left right + ; repl = node key₁ ⟪ proj1 value₁ , value ⟫ left right + ; origti = ti + ; origrb = rbi + ; treerb = treerb + ; replrb = crbt03 value₁ treerb + ; si = si + ; state = rebuild refl (crbt01 value₁ ) (λ ()) + } where + crbt01 : (value₁ : Color ∧ A) → black-depth (node key₁ ⟪ proj1 value₁ , value ⟫ left right) ≡ black-depth (node key₁ value₁ left right) + crbt01 ⟪ Red , proj4 ⟫ = refl + crbt01 ⟪ Black , proj4 ⟫ = refl + crbt03 : (value₁ : Color ∧ A) → RBtreeInvariant (node key₁ value₁ left right) → RBtreeInvariant (node key₁ ⟪ proj1 value₁ , value ⟫ left right) + crbt03 ⟪ Red , proj4 ⟫ (rb-red .key₁ .proj4 x x₁ x₂ rbi rbi₁) = rb-red key₁ _ x x₁ x₂ rbi rbi₁ + crbt03 ⟪ Black , proj4 ⟫ (rb-black .key₁ .proj4 x rbi rbi₁) = rb-black key₁ _ x rbi rbi₁ + keq : ( just key₁ ≡ just key ) → key₁ ≡ key + keq refl = refl + treerb : RBtreeInvariant (node key₁ value₁ left right) + treerb = PGtoRBinvariant1 _ orig rbi _ si + +-- +-- rotate and rebuild replaceTree and rb-invariant +-- +replaceRBP : {n m : Level} {A : Set n} {t : Set m} + → (key : ℕ) → (value : A) + → (orig : bt (Color ∧ A)) + → (stack : List (bt (Color ∧ A))) + → (r : RBI key value orig stack ) + → (next : (stack1 : List (bt (Color ∧ A))) + → (r : RBI key value orig stack1 ) + → length stack1 < length stack → t ) + → (exit : (stack1 : List (bt (Color ∧ A))) + → stack1 ≡ (orig ∷ []) + → RBI key value orig stack1 + → t ) → t +replaceRBP {n} {m} {A} {t} key value orig 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 + repl = RBI.repl r + insertCase4 : (tr0 : bt (Color ∧ A)) → tr0 ≡ orig + → (eq : stack ≡ RBI.tree r ∷ orig ∷ []) + → ( color repl ≡ Red ) ∨ (color (RBI.tree r) ≡ color repl) + → stackInvariant key (RBI.tree r) orig stack + → t + insertCase4 leaf eq1 eq 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 + insertCase4 tr0@(node key₁ value₁ left right) refl eq 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 = ? + 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 (orig ∷ []) refl record { + tree = orig + ; repl = node key₁ value₁ repl right + ; origti = RBI.origti r + ; origrb = RBI.origrb r + ; treerb = RBI.origrb r + ; replrb = rb08 cc + ; si = s-nil + ; state = top-black refl + } + rb07 (case1 repl-red) = exit (orig ∷ []) refl record { + tree = orig + ; repl = to-black (node key₁ value₁ repl right) + ; origti = RBI.origti r + ; origrb = RBI.origrb r + ; treerb = RBI.origrb r + ; replrb = rb-black _ _ rb06 (RBI.replrb r) (RBtreeRightDown _ _ (RBI.origrb r)) + ; si = s-nil + ; state = top-black refl + } + ... | tri≈ ¬a b ¬c = ⊥-elim ( si-property-pne _ _ stack eq si b ) -- can't happen + ... | 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 ) + rb06 : black-depth repl ≡ black-depth left + rb06 = ? + 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 (orig ∷ []) refl record { + tree = orig + ; repl = node key₁ value₁ left repl + ; origti = RBI.origti r + ; origrb = RBI.origrb r + ; treerb = RBI.origrb r + ; replrb = rb08 cc + ; si = s-nil + ; state = top-black refl + } + rb07 (case1 repl-red ) = exit (orig ∷ []) refl record { + tree = orig + ; repl = to-black (node key₁ value₁ left repl) + ; 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 + } + rebuildCase : (ceq : color (RBI.tree r) ≡ color repl) + → (bdepth-eq : black-depth repl ≡ black-depth (RBI.tree r)) + → (¬ RBI.tree r ≡ leaf) → t + rebuildCase ceq bdepth-eq ¬leaf with stackToPG (RBI.tree r) orig stack (RBI.si r) + ... | case1 x = exit stack x r where -- single node case + rb00 : stack ≡ orig ∷ [] → orig ≡ RBI.tree r + rb00 refl = si-property1 (RBI.si r) + ... | case2 (case1 x) = insertCase4 orig refl x (case2 ceq) (RBI.si r) -- one level stack, orig is parent of repl + ... | case2 (case2 pg) = rebuildCase1 pg where + rb00 : (pg : PG (Color ∧ A) key (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) key (RBI.tree r) stack) → RBtreeInvariant (PG.parent pg) + treerb pg = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (rb00 pg)) + rb08 : (pg : PG (Color ∧ A) key (RBI.tree r) stack) → treeInvariant (PG.parent pg) + rb08 pg = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (rb00 pg)) + rebuildCase1 : (PG (Color ∧ A) key (RBI.tree r) stack) → t + rebuildCase1 pg with PG.pg pg + ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = rebuildCase2 where + rebuildCase2 : t + rebuildCase2 = 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 → ¬ (k ≡ leaf)) (sym x) (λ ())) + } (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 : black-depth n1 ≡ black-depth repl + rb03 = ? + 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 (trans (sym ceq) cx) cx₁ (sym rb03) (RBI.replrb r) t₁ + ... | rb-black .kp value ex t t₁ = rb-black kp value (sym rb03) (RBI.replrb r) t₁ + rb05 : treeInvariant (node kp vp (RBI.tree r) n1 ) + rb05 = subst (λ k → treeInvariant k) x (rb08 pg) + rb04 : key < kp + rb04 = lt + 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 repl n1) ≡ black-depth (node kp vp (RBI.tree r) n1 ) + rb07 ⟪ Black , proj4 ⟫ = cong (λ k → suc (k ⊔ black-depth n1 )) bdepth-eq + rb07 ⟪ Red , proj4 ⟫ = cong (λ k → (k ⊔ black-depth n1 )) bdepth-eq + ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = rebuildCase2 where + rebuildCase2 : t + rebuildCase2 = 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 → ¬ (k ≡ leaf)) (sym x) (λ ())) + } (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 = ? + 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 = lt + 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-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = rebuildCase2 where + rebuildCase2 : t + rebuildCase2 = 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 → ¬ (k ≡ leaf)) (sym x) (λ ())) + } (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 : black-depth n1 ≡ black-depth repl + rb03 = ? + 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 (trans (sym ceq) cx) cx₁ (sym rb03) (RBI.replrb r) t₁ + ... | rb-black .kp value ex t t₁ = rb-black kp value (sym rb03) (RBI.replrb r) t₁ + rb05 : treeInvariant (node kp vp (RBI.tree r) n1) + rb05 = subst (λ k → treeInvariant k) x (rb08 pg) + rb04 : key < kp + rb04 = lt + 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 repl n1) ≡ black-depth (node kp vp (RBI.tree r) n1) + rb07 ⟪ Black , proj4 ⟫ = cong (λ k → suc (k ⊔ black-depth n1 )) bdepth-eq + rb07 ⟪ Red , proj4 ⟫ = cong (λ k → (k ⊔ black-depth n1 )) bdepth-eq + ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = rebuildCase2 where + rebuildCase2 : t + rebuildCase2 = 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 → ¬ (k ≡ leaf)) (sym x) (λ ())) + } (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 = ? + 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-> ¬leaf 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) key (RBI.tree r) stack) + → color repl ≡ Red → color (PG.uncle pg) ≡ Black → color (PG.parent pg) ≡ Red → t + insertCase5 leaf eq pg 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 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} lt x x₁ = insertCase52 where + insertCase52 : t + insertCase52 = next (PG.grand pg ∷ PG.rest pg) record { + tree = PG.grand pg + ; repl = rb01 + ; 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 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) + } rb15 where + 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 = lt + 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 + 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 + 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 = ? + 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 = ? + ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase52 where + insertCase52 : t + insertCase52 = next (PG.grand pg ∷ PG.rest pg) record { + tree = PG.grand pg + ; repl = rb01 + ; origti = RBI.origti r + ; origrb = RBI.origrb r + ; treerb = rb02 + ; replrb = rb10 + ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) + ; state = rebuild rb33 rb17 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) + } rb15 where + -- inner case, repl is decomposed + -- 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) + -- eq : node rkey vr rp-left rp-right ≡ RBI.repl r + rb01 : bt (Color ∧ A) + rb01 = to-black (node rkey vr (node kp vp n1 rp-left) (to-red (node kg vg rp-right (PG.uncle pg)))) + rb04 : kp < key + rb04 = 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)) + rb16 : color n1 ≡ Black + rb16 = proj1 (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 + rb33 : color (PG.grand pg) ≡ Black + rb33 = subst (λ k → color k ≡ Black ) (sym x₁) (sym (cong proj1 rb14)) + rb23 : vr ≡ ⟪ Red , proj2 vr ⟫ + rb23 with subst (λ k → color k ≡ Red ) (sym eq) repl-red + ... | refl = refl + rb20 : color rp-right ≡ Black + rb20 = proj2 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r) ) (cong proj1 rb23)) + rb24 : node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r)) (PG.uncle pg) ≡ PG.grand pg + rb24 = trans (trans (cong₂ (λ j k → node kg j (node kp k n1 (RBI.tree r)) (PG.uncle pg)) rb14 rb13 ) (cong (λ k → node kg vg k (PG.uncle pg)) (sym x))) (sym x₁) + rb25 : node rkey ⟪ Black , proj2 vr ⟫ (node kp ⟪ Red , proj2 vp ⟫ n1 rp-left) (node kg ⟪ Red , proj2 vg ⟫ rp-right (PG.uncle pg)) ≡ rb01 + rb25 = begin + node rkey ⟪ Black , proj2 vr ⟫ (node kp ⟪ Red , proj2 vp ⟫ n1 rp-left) (node kg ⟪ Red , proj2 vg ⟫ rp-right (PG.uncle pg)) + ≡⟨ cong (λ k → node _ _ (node kp k n1 rp-left) _ ) rb13 ⟩ + node rkey ⟪ Black , proj2 vr ⟫ (node kp vp n1 rp-left) (node kg ⟪ Red , proj2 vg ⟫ rp-right (PG.uncle pg)) ≡⟨ refl ⟩ + rb01 ∎ where open ≡-Reasoning + rb05 : RBtreeInvariant (PG.uncle pg) + rb05 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb02) + rb06 : RBtreeInvariant n1 + rb06 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x rb09) + rb26 : RBtreeInvariant rp-left + rb26 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r)) + rb28 : RBtreeInvariant rp-right + rb28 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r)) + rb31 : RBtreeInvariant (node rkey vr rp-left rp-right ) + rb31 = subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r) + rb18 : black-depth rp-right ≡ black-depth (PG.uncle pg) + rb18 = ? + rb27 : black-depth n1 ≡ black-depth rp-left + rb27 = ? + rb19 : black-depth (node kp vp n1 rp-left) ≡ black-depth rp-right ⊔ black-depth (PG.uncle pg) + rb19 = begin + black-depth (node kp vp n1 rp-left) ≡⟨ black-depth-resp A (node kp vp n1 rp-left) (node kp vp rp-left rp-left) refl refl refl rb27 refl ⟩ + black-depth (node kp vp rp-left rp-left) ≡⟨ black-depth-resp A (node kp vp rp-left rp-left) (node rkey vr rp-left rp-right) + refl refl (trans (sym (cong proj1 rb13)) (sym (cong proj1 rb23))) refl (RBtreeEQ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r))) ⟩ + black-depth (node rkey vr rp-left rp-right) ≡⟨ black-depth-cong A eq ⟩ + black-depth (RBI.repl r) ≡⟨ proj2 (red-children-eq1 (sym eq) repl-red (RBI.replrb r)) ⟩ + black-depth rp-right ≡⟨ sym ( ⊔-idem _ ) ⟩ + black-depth rp-right ⊔ black-depth rp-right ≡⟨ cong (λ k → black-depth rp-right ⊔ k) rb18 ⟩ + black-depth rp-right ⊔ black-depth (PG.uncle pg) ∎ + where open ≡-Reasoning + rb29 : color n1 ≡ Black + rb29 = proj1 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) x rb09) (sym (cong proj1 rb13)) ) + rb30 : color rp-left ≡ Black + rb30 = proj1 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r)) (cong proj1 rb23)) + rb32 : suc (black-depth (PG.uncle pg)) ≡ black-depth (PG.grand pg) + rb32 = sym (proj2 ( black-children-eq1 x₁ rb33 rb02 )) + rb10 : RBtreeInvariant (node rkey ⟪ Black , proj2 vr ⟫ (node kp vp n1 rp-left) (node kg ⟪ Red , proj2 vg ⟫ rp-right (PG.uncle pg))) + rb10 = rb-black _ _ rb19 (rbi-from-red-black _ _ kp vp rb06 rb26 rb27 rb29 rb30 rb13) (rb-red _ _ rb20 uncle-black rb18 rb28 rb05) + rb17 : suc (black-depth (node kp vp n1 rp-left) ⊔ (black-depth rp-right ⊔ black-depth (PG.uncle pg))) ≡ black-depth (PG.grand pg) + rb17 = begin + suc (black-depth (node kp vp n1 rp-left) ⊔ (black-depth rp-right ⊔ black-depth (PG.uncle pg))) ≡⟨ cong (λ k → suc (k ⊔ _)) rb19 ⟩ + suc ((black-depth rp-right ⊔ black-depth (PG.uncle pg)) ⊔ (black-depth rp-right ⊔ black-depth (PG.uncle pg))) ≡⟨ cong suc ( ⊔-idem _) ⟩ + suc (black-depth rp-right ⊔ black-depth (PG.uncle pg)) ≡⟨ cong (λ k → suc (k ⊔ _)) rb18 ⟩ + suc (black-depth (PG.uncle pg) ⊔ black-depth (PG.uncle pg)) ≡⟨ cong suc (⊔-idem _) ⟩ + suc (black-depth (PG.uncle pg)) ≡⟨ rb32 ⟩ + black-depth (PG.grand pg) ∎ + where open ≡-Reasoning + ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase52 where + insertCase52 : t + insertCase52 = next (PG.grand pg ∷ PG.rest pg) record { + tree = PG.grand pg + ; repl = rb01 + ; origti = RBI.origti r + ; origrb = RBI.origrb r + ; treerb = rb02 + ; replrb = rb10 + ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) + ; state = rebuild rb33 rb17 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) + } rb15 where + -- inner case, repl is decomposed + -- lt : key < kp + -- x : PG.parent pg ≡ node kp vp (RBI.tree r) n1 + -- x₁ : PG.grand pg ≡ node kg vg (PG.uncle pg) (PG.parent pg) + -- eq : node rkey vr rp-left rp-right ≡ RBI.repl r + rb01 : bt (Color ∧ A) + rb01 = to-black (node rkey vr (to-red (node kg vg (PG.uncle pg) rp-left )) (node kp vp rp-right n1)) + rb04 : key < kp + rb04 = 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)) + 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) (case2 pcolor) + ... | refl = refl + rb33 : color (PG.grand pg) ≡ Black + rb33 = subst (λ k → color k ≡ Black ) (sym x₁) (sym (cong proj1 rb14)) + rb23 : vr ≡ ⟪ Red , proj2 vr ⟫ + rb23 with subst (λ k → color k ≡ Red ) (sym eq) repl-red + ... | refl = refl + rb20 : color rp-right ≡ Black + rb20 = proj2 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r) ) (cong proj1 rb23)) + rb24 : node kg ⟪ Black , proj2 vg ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) ≡ PG.grand pg + rb24 = begin + node kg ⟪ Black , proj2 vg ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) + ≡⟨ cong₂ (λ j k → node kg j (PG.uncle pg) (node kp k (RBI.tree r) n1) ) rb14 rb13 ⟩ + node kg vg (PG.uncle pg) (node kp vp (RBI.tree r) n1) ≡⟨ cong (λ k → node kg vg (PG.uncle pg) k ) (sym x) ⟩ + node kg vg (PG.uncle pg) (PG.parent pg) ≡⟨ sym x₁ ⟩ + PG.grand pg ∎ where open ≡-Reasoning + rb25 : node rkey ⟪ Black , proj2 vr ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) rp-left) (node kp ⟪ Red , proj2 vp ⟫ rp-right n1) ≡ rb01 + rb25 = begin + node rkey ⟪ Black , proj2 vr ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) rp-left) (node kp ⟪ Red , proj2 vp ⟫ rp-right n1) + ≡⟨ cong (λ k → node rkey ⟪ Black , proj2 vr ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) rp-left) (node kp k rp-right n1)) rb13 ⟩ + node rkey ⟪ Black , proj2 vr ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) rp-left) (node kp vp rp-right n1) ≡⟨ refl ⟩ + rb01 ∎ where open ≡-Reasoning + rb05 : RBtreeInvariant (PG.uncle pg) + rb05 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb02) + rb06 : RBtreeInvariant n1 + rb06 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x rb09) + rb26 : RBtreeInvariant rp-left + rb26 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r)) + rb28 : RBtreeInvariant rp-right + rb28 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r)) + rb31 : RBtreeInvariant (node rkey vr rp-left rp-right ) + rb31 = subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r) + rb18 : black-depth (PG.uncle pg) ≡ black-depth rp-left + rb18 = ? + rb27 : black-depth rp-right ≡ black-depth n1 + rb27 = ? + rb19 : black-depth (PG.uncle pg) ⊔ black-depth rp-left ≡ black-depth (node kp vp rp-right n1) + rb19 = sym ( begin + black-depth (node kp vp rp-right n1) ≡⟨ black-depth-resp A (node kp vp rp-right n1) (node kp vp rp-right rp-right) refl refl refl refl (sym rb27) ⟩ + black-depth (node kp vp rp-right rp-right) ≡⟨ black-depth-resp A (node kp vp rp-right rp-right) (node rkey vr rp-left rp-right) + refl refl (trans (sym (cong proj1 rb13)) (sym (cong proj1 rb23))) (sym (RBtreeEQ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r)))) refl ⟩ + black-depth (node rkey vr rp-left rp-right) ≡⟨ black-depth-cong A eq ⟩ + black-depth (RBI.repl r) ≡⟨ proj1 (red-children-eq1 (sym eq) repl-red (RBI.replrb r)) ⟩ + black-depth rp-left ≡⟨ sym ( ⊔-idem _ ) ⟩ + black-depth rp-left ⊔ black-depth rp-left ≡⟨ cong (λ k → k ⊔ black-depth rp-left ) (sym rb18) ⟩ + black-depth (PG.uncle pg) ⊔ black-depth rp-left ∎ ) + where open ≡-Reasoning + rb29 : color n1 ≡ Black + rb29 = proj2 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) x rb09) (sym (cong proj1 rb13)) ) + rb30 : color rp-left ≡ Black + rb30 = proj1 (RBtreeChildrenColorBlack _ _ (subst (λ k → RBtreeInvariant k) (sym eq) (RBI.replrb r)) (cong proj1 rb23)) + rb32 : suc (black-depth (PG.uncle pg)) ≡ black-depth (PG.grand pg) + rb32 = sym (proj1 ( black-children-eq1 x₁ rb33 rb02 )) + rb10 : RBtreeInvariant (node rkey ⟪ Black , proj2 vr ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) rp-left ) (node kp vp rp-right n1) ) + rb10 = rb-black _ _ rb19 (rb-red _ _ uncle-black rb30 rb18 rb05 rb26 ) (rbi-from-red-black _ _ _ _ rb28 rb06 rb27 rb20 rb16 rb13 ) + rb17 : suc (black-depth (PG.uncle pg) ⊔ black-depth rp-left ⊔ black-depth (node kp vp rp-right n1)) ≡ black-depth (PG.grand pg) + rb17 = begin + suc (black-depth (PG.uncle pg) ⊔ black-depth rp-left ⊔ black-depth (node kp vp rp-right n1)) ≡⟨ cong (λ k → suc (_ ⊔ k)) (sym rb19) ⟩ + suc (black-depth (PG.uncle pg) ⊔ black-depth rp-left ⊔ (black-depth (PG.uncle pg) ⊔ black-depth rp-left)) ≡⟨ cong suc ( ⊔-idem _) ⟩ + suc (black-depth (PG.uncle pg) ⊔ black-depth rp-left ) ≡⟨ cong (λ k → suc (_ ⊔ k)) (sym rb18) ⟩ + suc (black-depth (PG.uncle pg) ⊔ black-depth (PG.uncle pg)) ≡⟨ cong suc (⊔-idem _) ⟩ + suc (black-depth (PG.uncle pg)) ≡⟨ rb32 ⟩ + black-depth (PG.grand pg) ∎ + where open ≡-Reasoning + ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = insertCase52 where + insertCase52 : t + insertCase52 = next (PG.grand pg ∷ PG.rest pg) record { + tree = PG.grand pg + ; repl = rb01 + ; origti = RBI.origti r + ; origrb = RBI.origrb r + ; treerb = rb02 + ; replrb = subst (λ k → RBtreeInvariant k) rb10 (rb-black _ _ rb18 (rb-red _ _ uncle-black rb16 rb19 rb05 rb06) (RBI.replrb r) ) + ; si = popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00) + ; state = rebuild rb33 rb17 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) + } rb15 where + -- outer case, repl is not decomposed + -- 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) + rb01 : bt (Color ∧ A) + rb01 = to-black (node kp vp (to-red (node kg vg (PG.uncle pg) n1) )(node rkey vr rp-left rp-right)) + rb04 : kp < key + rb04 = lt + rb16 : color n1 ≡ Black + rb16 = proj1 (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) (case2 pcolor) + ... | refl = refl + rb33 : color (PG.grand pg) ≡ Black + rb33 = subst (λ k → color k ≡ Black ) (sym x₁) (sym (cong proj1 rb14)) + rb10 : node kp ⟪ Black , proj2 vp ⟫ (node kg ⟪ Red , proj2 vg ⟫ (PG.uncle pg) n1 ) repl ≡ rb01 + rb10 = cong (λ k → node _ _ _ k ) (sym eq) + rb12 : node kg ⟪ Black , proj2 vg ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r)) ≡ PG.grand pg + rb12 = begin + node kg ⟪ Black , proj2 vg ⟫ (PG.uncle pg) (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r)) + ≡⟨ cong₂ (λ j k → node kg j (PG.uncle pg) (node kp k n1 (RBI.tree r) ) ) rb14 rb13 ⟩ + node kg vg (PG.uncle pg) _ ≡⟨ cong (λ k → node _ _ _ k) (sym x) ⟩ + node kg vg (PG.uncle pg) (PG.parent pg) ≡⟨ sym x₁ ⟩ + PG.grand pg ∎ where open ≡-Reasoning + rb05 : RBtreeInvariant (PG.uncle pg) + rb05 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb02) + rb06 : RBtreeInvariant n1 + rb06 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x rb09) + rb19 : black-depth (PG.uncle pg) ≡ black-depth n1 + rb19 = sym (trans (sym ( proj1 (red-children-eq x (sym (cong proj1 rb13)) rb09) )) (sym (RBtreeEQ (subst (λ k → RBtreeInvariant k) x₁ rb02)))) + rb18 : black-depth (PG.uncle pg) ⊔ black-depth n1 ≡ black-depth repl + rb18 = ? + rb17 : suc (black-depth (PG.uncle pg) ⊔ black-depth n1 ⊔ black-depth (node rkey vr rp-left rp-right)) ≡ black-depth (PG.grand pg) + rb17 = ? + replaceRBP1 : t + replaceRBP1 with RBI.state r + ... | rebuild ceq bdepth-eq ¬leaf = rebuildCase ceq bdepth-eq ¬leaf + ... | top-black eq = exit 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 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 (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) key (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) key (RBI.tree r) stack) → RBtreeInvariant (PG.parent pg) + treerb pg = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (rb00 pg)) + rb08 : (pg : PG (Color ∧ A) key (RBI.tree r) stack) → treeInvariant (PG.parent pg) + rb08 pg = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ (rb00 pg)) + insertCase1 : t + insertCase1 with PG.pg pg + ... | s2-s1p2 {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₂ (λ 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 + rb07 : black-depth repl ≡ black-depth n1 + rb07 = ? + rb05 : proj1 vp ≡ Black → black-depth rb01 ≡ black-depth (PG.parent pg) + rb05 refl = ? + 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} 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₂ (λ 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 + rb07 : black-depth repl ≡ black-depth n1 + rb07 = ? + rb05 : proj1 vp ≡ Black → black-depth rb01 ≡ black-depth (PG.parent pg) + rb05 refl = ? + 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₂ (λ 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 + rb07 : black-depth repl ≡ black-depth n1 + rb07 = ? + rb05 : proj1 vp ≡ Black → black-depth rb01 ≡ black-depth (PG.parent pg) + rb05 refl = ? + 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₂ (λ 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 + rb07 : black-depth repl ≡ black-depth n1 + rb07 = ? + rb05 : proj1 vp ≡ Black → black-depth rb01 ≡ black-depth (PG.parent pg) + rb05 refl = ? + 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 repl-red (cong color uneq) pcolor + ... | node key₁ ⟪ Black , value₁ ⟫ t₁ t₂ = insertCase5 repl refl pg 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} 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 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 + } 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 = lt + 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 = ? + rb12 : suc (black-depth repl ⊔ black-depth n1) ≡ black-depth (to-black (PG.uncle pg)) + rb12 = ? + 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 + } 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 = ? + rb12 : suc (black-depth n1 ⊔ black-depth repl) ≡ black-depth (to-black (PG.uncle pg)) + rb12 = ? + 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 + } 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 = ? + rb12 : black-depth (to-black (PG.uncle pg)) ≡ suc (black-depth repl ⊔ black-depth n1) + rb12 = ? + 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))) (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 ( 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 + 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-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 + } 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 = ? + rb12 : black-depth (to-black (PG.uncle pg)) ≡ suc (black-depth n1 ⊔ black-depth repl) + rb12 = ? + 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 + + +insertRBTreeP : {n m : Level} {A : Set n} {t : Set m} → (tree : bt (Color ∧ A)) → (key : ℕ) → (value : A) + → treeInvariant tree → RBtreeInvariant tree + → (exit : (stack : List (bt (Color ∧ A))) → stack ≡ (tree ∷ []) → RBI key value tree stack → t ) → t +insertRBTreeP {n} {m} {A} {t} orig key value ti rbi exit = TerminatingLoopS (bt (Color ∧ A) ∧ List (bt (Color ∧ A))) + {λ p → RBtreeInvariant (proj1 p) ∧ stackInvariant key (proj1 p) orig (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ orig , orig ∷ [] ⟫ ⟪ rbi , s-nil ⟫ + $ λ p RBP findLoop → findRBT key (proj1 p) orig (proj2 p) RBP (λ t1 s1 P2 lt1 → findLoop ⟪ t1 , s1 ⟫ P2 lt1 ) + $ λ tr1 st P2 O → createRBT key value orig rbi ti tr1 st (proj2 P2) O + $ λ st rbi → TerminatingLoopS (List (bt (Color ∧ A))) {λ stack → RBI key value orig stack } + (λ stack → length stack ) st rbi + $ λ stack rbi replaceLoop → replaceRBP key value orig stack rbi (λ stack1 rbi1 lt → replaceLoop stack1 rbi1 lt ) + $ λ stack eq r → exit stack eq r +