open import Level renaming (suc to succ ; zero to Zero )
module RBTree where

-- {
-- RBTree,
-- Node,
-- Color,
-- hight,
-- nulln,
-- empty,
-- singleton
-- }

open import Data.List
open import Data.Maybe
open import Data.Nat
open import Data.Bool
open import Data.Empty
open import Relation.Binary.PropositionalEquality
open import Relation.Binary
open import Relation.Binary.Core
open import Relation.Nullary
-- open import Level

-- Builtin Function

_==_ :  ℕ → ℕ → Bool
_==_ x y with compare x y
(x == .(ℕ.suc (x + k))) | less .x k = false
(x == .x) | equal .x = true
(.(ℕ.suc (y + k)) == y) | greater .y k = false

_-_ : ℕ → ℕ → ℕ
ℕ.zero - ℕ.zero = ℕ.zero
ℕ.zero - ℕ.suc y = ℕ.zero
ℕ.suc x - ℕ.zero = ℕ.suc x
ℕ.suc x - ℕ.suc y = x - y

contraposition : {m : Level } {A B : Set m} → (B → A) → (¬ A → ¬ B)
contraposition f = λ x y → x (f y)


compareTri1 : (n : ℕ) → zero <′ suc n
compareTri1 zero =   ≤′-refl
compareTri1 (suc n) =  ≤′-step ( compareTri1 n )

compareTri2 : (n m : ℕ) → n ≤′ m → suc n ≤′ suc m
compareTri2 _ _  ≤′-refl = ≤′-refl
compareTri2 n (suc m) ( ≤′-step p ) =  ≤′-step { suc n }  ( compareTri2 n m p )

<′dec : Set
<′dec = ∀ m n → Dec ( m ≤′ n )

compareTri6 : ∀ m {n} → ¬ m ≤′ n →  ¬ suc m ≤′ suc n

is≤′ :  <′dec
is≤′  zero zero = yes ≤′-refl
is≤′  zero (suc n) = yes (lemma n)
  where
     lemma :  (n : ℕ) → zero ≤′ suc n
     lemma zero =   ≤′-step  ≤′-refl
     lemma (suc n) =  ≤′-step (lemma n)
is≤′  (suc m) (zero) = no ( λ () )
is≤′  (suc m) (suc n) with is≤′ m n
... | yes p = yes ( compareTri2 _ _ p )
... | no p = no ( compareTri6 _ p )

compareTri20 : {n : ℕ} → ¬ suc n ≤′ zero
compareTri20 ()


compareTri21 : (n m : ℕ) → suc n ≤′ suc m →  n ≤′ m
compareTri21 _ _  ≤′-refl = ≤′-refl
compareTri21 (suc n) zero ( ≤′-step p ) = compareTri23 (suc n) ( ≤′-step p ) p
  where
        compareTri23 : (n : ℕ) → suc n ≤′ suc zero → suc n ≤′ zero →  n ≤′ zero
        compareTri23 zero ( ≤′-step p ) _ =   ≤′-refl
        compareTri23 zero ≤′-refl _ =   ≤′-refl
        compareTri23 (suc n1) ( ≤′-step p ) ()
compareTri21 n (suc m) ( ≤′-step p ) = ≤′-step (compareTri21 _ _ p)
compareTri21 zero zero ( ≤′-step p ) = ≤′-refl


compareTri3 : ∀ m {n} → ¬ m ≡ suc (m + n)
compareTri3 zero    ()
compareTri3 (suc m) eq = compareTri3 m (cong pred eq)

compareTri4' : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
compareTri4' m {n} with n Data.Nat.≟ m
... | yes refl  = λ x y → x refl
... | no  p  = λ x y → p ( cong pred y )

compareTri4 : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m
compareTri4 m = contraposition ( λ x → cong pred x )

-- compareTri6 : ∀ m {n} → ¬ m ≤′ n →  ¬ suc m ≤′ suc n
compareTri6  m {n} = λ x y → x (compareTri21 _ _ y)

compareTri5 : ∀ m {n} → ¬ m <′ n →  ¬ suc m <′ suc n
compareTri5  m {n}  = compareTri6 (suc m)


compareTri :  Trichotomous  _≡_ _<′_
compareTri zero zero = tri≈ ( λ ()) refl ( λ ())
compareTri zero (suc n) = tri< ( compareTri1 n )  ( λ ()) ( λ ())
compareTri (suc n) zero = tri> ( λ ()) ( λ ()) ( compareTri1 n )
compareTri (suc n) (suc m) with compareTri n m
... | tri< p q r = tri<  (compareTri2 (suc n) m p ) (compareTri4 _ q) ( compareTri5 _ r )
... | tri≈ p refl r = tri≈ (compareTri5 _ p) refl ( compareTri5 _ r )
... | tri> p q r = tri> ( compareTri5 _ p ) (compareTri4 _ q) (compareTri2 (suc m) n r )


data Color : Set where
  red : Color
  black : Color

record Node {a : Set} : Set where
  inductive
  field
    color : Color
    blackHeight : ℕ
    right : Node {a}
    datum : ℕ
    left : Node {a}
open Node

-- node は node であり 部分的に分けられた redblacktree そのもの

data RBTree {n : Level} (a : Set n) : Set n where
    leaf : RBTree a
    node : Color → ℕ → RBTree a → ℕ → RBTree a → RBTree a


record RBTreeBDel {n : Level} (a : Set n) : Set n where
  field
    tree : RBTree a
    bool : Bool
open RBTreeBDel


module _ { n m : Level} {a : Set n} {cg : Set m} where
  -- _,_ : (tree : RBTree a) → (b : Bool) → Set
  -- leaf , false = (leaf , false)
  -- leaf , true = {!!}
  -- (node x x₁ t x₂ t₁) , bb = {!!}


  hight? : RBTree a → ℕ
  hight? leaf = 0
  hight? (node c h l x r) = h

  isLeaf : RBTree a → Bool
  isLeaf leaf = true
  isLeaf (node x x₁ t x₂ t₁) = false

  empty : RBTree a
  empty = leaf

  singleton : ℕ → RBTree a
  singleton x = (node black 1 leaf x leaf)

  isMember : ℕ → RBTree ℕ → Bool
  isMember _ leaf = false
  isMember x (node _ _ l y r) with compare x y
  isMember x (node _ _ l y r) | less x k = isMember x l
  isMember x (node _ _ l x r) | equal x = true
  isMember x (node _ _ l y r) | greater y k = isMember x r

  blacks? : RBTree a → ℕ
  blacks? = blacks' 0
    where
      blacks' : ℕ → RBTree a → ℕ
      blacks' n leaf = (n + 1)
      blacks' n (node red _ l _ r) = (blacks' n l) + (blacks' n r)
      blacks' n (node black _ l _ r) = (blacks' (n + 1) l) + (blacks' (n + 1) r)

  reds : Color → RBTree a → Bool
  reds _ leaf = true
  reds red (node x x₁ t x₂ t₁) = false
  reds black (node c x₁ l x₂ r) = reds c l ∧ reds c r

  turnR : RBTree a → (RBTree a → cg) → cg
  turnR leaf  cg = cg leaf
  turnR (node _ h l x r) cg = cg (node red h l x r)

  turnB : RBTree a → (RBTree a → cg) → cg
  turnB leaf cg = cg leaf
  turnB (node _ h l x r) cg = cg (node black h l x r)

  minimum : RBTree ℕ → ℕ
  minimum (node c h leaf x r) = x
  minimum (node c h l x r) = minimum l
  minimum leaf = 774

  maximum : RBTree ℕ → ℕ
  maximum (node c x₁ t x leaf) = x
  maximum (node x x₁ t x₂ r) = maximum r
  maximum leaf = 0

  isRed : RBTree a → Bool
  isRed (node red x₁ t x₂ t₁) = true
  isRed _ = false

  isColorSame : Color → Color → (Bool → cg) → cg
  isColorSame red red cg = cg true
  isColorSame red black cg = cg false
  isColorSame black red cg = cg false
  isColorSame black black cg = cg true

  node→ℕ : Maybe (RBTree a) → Maybe ℕ
  node→ℕ (just leaf) = nothing
  node→ℕ (just (node x x₁ x₂ x₃ x₄)) = just x₃
  node→ℕ nothing = nothing


-- basic operations
-- Code Gear Style (CPS : Contination Passing Style)

-- balance




module _ { n m : Level} {a : Set n} {cg : Set m}  where

  balanceL' :  ℕ → RBTree a → ℕ → RBTree a → (RBTree a → cg) → cg
  balanceL' h (node red h1 (node red hl a x b) y c) z d cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
  balanceL' h (node red _ a x (node red _ b y c)) z d cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
  balanceL' h l x r cg = cg (node black h l x r)

  balanceR' : ℕ -> RBTree a -> ℕ -> RBTree a -> (RBTree a → cg) → cg
  balanceR' h a x (node red _ b y (node red _ c z d)) cg =  cg (node red (h + 1) (node black h a x b) y (node black h c z d))
  balanceR' h a x (node red _ (node red _ b y c) z d) cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
  balanceR' h l x r cg = cg (node black h l x r)

  balanceL : Color → ℕ → RBTree a → ℕ → RBTree a → (RBTree a → cg) → cg
  balanceL black h (node red h1 (node red hl a x b) y c) z d cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
  balanceL black h (node red _ a x (node red _ b y c)) z d cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
  balanceL k h l x r cg = cg (node k h l x r)

  balanceR : Color → ℕ -> RBTree a -> ℕ -> RBTree a -> (RBTree a → cg) → cg
  balanceR black h a x (node red _ b y (node red _ c z d)) cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
  balanceR black h a x (node red _ (node red _ b y c) z d) cg = cg (node red (h + 1) (node black h a x b) y (node black h c z d))
  balanceR k h l x r cg = cg (node k h l x r)

-- unbalance

  -- unbalanceL' : Color → ℕ -> RBTree a -> a -> RBTree a -> (RBTreeBDel a → cg) → cg
  -- unbalanceL' c h l@(node black _ _ _ _) x r cg = isColorSame c black ( λ issame → cg record { tree = {!!} ; bool = issame })
  -- unbalanceL' c h l x r cg = {!!}

  unbalanceL : Color → ℕ → RBTree a → ℕ → RBTree a → (RBTreeBDel a → cg) → cg
  unbalanceL c h l@(node black _ _ _ _) x r cg = turnR l (λ tl → (balanceL black h tl x r (λ t → isColorSame {n} {m} {a} {_} c black (λ issame → cg record {tree = t ; bool = issame}))))
  unbalanceL black h l@(node red lh ll lx lr@(node black _ _ _ _)) x r  cg = turnR lr (λ tlr → balanceL black h tlr x r (λ t → cg record { tree = (node black lh ll lx t) ; bool = false}))
  unbalanceL c h l x r  cg = cg record {tree = leaf ; bool = false}

  unbalanceR : Color → ℕ → RBTree a → ℕ → RBTree a → (RBTreeBDel a → cg) → cg
  unbalanceR c h l x r@(node black _ _ _ _) cg = turnR r (λ tr → balanceR black h l x r (λ t → isColorSame {n} {m} {a} {_} c black (λ issame → cg record {tree = t ; bool = issame})))
  unbalanceR black h l x (node red rh rl@(node black _ _ _ _) rx rr) cg = turnR rl (λ trl → balanceR black h l x trl (λ t → cg record { tree = (node black rh t rx rr); bool = false}))
  unbalanceR c h l x r cg  = cg record {tree = leaf ; bool = false}



{--
  Insert Function

    All Nodes → ℕ
    search Insert Location → O(log ℕ)
    fix Tree (balanceR,L)  → O(log ℕ)
    Root Child Color Fix   → O(1)
    Total → O(2 log ℕ + 1)
--}

  -- turnRtree : RBTree a → (RBTree a → cg) → cg
  -- turnRtree leaf cg = cg leaf
  -- -- turnRtree (node black h l@(node black _ _ _ _) x r@(node black _ _ _ _)) cg = turnRtree (node red h l x r) cg
  -- turnRtree (node c h l x r) cg = turnRtree r cg

  rootChildFix : RBTree a → (RBTree a → cg) → cg
  rootChildFix (node black h (node black lh ll@(node black llh lll llx llr) lx lr@(node black lrh lrl lrx lrr)) x (node black rh rl@(node black rlh rll rlx rlr) rx rr@(node black rrh rrl rrx rrr))) cg = cg (node black (h - 1) (node red (lh - 1) ll lx lr) x (node red (rh - 1) rl rx rr))
  rootChildFix n cg = cg n

  insert' : ℕ → RBTree a → (RBTree a → cg) → cg
  insert' kx leaf cg = cg (node red 1 leaf kx leaf)

  insert' kx (node black h l x r) cg with compare kx x
  insert' kx (node black h l x r) cg | less kx k = insert' kx l (λ t → balanceL' h t x r (λ tt → cg tt))
  insert' kx s@(node black h l x r) cg | equal kx = cg s
  insert' kx (node black h l x r) cg | greater x k = insert' kx r (λ t → balanceR' h l x t (λ tt → cg tt))

  insert' kx (node red h l x r) cg with compare kx x
  insert' kx (node red h l x r) cg | less kx k = insert' kx l (λ t → cg (node red h t x r))
  insert' kx s@(node red h l x r) cg | equal kx = cg s
  insert' kx (node red h l x r) cg | greater x k = insert' kx r (λ t → cg (node red h l x t))

  insert : ℕ → RBTree a → (RBTree a → cg) → cg
  insert kx t cg = insert' kx t (λ t1 → turnB t1 (λ t2 → rootChildFix t2 cg))


  get : ℕ → RBTree a → (Maybe (RBTree a) → cg) → cg
  get x leaf cg = cg nothing
  get x (node c h l x1 r) cg with compareTri x x1
  get x (node c h l x1 r) cg | tri< a ¬b ¬c = get x l cg
  get x t@(node c h l x1 r) cg | tri≈ ¬a b ¬c = cg (just t)
  get x (node c h l x1 r) cg | tri> ¬a ¬b c₁ = get x r cg



{- Check Balance, Color rule and hight calc -}

-- create RBTree from Nat List
fromList : List ℕ → RBTree ℕ
fromList [] = empty {_} {_} {ℕ} {Set}
fromList (x ∷ l) = (maketree x (empty {_} {_} {ℕ} {Set}) (λ t → fromList' l t (λ tt → tt)))
  where
    module _  {l : Level} {cg1 : Set l} {a : Set} where
      maketree : ℕ → RBTree a → (RBTree a → cg1) → cg1
      maketree x t1 cg = insert x t1 cg
      fromList' : List ℕ → RBTree a → (RBTree a → cg1) → cg1
      fromList' [] t cg = cg t
      fromList' (x1 ∷ nl) t cg = maketree x1 t (λ tt → fromList' nl tt (λ ttt → cg ttt))


c1 = fromList (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ 8 ∷ 9 ∷ [])
c2 = fromList (5 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 6 ∷ 7 ∷ 8 ∷ 9 ∷ [])
c3 = fromList (8 ∷ 7 ∷ 6 ∷ 1 ∷ 2 ∷ 5 ∷ 4 ∷ 3 ∷ 9 ∷ [])

cget = get 6 c1 (λ a → a)


proof-leaf : {l : Level} {D : Set l} (n : ℕ) → insert {_} {_} {ℕ} {Set} n leaf (λ t1 → get n t1 (λ n1 → (just n ≡ (node→ℕ {_} {_} {ℕ} {ℕ} n1))))
proof-leaf n with n Data.Nat.≟ n | compareTri n n
proof-leaf n | yes p | tri< a ¬b ¬c = ⊥-elim (¬b p)
proof-leaf n | yes p | tri≈ ¬a b ¬c = refl
proof-leaf n | yes p | tri> ¬a ¬b c = ⊥-elim (¬b p)
proof-leaf n | no ¬p | tri< a ¬b ¬c = ⊥-elim (¬c a)
proof-leaf n | no ¬p | tri≈ ¬a b ¬c = refl
proof-leaf n | no ¬p | tri> ¬a ¬b c = ⊥-elim (¬a c)




-- 任意の木だと insert でノードをどこに入れるか決められず計算が進まない
-- 任意の木の root が Nothing のケースはもちろんできる
-- proof1 : {l : Level} {D : Set l} (n : ℕ) → (t : RBTree D) → insert n t (λ t1 → get n t1 (λ n1 → (just n ≡ (root→ℕ n1))))
-- proof1 n t with n Data.Nat.≟ n | compareTri n n
-- proof1 n t | yes p | tri< a ¬b ¬c = ⊥-elim (¬b p)
-- proof1 n t | yes p | tri> ¬a ¬b c = ⊥-elim (¬b p)
-- proof1 n t | no ¬p | tri< a ¬b ¬c = ⊥-elim (¬c a)
-- proof1 n t | no ¬p | tri> ¬a ¬b c = ⊥-elim (¬a c)
-- proof1 n leaf | yes p | tri≈ ¬a b ¬c with compareTri n n
-- proof1 n leaf | yes p | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b p)
-- proof1 n leaf | yes p | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl
-- proof1 n leaf | yes p | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b p)
-- proof1 n (node x x₁ t x₂ t₁) | yes p | tri≈ ¬a b ¬c = {!!}
-- proof1 n t | no ¬p | tri≈ ¬a b ¬c = {!!}


{--
書くなら全ての探索が木の高さ分で終わることを証明しとく必要がありそう
あと探索で木の高さが消化されていくことも示す
stack の push は存在してるデータ構造に関係なく上に乗るから任意のstack で証明できる
Tree でデータの保存を確かめるには…？

tree で証明するくらいだったら、親子関係、
rb 含めると、色関係、枝の長さ、になりそう?
--}

module _ { n m : Level} {a : Set n} {cg : Set m}  where

{--
deleteMin' は後ろに bool(Color の変更情報?)を持ちながら再帰する
再帰に一つ関数が挟まってるけど互いに呼んでるからどう書くべきかわからん

```Haskell Source
deleteMin' (Node c h l x r)               = if d then (tD, m) else (tD', m)

((l', d), m) = deleteMin' l
tD  = unbalancedR c (h-1) l' x r
tD' = (Node c h l' x r, False)
```

たぶん ((l', d), m) の形になると deleteMin' がしたい
~~RBTreeBDel の bool 情報はleaf に着いたかどうかだけ~~ → ではなく unbalance する必要があるのかの確認

ん、じゃあ node の左に leaf がついてる最小パターン探せばいいのでは？

あるパターンは (leaf x leaf), (leaf x r) の2パターンと r が red のケースを含めて 3パターン
その上のノードからそれを確認すれば良いので
(node c h (node lc lh leaf lx leaf) x r) と lr が存在するケースを確認すると良い
終わった tree に対して unbalance するかしないかを確定させたら終わり
--}



  {-# TERMINATING #-}
  deleteMin' : RBTree ℕ → (RBTreeBDel ℕ → cg) → cg

  deleteMin' leaf cg = cg record {tree = leaf ; bool = false} -- unreachable case
  deleteMin' (node black _ leaf x leaf) cg = cg record {tree = leaf ; bool = true}
  deleteMin' (node black _ leaf x r@(node red _ _ _ _)) cg = turnB r (λ tr → cg record {tree = tr ; bool = false})
  deleteMin' (node red _ leaf x r) cg = cg record {tree = r ; bool = false}
  deleteMin' (node c h l x r) cg = deleteMin' l (λ dt → delCheck {n} {m} {a} dt (λ dct → cg dct))
    where
      delCheck : { n m : Level} {a : Set n} {cg : Set m} → RBTreeBDel ℕ → (RBTreeBDel ℕ → cg) → cg
      delCheck bt cg with (bool bt)
      delCheck record { tree = leaf ; bool = b } cg | false = cg record {tree = (node red 100 leaf 100 leaf) ; bool = b } -- unreachable case
      delCheck record { tree = leaf ; bool = b } cg | true = unbalanceR c (h - 1) leaf x r (λ result → cg result)
      -- delCheck record { tree = (node x₁ x₂ t₁ x₃ t₂) ; bool = b } cg | false = cg record {tree = (node x₁ x₂ t₁ x₃ t₂) ; bool = false}
      delCheck record { tree = (node x₁ x₂ t₁ x₃ t₂) ; bool = b } cg | _ = unbalanceR c (h - 1) (node x₁ x₂ t₁ x₃ t₂) x r (λ result → cg result)

{--
deleteMin では最後に帰ってきたやつを turnB
型は rbtree → (rbtree → cg) → cg

rbtree が tree のとき deleteMin' tree
((s, _), _) は RBTreeBDel から RBTree への変換なので outPutTree
--}

  deleteMin : RBTree ℕ → (RBTree ℕ → cg) → cg
  deleteMin leaf cg = cg leaf
  deleteMin tree cg = deleteMin' tree (λ dt → outPutTree {n} {m} {a} dt (λ dct → turnB dct (λ dctb → cg dctb)))
    where
      outPutTree : { n m : Level} {a : Set n} {cg : Set m} → RBTreeBDel ℕ → (RBTree ℕ → cg) → cg
      outPutTree record { tree = s ; bool = b } cg = cg s


  -- > delCheck の node があって false のケースも unbalanceしなきゃいけなかった
  d1 = deleteMin (fromList (3 ∷ 1 ∷ 2 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ []))
  l1 = fromList (1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ [])
  l2 = fromList ( 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ [])
  d2 = deleteMin (fromList ( 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ []))


-- delete' : {a : Set} → ℕ → RBTree ℕ → RBTreeBDel ℕ
-- delete' _ leaf = record { t = leaf ; b = false}
-- delete' x (node c h l y r) with compare x y
-- delete' x (node c h l y r) | less .x k = delCheck (delete' {ℕ} x l)
--   where
--     delCheck : RBTreeBDel ℕ → RBTreeBDel ℕ
--     delCheck bt with (b bt)
--     delCheck record { t = leaf ; b = b } | false = record {t = (node red 100 leaf 100 leaf) ; b = b } -- unreachable case
--     delCheck record { t = leaf ; b = b } | true = unbalanceR {ℕ} c (h - 1) leaf x r
--     delCheck record { t = (node x₁ x₂ t₁ x₃ t₂) ; b = b } | false = deleteMin' (node x₁ x₂ t₁ x₃ t₂)
--     delCheck record { t = (node x₁ (x₂) t₁ x₃ t₂) ; b = b } | true = unbalanceR {ℕ} c (h - 1) (node x₁ x₂ t₁ x₃ t₂) x r
-- delete' x (node c h l y r) | greater .y k = delCheck (delete' {ℕ} x r)
--   where
--     delCheck : RBTreeBDel ℕ → RBTreeBDel ℕ
--     delCheck bt with (b bt)
--     delCheck record { t = leaf ; b = b } | false = record {t = (node red 100 leaf 100 leaf) ; b = b } -- unreachable case
--     delCheck record { t = leaf ; b = b } | true = unbalanceR {ℕ} c (h - 1) leaf x r
--     delCheck record { t = (node x₁ x₂ t₁ x₃ t₂) ; b = b } | false = deleteMin' (node x₁ x₂ t₁ x₃ t₂)
--     delCheck record { t = (node x₁ (x₂) t₁ x₃ t₂) ; b = b } | true = unbalanceR {ℕ} c (h - 1) (node x₁ x₂ t₁ x₃ t₂) x r
-- delete' x (node c h l .x leaf) | equal .x with checkColor {ℕ} c black
-- delete' x (node c h l .x leaf) | equal .x | false = record {t = l ; b = false}
-- delete' x (node c h l .x leaf) | equal .x | true = blackify l
--   where
--     blackify : RBTree ℕ → RBTreeBDel ℕ
--     blackify (node red x₂ a x₃ a₁) = record {t = turnB {ℕ} (node red x₂ a x₃ a₁) ; b = false}
--     blackify s = record {t = s; b = true}
-- delete' x (node c h l .x (node x₁ x₂ r x₃ r₁)) | equal .x with r
-- delete' x (node c h l .x (node x₁ x₂ r x₃ r₁)) | equal .x | leaf with checkColor {ℕ} c black
-- delete' x (node c h l .x (node x₁ x₂ r x₃ r₁)) | equal .x | leaf | false = blackify l
--   where
--     blackify : RBTree ℕ → RBTreeBDel ℕ
--     blackify (node red x₂ a x₃ a₁) = record {t = turnB {ℕ} (node red x₂ a x₃ a₁) ; b = false}
--     blackify s = record {t = s; b = true}
-- delete' x (node c h l .x (node x₁ x₂ r x₃ r₁)) | equal .x | leaf | true = record {t = l ; b = false}
-- delete' x (node c h l .x (node x₁ x₂ r x₃ r₁)) | equal .x | node x₄ x₅ rnod x₆ rnod₁ = {!!}

--   -- where
--   -- delCheck : RBTreeBDel ℕ → RBTreeBDel ℕ
--   -- delCheck bt with (b bt)
--   -- delCheck record { t = leaf ; b = b } | false = record {t = (node red 100 leaf 100 leaf) ; b = b } -- unreachable case
--   -- delCheck record { t = leaf ; b = b } | true = unbalanceR {ℕ} c (h - 1) leaf x r
--   -- delCheck record { t = (node x₁ x₂ t₁ x₃ t₂) ; b = b } | false = deleteMin' (node x₁ x₂ t₁ x₃ t₂)
--   -- delCheck record { t = (node x₁ (x₂) t₁ x₃ t₂) ; b = b } | true = unbalanceR {ℕ} c (h - 1) (node x₁ x₂ t₁ x₃ t₂) x r
-- -- 謎フラグがtrue なら バランスしろとのお達しなのでどっかで持ちましょうはい。
-- -- 多分 record で適当に持つのがよいっぽい

-- delete : {a : Set} → ℕ → RBTree ℕ → RBTree ℕ
-- delete kx t = turnB {ℕ} (outPutTree (delete' {ℕ} kx t))
--   where
--     outPutTree : RBTreeBDel ℕ → RBTree ℕ
--     outPutTree record { t = s ; b = b } = s

-- proofs
-- isOrdered : RBTree a → Bool
-- isOrdered t = {!!}

-- isBlackSame : RBTree a → Bool
-- isBlackSame t = {!!}

-- isBalanced : RBTree a → Bool
-- isBalanced t = {!!}