Mercurial > hg > Gears > GearsAgda

view work.agda @ 794:2a07b50f4bc0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 23 Oct 2023 19:29:43 +0900
parents 12e19644535e
children 6f27c2c18035
line wrap: on
line source

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

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

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

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

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


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 : ℕ} {value : 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≡ leaf (node key value t2 t3) ri1 ri2 rip = {!!} --rip kara mitibiki daseru  RBinvariant kara toreruka
blackdepth≡ (node key value t1 t3) leaf ri1 ri2 rip = {!!}
blackdepth≡ (node key value t1 t3) (node key₁ value₁ t2 t4) ri1 ri2 rip = {!!}


{-
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 = {!!}
-}