Mercurial > hg > Gears > GearsAgda
changeset 939:3fee93d41dc1
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 14 Jun 2024 22:59:29 +0900 |
| parents | cf9de6f45d50 |
| children | b2537fa14a75 |
| files | hoareBinaryTree2.agda |
| diffstat | 1 files changed, 1850 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/hoareBinaryTree2.agda Fri Jun 14 22:59:29 2024 +0900 @@ -0,0 +1,1850 @@ +module hoareBinaryTree2 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) + +data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt A ) → Set n where + r-leaf : replacedTree key value leaf (node key value leaf leaf) + r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁) + r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A} + → k < key → replacedTree key value t2 t → replacedTree key value (node k v1 t1 t2) (node k v1 t1 t) + r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A} + → key < k → replacedTree key value t1 t → replacedTree key value (node k v1 t1 t2) (node k v1 t t2) + +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 +... | () + + +rt-property1 : {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf ) +rt-property1 {n} {A} key value .leaf .(node key value leaf leaf) r-leaf () +rt-property1 {n} {A} key value .(node key _ _ _) .(node key value _ _) r-node () +rt-property1 {n} {A} key value .(node _ _ _ _) _ (r-right x rt) = λ () +rt-property1 {n} {A} key value .(node _ _ _ _) _ (r-left x rt) = λ () + +rt-property-leaf : {n : Level} {A : Set n} {key : ℕ} {value : A} {repl : bt A} → replacedTree key value leaf repl → repl ≡ node key value leaf leaf +rt-property-leaf r-leaf = refl + +rt-property-¬leaf : {n : Level} {A : Set n} {key : ℕ} {value : A} {tree : bt A} → ¬ replacedTree key value tree leaf +rt-property-¬leaf () + +rt-property-key : {n : Level} {A : Set n} {key key₂ key₃ : ℕ} {value value₂ value₃ : A} {left left₁ right₂ right₃ : bt A} + → replacedTree key value (node key₂ value₂ left right₂) (node key₃ value₃ left₁ right₃) → key₂ ≡ key₃ +rt-property-key r-node = refl +rt-property-key (r-right x ri) = refl +rt-property-key (r-left x ri) = refl + + +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 + 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 = ? + +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) + → replacedTree key value tree repl → key₁ < key → tr> key₁ tree → tr> key₁ repl +ri-tr> .leaf .(node key value leaf leaf) key key₁ value r-leaf a tgt = ⟪ a , ⟪ tt , tt ⟫ ⟫ +ri-tr> .(node key _ _ _) .(node key value _ _) key key₁ value r-node a tgt = ⟪ a , ⟪ proj1 (proj2 tgt) , proj2 (proj2 tgt) ⟫ ⟫ +ri-tr> .(node _ _ _ _) .(node _ _ _ _) key key₁ value (r-right x ri) a tgt = ⟪ proj1 tgt , ⟪ proj1 (proj2 tgt) , ri-tr> _ _ _ _ _ ri a (proj2 (proj2 tgt)) ⟫ ⟫ +ri-tr> .(node _ _ _ _) .(node _ _ _ _) key key₁ value (r-left x ri) a tgt = ⟪ proj1 tgt , ⟪ ri-tr> _ _ _ _ _ ri a (proj1 (proj2 tgt)) , proj2 (proj2 tgt) ⟫ ⟫ + +ri-tr< : {n : Level} {A : Set n} → (tree repl : bt A) → (key key₁ : ℕ) → (value : A) + → replacedTree key value tree repl → key < key₁ → tr< key₁ tree → tr< key₁ repl +ri-tr< .leaf .(node key value leaf leaf) key key₁ value r-leaf a tgt = ⟪ a , ⟪ tt , tt ⟫ ⟫ +ri-tr< .(node key _ _ _) .(node key value _ _) key key₁ value r-node a tgt = ⟪ a , ⟪ proj1 (proj2 tgt) , proj2 (proj2 tgt) ⟫ ⟫ +ri-tr< .(node _ _ _ _) .(node _ _ _ _) key key₁ value (r-right x ri) a tgt = ⟪ proj1 tgt , ⟪ proj1 (proj2 tgt) , ri-tr< _ _ _ _ _ ri a (proj2 (proj2 tgt)) ⟫ ⟫ +ri-tr< .(node _ _ _ _) .(node _ _ _ _) key key₁ value (r-left x ri) a tgt = ⟪ proj1 tgt , ⟪ ri-tr< _ _ _ _ _ ri a (proj1 (proj2 tgt)) , proj2 (proj2 tgt) ⟫ ⟫ + +<-tr> : {n : Level} {A : Set n} → {tree : bt A} → {key₁ key₂ : ℕ} → tr> key₁ tree → key₂ < key₁ → tr> key₂ tree +<-tr> {n} {A} {leaf} {key₁} {key₂} tr lt = tt +<-tr> {n} {A} {node key value t t₁} {key₁} {key₂} tr lt = ⟪ <-trans lt (proj1 tr) , ⟪ <-tr> (proj1 (proj2 tr)) lt , <-tr> (proj2 (proj2 tr)) lt ⟫ ⟫ + +>-tr< : {n : Level} {A : Set n} → {tree : bt A} → {key₁ key₂ : ℕ} → tr< key₁ tree → key₁ < key₂ → tr< key₂ tree +>-tr< {n} {A} {leaf} {key₁} {key₂} tr lt = tt +>-tr< {n} {A} {node key value t t₁} {key₁} {key₂} tr lt = ⟪ <-trans (proj1 tr) lt , ⟪ >-tr< (proj1 (proj2 tr)) lt , >-tr< (proj2 (proj2 tr)) lt ⟫ ⟫ + +RTtoTI0 : {n : Level} {A : Set n} → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant tree + → replacedTree key value tree repl → treeInvariant repl +RTtoTI0 .leaf .(node key value leaf leaf) key value ti r-leaf = t-single key value +RTtoTI0 .(node key _ leaf leaf) .(node key value leaf leaf) key value (t-single .key _) r-node = t-single key value +RTtoTI0 .(node key _ leaf (node _ _ _ _)) .(node key value leaf (node _ _ _ _)) key value (t-right _ _ x a b ti) r-node = t-right _ _ x a b ti +RTtoTI0 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left _ _ x a b ti) r-node = t-left _ _ x a b ti +RTtoTI0 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node _ _ _ x x₁ a b c d ti ti₁) r-node = t-node _ _ _ x x₁ a b c d ti ti₁ +-- r-right case +RTtoTI0 (node _ _ leaf leaf) (node _ _ leaf .(node key value leaf leaf)) key value (t-single _ _) (r-right x r-leaf) = t-right _ _ x _ _ (t-single key value) +RTtoTI0 (node _ _ leaf right@(node _ _ _ _)) (node key₁ value₁ leaf leaf) key value (t-right _ _ x₁ a b ti) (r-right x ri) = t-single key₁ value₁ +RTtoTI0 (node key₁ _ leaf right@(node key₂ _ left₁ right₁)) (node key₁ value₁ leaf right₃@(node key₃ _ left₂ right₂)) key value (t-right key₄ key₅ x₁ a b ti) (r-right x ri) = + t-right _ _ (subst (λ k → key₁ < k ) (rt-property-key ri) x₁) (rr00 ri a ) (rr02 ri b) (RTtoTI0 right right₃ key value ti ri) where + rr00 : replacedTree key value (node key₂ _ left₁ right₁) (node key₃ _ left₂ right₂) → tr> key₁ left₁ → tr> key₁ left₂ + rr00 r-node tb = tb + rr00 (r-right x ri) tb = tb + rr00 (r-left x₂ ri) tb = ri-tr> _ _ _ _ _ ri x tb + rr02 : replacedTree key value (node key₂ _ left₁ right₁) (node key₃ _ left₂ right₂) → tr> key₁ right₁ → tr> key₁ right₂ + rr02 r-node tb = tb + rr02 (r-right x₂ ri) tb = ri-tr> _ _ _ _ _ ri x tb + rr02 (r-left x ri) tb = tb +RTtoTI0 (node key₁ _ (node _ _ _ _) leaf) (node key₁ _ (node key₃ value left right) leaf) key value₁ (t-left _ _ x₁ a b ti) (r-right x ()) +RTtoTI0 (node key₁ _ (node key₃ _ _ _) leaf) (node key₁ _ (node key₃ value₃ _ _) (node key value leaf leaf)) key value (t-left _ _ x₁ a b ti) (r-right x r-leaf) = + t-node _ _ _ x₁ x a b tt tt ti (t-single key value) +RTtoTI0 (node key₁ _ (node _ _ left₀ right₀) (node key₂ _ left₁ right₁)) (node key₁ _ (node _ _ left₂ right₂) (node key₃ _ left₃ right₃)) key value (t-node _ _ _ x₁ x₂ a b c d ti ti₁) (r-right x ri) = + t-node _ _ _ x₁ (subst (λ k → key₁ < k ) (rt-property-key ri) x₂) a b (rr00 ri c) (rr02 ri d) ti (RTtoTI0 _ _ key value ti₁ ri) where + rr00 : replacedTree key value (node key₂ _ _ _) (node key₃ _ _ _) → tr> key₁ left₁ → tr> key₁ left₃ + rr00 r-node tb = tb + rr00 (r-right x₃ ri) tb = tb + rr00 (r-left x₃ ri) tb = ri-tr> _ _ _ _ _ ri x tb + rr02 : replacedTree key value (node key₂ _ _ _) (node key₃ _ _ _) → tr> key₁ right₁ → tr> key₁ right₃ + rr02 r-node tb = tb + rr02 (r-right x₃ ri) tb = ri-tr> _ _ _ _ _ ri x tb + rr02 (r-left x₃ ri) tb = tb +-- r-left case +RTtoTI0 .(node _ _ leaf leaf) .(node _ _ (node key value leaf leaf) leaf) key value (t-single _ _) (r-left x r-leaf) = t-left _ _ x tt tt (t-single _ _ ) +RTtoTI0 .(node _ _ leaf (node _ _ _ _)) (node key₁ value₁ (node key value leaf leaf) (node _ _ _ _)) key value (t-right _ _ x₁ a b ti) (r-left x r-leaf) = + t-node _ _ _ x x₁ tt tt a b (t-single key value) ti +RTtoTI0 (node key₃ _ (node key₂ _ left₁ right₁) leaf) (node key₃ _ (node key₁ value₁ left₂ right₂) leaf) key value (t-left _ _ x₁ a b ti) (r-left x ri) = + t-left _ _ (subst (λ k → k < key₃ ) (rt-property-key ri) x₁) (rr00 ri a) (rr02 ri b) (RTtoTI0 _ _ key value ti ri) where -- key₁ < key₃ + rr00 : replacedTree key value (node key₂ _ left₁ right₁) (node key₁ _ left₂ right₂) → tr< key₃ left₁ → tr< key₃ left₂ + rr00 r-node tb = tb + rr00 (r-right x₂ ri) tb = tb + rr00 (r-left x₂ ri) tb = ri-tr< _ _ _ _ _ ri x tb + rr02 : replacedTree key value (node key₂ _ left₁ right₁) (node key₁ _ left₂ right₂) → tr< key₃ right₁ → tr< key₃ right₂ + rr02 r-node tb = tb + rr02 (r-right x₃ ri) tb = ri-tr< _ _ _ _ _ ri x tb + rr02 (r-left x₃ ri) tb = tb +RTtoTI0 (node key₁ _ (node key₂ _ left₂ right₂) (node key₃ _ left₃ right₃)) (node key₁ _ (node key₄ _ left₄ right₄) (node key₅ _ left₅ right₅)) key value (t-node _ _ _ x₁ x₂ a b c d ti ti₁) (r-left x ri) = + t-node _ _ _ (subst (λ k → k < key₁ ) (rt-property-key ri) x₁) x₂ (rr00 ri a) (rr02 ri b) c d (RTtoTI0 _ _ key value ti ri) ti₁ where + rr00 : replacedTree key value (node key₂ _ left₂ right₂) (node key₄ _ left₄ right₄) → tr< key₁ left₂ → tr< key₁ left₄ + rr00 r-node tb = tb + rr00 (r-right x₃ ri) tb = tb + rr00 (r-left x₃ ri) tb = ri-tr< _ _ _ _ _ ri x tb + rr02 : replacedTree key value (node key₂ _ left₂ right₂) (node key₄ _ left₄ right₄) → tr< key₁ right₂ → tr< key₁ right₄ + rr02 r-node tb = tb + rr02 (r-right x₃ ri) tb = ri-tr< _ _ _ _ _ ri x tb + rr02 (r-left x₃ ri) tb = tb + +-- RTtoTI1 : {n : Level} {A : Set n} → (tree repl : bt A) → (key : ℕ) → (value : A) → treeInvariant repl +-- → replacedTree key value tree repl → treeInvariant tree +-- RTtoTI1 .leaf .(node key value leaf leaf) key value ti r-leaf = t-leaf +-- RTtoTI1 (node key value₁ leaf leaf) .(node key value leaf leaf) key value (t-single .key .value) r-node = t-single key value₁ +-- RTtoTI1 .(node key _ leaf (node _ _ _ _)) .(node key value leaf (node _ _ _ _)) key value (t-right _ _ x a b ti) r-node = t-right _ _ x a b ti +-- RTtoTI1 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left _ _ x a b ti) r-node = t-left _ _ x a b ti +-- RTtoTI1 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node _ _ _ x x₁ a b c d ti ti₁) r-node = t-node _ _ _ x x₁ a b c d ti ti₁ +-- -- r-right case +-- RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ leaf (node _ _ _ _)) key value (t-right _ _ x₁ a b ti) (r-right x r-leaf) = t-single key₁ value₁ +-- RTtoTI1 (node key₁ value₁ leaf (node key₂ value₂ t2 t3)) (node key₁ _ leaf (node key₃ _ _ _)) key value (t-right _ _ x₁ a b ti) (r-right x ri) = +-- t-right _ _ (subst (λ k → key₁ < k ) (sym (rt-property-key ri)) x₁) ? ? (RTtoTI1 _ _ key value ti ri) -- key₁ < key₂ +-- RTtoTI1 (node _ _ (node _ _ _ _) leaf) (node _ _ (node _ _ _ _) (node key value _ _)) key value (t-node _ _ _ x₁ x₂ a b c d ti ti₁) (r-right x r-leaf) = +-- t-left _ _ x₁ ? ? ti +-- RTtoTI1 (node key₄ _ (node key₃ _ _ _) (node key₁ value₁ n n₁)) (node key₄ _ (node key₃ _ _ _) (node key₂ _ _ _)) key value (t-node _ _ _ x₁ x₂ a b c d ti ti₁) (r-right x ri) = t-node _ _ _ x₁ (subst (λ k → key₄ < k ) (sym (rt-property-key ri)) x₂) a b ? ? ti (RTtoTI1 _ _ key value ti₁ ri) -- key₄ < key₁ +-- -- r-left case +-- RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ _ leaf) key value (t-left _ _ x₁ a b ti) (r-left x ri) = t-single key₁ value₁ +-- RTtoTI1 (node key₁ _ (node key₂ value₁ n n₁) leaf) (node key₁ _ (node key₃ _ _ _) leaf) key value (t-left _ _ x₁ a b ti) (r-left x ri) = +-- t-left _ _ (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) ? ? (RTtoTI1 _ _ key value ti ri) -- key₂ < key₁ +-- RTtoTI1 (node key₁ value₁ leaf _) (node key₁ _ _ _) key value (t-node _ _ _ x₁ x₂ a b c d ti ti₁) (r-left x r-leaf) = t-right _ _ x₂ c d ti₁ +-- 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₁ + +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 = + TerminatingLoopS (bt A ∧ List (bt A) ) {λ p → treeInvariant (proj1 p) ∧ stackInvariant key (proj1 p) tree (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tree , tree ∷ [] ⟫ ⟪ P0 , 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 = P0 ; 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 ⟪ RTtoTI0 _ _ _ _ (proj1 P) (proj2 P) , proj2 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 + +-- 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 + +data replacedRBTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt (Color ∧ A) ) → Set n where + -- no rotation case + rbr-leaf : replacedRBTree key value leaf (node key ⟪ Red , value ⟫ leaf leaf) + rbr-node : {value₁ : A} → {ca : Color } → {t t₁ : bt (Color ∧ A)} + → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ ca , value ⟫ t t₁) + rbr-right : {k : ℕ } {v1 : A} → {ca : Color} → {t t1 t2 : bt (Color ∧ A)} + → color t2 ≡ color t + → k < key → replacedRBTree key value t2 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ ca , v1 ⟫ t1 t) + rbr-left : {k : ℕ } {v1 : A} → {ca : Color} → {t t1 t2 : bt (Color ∧ A)} + → color t1 ≡ color t + → key < k → replacedRBTree key value t1 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ ca , v1 ⟫ t t2) -- k < key → key < k + -- in all other case, color of replaced node is changed from Black to Red + -- case1 parent is black + rbr-black-right : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} + → color t₂ ≡ Red → key₁ < key → replacedRBTree key value t₁ t₂ + → replacedRBTree key value (node key₁ ⟪ Black , value₁ ⟫ t t₁) (node key₁ ⟪ Black , value₁ ⟫ t t₂) + rbr-black-left : {t t₁ t₂ : bt (Color ∧ A)} {value₁ : A} {key₁ : ℕ} + → color t₂ ≡ Red → key < key₁ → replacedRBTree key value t₁ t₂ + → replacedRBTree key value (node key₁ ⟪ Black , value₁ ⟫ t₁ t) (node key₁ ⟪ Black , value₁ ⟫ t₂ t) + + -- case2 both parent and uncle are red (should we check uncle color?), flip color and up + rbr-flip-ll : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} + → color t₂ ≡ Red → color uncle ≡ Red → key < kp → replacedRBTree key value t₁ t₂ + → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₁ t) uncle) + (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t₂ t) (to-black uncle)) + rbr-flip-lr : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} + → color t₂ ≡ Red → color uncle ≡ Red → kp < key → key < kg → replacedRBTree key value t₁ t₂ + → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁) uncle) + (node kg ⟪ Red , vg ⟫ (node kp ⟪ Black , vp ⟫ t t₂) (to-black uncle)) + rbr-flip-rl : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} + → color t₂ ≡ Red → color uncle ≡ Red → kg < key → key < kp → replacedRBTree key value t₁ t₂ + → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t₁ t)) + (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t₂ t)) + rbr-flip-rr : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} + → color t₂ ≡ Red → color uncle ≡ Red → kp < key → replacedRBTree key value t₁ t₂ + → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t t₁)) + (node kg ⟪ Red , vg ⟫ (to-black uncle) (node kp ⟪ Black , vp ⟫ t t₂)) + + -- case6 the node is outer, rotate grand + rbr-rotate-ll : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} + → color t₂ ≡ Red → key < kp → replacedRBTree key value t₁ t₂ + → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t₁ t) uncle) + (node kp ⟪ Black , vp ⟫ t₂ (node kg ⟪ Red , vg ⟫ t uncle)) + rbr-rotate-rr : {t t₁ t₂ uncle : bt (Color ∧ A)} {kg kp : ℕ} {vg vp : A} + → color t₂ ≡ Red → kp < key → replacedRBTree key value t₁ t₂ + → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t t₁)) + (node kp ⟪ Black , vp ⟫ (node kg ⟪ Red , vg ⟫ uncle t) t₂ ) + -- case56 the node is inner, make it outer and rotate grand + rbr-rotate-lr : {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} + → color t₃ ≡ Black → kp < key → key < kg + → replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃) + → replacedRBTree key value (node kg ⟪ Black , vg ⟫ (node kp ⟪ Red , vp ⟫ t t₁) uncle) + (node kn ⟪ Black , vn ⟫ (node kp ⟪ Red , vp ⟫ t t₂) (node kg ⟪ Red , vg ⟫ t₃ uncle)) + rbr-rotate-rl : {t t₁ uncle : bt (Color ∧ A)} (t₂ t₃ : bt (Color ∧ A)) (kg kp kn : ℕ) {vg vp vn : A} + → color t₃ ≡ Black → kg < key → key < kp + → replacedRBTree key value t₁ (node kn ⟪ Red , vn ⟫ t₂ t₃) + → replacedRBTree key value (node kg ⟪ Black , vg ⟫ uncle (node kp ⟪ Red , vp ⟫ t₁ t)) + (node kn ⟪ Black , vn ⟫ (node kg ⟪ Red , vg ⟫ uncle t₂) (node kp ⟪ Red , vp ⟫ t₃ t)) + + +-- +-- 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) + → (rotated : replacedRBTree key value tree repl) + → 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 + → (rotated : replacedRBTree key value tree repl) + → RBI-state key value tree repl stack -- two stages up + top-black : {tree repl : bt (Color ∧ A) } → {stack : List (bt (Color ∧ A))} → stack ≡ tree ∷ [] + → (rotated : replacedRBTree key value tree repl ∨ replacedRBTree key value (to-black tree) repl) + → RBI-state key value tree repl stack + +record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig : 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) + +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 + +RB-repl-node : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A)) → {key : ℕ} → {value : A} + → replacedRBTree key value tree repl → ¬ ( repl ≡ leaf) +RB-repl-node {n} {A} .leaf .(node _ ⟪ Red , _ ⟫ leaf leaf) rbr-leaf () +RB-repl-node {n} {A} .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) rbr-node () +RB-repl-node {n} {A} .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) (rbr-right x x₁ rpl) () +RB-repl-node {n} {A} .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) (rbr-left x x₁ rpl) () +RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) (rbr-black-right x x₁ rpl) () +RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) (rbr-black-left x x₁ rpl) () +RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) (rbr-flip-ll x x₁ x₂ rpl) () +RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) (rbr-flip-lr x x₁ x₂ x₃ rpl) () +RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) (rbr-flip-rl x x₁ x₂ x₃ rpl) () +RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) (rbr-flip-rr x x₁ x₂ rpl) () +RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) (rbr-rotate-ll x x₁ rpl) () +RB-repl-node {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) (rbr-rotate-rr x x₁ rpl) () +RB-repl-node {n} {A} .(node kg ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ _) _) .(node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₂) (node kg ⟪ Red , _ ⟫ t₃ _)) (rbr-rotate-lr t₂ t₃ kg kp kn x x₁ x₂ rpl) () +RB-repl-node {n} {A} .(node kg ⟪ Black , _ ⟫ _ (node kp ⟪ Red , _ ⟫ _ _)) .(node kn ⟪ Black , _ ⟫ (node kg ⟪ Red , _ ⟫ _ t₂) (node kp ⟪ Red , _ ⟫ t₃ _)) (rbr-rotate-rl t₂ t₃ kg kp kn x x₁ x₂ rpl) () + +RB-repl→eq : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A)) → {key : ℕ} → {value : A} + → RBtreeInvariant tree + → replacedRBTree key value tree repl → black-depth tree ≡ black-depth repl +RB-repl→eq {n} {A} .leaf .(node _ ⟪ Red , _ ⟫ leaf leaf) rbt rbr-leaf = refl +RB-repl→eq {n} {A} (node _ ⟪ Red , _ ⟫ _ _) .(node _ ⟪ Red , _ ⟫ _ _) rbt rbr-node = refl +RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) rbt rbr-node = refl +RB-repl→eq {n} {A} (node _ ⟪ Red , _ ⟫ left _) .(node _ ⟪ Red , _ ⟫ left _) (rb-red _ _ x₂ x₃ x₄ rbt rbt₁) (rbr-right x x₁ t) = + cong (λ k → black-depth left ⊔ k ) (RB-repl→eq _ _ rbt₁ t) +RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ left _) .(node _ ⟪ Black , _ ⟫ left _) (rb-black _ _ x₂ rbt rbt₁) (rbr-right x x₁ t) = + cong (λ k → suc (black-depth left ⊔ k)) (RB-repl→eq _ _ rbt₁ t) +RB-repl→eq {n} {A} (node _ ⟪ Red , _ ⟫ _ right) .(node _ ⟪ Red , _ ⟫ _ right) (rb-red _ _ x₂ x₃ x₄ rbt rbt₁) (rbr-left x x₁ t) = cong (λ k → k ⊔ black-depth right) (RB-repl→eq _ _ rbt t) +RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ _ right) .(node _ ⟪ Black , _ ⟫ _ right) (rb-black _ _ x₂ rbt rbt₁) (rbr-left x x₁ t) = cong (λ k → suc (k ⊔ black-depth right)) (RB-repl→eq _ _ rbt t) +RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ t₁ _) .(node _ ⟪ Black , _ ⟫ t₁ _) (rb-black _ _ x₂ rbt rbt₁) (rbr-black-right x x₁ t) = cong (λ k → suc (black-depth t₁ ⊔ k)) (RB-repl→eq _ _ rbt₁ t) +RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ _ t₁) .(node _ ⟪ Black , _ ⟫ _ t₁) (rb-black _ _ x₂ rbt rbt₁) (rbr-black-left x x₁ t) = cong (λ k → suc (k ⊔ black-depth t₁)) (RB-repl→eq _ _ rbt t) +RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ t₁ t₂) t₃) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ t₄ t₂) (to-black t₃)) (rb-black _ _ x₃ (rb-red _ _ x₄ x₅ x₆ rbt rbt₂) rbt₁) (rbr-flip-ll {_} {_} {t₄} x x₁ x₂ t) = begin + suc (black-depth t₁ ⊔ black-depth t₂ ⊔ black-depth t₃) ≡⟨ cong (λ k → suc (k ⊔ black-depth t₂ ⊔ black-depth t₃)) (RB-repl→eq _ _ rbt t) ⟩ + suc (black-depth t₄ ⊔ black-depth t₂) ⊔ suc (black-depth t₃) ≡⟨ cong (λ k → suc (black-depth t₄ ⊔ black-depth t₂) ⊔ k ) ( to-black-eq t₃ x₁ ) ⟩ + suc (black-depth t₄ ⊔ black-depth t₂) ⊔ black-depth (to-black t₃) ∎ + where open ≡-Reasoning +RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ t₁ t₂) t₃) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ t₁ t₄) (to-black t₃)) (rb-black _ _ x₄ (rb-red _ _ x₅ x₆ x₇ rbt rbt₂) rbt₁) (rbr-flip-lr {_} {_} {t₄} x x₁ x₂ x₃ t) = begin + suc (black-depth t₁ ⊔ black-depth t₂) ⊔ suc (black-depth t₃) ≡⟨ cong (λ k → suc (black-depth t₁ ⊔ black-depth t₂) ⊔ k ) ( to-black-eq t₃ x₁ ) ⟩ + suc (black-depth t₁ ⊔ black-depth t₂) ⊔ black-depth (to-black t₃) ≡⟨ cong (λ k → suc (black-depth t₁ ⊔ k ) ⊔ black-depth (to-black t₃)) (RB-repl→eq _ _ rbt₂ t) ⟩ + suc (black-depth t₁ ⊔ black-depth t₄) ⊔ black-depth (to-black t₃) ∎ + where open ≡-Reasoning +RB-repl→eq {n} {A} (node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black t₄) (node _ ⟪ Black , _ ⟫ t₃ t₁)) (rb-black _ _ x₄ rbt (rb-red _ _ x₅ x₆ x₇ rbt₁ rbt₂)) (rbr-flip-rl {t₁} {t₂} {t₃} {t₄} x x₁ x₂ x₃ t) = begin + suc (black-depth t₄ ⊔ (black-depth t₂ ⊔ black-depth t₁)) ≡⟨ cong (λ k → suc (black-depth t₄ ⊔ ( k ⊔ black-depth t₁)) ) (RB-repl→eq _ _ rbt₁ t) ⟩ + suc (black-depth t₄ ⊔ (black-depth t₃ ⊔ black-depth t₁)) ≡⟨ cong (λ k → k ⊔ suc (black-depth t₃ ⊔ black-depth t₁)) ( to-black-eq t₄ x₁ ) ⟩ + black-depth (to-black t₄) ⊔ suc (black-depth t₃ ⊔ black-depth t₁) ∎ + where open ≡-Reasoning +RB-repl→eq {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) (rb-black _ _ x₃ rbt (rb-red _ _ x₄ x₅ x₆ rbt₁ rbt₂)) (rbr-flip-rr {t₁} {t₂} {t₃} {t₄} x x₁ x₂ t) = begin + suc (black-depth t₄ ⊔ (black-depth t₁ ⊔ black-depth t₂)) ≡⟨ cong (λ k → suc (black-depth t₄ ⊔ (black-depth t₁ ⊔ k ))) ( RB-repl→eq _ _ rbt₂ t) ⟩ + suc (black-depth t₄ ⊔ (black-depth t₁ ⊔ black-depth t₃)) ≡⟨ cong (λ k → k ⊔ suc (black-depth t₁ ⊔ black-depth t₃)) ( to-black-eq t₄ x₁ ) ⟩ + black-depth (to-black t₄) ⊔ suc (black-depth t₁ ⊔ black-depth t₃) ∎ + where open ≡-Reasoning +RB-repl→eq {n} {A} .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) (rb-black _ _ x₂ (rb-red _ _ x₃ x₄ x₅ rbt rbt₂) rbt₁) (rbr-rotate-ll {t₁} {t₂} {t₃} {t₄} x x₁ t) = begin + suc (black-depth t₂ ⊔ black-depth t₁ ⊔ black-depth t₄) ≡⟨ cong suc ( ⊔-assoc (black-depth t₂) (black-depth t₁) (black-depth t₄)) ⟩ + suc (black-depth t₂ ⊔ (black-depth t₁ ⊔ black-depth t₄)) ≡⟨ cong (λ k → suc (k ⊔ (black-depth t₁ ⊔ black-depth t₄)) ) (RB-repl→eq _ _ rbt t) ⟩ + suc (black-depth t₃ ⊔ (black-depth t₁ ⊔ black-depth t₄)) ∎ + where open ≡-Reasoning +RB-repl→eq {n} {A} .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) (rb-black _ _ x₂ rbt (rb-red _ _ x₃ x₄ x₅ rbt₁ rbt₂)) (rbr-rotate-rr {t₁} {t₂} {t₃} {t₄} x x₁ t) = begin + suc (black-depth t₄ ⊔ (black-depth t₁ ⊔ black-depth t₂)) ≡⟨ cong (λ k → suc (black-depth t₄ ⊔ (black-depth t₁ ⊔ k ))) ( RB-repl→eq _ _ rbt₂ t) ⟩ + suc (black-depth t₄ ⊔ (black-depth t₁ ⊔ black-depth t₃)) ≡⟨ cong suc (sym ( ⊔-assoc (black-depth t₄) (black-depth t₁) (black-depth t₃))) ⟩ + suc (black-depth t₄ ⊔ black-depth t₁ ⊔ black-depth t₃) ∎ + where open ≡-Reasoning +RB-repl→eq {n} {A} .(node kg ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ _) _) .(node kn ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ t₂) (node kg ⟪ Red , _ ⟫ t₃ _)) (rb-black .kg _ x₃ (rb-red .kp _ x₄ x₅ x₆ rbt rbt₂) rbt₁) (rbr-rotate-lr {t₀} {t₁} {uncle} t₂ t₃ kg kp kn x x₁ x₂ t) = begin + suc (black-depth t₀ ⊔ black-depth t₁ ⊔ black-depth uncle) ≡⟨ cong suc ( ⊔-assoc (black-depth t₀) (black-depth t₁) (black-depth uncle)) ⟩ + suc (black-depth t₀ ⊔ (black-depth t₁ ⊔ black-depth uncle)) ≡⟨ cong (λ k → suc (black-depth t₀ ⊔ (k ⊔ black-depth uncle))) (RB-repl→eq _ _ rbt₂ t) ⟩ + suc (black-depth t₀ ⊔ ((black-depth t₂ ⊔ black-depth t₃) ⊔ black-depth uncle)) ≡⟨ cong (λ k → suc (black-depth t₀ ⊔ k )) ( ⊔-assoc (black-depth t₂) (black-depth t₃) (black-depth uncle)) ⟩ + suc (black-depth t₀ ⊔ (black-depth t₂ ⊔ (black-depth t₃ ⊔ black-depth uncle))) ≡⟨ cong suc (sym ( ⊔-assoc (black-depth t₀) (black-depth t₂) (black-depth t₃ ⊔ black-depth uncle))) ⟩ + suc (black-depth t₀ ⊔ black-depth t₂ ⊔ (black-depth t₃ ⊔ black-depth uncle)) ∎ + where open ≡-Reasoning +RB-repl→eq {n} {A} .(node kg ⟪ Black , _ ⟫ _ (node kp ⟪ Red , _ ⟫ _ _)) .(node kn ⟪ Black , _ ⟫ (node kg ⟪ Red , _ ⟫ _ t₂) (node kp ⟪ Red , _ ⟫ t₃ _)) (rb-black .kg _ x₃ rbt (rb-red .kp _ x₄ x₅ x₆ rbt₁ rbt₂)) (rbr-rotate-rl {t₀} {t₁} {uncle} t₂ t₃ kg kp kn x x₁ x₂ t) = begin + suc (black-depth uncle ⊔ (black-depth t₁ ⊔ black-depth t₀)) ≡⟨ cong (λ k → suc (black-depth uncle ⊔ (k ⊔ black-depth t₀))) (RB-repl→eq _ _ rbt₁ t) ⟩ + suc (black-depth uncle ⊔ ((black-depth t₂ ⊔ black-depth t₃) ⊔ black-depth t₀)) ≡⟨ cong (λ k → suc (black-depth uncle ⊔ k)) ( ⊔-assoc (black-depth t₂) (black-depth t₃) (black-depth t₀)) ⟩ + suc (black-depth uncle ⊔ (black-depth t₂ ⊔ (black-depth t₃ ⊔ black-depth t₀))) ≡⟨ cong suc (sym ( ⊔-assoc (black-depth uncle) (black-depth t₂) (black-depth t₃ ⊔ black-depth t₀))) ⟩ + suc (black-depth uncle ⊔ black-depth t₂ ⊔ (black-depth t₃ ⊔ black-depth t₀)) ∎ + where open ≡-Reasoning + + +RB-repl→ti> : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A)) → (key key₁ : ℕ) → (value : A) + → replacedRBTree key value tree repl → key₁ < key → tr> key₁ tree → tr> key₁ repl +RB-repl→ti> .leaf .(node key ⟪ Red , value ⟫ leaf leaf) key key₁ value rbr-leaf lt tr = ⟪ lt , ⟪ tt , tt ⟫ ⟫ +RB-repl→ti> .(node key ⟪ _ , _ ⟫ _ _) .(node key ⟪ _ , value ⟫ _ _) key key₁ value (rbr-node ) lt tr = tr +RB-repl→ti> .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-right _ x rbt) lt tr + = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti> _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫ +RB-repl→ti> .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-left _ x rbt) lt tr + = ⟪ proj1 tr , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt (proj1 (proj2 tr)) , proj2 (proj2 tr) ⟫ ⟫ +RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-right x _ rbt) lt tr + = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti> _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫ +RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-left x _ rbt) lt tr + = ⟪ proj1 tr , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt (proj1 (proj2 tr)) , proj2 (proj2 tr) ⟫ ⟫ +RB-repl→ti> .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value (rbr-flip-ll x _ _ rbt) lt tr + = ⟪ proj1 tr , ⟪ ⟪ proj1 (proj1 (proj2 tr)) , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt (proj1 (proj2 (proj1 (proj2 tr)))) + , proj2 (proj2 (proj1 (proj2 tr))) ⟫ ⟫ , tr>-to-black (proj2 (proj2 tr)) ⟫ ⟫ +RB-repl→ti> .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value + (rbr-flip-lr x _ _ _ rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , RB-repl→ti> _ _ _ _ _ rbt lt tr7 ⟫ ⟫ , tr>-to-black tr5 ⟫ ⟫ +RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key key₁ value + (rbr-flip-rl x _ _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr3 , ⟪ tr>-to-black tr5 , ⟪ tr4 , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt tr6 , tr7 ⟫ ⟫ ⟫ ⟫ +RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key key₁ value + (rbr-flip-rr x _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr3 , ⟪ tr>-to-black tr5 , ⟪ tr4 , ⟪ tr6 , RB-repl→ti> _ _ _ _ _ rbt lt tr7 ⟫ ⟫ ⟫ ⟫ +RB-repl→ti> .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value + (rbr-rotate-ll x lt2 rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ tr4 , ⟪ RB-repl→ti> _ _ _ _ _ rbt lt tr6 , ⟪ tr3 , ⟪ tr7 , tr5 ⟫ ⟫ ⟫ ⟫ +RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) key key₁ value + (rbr-rotate-rr x lt2 rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr4 , ⟪ ⟪ tr3 , ⟪ tr5 , tr6 ⟫ ⟫ , RB-repl→ti> _ _ _ _ _ rbt lt tr7 ⟫ ⟫ +RB-repl→ti> (node kg ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ _) _) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value + (rbr-rotate-lr left right _ _ kn _ _ _ rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ rr00 , ⟪ ⟪ tr4 , ⟪ tr6 , proj1 (proj2 rr01) ⟫ ⟫ , ⟪ tr3 , ⟪ proj2 (proj2 rr01) , tr5 ⟫ ⟫ ⟫ ⟫ where + rr01 : (key₁ < kn) ∧ tr> key₁ left ∧ tr> key₁ right + rr01 = RB-repl→ti> _ _ _ _ _ rbt lt tr7 + rr00 : key₁ < kn + rr00 = proj1 rr01 +RB-repl→ti> .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value + (rbr-rotate-rl left right kg kp kn _ _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ rr00 , ⟪ ⟪ tr3 , ⟪ tr5 , proj1 (proj2 rr01) ⟫ ⟫ , ⟪ tr4 , ⟪ proj2 (proj2 rr01) , tr7 ⟫ ⟫ ⟫ ⟫ where + rr01 : (key₁ < kn) ∧ tr> key₁ left ∧ tr> key₁ right + rr01 = RB-repl→ti> _ _ _ _ _ rbt lt tr6 + rr00 : key₁ < kn + rr00 = proj1 rr01 + +RB-repl→ti< : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A)) → (key key₁ : ℕ) → (value : A) + → replacedRBTree key value tree repl → key < key₁ → tr< key₁ tree → tr< key₁ repl +RB-repl→ti< .leaf .(node key ⟪ Red , value ⟫ leaf leaf) key key₁ value rbr-leaf lt tr = ⟪ lt , ⟪ tt , tt ⟫ ⟫ +RB-repl→ti< .(node key ⟪ _ , _ ⟫ _ _) .(node key ⟪ _ , value ⟫ _ _) key key₁ value (rbr-node ) lt tr = tr +RB-repl→ti< .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-right _ x rbt) lt tr + = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti< _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫ +RB-repl→ti< .(node _ ⟪ _ , _ ⟫ _ _) .(node _ ⟪ _ , _ ⟫ _ _) key key₁ value (rbr-left _ x rbt) lt tr + = ⟪ proj1 tr , ⟪ RB-repl→ti< _ _ _ _ _ rbt lt (proj1 (proj2 tr)) , proj2 (proj2 tr) ⟫ ⟫ +RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-right x _ rbt) lt tr + = ⟪ proj1 tr , ⟪ proj1 (proj2 tr) , RB-repl→ti< _ _ _ _ _ rbt lt (proj2 (proj2 tr)) ⟫ ⟫ +RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ _) .(node _ ⟪ Black , _ ⟫ _ _) key key₁ value (rbr-black-left x _ rbt) lt tr + = ⟪ proj1 tr , ⟪ RB-repl→ti< _ _ _ _ _ rbt lt (proj1 (proj2 tr)) , proj2 (proj2 tr) ⟫ ⟫ +RB-repl→ti< .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value (rbr-flip-ll x _ _ rbt) lt tr + = ⟪ proj1 tr , ⟪ ⟪ proj1 (proj1 (proj2 tr)) , ⟪ RB-repl→ti< _ _ _ _ _ rbt lt (proj1 (proj2 (proj1 (proj2 tr)))) + , proj2 (proj2 (proj1 (proj2 tr))) ⟫ ⟫ , tr<-to-black (proj2 (proj2 tr)) ⟫ ⟫ +RB-repl→ti< .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Red , _ ⟫ (node _ ⟪ Black , _ ⟫ _ _) (to-black _)) key key₁ value + (rbr-flip-lr x _ _ _ rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , RB-repl→ti< _ _ _ _ _ rbt lt tr7 ⟫ ⟫ , tr<-to-black tr5 ⟫ ⟫ +RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key key₁ value + (rbr-flip-rl x _ _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr3 , ⟪ tr<-to-black tr5 , ⟪ tr4 , ⟪ RB-repl→ti< _ _ _ _ _ rbt lt tr6 , tr7 ⟫ ⟫ ⟫ ⟫ +RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Red , _ ⟫ (to-black _) (node _ ⟪ Black , _ ⟫ _ _)) key key₁ value + (rbr-flip-rr x _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr3 , ⟪ tr<-to-black tr5 , ⟪ tr4 , ⟪ tr6 , RB-repl→ti< _ _ _ _ _ rbt lt tr7 ⟫ ⟫ ⟫ ⟫ +RB-repl→ti< .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value + (rbr-rotate-ll x lt2 rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ tr4 , ⟪ RB-repl→ti< _ _ _ _ _ rbt lt tr6 , ⟪ tr3 , ⟪ tr7 , tr5 ⟫ ⟫ ⟫ ⟫ +RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) _) key key₁ value + (rbr-rotate-rr x lt2 rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ tr4 , ⟪ ⟪ tr3 , ⟪ tr5 , tr6 ⟫ ⟫ , RB-repl→ti< _ _ _ _ _ rbt lt tr7 ⟫ ⟫ +RB-repl→ti< (node kg ⟪ Black , _ ⟫ (node kp ⟪ Red , _ ⟫ _ _) _) (node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value + (rbr-rotate-lr left right _ _ kn _ _ _ rbt) lt ⟪ tr3 , ⟪ ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ , tr5 ⟫ ⟫ = ⟪ rr00 , ⟪ ⟪ tr4 , ⟪ tr6 , proj1 (proj2 rr01) ⟫ ⟫ , ⟪ tr3 , ⟪ proj2 (proj2 rr01) , tr5 ⟫ ⟫ ⟫ ⟫ where + rr01 : (kn < key₁ ) ∧ tr< key₁ left ∧ tr< key₁ right + rr01 = RB-repl→ti< _ _ _ _ _ rbt lt tr7 + rr00 : kn < key₁ + rr00 = proj1 rr01 +RB-repl→ti< .(node _ ⟪ Black , _ ⟫ _ (node _ ⟪ Red , _ ⟫ _ _)) .(node _ ⟪ Black , _ ⟫ (node _ ⟪ Red , _ ⟫ _ _) (node _ ⟪ Red , _ ⟫ _ _)) key key₁ value + (rbr-rotate-rl left right kg kp kn _ _ _ rbt) lt ⟪ tr3 , ⟪ tr5 , ⟪ tr4 , ⟪ tr6 , tr7 ⟫ ⟫ ⟫ ⟫ = ⟪ rr00 , ⟪ ⟪ tr3 , ⟪ tr5 , proj1 (proj2 rr01) ⟫ ⟫ , ⟪ tr4 , ⟪ proj2 (proj2 rr01) , tr7 ⟫ ⟫ ⟫ ⟫ where + rr01 : (kn < key₁ ) ∧ tr< key₁ left ∧ tr< key₁ right + rr01 = RB-repl→ti< _ _ _ _ _ rbt lt tr6 + rr00 : kn < key₁ + rr00 = proj1 rr01 + +RB-repl→ti : {n : Level} {A : Set n} → (tree repl : bt (Color ∧ A) ) → (key : ℕ ) → (value : A) → treeInvariant tree + → replacedRBTree key value tree repl → treeInvariant repl +RB-repl→ti = ? + + +-- +-- 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 rbr-leaf + } 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₁ ) (λ ()) crbt04 + } 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 + crbt04 : replacedRBTree key value (node key₁ value₁ left right) (node key₁ ⟪ proj1 value₁ , value ⟫ left right) + crbt04 = subst (λ k → replacedRBTree k value (node key₁ value₁ left right) (node key₁ ⟪ proj1 value₁ , value ⟫ left right)) (keq eq) rbr-node +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 rbr-leaf + } + 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₁ ) (λ ()) crbt04 + } 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 + crbt04 : replacedRBTree key value (node key₁ value₁ left right) (node key₁ ⟪ proj1 value₁ , value ⟫ left right) + crbt04 = subst (λ k → replacedRBTree k value (node key₁ value₁ left right) (node key₁ ⟪ proj1 value₁ , value ⟫ left right)) (keq eq) rbr-node + 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 ∷ []) + → (rot : replacedRBTree key value (RBI.tree r) repl) + → ( color repl ≡ Red ) ∨ (color (RBI.tree r) ≡ color repl) + → stackInvariant key (RBI.tree r) orig stack + → t + insertCase4 leaf eq1 eq rot col si = ⊥-elim (rb04 eq eq1 si) where -- can't happen + rb04 : {stack : List ( bt ( Color ∧ A))} → stack ≡ RBI.tree r ∷ orig ∷ [] → leaf ≡ orig → stackInvariant key (RBI.tree r) orig stack → ⊥ + rb04 refl refl (s-right tree leaf tree₁ x si) = si-property2 _ (s-right tree leaf tree₁ x si) refl + rb04 refl refl (s-left tree₁ leaf tree x si) = si-property2 _ (s-left tree₁ leaf tree x si) refl + insertCase4 tr0@(node key₁ value₁ left right) refl eq rot col si with <-cmp key key₁ + ... | tri< a ¬b ¬c = rb07 col where + rb04 : stackInvariant key (RBI.tree r) orig stack → stack ≡ RBI.tree r ∷ orig ∷ [] → tr0 ≡ orig → left ≡ RBI.tree r + rb04 (s-left tree₁ .(node key₁ value₁ left right) tree {key₂} x s-nil) refl refl = refl + rb04 (s-right tree .(node key₁ _ tree₁ tree) tree₁ x s-nil) refl refl with si-property1 si + ... | refl = ⊥-elim ( nat-<> x a ) + rb06 : black-depth repl ≡ black-depth right + rb06 = begin + black-depth repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ + black-depth (RBI.tree r) ≡⟨ cong black-depth (sym (rb04 si eq refl)) ⟩ + black-depth left ≡⟨ (RBtreeEQ (RBI.origrb r)) ⟩ + black-depth right ∎ + where open ≡-Reasoning + rb08 : (color (RBI.tree r) ≡ color repl) → RBtreeInvariant (node key₁ value₁ repl right) + rb08 ceq with proj1 value₁ in coeq + ... | Red = subst (λ k → RBtreeInvariant (node key₁ k repl right)) (cong (λ k → ⟪ k , _ ⟫) (sym coeq) ) + (rb-red _ (proj2 value₁) rb09 (proj2 (RBtreeChildrenColorBlack _ _ (RBI.origrb r) coeq)) rb06 (RBI.replrb r) + (RBtreeRightDown _ _ (RBI.origrb r))) where + rb09 : color repl ≡ Black + rb09 = trans (trans (sym ceq) (sym (cong color (rb04 si eq refl) ))) (proj1 (RBtreeChildrenColorBlack _ _ (RBI.origrb r) coeq)) + ... | Black = subst (λ k → RBtreeInvariant (node key₁ k repl right)) (cong (λ k → ⟪ k , _ ⟫) (sym coeq) ) + (rb-black _ (proj2 value₁) rb06 (RBI.replrb r) (RBtreeRightDown _ _ (RBI.origrb r))) + rb07 : ( color repl ≡ Red ) ∨ (color (RBI.tree r) ≡ color repl) → t + rb07 (case2 cc ) = exit (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 (case1 (rbr-left (trans (cong color (rb04 si eq refl)) cc) a (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) rot))) + } + rb07 (case1 repl-red) = exit (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 (case2 (rbr-black-left repl-red a (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) rot))) + } + ... | tri≈ ¬a b ¬c = ⊥-elim ( 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 = begin + black-depth repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ + black-depth (RBI.tree r) ≡⟨ cong black-depth (sym (rb04 si eq refl)) ⟩ + black-depth right ≡⟨ (sym (RBtreeEQ (RBI.origrb r))) ⟩ + black-depth left ∎ + where open ≡-Reasoning + rb08 : (color (RBI.tree r) ≡ color repl) → RBtreeInvariant (node key₁ value₁ left repl ) + rb08 ceq with proj1 value₁ in coeq + ... | Red = subst (λ k → RBtreeInvariant (node key₁ k left repl )) (cong (λ k → ⟪ k , _ ⟫) (sym coeq) ) + (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 (case1 (rbr-right (trans (cong color (rb04 si eq refl)) cc) c (subst (λ k → replacedRBTree key value k repl) (sym (rb04 si eq refl)) rot))) + } + rb07 (case1 repl-red ) = exit (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 (case2 (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) + → (rot : replacedRBTree key value (RBI.tree r) repl ) → t + rebuildCase ceq bdepth-eq ¬leaf rot 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 rot (case2 ceq) (RBI.si r) -- one level stack, orig is parent of repl + ... | case2 (case2 pg) = rebuildCase1 pg where + rb00 : (pg : PG (Color ∧ A) 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 (λ 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 + rb01 : bt (Color ∧ A) + rb01 = node kp vp repl n1 + rb03 : black-depth n1 ≡ black-depth repl + rb03 = trans (sym (RBtreeEQ (subst (λ k → RBtreeInvariant k) x (treerb pg)))) (RB-repl→eq _ _ (RBI.treerb r) rot) + rb02 : RBtreeInvariant rb01 + rb02 with subst (λ k → RBtreeInvariant k) x (treerb pg) + ... | rb-red .kp value cx cx₁ ex₂ t t₁ = rb-red kp value (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 (λ k → replacedRBTree key value k rb01) (sym x) (rbr-right ceq rb04 rot)) + } (subst₂ (λ j k → j < length k ) refl (sym (PG.stack=gp pg)) ≤-refl) where + rb01 : bt (Color ∧ A) + rb01 = node kp vp n1 repl + rb03 : black-depth n1 ≡ black-depth repl + rb03 = trans (RBtreeEQ (subst (λ k → RBtreeInvariant k) x (treerb pg))) ((RB-repl→eq _ _ (RBI.treerb r) rot)) + rb02 : RBtreeInvariant rb01 + rb02 with subst (λ k → RBtreeInvariant k) x (treerb pg) + ... | rb-red .kp value cx cx₁ ex₂ t t₁ = rb-red kp value cx (trans (sym ceq) cx₁) rb03 t (RBI.replrb r) + ... | rb-black .kp value ex t t₁ = rb-black kp value rb03 t (RBI.replrb r) + rb05 : treeInvariant (node kp vp n1 (RBI.tree r) ) + rb05 = subst (λ k → treeInvariant k) x (rb08 pg) + rb04 : kp < key + rb04 = 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 (λ 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 + rb01 : bt (Color ∧ A) + rb01 = node kp vp repl n1 + rb03 : black-depth n1 ≡ black-depth repl + rb03 = trans (sym (RBtreeEQ (subst (λ k → RBtreeInvariant k) x (treerb pg)))) ((RB-repl→eq _ _ (RBI.treerb r) rot)) + rb02 : RBtreeInvariant rb01 + rb02 with subst (λ k → RBtreeInvariant k) x (treerb pg) + ... | rb-red .kp value cx cx₁ ex₂ t t₁ = rb-red kp value (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 (λ k → replacedRBTree key value k rb01) (sym x) (rbr-right ceq rb04 rot)) + } (subst₂ (λ j k → j < length k ) refl (sym (PG.stack=gp pg)) ≤-refl) where + rb01 : bt (Color ∧ A) + rb01 = node kp vp n1 repl + rb03 : black-depth n1 ≡ black-depth repl + rb03 = trans (RBtreeEQ (subst (λ k → RBtreeInvariant k) x (treerb pg))) ((RB-repl→eq _ _ (RBI.treerb r) rot)) + rb02 : RBtreeInvariant rb01 + rb02 with subst (λ k → RBtreeInvariant k) x (treerb pg) + ... | rb-red .kp value cx cx₁ ex₂ t t₁ = rb-red kp value cx (trans (sym ceq) cx₁) rb03 t (RBI.replrb r) + ... | rb-black .kp value ex t t₁ = rb-black kp value rb03 t (RBI.replrb r) + rb05 : treeInvariant (node kp vp n1 (RBI.tree r)) + rb05 = subst (λ k → treeInvariant k) x (rb08 pg) + rb04 : kp < key + rb04 = si-property-> ¬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) + → (rot : replacedRBTree key value (RBI.tree r) repl) + → color repl ≡ Red → color (PG.uncle pg) ≡ Black → color (PG.parent pg) ≡ Red → t + insertCase5 leaf eq pg rot repl-red uncle-black pcolor = ⊥-elim ( rb00 repl repl-red (cong color (sym eq))) where + rb00 : (repl : bt (Color ∧ A)) → color repl ≡ Red → color repl ≡ Black → ⊥ + rb00 (node key ⟪ Black , proj4 ⟫ repl repl₁) () eq1 + rb00 (node key ⟪ Red , proj4 ⟫ repl repl₁) eq () + insertCase5 (node rkey vr rp-left rp-right) eq pg rot repl-red uncle-black pcolor = insertCase51 where + rb00 : stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) + rb00 = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r) + rb15 : suc (length (PG.rest pg)) < length stack + rb15 = begin + suc (suc (length (PG.rest pg))) ≤⟨ <-trans (n<1+n _) (n<1+n _) ⟩ + length (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) ≡⟨ cong length (sym (PG.stack=gp pg)) ⟩ + length stack ∎ + where open ≤-Reasoning + rb02 : RBtreeInvariant (PG.grand pg) + rb02 = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)) + rb09 : RBtreeInvariant (PG.parent pg) + rb09 = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ rb00) + rb08 : treeInvariant (PG.parent pg) + rb08 = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00) + + insertCase51 : t + insertCase51 with PG.pg pg + ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} 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₁) (λ ())) rb11 + } 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 + rb03 : replacedRBTree key value (node kg _ (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) (PG.uncle pg)) + (node kp ⟪ Black , proj2 vp ⟫ repl (node kg ⟪ Red , proj2 vg ⟫ n1 (PG.uncle pg))) + rb03 = rbr-rotate-ll repl-red rb04 rot + rb10 : node kp ⟪ Black , proj2 vp ⟫ repl (node kg ⟪ Red , proj2 vg ⟫ n1 (PG.uncle pg)) ≡ rb01 + rb10 = begin + to-black (node kp vp repl (to-red (node kg vg n1 (PG.uncle pg)))) ≡⟨ cong (λ k → node _ _ k _) (sym eq) ⟩ + rb01 ∎ where open ≡-Reasoning + rb12 : node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) (PG.uncle pg) ≡ PG.grand pg + rb12 = begin + node kg ⟪ Black , proj2 vg ⟫ (node kp ⟪ Red , proj2 vp ⟫ (RBI.tree r) n1) (PG.uncle pg) + ≡⟨ cong₂ (λ j k → node kg j (node kp k (RBI.tree r) n1) (PG.uncle pg) ) rb14 rb13 ⟩ + node kg vg _ (PG.uncle pg) ≡⟨ cong (λ k → node _ _ k _) (sym x) ⟩ + node kg vg (PG.parent pg) (PG.uncle pg) ≡⟨ sym x₁ ⟩ + PG.grand pg ∎ where open ≡-Reasoning + rb11 : replacedRBTree key value (PG.grand pg) rb01 + rb11 = subst₂ (λ j k → replacedRBTree key value j k) rb12 rb10 rb03 + rb05 : RBtreeInvariant (PG.uncle pg) + rb05 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb02) + rb06 : RBtreeInvariant n1 + rb06 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x rb09) + rb19 : black-depth n1 ≡ black-depth (PG.uncle pg) + rb19 = trans (sym ( proj2 (red-children-eq x (sym (cong proj1 rb13)) rb09) )) (RBtreeEQ (subst (λ k → RBtreeInvariant k) x₁ rb02)) + rb18 : black-depth repl ≡ black-depth n1 ⊔ black-depth (PG.uncle pg) + rb18 = begin + black-depth repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ + black-depth (RBI.tree r) ≡⟨ RBtreeEQ (subst (λ k → RBtreeInvariant k) x rb09) ⟩ + black-depth n1 ≡⟨ sym (⊔-idem (black-depth n1)) ⟩ + black-depth n1 ⊔ black-depth n1 ≡⟨ cong (λ k → black-depth n1 ⊔ k) rb19 ⟩ + black-depth n1 ⊔ black-depth (PG.uncle pg) ∎ where open ≡-Reasoning + rb17 : suc (black-depth (node rkey vr rp-left rp-right) ⊔ (black-depth n1 ⊔ black-depth (PG.uncle pg))) ≡ black-depth (PG.grand pg) + rb17 = begin + suc (black-depth (node rkey vr rp-left rp-right) ⊔ (black-depth n1 ⊔ black-depth (PG.uncle pg))) + ≡⟨ cong₂ (λ j k → suc (black-depth j ⊔ k)) eq (sym rb18) ⟩ + suc (black-depth repl ⊔ black-depth repl) ≡⟨ ⊔-idem _ ⟩ + suc (black-depth repl ) ≡⟨ cong suc (sym (RB-repl→eq _ _ (RBI.treerb r) rot)) ⟩ + suc (black-depth (RBI.tree r) ) ≡⟨ cong suc (sym (proj1 (red-children-eq x (cong proj1 (sym rb13)) rb09))) ⟩ + suc (black-depth (PG.parent pg) ) ≡⟨ sym (proj1 (black-children-eq refl (cong proj1 (sym rb14)) (subst (λ k → RBtreeInvariant k) x₁ rb02))) ⟩ + black-depth (node kg vg (PG.parent pg) (PG.uncle pg)) ≡⟨ cong black-depth (sym x₁) ⟩ + black-depth (PG.grand pg) ∎ where open ≡-Reasoning + -- lt : key < kp + -- x : PG.parent pg ≡ node kp vp (RBI.tree r) n1 + -- x₁ : PG.grand pg ≡ node kg vg (PG.parent pg) (PG.uncle pg) + -- eq : node rkey vr rp-left rp-right ≡ RBI.repl r + ... | 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 (trans (cong color x₁) (cong proj1 (sym rb14))) rb17 (subst (λ k → ¬ (k ≡ leaf)) (sym x₁) (λ ())) rb11 + } 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) + -- 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)) + rb03 : replacedRBTree key value (node kg _ (node kp _ n1 (RBI.tree r)) (PG.uncle pg)) + (node rkey ⟪ Black , proj2 vr ⟫ (node kp ⟪ Red , proj2 vp ⟫ n1 rp-left) (node kg ⟪ Red , proj2 vg ⟫ rp-right (PG.uncle pg))) + rb03 = rbr-rotate-lr rp-left rp-right kg kp rkey rb20 rb04 rb21 + (subst (λ k → replacedRBTree key value (RBI.tree r) k) (trans (sym eq) (cong (λ k → node rkey k rp-left rp-right) rb23 )) rot ) + 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 + rb11 : replacedRBTree key value (PG.grand pg) rb01 + rb11 = subst₂ (λ j k → replacedRBTree key value j k) rb24 rb25 rb03 + 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 = begin + black-depth rp-right ≡⟨ sym (proj2 (red-children-eq (cong (λ k → node rkey k rp-left rp-right) rb23) refl rb31 )) ⟩ + black-depth (node rkey vr rp-left rp-right) ≡⟨ cong black-depth eq ⟩ + black-depth (RBI.repl r) ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ + black-depth (RBI.tree r) ≡⟨ sym (proj2 (red-children-eq refl refl + (subst (λ k → RBtreeInvariant k) (trans x (cong (λ k → node kp k n1 (RBI.tree r) ) (sym rb13) )) rb09))) ⟩ + black-depth (node kp ⟪ Red , proj2 vp ⟫ n1 (RBI.tree r)) ≡⟨ black-depth-cong _ (cong (λ k → node kp k n1 (RBI.tree r)) rb13) ⟩ + black-depth (node kp vp n1 (RBI.tree r)) ≡⟨ black-depth-cong _ (sym x) ⟩ + black-depth (PG.parent pg) ≡⟨ RBtreeEQ (subst (λ k → RBtreeInvariant k) x₁ rb02 ) ⟩ + black-depth (PG.uncle pg) ∎ where open ≡-Reasoning + rb27 : black-depth n1 ≡ black-depth rp-left + rb27 = begin + black-depth n1 ≡⟨ RBtreeEQ (subst (λ k → RBtreeInvariant k) x rb09) ⟩ + black-depth (RBI.tree r) ≡⟨ RB-repl→eq _ _ (RBI.treerb r) rot ⟩ + black-depth (RBI.repl r) ≡⟨ cong black-depth (sym eq) ⟩ + black-depth (node rkey vr rp-left rp-right) ≡⟨ black-depth-cong _ (cong (λ k → node rkey k rp-left rp-right) rb23) ⟩ + black-depth (node rkey ⟪ Red , proj2 vr ⟫ rp-left rp-right) ≡⟨⟩ + black-depth rp-left ⊔ black-depth rp-right ≡⟨ cong (λ k → black-depth rp-left ⊔ k) (sym (RBtreeEQ rb31)) ⟩ + black-depth rp-left ⊔ black-depth rp-left ≡⟨ ⊔-idem _ ⟩ + black-depth rp-left ∎ + where open ≡-Reasoning + 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) ≡⟨ cong (λ k → black-depth (node kp k n1 _)) (sym rb13) ⟩ + black-depth (node kp ⟪ Red , proj2 vp ⟫ n1 rp-left) ≡⟨⟩ + black-depth n1 ⊔ black-depth rp-left ≡⟨ cong (λ k → k ⊔ black-depth rp-left) rb27 ⟩ + black-depth rp-left ⊔ black-depth rp-left ≡⟨ ⊔-idem _ ⟩ + black-depth rp-left ≡⟨ RBtreeEQ rb31 ⟩ + 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₁ = ? + ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? + replaceRBP1 : t + replaceRBP1 with RBI.state r + ... | rebuild ceq bdepth-eq ¬leaf rot = rebuildCase ceq bdepth-eq ¬leaf rot + ... | top-black eq rot = 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 rot with stackToPG (RBI.tree r) orig stack (RBI.si r) + ... | case1 eq = exit stack eq r -- no stack, replace top node + ... | case2 (case1 eq) = insertCase4 orig refl eq rot (case1 repl-red) (RBI.si r) -- one level stack, orig is parent of repl + ... | case2 (case2 pg) with color (PG.parent pg) in pcolor + ... | 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 (λ k → replacedRBTree key value k (node kp vp repl n1) ) (sym x) (rb02 rb04 )) + } (subst₂ (λ j k → j < length k ) refl (sym (PG.stack=gp pg)) ≤-refl) where + rb01 : bt (Color ∧ A) + rb01 = node kp vp repl n1 + rb03 : key < kp + rb03 = lt + rb04 : ⟪ Black , proj2 vp ⟫ ≡ vp + rb04 with subst (λ k → color k ≡ Black) x pcolor + ... | refl = refl + rb02 : ⟪ Black , proj2 vp ⟫ ≡ vp → replacedRBTree key value (node kp vp (RBI.tree r) n1) (node kp vp repl n1) + rb02 eq = subst (λ k → replacedRBTree key value (node kp k (RBI.tree r) n1) (node kp k repl n1)) eq (rbr-black-left repl-red rb03 rot ) + rb07 : black-depth repl ≡ black-depth n1 + rb07 = begin + black-depth repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ + black-depth (RBI.tree r) ≡⟨ RBtreeEQ (subst (λ k → RBtreeInvariant k) x (treerb pg)) ⟩ + black-depth n1 ∎ + where open ≡-Reasoning + rb05 : proj1 vp ≡ Black → black-depth rb01 ≡ black-depth (PG.parent pg) + rb05 refl = begin + suc (black-depth repl ⊔ black-depth n1) ≡⟨ cong suc (cong (λ k → k ⊔ black-depth n1) (sym (RB-repl→eq _ _ (RBI.treerb r) rot))) ⟩ + suc (black-depth (RBI.tree r) ⊔ black-depth n1) ≡⟨ refl ⟩ + black-depth (node kp vp (RBI.tree r) n1) ≡⟨ cong black-depth (sym x) ⟩ + black-depth (PG.parent pg) ∎ + where open ≡-Reasoning + rb06 : RBtreeInvariant rb01 + rb06 = subst (λ k → RBtreeInvariant (node kp k repl n1)) rb04 + ( rb-black _ _ rb07 (RBI.replrb r) (RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x (treerb pg)))) + insertCase1 | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? + insertCase1 | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? + insertCase1 | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = ? + ... | Red with PG.uncle pg in uneq + ... | leaf = insertCase5 repl refl pg rot repl-red (cong color uneq) pcolor + ... | node key₁ ⟪ Black , value₁ ⟫ t₁ t₂ = insertCase5 repl refl pg rot repl-red (cong color uneq) pcolor + ... | node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ with PG.pg pg -- insertCase2 : uncle and parent are Red, flip color and go up by two level + ... | s2-s1p2 {kp} {kg} {vp} {vg} {n1} {n2} 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 (subst₂ (λ j k → replacedRBTree key value j k ) (sym rb09) refl (rbr-flip-ll repl-red (rb05 refl uneq) rb06 rot)) + } rb15 where + rb00 : stackInvariant key (RBI.tree r) orig (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) + rb00 = subst (λ k → stackInvariant key (RBI.tree r) orig k) (PG.stack=gp pg) (RBI.si r) + rb01 : RBtreeInvariant (PG.grand pg) + rb01 = PGtoRBinvariant1 _ orig (RBI.origrb r) _ (popStackInvariant _ _ _ _ _ (popStackInvariant _ _ _ _ _ rb00)) + rb02 : RBtreeInvariant (PG.uncle pg) + rb02 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01) + rb03 : RBtreeInvariant (PG.parent pg) + rb03 = RBtreeLeftDown _ _ (subst (λ k → RBtreeInvariant k) x₁ rb01) + rb04 : RBtreeInvariant n1 + rb04 = RBtreeRightDown _ _ (subst (λ k → RBtreeInvariant k) x rb03) + rb05 : { tree : bt (Color ∧ A) } → tree ≡ PG.uncle pg → tree ≡ node key₁ ⟪ Red , value₁ ⟫ t₁ t₂ → color (PG.uncle pg) ≡ Red + rb05 refl refl = refl + rb08 : treeInvariant (PG.parent pg) + rb08 = siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00) + rb07 : treeInvariant (node kp vp (RBI.tree r) n1) + rb07 = subst (λ k → treeInvariant k) x (siToTreeinvariant _ _ _ _ (RBI.origti r) (popStackInvariant _ _ _ _ _ rb00)) + rb06 : key < kp + rb06 = 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 = begin + black-depth repl ≡⟨ sym (RB-repl→eq _ _ (RBI.treerb r) rot) ⟩ + black-depth (RBI.tree r) ≡⟨ RBtreeEQ (subst (λ k → RBtreeInvariant k) x rb03) ⟩ + black-depth n1 ∎ + where open ≡-Reasoning + rb12 : suc (black-depth repl ⊔ black-depth n1) ≡ black-depth (to-black (PG.uncle pg)) + rb12 = begin + suc (black-depth repl ⊔ black-depth n1) ≡⟨ cong (λ k → suc (k ⊔ black-depth n1)) (sym (RB-repl→eq _ _ (RBI.treerb r) rot)) ⟩ + suc (black-depth (RBI.tree r) ⊔ black-depth n1) ≡⟨ cong (λ k → suc (k ⊔ black-depth n1)) (RBtreeEQ (subst (λ k → RBtreeInvariant k) x rb03)) ⟩ + suc (black-depth n1 ⊔ black-depth n1) ≡⟨ ⊔-idem _ ⟩ + suc (black-depth n1 ) ≡⟨ cong suc (sym (proj2 (red-children-eq x (cong proj1 rb11) rb03 ))) ⟩ + suc (black-depth (PG.parent pg)) ≡⟨ cong suc (RBtreeEQ (subst (λ k → RBtreeInvariant k) x₁ rb01)) ⟩ + suc (black-depth (PG.uncle pg)) ≡⟨ to-black-eq (PG.uncle pg) (cong color uneq ) ⟩ + black-depth (to-black (PG.uncle pg)) ∎ + where open ≡-Reasoning + rb17 : suc (black-depth repl ⊔ black-depth n1) ⊔ black-depth (to-black (PG.uncle pg)) ≡ black-depth (PG.grand pg) + rb17 = begin + suc (black-depth repl ⊔ black-depth n1) ⊔ black-depth (to-black (PG.uncle pg)) ≡⟨ cong (λ k → k ⊔ black-depth (to-black (PG.uncle pg))) rb12 ⟩ + black-depth (to-black (PG.uncle pg)) ⊔ black-depth (to-black (PG.uncle pg)) ≡⟨ ⊔-idem _ ⟩ + black-depth (to-black (PG.uncle pg)) ≡⟨ sym (to-black-eq (PG.uncle pg) (cong color uneq )) ⟩ + suc (black-depth (PG.uncle pg)) ≡⟨ sym ( proj2 (black-children-eq x₁ (cong proj1 rb10) rb01 )) ⟩ + black-depth (PG.grand pg) ∎ + where open ≡-Reasoning + rb15 : suc (length (PG.rest pg)) < length stack + rb15 = begin + suc (suc (length (PG.rest pg))) ≤⟨ <-trans (n<1+n _) (n<1+n _) ⟩ + length (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) ≡⟨ cong length (sym (PG.stack=gp pg)) ⟩ + length stack ∎ + where open ≤-Reasoning + ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = {!!} + ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = {!!} + ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} lt x x₁ = {!!} +