module work 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

zero≢suc : { m : ℕ } → zero ≡ suc m → ⊥
zero≢suc ()
suc≢zero : {m : ℕ } → suc m ≡ zero → ⊥ 
suc≢zero ()
{-# TERMINATING #-}
DepthCal : ( l m n : ℕ ) → l ≡ m ⊔ n
DepthCal zero zero zero  = refl 
DepthCal zero zero (suc n)  = ⊥-elim (zero≢suc (DepthCal zero zero (suc n)))
DepthCal zero (suc m) zero  = ⊥-elim (zero≢suc (DepthCal zero (suc m) zero))
DepthCal zero (suc m) (suc n)  = ⊥-elim (zero≢suc (DepthCal zero (suc m) (suc n)))
DepthCal (suc l) zero zero  = ⊥-elim (suc≢zero (DepthCal (suc l) zero zero ))
DepthCal (suc l) zero (suc n)  with <-cmp (suc l) (suc n)
... | tri< a ¬b ¬c = ⊥-elim (¬b (DepthCal (suc l) zero (suc n) ))
... | tri≈ ¬a b ¬c = cong suc (suc-injective b)
... | tri> ¬a ¬b c = ⊥-elim (¬b (DepthCal (suc l) zero (suc n) ))
DepthCal (suc l) (suc m) zero  with <-cmp (suc l) (suc m)
... | tri< a ¬b ¬c = ⊥-elim (¬b (DepthCal (suc l) (suc m) zero ))
... | tri≈ ¬a b ¬c = cong suc (suc-injective b)
... | tri> ¬a ¬b c = ⊥-elim (¬b (DepthCal (suc l) (suc m) zero ))
DepthCal (suc l) (suc m) (suc n) = cong suc (DepthCal l m n ) 


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 leaf = nothing 
node-key (node key value tree tree₁) =  just key

node-value : {n : Level} {A : Set n} → bt A → Maybe A 
node-value leaf = nothing
node-value (node key value tree tree₁) = just value

bt-depth : {n : Level} {A : Set n} → (tree : bt A) → ℕ
bt-depth leaf = 0
bt-depth (node key value tree tree₁) = suc (bt-depth tree ⊔ bt-depth tree₁)
--一番下のleaf =0から戻るたびにsucをしていく
treeTest1  : bt ℕ
treeTest1  =  node 0 0 leaf (node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf))

--        0         0
--       /  \
--     leaf  3      1
--         /  \
--        2     5   2
--       / \
--      1  leaf     3
--     / \
--   leaf leaf      4

treeTest2  : bt ℕ
treeTest2  =  node 3 1 (node 2 5 (node 1 7 leaf leaf ) leaf) (node 5 5 leaf leaf)



testdb : ℕ
testdb = bt-depth treeTest1 -- 4

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-left : {key key1 : ℕ} → {value value1 : A} → {t1 t2 : bt A} → key < key1
   → treeInvariant (node key value t1 t2)
   → treeInvariant (node key1 value1 (node key value t1 t2) leaf)
  
  t-right : {key key1 : ℕ} → {value value1 : A} → {t1 t2 : bt A} → key < key1
   → treeInvariant (node key1 value1 t1 t2)
   → treeInvariant (node key value leaf (node key1 value1 t1 t2))

  t-node : {key key1 key2 : ℕ}→ {value value1 value2 : A} → {t1 t2 t3 t4 : bt A} → key1 < key → key < key2
   → treeInvariant (node key1 value1 t1 t2)
   → treeInvariant (node key2 value2 t3 t4)
   → treeInvariant (node key value (node key1 value1 t1 t2) (node key2 value2 t3 t4))

{-
treekey : {n : Level} {A : Set n} →  {key key1 : ℕ} {value value1 : A} {t1 t2 : bt A} → treeInvariant (node key value (node key1 value1 t1 t2) leaf) → key1 < key 
treekey (t-left x x₁) = x  -- normal level
--treekey t-single key value  = {!!}
-}

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 : {key1 : ℕ } → {value : A }  → {tree0 t1 t2 : bt A } → {st : List (bt A)}
  → key1 < key 
  → stackInvariant key (node key1 value t1 t2) tree0 st
  → stackInvariant key t2 tree0 (t2 ∷ st)
 
 s-left : {key1 : ℕ } → {value : A }  → {tree0 t1 t2 : bt A } → {st : List (bt A)}
  → key < key1
  → stackInvariant key (node key1 value t1 t2) tree0 st
  → stackInvariant key t1 tree0 (t1 ∷ 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} → {left right : bt A} → replacedTree key value (node key value₁ left right) (node key value left right)
  
  -- key is the repl's key , so need comp key and key1
  r-left : {key1 : ℕ} {value1 : A }→ {left right repl : bt A} → key < key1
   → replacedTree key value left repl → replacedTree key value (node key1 value1 left right) (node key1 value1 repl right)

  r-right : {key1 : ℕ } {value1 : A} → {left right repl : bt A} → key1 < key
   → replacedTree key value right repl → replacedTree key value (node key1 value1 left right) (node key1 value1 left repl)


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} {key : ℕ} {value : A} → (tleft tright : bt A)
 → treeInvariant (node key value tleft tright)
 → treeInvariant tleft
treeLeftDown leaf leaf (t-single key value) = t-leaf
treeLeftDown leaf (node key value t1 t2) (t-right x ti) = t-leaf
treeLeftDown (node key value t t₁) leaf (t-left x ti) = ti
treeLeftDown (node key value t t₁) (node key₁ value₁ t1 t2) (t-node x x1 ti ti2 ) = ti

treeRightDown : {n : Level} {A : Set n} {key : ℕ} {value : A} → (tleft tright : bt A)
 → treeInvariant (node key value tleft tright)
 → treeInvariant tright
treeRightDown leaf leaf (t-single key value) = t-leaf
treeRightDown leaf (node key value t1 t2) (t-right x ti) = ti

treeRightDown (node key value t t₁) leaf (t-left x ti) = t-leaf
treeRightDown (node key value t t₁) (node key₁ value₁ t1 t2) (t-node x x1 ti ti2 ) = ti2


findP : {n m : Level} {A : Set n} {t : Set n} → (tkey : ℕ) → (top orig : bt A) → (st : List (bt A))
 → (treeInvariant top)
 → stackInvariant tkey top orig st
 → (next : (newtop : bt A) → (stack : List (bt A))
         → (treeInvariant newtop)
         → (stackInvariant tkey newtop orig stack)
         → bt-depth newtop < bt-depth top → t) 
 → (exit : (newtop : bt A) → (stack : List (bt A))
         → (treeInvariant newtop)
         → (stackInvariant tkey newtop orig stack) --need new stack ?
         → (newtop ≡ leaf) ∨ (node-key newtop ≡ just tkey) → t)
 → t
findP tkey leaf orig st ti si next exit = exit leaf st ti si (case1 refl)
findP tkey (node key value tl tr) orig st ti si next exit with <-cmp tkey key
findP tkey top orig st ti si next exit | tri≈ ¬a refl ¬c = exit top st ti si (case2 refl)
findP tkey (node key value tl tr) orig st ti si next exit | tri< a ¬b ¬c = next tl (tl ∷ st) (treeLeftDown tl tr ti) (s-left a si) (s≤s (m≤m⊔n (bt-depth tl) (bt-depth tr)))

findP tkey (node key value tl tr) orig st ti si next exit | tri> ¬a ¬b c = next tr (tr ∷ st) (treeRightDown tl tr ti) (s-right c si) (s≤s (m≤n⊔m (bt-depth tl) (bt-depth tr)))


--RBT
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))

RBTreeTest : bt (Color ∧ ℕ)
RBTreeTest = node 8 ⟪ Black , 200 ⟫ (node 5 ⟪ Red , 100 ⟫ (_) (_)) (node 10 ⟪ Red , 300 ⟫ (_) (_))

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 : {c : Color} → (key : ℕ) → (value : A) →  RBtreeInvariant (node key ⟪ c , 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)} → {c : Color} → key₁ < key
       → 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 (node key  ⟪ Black  , value  ⟫ t₁ t₂) ≡ black-depth (node key₂ ⟪ Black , value₂ ⟫ t₃ t₄)
       → RBtreeInvariant (node key ⟪ Black , value ⟫ t₁ 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 (node key  ⟪ c  , value  ⟫ t₁ t₂) ≡ black-depth (node key₂ ⟪ c₁ , value₂ ⟫ t₃ t₄)
       → RBtreeInvariant (node key  ⟪ c  , value  ⟫ t₁ 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-node : {t : bt A } → rotatedTree t t
  --     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 bde til tir) = til --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 tir) = til
RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir) = til
RBtreeLeftDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir) = til
RBtreeLeftDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde til 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 bde til tir ) = tir --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 bde til tir) = tir
RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Black , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir) = tir
RBtreeRightDown (node key ⟪ Black , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir) = tir
RBtreeRightDown (node key ⟪ Red , value ⟫ t t₁) (node key₁ ⟪ Red , value1 ⟫ t1 t2) (rb-node-black x x1 bde til tir) = tir


blackdepth≡ : {n : Level } {A : Set n} → {C : Color} {key key1 : ℕ} {value value1 : A}  →  (tree1 tree2 : bt (Color ∧ A))
  → RBtreeInvariant tree1
  → RBtreeInvariant tree2
  → RBtreeInvariant (node key ⟪ C , value ⟫ tree1 tree2)
  → black-depth tree1 ≡ black-depth tree2
blackdepth≡  leaf leaf ri1 ri2 rip = refl
blackdepth≡ {n} {A} leaf (node key .(⟪ Black , _ ⟫) t2 t3) ri1 ri2 (rb-right-red x x₁ rip) = DepthCal (black-depth {n} {A} leaf) (black-depth (node key ⟪ Black , _ ⟫ t2 t3)) 0
blackdepth≡ {n} {A} leaf (node key .(⟪ _ , _ ⟫) t2 t3) ri1 ri2 (rb-right-black x x₁ rip) = DepthCal (black-depth {n} {A} leaf) (black-depth (node key ⟪ _ , _ ⟫ t2 t3) ) (black-depth (node key ⟪ _ , _ ⟫ t2 t3))
blackdepth≡ {n} {A} (node key .(⟪ Black , _ ⟫) t1 t3) leaf ri1 ri2 (rb-left-red x x₁ rip) = DepthCal (black-depth (node key ⟪ Black , _ ⟫ t1 t3))  (black-depth {n} {A} leaf)  0
blackdepth≡ {n} {A} (node key .(⟪ _ , _ ⟫) t1 t3) leaf ri1 ri2 (rb-left-black x x₁ rip) = DepthCal (black-depth (node key ⟪ _ , _ ⟫ t1 t3)) (black-depth {n} {A} leaf) 0
blackdepth≡ (node key .(⟪ Black , _ ⟫) t1 t3) (node key₁ .(⟪ Black , _ ⟫) t2 t4) ri1 ri2 (rb-node-red x x₁ x₂ rip rip₁) = DepthCal (black-depth  (node key ⟪ Black , _ ⟫ t1 t3)) (black-depth (node key₁ ⟪ Black , _ ⟫ t2 t4)) 0
blackdepth≡ (node key .(⟪ _ , _ ⟫) t1 t3) (node key₁ .(⟪ _ , _ ⟫) t2 t4) ri1 ri2 (rb-node-black x x₁ x₂ rip rip₁) = DepthCal (black-depth (node key ⟪ _ , _ ⟫ t1 t3)) ( black-depth (node key₁ ⟪ _ , _ ⟫ t2 t4))  (black-depth (node key₁ (⟪ _ , _ ⟫) t2 t4))

findRBT : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt (Color ∧ A) ) 
           → (stack : List (bt (Color ∧ A)))
           → RBtreeInvariant tree ∧ stackInvariant key tree tree0 stack
           → (next : (tree1 : bt (Color ∧ A) ) → (stack : List (bt (Color ∧ A)))
                   → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
                   → bt-depth tree1 < bt-depth tree → t )
           → (exit : (tree1 : bt (Color ∧ A)) → (stack : List (bt (Color ∧ A))) 
                 → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
                 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
findRBT key leaf tree0 stack inv next exit = exit leaf stack inv (case1 refl)
findRBT key (node key₁ value left right) tree0 stack inv next exit with <-cmp key key₁
findRBT key (node key₁ value left right) tree0 stack inv next exit | tri< a ¬b ¬c
 = next left (left ∷ stack) ⟪ RBtreeLeftDown left right (_∧_.proj1 inv) , s-left a (_∧_.proj2 inv) ⟫  depth-1<
findRBT key n tree0 stack inv _ exit | tri≈ ¬a refl ¬c = exit n stack inv (case2 refl)
findRBT key (node key₁ value left right) tree0 stack inv next exit | tri> ¬a ¬b c
 = next right (right ∷ stack) ⟪ RBtreeRightDown left right (_∧_.proj1 inv) , s-right c (_∧_.proj2 inv) ⟫  depth-2<

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


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
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

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 _∧_
--findRBTree : (exit : )
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

findTest : {n m : Level} {A : Set n } {t : Set m }
 → (key : ℕ)
 → (tree0 : bt (Color ∧ A))
 → RBtreeInvariant tree0
 → (exit : (tree1 : bt (Color ∧ A))
   → (stack : List (bt (Color ∧ A)))
   → RBtreeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
   → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
findTest {n} {m} {A} {t} k tr0 rb0 exit = TerminatingLoopS (bt (Color ∧ A) ∧ List (bt (Color ∧ A))) {λ p → RBtreeInvariant (proj1 p) ∧ stackInvariant k (proj1 p) tr0 (proj2 p) } (λ p → bt-depth (proj1 p)) ⟪ tr0 , tr0 ∷ [] ⟫ ⟪ rb0 , s-nil ⟫
       $ λ p P loop → findRBT k (proj1 p) tr0 (proj2 p) P (λ t s P1 lt → loop ⟪ t ,  s  ⟫ P1 lt ) 
       $ λ tr1 st P2 O → exit tr1 st P2 O

testRBTree0 :  bt (Color ∧ ℕ)
testRBTree0 = node 8 ⟪ Black , 800 ⟫ (node 5 ⟪ Red , 500 ⟫ (node 2 ⟪ Black , 200 ⟫ leaf leaf) (node 6 ⟪ Black , 600 ⟫ leaf leaf)) (node 10 ⟪ Red , 1000 ⟫ (leaf) (node 15 ⟪ Black , 1500 ⟫ (node 14 ⟪ Red , 1400 ⟫ leaf leaf) leaf))
testRBTree : bt (Color ∧ ℕ)
testRBTree = node 10 ⟪ Red , 1000 ⟫ _ _

record result {n : Level} {A : Set n} {key : ℕ} {tree0 : bt (Color ∧ A)} : Set n where
   field
     tree : bt (Color ∧ A)
     stack : List (bt (Color ∧ A))
     ti : RBtreeInvariant tree
     si : stackInvariant key tree tree0 stack
          
testRBI0 : RBtreeInvariant testRBTree0
testRBI0 = rb-node-black (add< 2) (add< 1) refl (rb-node-red (add< 2) (add< 0) refl (rb-single 2 200) (rb-single 6 600)) (rb-right-red (add< 4) refl (rb-left-black (add< 0) refl (rb-single 14 1400) ))

findRBTreeTest : result
findRBTreeTest = findTest 14 testRBTree0 testRBI0
       $ λ tr s P O → (record {tree = tr ; stack = s ; ti = (proj1 P) ; si = (proj2 P)}) 
       
      
{-
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
       od d rd : ℕ
       tree rot : bt (Color ∧ A)
       origti : treeInvariant orig 
       origrb : RBtreeInvariant orig 
       treerb : RBtreeInvariant tree 
       replrb : RBtreeInvariant repl 
       d=rd : ( d ≡ rd ) ∨ ((suc d ≡ rd ) ∧ (color tree ≡ Red))
       si : stackInvariant key tree orig stack
       rotated : rotatedTree tree rot
       ri : replacedRBTree key value (child-replaced key rot ) repl


rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) ) 
           → RBtreeInvariant parent 
           → RBtreeInvariant repl 
           → {left right : bt (Color ∧ A)} → parent ≡ node key ⟪ Black , value ⟫ left right
           →    (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl  ) )
             ∧  (color left  ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) )
rbi-case1 {n} {A} {key} parent repl rbtip rbtir x = ⟪ {!!} , {!!} ⟫

blackdepth≡ : {n : Level } {A : Set n} → {C : Color} {key key1 : ℕ} {value value1 : A} → (tree1 tree2 : bt (Color ∧ A))
  → RBtreeInvariant tree1
  → RBtreeInvariant tree2
  → RBtreeInvariant (node key ⟪ C , value ⟫ tree1 tree2)
  → black-depth tree1 ≡ black-depth tree2
blackdepth≡ leaf leaf ri1 ri2 rip = refl 
blackdepth≡ {n} {A}  leaf (node key .(⟪ Black , _ ⟫) t2 t3) ri1 ri2 (rb-right-red x x₁ rip) =  DepthCal (black-depth {n} {A} leaf) (black-depth (node key ⟪ Black , _ ⟫ t2 t3)) 0
blackdepth≡ {n} {A} leaf (node key .(⟪ _ , _ ⟫) t2 t3) ri1 ri2 (rb-right-black x x₁ rip) =  DepthCal (black-depth {n} {A} leaf) (black-depth (node key ⟪ _ , _ ⟫ t2 t3) ) (black-depth (node key ⟪ _ , _ ⟫ t2 t3) ) 
blackdepth≡ {n} {A} (node key .(⟪ Black , _ ⟫) t1 t3) leaf ri1 ri2 (rb-left-red x x₁ rip) =  DepthCal (black-depth (node key ⟪ Black , _ ⟫ t1 t3))  (black-depth {n} {A} leaf)  0
blackdepth≡ {n} {A} (node key .(⟪ _ , _ ⟫) t1 t3) leaf ri1 ri2 (rb-left-black x x₁ rip) = DepthCal (black-depth (node key ⟪ _ , _ ⟫ t1 t3)) (black-depth {n} {A} leaf) 0
blackdepth≡ (node key .(⟪ Black , _ ⟫) t1 t3) (node key₁ .(⟪ Black , _ ⟫) t2 t4) ri1 ri2 (rb-node-red x x₁ x₂ rip x₃ rip₁) = DepthCal (black-depth  (node key ⟪ Black , _ ⟫ t1 t3)) (black-depth (node key₁ ⟪ Black , _ ⟫ t2 t4)) 0
blackdepth≡ (node key .(⟪ _ , _ ⟫) t1 t3) (node key₁ .(⟪ _ , _ ⟫) t2 t4) ri1 ri2 (rb-node-black x x₁ x₂ rip x₃ rip₁) = DepthCal (black-depth (node key ⟪ _ , _ ⟫ t1 t3)) ( black-depth (node key₁ ⟪ _ , _ ⟫ t2 t4))  (black-depth (node key₁ (⟪ _ , _ ⟫) t2 t4))

rb08 : {n : Level } {A : Set n}{key key1 : ℕ} {value value1 : A} {c c1 : Color} {t₁ t₂ t₃ t₄ : bt (Color ∧ A)}
 →  black-depth (node key ⟪ c , value ⟫ t₁ t₂) ≡ black-depth (node key1 ⟪ c1 , value1 ⟫ t₃ t₄)
rb08 = {!!}

{-
rbi-case1 : {n : Level} {A : Set n} → {key : ℕ} → {value : A} → (parent repl : bt (Color ∧ A) )                        
           → RBtreeInvariant parent                    
           → RBtreeInvariant repl                                                                                                 → (left right : bt (Color ∧ A)) → parent ≡ node key ⟪ Black , value ⟫ left right
           → RBtreeInvariant left
           → RBtreeInvariant right
           →    (color right ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ left repl  ) )                                                          ∧  (color left  ≡ Red → RBtreeInvariant (node key ⟪ Black , value ⟫ repl right ) )
           
rbi-case1 {n} {A} {key} (node key1 ⟪ Black , value1 ⟫ l r) leaf rbip rbir (node key3 ⟪ Red , val3 ⟫ la ra) (node key4-- ⟪ Red , val4 ⟫ lb rb) pa li ri = {!!}
-}

-}