Mercurial > hg > Gears > GearsAgda
view hoareBinaryTree1.agda @ 796:e1737f00a7aa
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 26 Oct 2023 18:11:17 +0900 |
| parents | e9ba6a5bc64b |
| children | 03831d974342 |
line wrap: on
line source
module hoareBinaryTree1 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₁ ) open import Data.Unit hiding ( _≟_ ) -- ; _≤?_ ; _≤_) 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₁ → 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₁ → 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₂ → 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 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) (t-node (add< 0) (add< 1) (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-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 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 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 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₁ 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 t) = t-right x t replaceTree1 k v1 value (t-left x t) = t-left x t replaceTree1 k v1 value (t-node x x₁ t t₁) = t-node x x₁ 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 record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A ) (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where field tree0 : bt A ti : treeInvariant tree0 si : stackInvariant key tree tree0 stack ri : replacedTree key value (child-replaced key tree ) repl ci : C tree repl stack -- data continuation record replacePR' {n : Level} {A : Set n} (key : ℕ) (value : A) (orig : bt A ) (stack : List (bt A)) : Set n where field tree repl : bt A ti : treeInvariant orig si : stackInvariant key tree orig stack ri : replacedTree key value (child-replaced key tree) repl -- treeInvariant of tree and repl is inferred from ti, si and ri. replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A) → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value (child-replaced key tree) tree1 → t) → t replaceNodeP k v1 leaf C P next = next (node k v1 leaf leaf) (t-single k v1 ) r-leaf replaceNodeP k v1 (node .k value t t₁) (case2 refl) P next = next (node k v1 t t₁) (replaceTree1 k value v1 P) (subst (λ j → replacedTree k v1 j (node k v1 t t₁) ) repl00 r-node) where repl00 : node k value t t₁ ≡ child-replaced k (node k value t t₁) repl00 with <-cmp k k ... | tri< a ¬b ¬c = ⊥-elim (¬b refl) ... | tri≈ ¬a b ¬c = refl ... | tri> ¬a ¬b c = ⊥-elim (¬b refl) replaceP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → {tree : bt A} ( repl : bt A) → (stack : List (bt A)) → replacePR key value tree repl stack (λ _ _ _ → Lift n ⊤) → (next : ℕ → A → {tree1 : bt A } (repl : bt A) → (stack1 : List (bt A)) → replacePR key value tree1 repl stack1 (λ _ _ _ → Lift n ⊤) → length stack1 < length stack → t) → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t replaceP key value {tree} repl [] Pre next exit = ⊥-elim ( si-property0 (replacePR.si Pre) refl ) -- can't happen replaceP key value {tree} repl (leaf ∷ []) Pre next exit with si-property-last _ _ _ _ (replacePR.si Pre)-- tree0 ≡ leaf ... | refl = exit (replacePR.tree0 Pre) (node key value leaf leaf) ⟪ replacePR.ti Pre , r-leaf ⟫ replaceP key value {tree} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁ ... | tri< a ¬b ¬c = exit (replacePR.tree0 Pre) (node key₁ value₁ repl right ) ⟪ replacePR.ti Pre , repl01 ⟫ where repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ repl right ) repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre) repl01 | refl | refl = subst (λ k → replacedTree key value (node key₁ value₁ k right ) (node key₁ value₁ repl right )) repl02 (r-left a repl03) where repl03 : replacedTree key value ( child-replaced key (node key₁ value₁ left right)) repl repl03 = replacePR.ri Pre repl02 : child-replaced key (node key₁ value₁ left right) ≡ left repl02 with <-cmp key key₁ ... | tri< a ¬b ¬c = refl ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a a) ... | tri> ¬a ¬b c = ⊥-elim ( ¬a a) ... | tri≈ ¬a b ¬c = exit (replacePR.tree0 Pre) repl ⟪ replacePR.ti Pre , repl01 ⟫ where repl01 : replacedTree key value (replacePR.tree0 Pre) repl repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre) repl01 | refl | refl = subst (λ k → replacedTree key value k repl) repl02 (replacePR.ri Pre) where repl02 : child-replaced key (node key₁ value₁ left right) ≡ node key₁ value₁ left right repl02 with <-cmp key key₁ ... | tri< a ¬b ¬c = ⊥-elim ( ¬b b) ... | tri≈ ¬a b ¬c = refl ... | tri> ¬a ¬b c = ⊥-elim ( ¬b b) ... | tri> ¬a ¬b c = exit (replacePR.tree0 Pre) (node key₁ value₁ left repl ) ⟪ replacePR.ti Pre , repl01 ⟫ where repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ left repl ) repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre) repl01 | refl | refl = subst (λ k → replacedTree key value (node key₁ value₁ left k ) (node key₁ value₁ left repl )) repl02 (r-right c repl03) where repl03 : replacedTree key value ( child-replaced key (node key₁ value₁ left right)) repl repl03 = replacePR.ri Pre repl02 : child-replaced key (node key₁ value₁ left right) ≡ right repl02 with <-cmp key key₁ ... | tri< a ¬b ¬c = ⊥-elim ( ¬c c) ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c c) ... | tri> ¬a ¬b c = refl replaceP {n} {_} {A} key value {tree} repl (leaf ∷ st@(tree1 ∷ st1)) Pre next exit = next key value repl st Post ≤-refl where Post : replacePR key value tree1 repl (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤) Post with replacePR.si Pre ... | s-right _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where repl09 : tree1 ≡ node key₂ v1 tree₁ leaf repl09 = si-property1 si repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) repl10 with si-property1 si ... | refl = si repl07 : child-replaced key (node key₂ v1 tree₁ leaf) ≡ leaf repl07 with <-cmp key key₂ ... | tri< a ¬b ¬c = ⊥-elim (¬c x) ... | tri≈ ¬a b ¬c = ⊥-elim (¬c x) ... | tri> ¬a ¬b c = refl repl12 : replacedTree key value (child-replaced key tree1 ) repl repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07 ) ) (sym (rt-property-leaf (replacePR.ri Pre))) r-leaf ... | s-left _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where repl09 : tree1 ≡ node key₂ v1 leaf tree₁ repl09 = si-property1 si repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) repl10 with si-property1 si ... | refl = si repl07 : child-replaced key (node key₂ v1 leaf tree₁ ) ≡ leaf repl07 with <-cmp key key₂ ... | tri< a ¬b ¬c = refl ... | tri≈ ¬a b ¬c = ⊥-elim (¬a x) ... | tri> ¬a ¬b c = ⊥-elim (¬a x) repl12 : replacedTree key value (child-replaced key tree1 ) repl repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07) ) (sym (rt-property-leaf (replacePR.ri Pre ))) r-leaf -- repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07 ) ) (sym (rt-property-leaf (replacePR.ri Pre))) r-leaf replaceP {n} {_} {A} key value {tree} repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit with <-cmp key key₁ ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st Post ≤-refl where Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤) Post with replacePR.si Pre ... | s-right _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right) repl09 = si-property1 si repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) repl10 with si-property1 si ... | refl = si repl03 : child-replaced key (node key₁ value₁ left right) ≡ left repl03 with <-cmp key key₁ ... | tri< a1 ¬b ¬c = refl ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a) ... | tri> ¬a ¬b c = ⊥-elim (¬a a) repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right repl02 with repl09 | <-cmp key key₂ ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt) ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt) ... | refl | tri> ¬a ¬b c = refl repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1 repl04 = begin node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03 ⟩ node key₁ value₁ left right ≡⟨ sym repl02 ⟩ child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ child-replaced key tree1 ∎ where open ≡-Reasoning repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ repl right) repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right) ) repl04 (r-left a (replacePR.ri Pre)) ... | s-left _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁ repl09 = si-property1 si repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) repl10 with si-property1 si ... | refl = si repl03 : child-replaced key (node key₁ value₁ left right) ≡ left repl03 with <-cmp key key₁ ... | tri< a1 ¬b ¬c = refl ... | tri≈ ¬a b ¬c = ⊥-elim (¬a a) ... | tri> ¬a ¬b c = ⊥-elim (¬a a) repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right repl02 with repl09 | <-cmp key key₂ ... | refl | tri< a ¬b ¬c = refl ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt) ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt) repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1 repl04 = begin node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡⟨ cong (λ k → node key₁ value₁ k right) repl03 ⟩ node key₁ value₁ left right ≡⟨ sym repl02 ⟩ child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ child-replaced key tree1 ∎ where open ≡-Reasoning repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ repl right) repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right) ) repl04 (r-left a (replacePR.ri Pre)) ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st Post ≤-refl where Post : replacePR key value tree1 (node key₁ value left right ) (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤) Post with replacePR.si Pre ... | s-right _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 b ; ci = lift tt } where repl09 : tree1 ≡ node key₂ v1 tree₁ tree -- (node key₁ value₁ left right) repl09 = si-property1 si repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) repl10 with si-property1 si ... | refl = si repl07 : child-replaced key (node key₂ v1 tree₁ tree) ≡ tree repl07 with <-cmp key key₂ ... | tri< a ¬b ¬c = ⊥-elim (¬c x) ... | tri≈ ¬a b ¬c = ⊥-elim (¬c x) ... | tri> ¬a ¬b c = refl repl12 : (key ≡ key₁) → replacedTree key value (child-replaced key tree1 ) (node key₁ value left right ) repl12 refl with repl09 ... | refl = subst (λ k → replacedTree key value k (node key₁ value left right )) (sym repl07) r-node ... | s-left _ _ tree₁ {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 b ; ci = lift tt } where repl09 : tree1 ≡ node key₂ v1 tree tree₁ repl09 = si-property1 si repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) repl10 with si-property1 si ... | refl = si repl07 : child-replaced key (node key₂ v1 tree tree₁ ) ≡ tree repl07 with <-cmp key key₂ ... | tri< a ¬b ¬c = refl ... | tri≈ ¬a b ¬c = ⊥-elim (¬a x) ... | tri> ¬a ¬b c = ⊥-elim (¬a x) repl12 : (key ≡ key₁) → replacedTree key value (child-replaced key tree1 ) (node key₁ value left right ) repl12 refl with repl09 ... | refl = subst (λ k → replacedTree key value k (node key₁ value left right )) (sym repl07) r-node ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st Post ≤-refl where Post : replacePR key value tree1 (node key₁ value₁ left repl ) st (λ _ _ _ → Lift n ⊤) Post with replacePR.si Pre ... | s-right _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right) repl09 = si-property1 si repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) repl10 with si-property1 si ... | refl = si repl03 : child-replaced key (node key₁ value₁ left right) ≡ right repl03 with <-cmp key key₁ ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c) ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c) ... | tri> ¬a ¬b c = refl repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right repl02 with repl09 | <-cmp key key₂ ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt) ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt) ... | refl | tri> ¬a ¬b c = refl repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1 repl04 = begin node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩ node key₁ value₁ left right ≡⟨ sym repl02 ⟩ child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ child-replaced key tree1 ∎ where open ≡-Reasoning repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ left repl) repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ left repl) ) repl04 (r-right c (replacePR.ri Pre)) ... | s-left _ _ tree₁ {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁ repl09 = si-property1 si repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) repl10 with si-property1 si ... | refl = si repl03 : child-replaced key (node key₁ value₁ left right) ≡ right repl03 with <-cmp key key₁ ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c) ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c) ... | tri> ¬a ¬b c = refl repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right repl02 with repl09 | <-cmp key key₂ ... | refl | tri< a ¬b ¬c = refl ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt) ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt) repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1 repl04 = begin node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩ node key₁ value₁ left right ≡⟨ sym repl02 ⟩ child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩ child-replaced key tree1 ∎ where open ≡-Reasoning repl12 : replacedTree key value (child-replaced key tree1 ) (node key₁ value₁ left repl) repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ left repl) ) repl04 (r-right c (replacePR.ri Pre)) TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) → (r : Index) → (p : Invraiant r) → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r) ... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) ... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (m≤n⇒m≤1+n lt1) p1 lt1 ) where TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j → Invraiant r1 → reduce r1 < reduce r → t TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) TerminatingLoop1 (suc j) r r1 n≤j p1 lt with <-cmp (reduce r1) (suc j) ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 ) ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c n≤j ) open _∧_ 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 ti) r-node = t-right x ti RTtoTI0 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x ti) r-node = t-left x ti RTtoTI0 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node x x₁ ti ti₁) r-node = t-node x x₁ 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₁ ti) (r-right x ri) = t-single key₁ value₁ RTtoTI0 (node key₁ _ leaf right@(node key₂ _ _ _)) (node key₁ value₁ leaf right₁@(node key₃ _ _ _)) key value (t-right x₁ ti) (r-right x ri) = t-right (subst (λ k → key₁ < k ) (rt-property-key ri) x₁) (RTtoTI0 _ _ key value ti ri) RTtoTI0 (node key₁ _ (node _ _ _ _) leaf) (node key₁ _ (node key₃ value left right) leaf) key value₁ (t-left x₁ 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₁ ti) (r-right x r-leaf) = t-node x₁ x ti (t-single key value) RTtoTI0 (node key₁ _ (node _ _ _ _) (node key₂ _ _ _)) (node key₁ _ (node _ _ _ _) (node key₃ _ _ _)) key value (t-node x₁ x₂ ti ti₁) (r-right x ri) = t-node x₁ (subst (λ k → key₁ < k) (rt-property-key ri) x₂) ti (RTtoTI0 _ _ key value ti₁ ri) -- 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 (t-single _ _ ) RTtoTI0 .(node _ _ leaf (node _ _ _ _)) (node key₁ value₁ (node key value leaf leaf) (node _ _ _ _)) key value (t-right x₁ ti) (r-left x r-leaf) = t-node x x₁ (t-single key value) ti RTtoTI0 (node key₃ _ (node key₂ _ _ _) leaf) (node key₃ _ (node key₁ value₁ left left₁) leaf) key value (t-left x₁ ti) (r-left x ri) = t-left (subst (λ k → k < key₃ ) (rt-property-key ri) x₁) (RTtoTI0 _ _ key value ti ri) -- key₁ < key₃ RTtoTI0 (node key₁ _ (node key₂ _ _ _) (node _ _ _ _)) (node key₁ _ (node key₃ _ _ _) (node _ _ _ _)) key value (t-node x₁ x₂ ti ti₁) (r-left x ri) = t-node (subst (λ k → k < key₁ ) (rt-property-key ri) x₁) x₂ (RTtoTI0 _ _ key value ti ri) ti₁ 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 ti) r-node = t-right x ti RTtoTI1 .(node key _ (node _ _ _ _) leaf) .(node key value (node _ _ _ _) leaf) key value (t-left x ti) r-node = t-left x ti RTtoTI1 .(node key _ (node _ _ _ _) (node _ _ _ _)) .(node key value (node _ _ _ _) (node _ _ _ _)) key value (t-node x x₁ ti ti₁) r-node = t-node x x₁ ti ti₁ -- r-right case RTtoTI1 (node key₁ value₁ leaf leaf) (node key₁ _ leaf (node _ _ _ _)) key value (t-right x₁ 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₁ 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₂ 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₂ ti ti₁) (r-right x ri) = t-node x₁ (subst (λ k → key₄ < k ) (sym (rt-property-key ri)) x₂) 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₁ 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₁ 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₂ ti ti₁) (r-left x r-leaf) = t-right x₂ ti₁ RTtoTI1 (node key₁ value₁ (node key₂ value₂ n n₁) _) (node key₁ _ _ _) key value (t-node x₁ x₂ ti ti₁) (r-left x ri) = t-node (subst (λ k → k < key₁ ) (sym (rt-property-key ri)) x₁) x₂ (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 black-depth : {n : Level} {A : Set n} → (tree : bt (Color ∧ A) ) → ℕ black-depth leaf = 0 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₁ ) data RBtreeInvariant {n : Level} {A : Set n} : (tree : bt (Color ∧ A)) → Set n where rb-leaf : RBtreeInvariant leaf rb-single : (key : ℕ) → (value : A) → RBtreeInvariant (node key ⟪ Black , value ⟫ leaf leaf) rb-right-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → black-depth t ≡ black-depth t₁ → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) → RBtreeInvariant (node key ⟪ Red , value ⟫ leaf (node key₁ ⟪ Black , value₁ ⟫ t t₁)) rb-right-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {c : Color} → black-depth t ≡ black-depth t₁ → RBtreeInvariant (node key₁ ⟪ c , value₁ ⟫ t t₁) → RBtreeInvariant (node key ⟪ Black , value ⟫ leaf (node key₁ ⟪ c , value₁ ⟫ t t₁)) rb-left-red : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → black-depth t ≡ black-depth t₁ → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ t t₁) → RBtreeInvariant (node key ⟪ Red , value ⟫ (node key₁ ⟪ Black , value₁ ⟫ t t₁) leaf ) rb-left-black : {key key₁ : ℕ} → {value value₁ : A} → {t t₁ : bt (Color ∧ A)} → key < key₁ → {c : Color} → black-depth t ≡ black-depth t₁ → RBtreeInvariant (node key₁ ⟪ c , value₁ ⟫ t t₁) → RBtreeInvariant (node key ⟪ Black , value ⟫ (node key₁ ⟪ c , value₁ ⟫ t t₁) leaf) rb-node-red : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ → black-depth t₁ ≡ black-depth t₂ → RBtreeInvariant (node key ⟪ Black , value ⟫ t₁ t₂) → black-depth t₃ ≡ black-depth t₄ → RBtreeInvariant (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄) → RBtreeInvariant (node key₁ ⟪ Red , value₁ ⟫ (node key ⟪ Black , value ⟫ t₁ t₂) (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄)) rb-node-black : {key key₁ key₂ : ℕ} → {value value₁ value₂ : A} → {t₁ t₂ t₃ t₄ : bt (Color ∧ A)} → key < key₁ → key₁ < key₂ → {c c₁ : Color} → black-depth t₁ ≡ black-depth t₂ → RBtreeInvariant (node key ⟪ c , value ⟫ t₁ t₂) → black-depth t₃ ≡ black-depth t₄ → RBtreeInvariant (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄) → RBtreeInvariant (node key₁ ⟪ Black , value₁ ⟫ (node key ⟪ c , value ⟫ t₁ t₂) (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄)) data rotatedTree {n : Level} {A : Set n} : (before after : bt A) → Set n where rtt-unit : {t : bt A} → rotatedTree t t rtt-node : {left left' right right' : bt A} → {ke : ℕ} {ve : A} → rotatedTree left left' → rotatedTree right right' → rotatedTree (node ke ve left right) (node ke ve left' right') -- a b -- b c d a -- d e e c -- rtt-right : {ka kb kc kd ke : ℕ} {va vb vc vd ve : A} → {c d e c1 d1 e1 : bt A} → {ctl ctr dtl dtr etl etr : bt A} --kd < kb < ke < ka< kc → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A} → kd < kb → kb < ke → ke < ka → ka < kc → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1) → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1) → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1) → rotatedTree (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr)) (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1))) rtt-left : {ka kb kc kd ke : ℕ} {va vb vc vd ve : A} → {c d e c1 d1 e1 : bt A} → {ctl ctr dtl dtr etl etr : bt A} --kd < kb < ke < ka< kc → {ctl1 ctr1 dtl1 dtr1 etl1 etr1 : bt A} -- after child → kd < kb → kb < ke → ke < ka → ka < kc → rotatedTree (node ke ve etl etr) (node ke ve etl1 etr1) → rotatedTree (node kd vd dtl dtr) (node kd vd dtl1 dtr1) → rotatedTree (node kc vc ctl ctr) (node kc vc ctl1 ctr1) → rotatedTree (node kb vb (node kd vd dtl1 dtr1) (node ka va (node ke ve etl1 etr1) (node kc vc ctl1 ctr1))) (node ka va (node kb vb (node kd vd dtl dtr) (node ke ve etl etr)) (node kc vc ctl ctr)) RBtreeLeftDown : {n : Level} {A : Set n} {key : ℕ} {value : A} {c : Color} → (tleft tright : bt (Color ∧ A)) → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright) → RBtreeInvariant tleft RBtreeLeftDown leaf leaf (rb-single k1 v) = rb-leaf RBtreeLeftDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-red x bde rbti) = rb-leaf RBtreeLeftDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-black x bde rbti) = rb-leaf RBtreeLeftDown leaf (node key ⟪ Red , value ⟫ t1 t2 ) (rb-right-black x bde rbti)= rb-leaf RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-black x bde ti) = ti RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-red x bde ti)= ti RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) leaf (rb-left-black x bde ti) = ti RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til bde2 tir) = til RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = til RBtreeRightDown : {n : Level} {A : Set n} { key : ℕ} {value : A} {c : Color} → (tleft tright : bt (Color ∧ A)) → RBtreeInvariant (node key ⟪ c , value ⟫ tleft tright) → RBtreeInvariant tright RBtreeRightDown leaf leaf (rb-single k1 v1 ) = rb-leaf RBtreeRightDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-red x bde rbti) = rbti RBtreeRightDown leaf (node key ⟪ Black , value ⟫ t1 t2 ) (rb-right-black x bde rbti) = rbti RBtreeRightDown leaf (node key ⟪ Red , value ⟫ t1 t2 ) (rb-right-black x bde rbti)= rbti RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-black x bde ti) = rb-leaf RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) leaf (rb-left-red x bde ti) = rb-leaf RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) leaf (rb-left-black x bde ti) = rb-leaf RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-red x x1 bde1 til bde2 tir) = tir RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde1 til bde2 tir) = tir findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A))) → treeInvariant tree ∧ stackInvariant key tree tree0 stack → RBtreeInvariant tree → (next : (tree1 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A))) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → RBtreeInvariant tree1 → bt-depth tree1 < bt-depth tree → t ) → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → RBtreeInvariant tree1 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t findRBT key leaf tree0 stack ti rb0 next exit = exit leaf stack ti rb0 (case1 refl) findRBT key n@(node key₁ value left right) tree0 stack ti rb0 next exit with <-cmp key key₁ findRBT key (node key₁ value left right) tree0 stack ti rb0 next exit | tri< a ¬b ¬c = next left (left ∷ stack) ⟪ treeLeftDown left right (_∧_.proj1 ti) , s-left _ _ _ a (_∧_.proj2 ti) ⟫ (RBtreeLeftDown left right rb0) depth-1< findRBT key n tree0 stack ti rb0 _ exit | tri≈ ¬a refl ¬c = exit n stack ti rb0 (case2 refl) findRBT key (node key₁ value left right) tree0 stack ti rb0 next exit | tri> ¬a ¬b c = next right (right ∷ stack) ⟪ treeRightDown left right (_∧_.proj1 ti), s-right _ _ _ c (_∧_.proj2 ti) ⟫ (RBtreeRightDown left right rb0) depth-2< data replacedRBTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (before after : bt (Color ∧ A) ) → Set n where rbr-leaf : {ca cb : Color} → replacedRBTree key value leaf (node key ⟪ cb , value ⟫ leaf leaf) rbr-node : {value₁ : A} → {ca cb : Color } → {t t₁ : bt (Color ∧ A)} → replacedRBTree key value (node key ⟪ ca , value₁ ⟫ t t₁) (node key ⟪ cb , value ⟫ t t₁) rbr-right : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)} → k < key → replacedRBTree key value t2 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t1 t) rbr-left : {k : ℕ } {v1 : A} → {ca cb : Color} → {t t1 t2 : bt (Color ∧ A)} → k < key → replacedRBTree key value t1 t → replacedRBTree key value (node k ⟪ ca , v1 ⟫ t1 t2) (node k ⟪ cb , v1 ⟫ t t2) data ParentGrand {n : Level} {A : Set n} (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 } → parent ≡ node kp vp self n1 → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand s2-1sp2 : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } → parent ≡ node kp vp n1 self → grand ≡ node kg vg parent n2 → ParentGrand self parent n2 grand s2-s12p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } → parent ≡ node kp vp self n1 → grand ≡ node kg vg n2 parent → ParentGrand self parent n2 grand s2-1s2p : {kp kg : ℕ} {vp vg : A} → {n1 n2 : bt A} {parent grand : bt A } → parent ≡ node kp vp n1 self → grand ≡ node kg vg n2 parent → ParentGrand self parent n2 grand record PG {n : Level } (A : Set n) (self : bt A) (stack : List (bt A)) : Set n where field parent grand uncle : bt A pg : ParentGrand self parent uncle grand rest : List (bt A) stack=gp : stack ≡ ( self ∷ parent ∷ grand ∷ rest ) record RBI {n : Level} {A : Set n} (key : ℕ) (value : A) (orig repl : bt (Color ∧ A) ) (stack : List (bt (Color ∧ A))) : Set n where field tree rot : 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 rotated : rotatedTree tree rot ri : replacedRBTree key value (child-replaced key rot ) repl repl-red : color repl ≡ Red repl-eq : black-depth (child-replaced key rot ) ≡ black-depth repl 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 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 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 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 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 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 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 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 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 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 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 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 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 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 PGtoRBinvariant : {n : Level} {A : Set n} → {key d0 ds dp dg : ℕ } → (tree orig : bt (Color ∧ A) ) → RBtreeInvariant orig → (stack : List (bt (Color ∧ A))) → (pg : PG (Color ∧ A) tree stack ) → RBtreeInvariant tree ∧ RBtreeInvariant (PG.parent pg) ∧ RBtreeInvariant (PG.grand pg) PGtoRBinvariant = {!!} 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 -- findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) ) -- → (stack : List (bt (Color ∧ A))) → treeInvariant tree0 ∧ stackInvariant key tree tree0 stack -- → {d : ℕ} → RBtreeInvariant tree0 -- → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) -- → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack -- → {d1 : ℕ} → RBtreeInvariant tree1 -- → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t --findRBT {_} {_} {A} {t} key tree0 leaf stack ti {d} rb0 exit = {!!} --findRBT {_} {_} {A} {t} key tree0 (node key₁ value left right) stack ti {d} rb0 exit with <-cmp key key₁ --... | tri< a ¬b ¬c = {!!} --... | tri≈ ¬a b ¬c = {!!} --... | tri> ¬a ¬b c = {!!} rotateLeft : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (orig tree : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → (r : RBI key value orig tree stack ) → (next : (current : bt (Color ∧ A)) → (stack1 : List (bt (Color ∧ A))) → (r : RBI key value orig current stack1 ) → length stack1 < length stack → t ) → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A))) → stack1 ≡ (orig ∷ []) → RBI key value orig repl stack1 → t ) → t rotateLeft {n} {m} {A} {t} key value = {!!} where rotateLeft1 : t rotateLeft1 with stackToPG {!!} {!!} {!!} {!!} ... | case1 x = {!!} -- {!!} {!!} {!!} {!!} rr ... | case2 (case1 x) = {!!} ... | case2 (case2 pg) = {!!} rotateRight : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (orig tree : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → (r : RBI key value orig tree stack ) → (next : (current : bt (Color ∧ A)) → (stack1 : List (bt (Color ∧ A))) → (r : RBI key value orig current stack1 ) → length stack1 < length stack → t ) → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A))) → stack1 ≡ (orig ∷ []) → RBI key value orig repl stack1 → t ) → t rotateRight {n} {m} {A} {t} key value = {!!} where rotateRight1 : t rotateRight1 with stackToPG {!!} {!!} {!!} {!!} ... | case1 x = {!!} ... | case2 (case1 x) = {!!} ... | case2 (case2 pg) = {!!} insertCase5 : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (orig tree : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → (r : RBI key value orig tree stack ) → (next : (tree1 : (bt (Color ∧ A))) → (stack1 : List (bt (Color ∧ A))) → (r : RBI key value orig tree1 stack1 ) → length stack1 < length stack → t ) → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A))) → stack1 ≡ (orig ∷ []) → RBI key value orig repl stack1 → t ) → t insertCase5 {n} {m} {A} {t} key value = {!!} where insertCase51 : t insertCase51 with stackToPG {!!} {!!} {!!} {!!} ... | case1 eq = {!!} ... | case2 (case1 eq ) = {!!} ... | case2 (case2 pg) with PG.pg pg ... | s2-s1p2 x x₁ = {!!} -- rotateRight {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit -- x : PG.parent pg ≡ node kp vp tree n1 -- x₁ : PG.grand pg ≡ node kg vg (PG.parent pg) (PG.uncle pg) ... | s2-1sp2 x x₁ = {!!} -- rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit ... | s2-s12p x x₁ = {!!} -- rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit ... | s2-1s2p x x₁ = {!!} -- rotateLeft {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} next exit -- = insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg) -- if we have replacedNode on RBTree, we have RBtreeInvariant replaceRBP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (orig repl : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → (r : RBI key value orig repl stack ) → (next : (repl1 : (bt (Color ∧ A))) → (stack1 : List (bt (Color ∧ A))) → (r : RBI key value orig repl1 stack1 ) → length stack1 < length stack → t ) → (exit : (repl : bt (Color ∧ A) ) → (stack1 : List (bt (Color ∧ A))) → stack1 ≡ (orig ∷ []) → RBI key value orig repl stack1 → t ) → t replaceRBP {n} {m} {A} {t} key value orig repl stack r next exit = insertCase1 where insertCase2 : (tree parent uncle grand : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) → (si : stackInvariant key tree orig stack ) → (pg : ParentGrand tree parent uncle grand ) → t insertCase2 tree leaf uncle grand stack si (s2-s1p2 () x₁) insertCase2 tree leaf uncle grand stack si (s2-1sp2 () x₁) insertCase2 tree leaf uncle grand stack si (s2-s12p () x₁) insertCase2 tree leaf uncle grand stack si (s2-1s2p () x₁) insertCase2 tree parent@(node kp ⟪ Red , _ ⟫ _ _) uncle grand stack si pg = {!!} -- next {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) leaf grand stack si pg = {!!} insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Red , _ ⟫ _ _ ) grand stack si pg = {!!} -- next {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} {!!} insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-s1p2 x x₁) = {!!} -- insertCase5 key value orig tree {!!} rbio {!!} {!!} stack si {!!} ri {!!} {!!} next exit -- tree is left of parent, parent is left of grand -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp tree n1 -- grand ≡ node kg vg (node kp ⟪ Black , proj3 ⟫ left right) (node ku ⟪ Black , proj4 ⟫ left₁ right₁) insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-1sp2 x x₁) = {!!} -- rotateLeft key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!} -- (λ a b c d e f h i j k l m → insertCase5 key value a b c d {!!} {!!} h i j k l {!!} {!!} next exit ) exit -- tree is right of parent, parent is left of grand rotateLeft -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree -- grand ≡ node kg vg (node kp ⟪ Black , proj3 ⟫ left right) (node ku ⟪ Black , proj4 ⟫ left₁ right₁) insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-s12p x x₁) = {!!} -- rotateRight key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!} -- (λ a b c d e f h i j k l m → insertCase5 key value a b c d {!!} {!!} h i j k l {!!} {!!} next exit ) exit -- tree is left of parent, parent is right of grand, rotateRight -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp tree n1 -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right) insertCase2 tree parent@(node kp ⟪ Black , _ ⟫ _ _) (node ku ⟪ Black , _ ⟫ _ _) grand stack si (s2-1s2p x x₁) = {!!} -- insertCase5 key value orig tree {!!} repl rbio {!!} {!!} stack si {!!} ri {!!} {!!} next exit -- tree is right of parent, parent is right of grand -- node kp ⟪ Black , proj3 ⟫ left right ≡ node kp₁ vp n1 tree -- grand ≡ node kg vg (node ku ⟪ Black , proj4 ⟫ left₁ right₁) (node kp ⟪ Black , proj3 ⟫ left right) insertCase1 : t insertCase1 with stackToPG (RBI.tree r) orig stack (RBI.si r) ... | case1 eq = exit repl stack eq r -- no stack, replace top node ... | case2 (case1 eq) = insertCase12 orig refl (RBI.si r) where -- one level stack, orig is parent of repl rb01 : stackInvariant key (RBI.tree r) orig stack rb01 = RBI.si r insertCase12 : (tr0 : bt (Color ∧ A)) → tr0 ≡ orig → stackInvariant key (RBI.tree r) orig stack → t insertCase12 leaf eq1 si = ? -- can't happen insertCase12 tr0@(node key₁ value₁ left right) refl si with <-cmp key key₁ | child-replaced key (node key₁ value₁ left (RBI.rot r)) in eqcr ... | tri< a ¬b ¬c | cr = ? ... | tri≈ ¬a b ¬c | cr = ? -- can't happen ... | tri> ¬a ¬b c | cr = insertCase13 value₁ refl where -- -- orig B -- / \ -- left tree → rot → repl R -- -- B => B B => B -- / \ / \ / \ rotate L / \ -- L L1 L R3 L R -- bad B B -- / \ / \ / \ 1 : child-replace --- L L2 L B L L 2: child-replace ( unbalanced ) -- / \ 3: child-replace ( rotated / balanced ) -- L L -- 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 ) insertCase13 : (v : Color ∧ A ) → v ≡ value₁ → t insertCase13 ⟪ Black , value₄ ⟫ refl = exit (node key₁ ⟪ Red , value₄ ⟫ left repl) (orig ∷ []) refl record { tree = orig ; rot = node key₁ value₁ left (RBI.rot r) ; origti = RBI.origti r ; origrb = RBI.origrb r ; treerb = RBI.origrb r ; replrb = proj1 rb05 ; si = s-nil ; rotated = subst (λ k → rotatedTree k (node key₁ value₁ left (RBI.rot r))) ( trans (cong (λ k → node key₁ value₁ left k) (sym (rb04 si eq refl))) refl) (rtt-node rtt-unit (RBI.rotated r)) ; ri = proj2 rb05 ; repl-red = refl ; repl-eq = rb07 } where rb07 : black-depth (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) ≡ black-depth left ⊔ black-depth repl rb07 = ? -- rb05 should more general rb05 : RBtreeInvariant (node key₁ ⟪ Red , value₄ ⟫ left repl) ∧ replacedRBTree key value (child-replaced key (node key₁ ⟪ Black , value₄ ⟫ left (RBI.rot r))) (node key₁ ⟪ Red , value₄ ⟫ left repl) rb05 with RBI.origrb r | rb04 si eq refl | RBI.replrb r in eqrepl ... | rb-single key₂ value₂ | refl | rb-single key value = ? ... | rb-single key₂ value₂ | refl | rb-right-red x x₁ rb = ? ... | rb-single key₂ value₂ | refl | rb-right-black x x₁ rb = ? ... | rb-single key₂ value₂ | refl | rb-left-red x x₁ rb = ? ... | rb-single key₂ value₂ | refl | rb-left-black x x₁ rb = ? ... | rb-single key₂ value₂ | refl | rb-node-red x x₁ x₂ rb x₃ rb₁ = ? ... | rb-single key₂ value₂ | refl | rb-node-black x x₁ x₂ rb x₃ rb₁ = ? ... | rb-right-black x x₁ t | refl | rb = ? ... | rb-left-black x x₁ t | refl | rb = ? ... | rb-node-black x x₁ x₂ t x₃ t₁ | refl | rb = ? insertCase13 ⟪ Red , value₄ ⟫ eq with color (RBI.tree r) ... | Black = exit ? ? ? ? ... | Red = exit ? ? ? ? -- r = orig RBI.tree b -- / \ => / \ -- b b → r RBI.tree r r = orig o (r/b) ... | case2 (case2 pg) = {!!} -- insertCase2 tree (PG.parent pg) (PG.uncle pg) (PG.grand pg) stack si (PG.pg pg)