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)