module hoareBinaryTree where

open import Level renaming (zero to Z ; suc to succ)

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


SingleLinkedStack = List

emptySingleLinkedStack :  {n : Level } {Data : Set n} -> SingleLinkedStack Data
emptySingleLinkedStack = []

clearSingleLinkedStack : {n m : Level } {Data : Set n} {t : Set m} -> SingleLinkedStack Data  → ( SingleLinkedStack Data → t) → t
clearSingleLinkedStack [] cg = cg []
clearSingleLinkedStack (x ∷ as) cg = cg []

pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> List Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
pushSingleLinkedStack stack datum next = next ( datum ∷ stack )


popSingleLinkedStack : {n m : Level } {t : Set m } {a  : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
popSingleLinkedStack [] cs = cs [] nothing
popSingleLinkedStack (data1 ∷ s)  cs = cs s (just data1)



emptySigmaStack : {n : Level } { Data : Set n} → List Data
emptySigmaStack = []

pushSigmaStack : {n m : Level} {d d2 : Set n} {t : Set m} → d2 → List d  → (List (d × d2) → t) → t
pushSigmaStack {n} {m} {d} d2 st next = next (Data.List.zip (st) (d2 ∷ []) )

tt = pushSigmaStack 3 (true ∷ []) (λ st → st)

_iso_ : {n : Level} {a : Set n} → ℕ → ℕ → Set
d iso d' = (¬ (suc d ≤ d')) ∧ (¬ (suc d' ≤ d))

iso-intro : {n : Level} {a : Set n} {x y : ℕ} → ¬ (suc x ≤ y) → ¬ (suc y ≤ x) → _iso_ {n} {a} x y
iso-intro = λ z z₁ → record { proj1 = z ; proj2 = z₁ }


{--
  data A B : C → D → Set where の A B と C → D の差は？
  
 --}

data bt {n : Level} {a : Set n} : Set n where --  (a : Setn)
  bt-leaf : ⦃ l u : ℕ ⦄ → l ≤ u → bt
  bt-node : ⦃ l l' u u' : ℕ ⦄ → (d : ℕ) →
             bt {n} {a}  → bt {n} {a} → l ≤ l' → u' ≤ u → bt 

--
--
--  no children , having left node , having right node , having both
--
data bt' {n : Level} (A : Set n) : (key : ℕ) →  Set n where --  (a : Setn)
  bt'-leaf : (key : ℕ) → bt' A key
  bt'-node : { l r : ℕ } → (key : ℕ) → (value : A) →
             bt' {n} A l  → bt' {n} A r → l ≤ key → key ≤ r → bt' A key

data bt'-path {n : Level} (A : Set n) : Set n where --  (a : Setn)
  bt'-left  : (key : ℕ) → {left-key : ℕ} → (bt' A left-key ) → (key ≤ left-key) → bt'-path A
  bt'-right : (key : ℕ) → {right-key : ℕ} → (bt' A right-key ) → (right-key ≤ key) → bt'-path A


test = bt'-left {Z} {ℕ} 3 {5} (bt'-leaf 5) (s≤s (s≤s (s≤s {!!})))

bt-find' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (tree : bt' A tn ) → List (bt'-path A )
    → ( {key1 : ℕ } → bt' A  key1 → List (bt'-path A ) → t ) → t
bt-find' key tr@(bt'-leaf key₁) stack next = next tr stack  -- no key found
bt-find' key (bt'-node key₁ value tree tree₁ x x₁) stack next with <-cmp key key₁
bt-find' key tr@(bt'-node {l} {r} key₁ value tree tree₁ x x₁) stack next | tri< a ¬b ¬c =
         bt-find' key tree ( (bt'-left key {key₁} tr {!!} )  ∷ stack)  next
bt-find' key found@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri≈ ¬a b ¬c = next found stack
bt-find' key tr@(bt'-node key₁ value tree tree₁ x x₁) stack next | tri> ¬a ¬b c = 
         bt-find' key tree ( (bt'-right key {key₁} tr {!!} )  ∷ stack)  next

a<sa : { a : ℕ } → a < suc a
a<sa {zero} = s≤s z≤n
a<sa {suc a} = s≤s a<sa 

pa<a : { a : ℕ } → pred (suc a) < suc a
pa<a {zero} = s≤s z≤n
pa<a {suc a} = s≤s pa<a

bt-replace' : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (key : ℕ) → (value : A ) → (tree : bt' A tn ) → List (bt'-path A )
    → ( {key1 : ℕ } → bt' A  key1 → t ) → t
bt-replace' {n} {m} {A} {t} {tn} key value node stack next = bt-replace1 tn node where
         bt-replace0 : {tn : ℕ } (node : bt' A tn ) → List (bt'-path A ) → t
         bt-replace0 node [] = next node 
         bt-replace0 node (bt'-left key x x₁ ∷ stack) = {!!}
         bt-replace0 node (bt'-right key x x₁ ∷ stack) = {!!}
         bt-replace1 : (tn : ℕ ) (tree : bt' A tn ) → t
         bt-replace1 tn (bt'-leaf key0) = bt-replace0 (bt'-node tn value
              (bt'-leaf (pred tn)) (bt'-leaf (suc tn) ){!!} {!!}) stack
         bt-replace1 tn (bt'-node key value node node₁ x x₁) = bt-replace0 (bt'-node key value node node₁ x x₁) stack

bt-find'-assert1 : {n m : Level} {A : Set n} {t : Set m} → Set n
bt-find'-assert1 {n} {m} {A} {t} = (key : ℕ) →  (val : A) → bt-find' key {!!} {!!} (λ tree stack → {!!})


-- find'-support : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → (d : ℕ) → (tree : bt' {n} {a} ) → SingleLinkedStack (bt' {n} {a} ) → ( (bt' {n} {a} ) → SingleLinkedStack (bt' {n} {a} ) → Maybe (Σ ℕ (λ d' → _iso_  {n} {a} d d')) → t ) → t

-- find'-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key leaf@(bt'-leaf x) st cg = cg leaf st nothing
-- find'-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt'-node d tree₁ tree₂ x x₁) st cg with <-cmp key d
-- find'-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt'-node d tree₁ tree₂ x x₁) st cg | tri≈ ¬a b ¬c = cg node st (just (d , iso-intro {n} {a} ¬a ¬c))

-- find'-support {n} {m} {a} {t}  key node@(bt'-node ⦃ nl ⦄ ⦃ l' ⦄ ⦃ nu ⦄ ⦃ u' ⦄ d L R x x₁) st cg | tri< a₁ ¬b ¬c =
--                          pushSingleLinkedStack st node
--                          (λ st2 → find'-support {n} {m} {a} {t} {{l'}} {{d}} key L st2 cg)

-- find'-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt'-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d L R x x₁) st cg | tri> ¬a ¬b c = pushSingleLinkedStack st node
--                          (λ st2 → find'-support {n} {m} {a} {t} {{d}} {{lr'}} key R st2 cg)



lleaf : {n : Level} {a : Set n} → bt {n} {a} 
lleaf = (bt-leaf ⦃ 0 ⦄ ⦃ 3 ⦄ z≤n)

lleaf1 : {n : Level} {A : Set n} → (0 < 3)  → (a : A) → (d : ℕ ) → bt' {n} A d
lleaf1 0<3 a d = bt'-leaf d

test-node1 : bt' ℕ 3
test-node1 = bt'-node (3) 3 (bt'-leaf 2) (bt'-leaf 4) (s≤s (s≤s {!!})) (s≤s (s≤s (s≤s {!!})))


rleaf : {n : Level} {a : Set n} → bt {n} {a} 
rleaf = (bt-leaf ⦃ 3 ⦄ ⦃ 3 ⦄ (s≤s (s≤s (s≤s z≤n))))

test-node : {n : Level} {a : Set n} → bt {n} {a} 
test-node {n} {a} = (bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ 4 ⦄ ⦃ 4 ⦄ 3 lleaf rleaf z≤n ≤-refl )

-- stt : {n m : Level} {a : Set n} {t : Set m} → {!!}
-- stt {n} {m} {a} {t} = pushSingleLinkedStack  [] (test-node ) (λ st → pushSingleLinkedStack st lleaf (λ st2 → st2) )



-- search の {{ l }} {{ u }} はその時みている node の 大小。 l が小さく u が大きい
-- ここでは d が現在の node のkey値なので比較後のsearch では値が変わる
bt-search : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → bt {n} {a} → (Maybe (Σ ℕ (λ d' → _iso_  {n} {a} d d')) → t ) → t
bt-search {n} {m} {a} {t} key (bt-leaf x) cg = cg nothing
bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg with <-cmp key d
bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri< a₁ ¬b ¬c =  bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg
bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c))
bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ ll ⦄ ⦃ l' ⦄ ⦃ uu ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg

-- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri< a₁ ¬b ¬c = ? -- bt-search ⦃ l' ⦄ ⦃ d ⦄ key L cg
-- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d L R x x₁) cg | tri≈ ¬a b ¬c = cg (just (d , iso-intro {n} {a} ¬a ¬c))
-- bt-search {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node ⦃ l ⦄ ⦃ l' ⦄ ⦃ u ⦄ ⦃ u' ⦄ d L R x x₁) cg | tri> ¬a ¬b c = bt-search ⦃ d ⦄ ⦃ u' ⦄ key R cg


-- この辺の test を書くときは型を考えるのがやや面倒なので先に動作を書いてから型を ? から補間するとよさそう
bt-search-test : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (x : (x₁ : Maybe (Σ ℕ (λ z → ((x₂ : 4 ≤ z) → ⊥) ∧ ((x₂ : suc z ≤ 3) → ⊥)))) → t) → t
bt-search-test {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 3 test-node

bt-search-test-bad : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (x : (x₁ : Maybe (Σ ℕ (λ z → ((x₂ : 8 ≤ z) → ⊥) ∧ ((x₂ : suc z ≤ 7) → ⊥)))) → t) → t
bt-search-test-bad {n} {m} {a} {t} = bt-search {n} {m} {a} {t} ⦃ zero ⦄ ⦃ 4 ⦄ 7 test-node


-- up-some : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ {d : ℕ} → (Maybe (Σ ℕ (λ d' → _iso_  {n} {a} d d'))) → (Maybe ℕ)
-- up-some (just (fst , snd)) = just fst
-- up-some nothing = nothing

search-lem : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (key : ℕ) → (tree : bt {n} {a} ) → bt-search ⦃ l ⦄ ⦃ u ⦄ key tree (λ gdata → gdata ≡ gdata)
search-lem {n} {m} {a} {t} key (bt-leaf x) = refl
search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) with <-cmp key d
search-lem {n} {m} {a} {t} key (bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri< lt ¬eq ¬gt = search-lem {n} {m} {a} {t} ⦃ ll' ⦄ ⦃ d ⦄  key tree₁
search-lem {n} {m} {a} {t} key (bt-node d tree₁ tree₂ x x₁) | tri≈ ¬lt eq ¬gt = refl
search-lem {n} {m} {a} {t} key (bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d tree₁ tree₂ x x₁) | tri> ¬lt ¬eq gt = search-lem {n} {m} {a} {t} ⦃ d ⦄ ⦃ lr' ⦄  key tree₂


-- bt-find 
find-support : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → (d : ℕ) → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → Maybe (Σ ℕ (λ d' → _iso_  {n} {a} d d')) → t ) → t

find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key leaf@(bt-leaf x) st cg = cg leaf st nothing
find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key (bt-node d tree₁ tree₂ x x₁) st cg with <-cmp key d
find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt-node d tree₁ tree₂ x x₁) st cg | tri≈ ¬a b ¬c = cg node st (just (d , iso-intro {n} {a} ¬a ¬c))

find-support {n} {m} {a} {t}  key node@(bt-node ⦃ nl ⦄ ⦃ l' ⦄ ⦃ nu ⦄ ⦃ u' ⦄ d L R x x₁) st cg | tri< a₁ ¬b ¬c =
                         pushSingleLinkedStack st node
                         (λ st2 → find-support {n} {m} {a} {t} {{l'}} {{d}} key L st2 cg)

find-support {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key node@(bt-node ⦃ ll ⦄ ⦃ ll' ⦄ ⦃ lr ⦄ ⦃ lr' ⦄ d L R x x₁) st cg | tri> ¬a ¬b c = pushSingleLinkedStack st node
                         (λ st2 → find-support {n} {m} {a} {t} {{d}} {{lr'}} key R st2 cg)

bt-find : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → (d : ℕ) → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → Maybe (Σ ℕ (λ d' → _iso_  {n} {a} d d')) → t ) → t
bt-find {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ key tr st cg = clearSingleLinkedStack st
                              (λ cst → find-support ⦃ l ⦄  ⦃ u ⦄ key tr cst cg)

find-test : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → List bt -- ?
find-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ = bt-find {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 3 test-node [] (λ tt st ad → st)
{-- result
    λ {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ →
    bt-node 3 (bt-leaf z≤n) (bt-leaf (s≤s (s≤s (s≤s z≤n)))) z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) ∷ []
--}

find-lem : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → (d : ℕ) → (tree : bt {n} {a}) → (st : List (bt {n} {a})) → find-support {{l}} {{u}} d tree st (λ ta st ad → ta ≡ ta)
find-lem d (bt-leaf x) st = refl
find-lem d (bt-node d₁ tree tree₁ x x₁) st with <-cmp d d₁
find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri≈ ¬a b ¬c = refl


find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c with  tri< a ¬b ¬c
find-lem {n} {m} {a} {t} {{l}} {{u}} d (bt-node d₁ tree tree₁ x x₁) st | tri< lt ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = find-lem {n} {m} {a} {t} {{l}} {{u}} d tree {!!}
find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = {!!}
find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = {!!}

find-lem d (bt-node d₁ tree tree₁ x x₁) st | tri> ¬a ¬b c = {!!}

bt-singleton :{n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → (d : ℕ) → ( (bt {n} {a} ) → t ) → t
bt-singleton {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d cg = cg (bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (bt-leaf ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (bt-leaf  ⦃ d ⦄  ⦃ d ⦄ ≤-refl) z≤n ≤-refl)


singleton-test : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → bt -- ?
singleton-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄  = bt-singleton {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 10 λ x → x


replace-helper : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → (tree : bt {n} {a} ) → SingleLinkedStack (bt {n} {a} ) → ( (bt {n} {a} ) → t ) → t
replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree [] cg = cg tree
replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree@(bt-node d L R x₁ x₂) (bt-leaf x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg  -- Unknown Case
replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ (bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg with <-cmp d d₁
replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg | tri< a₁ ¬b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ subt x₃ x₄ x₅) st cg
replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg | tri≈ ¬a b ¬c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ subt x₃ x₄ x₅) st cg
replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ subt@(bt-node d tree tree₁ x₁ x₂) (bt-node d₁ x x₃ x₄ x₅ ∷ st) cg | tri> ¬a ¬b c = replace-helper ⦃ l ⦄ ⦃ u ⦄ (bt-node d₁ x₃ subt x₄ x₅) st cg
replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tree (x ∷ st) cg = replace-helper ⦃ l ⦄ ⦃ u ⦄ tree st cg  -- Unknown Case



bt-replace : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄
           → (d : ℕ) → (bt {n} {a} ) → SingleLinkedStack (bt {n} {a} )
           → Maybe (Σ ℕ (λ d' → _iso_  {n} {a} d d')) → ( (bt {n} {a} ) → t ) → t
bt-replace {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d tree st eqP cg = replace-helper {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ ((bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ d ⦄ ⦃ d ⦄ d (bt-leaf ⦃ 0 ⦄ ⦃ d ⦄ z≤n ) (bt-leaf  ⦃ d ⦄  ⦃ d ⦄ ≤-refl) z≤n ≤-refl)) st cg



-- 証明に insert がはいっててほしい
bt-insert : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (d : ℕ) → (tree : bt {n} {a})
            → ((bt {n} {a}) → t) → t

bt-insert {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ d tree cg = bt-find {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ d tree [] (λ tt st ad → bt-replace ⦃ l ⦄ ⦃ u ⦄ d tt st ad cg )

pickKey : {n m : Level} {a : Set n} {t : Set m} ⦃ l u : ℕ ⦄ → (tree : bt {n} {a}) → Maybe ℕ
pickKey (bt-leaf x) = nothing
pickKey (bt-node d tree tree₁ x x₁) = just d

insert-test : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → bt -- ?
insert-test {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄  = bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 1 test-node λ x → x

insert-test-l : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → bt -- ?
insert-test-l {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄  = bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ 1 (lleaf) λ x → x


insert-lem : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → (d : ℕ) → (tree : bt {n} {a})
             → bt-insert {n} {_} {a} ⦃ l ⦄ ⦃ u ⦄ d tree (λ tree1 → bt-find ⦃ l ⦄ ⦃ u ⦄ d tree1 []
             (λ tt st ad → (pickKey {n} {m} {a} {t} ⦃ l ⦄ ⦃ u ⦄ tt)  ≡ just d ) )


insert-lem d (bt-leaf x) with <-cmp d d -- bt-insert d (bt-leaf x) (λ tree1 → {!!})
insert-lem d (bt-leaf x) | tri< a ¬b ¬c = ⊥-elim (¬b refl)
insert-lem d (bt-leaf x) | tri≈ ¬a b ¬c = refl
insert-lem d (bt-leaf x) | tri> ¬a ¬b c = ⊥-elim (¬b refl)
insert-lem d (bt-node d₁ tree tree₁ x x₁) with <-cmp d d₁
 -- bt-insert d (bt-node d₁ tree tree₁ x x₁) (λ tree1 → {!!})
insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c with <-cmp d d
insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl)
insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl
insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl)

insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri< a ¬b ¬c = {!!}
  where
    lem-helper : find-support ⦃ {!!} ⦄ ⦃ {!!} ⦄ d tree (bt-node d₁ tree tree₁ x x₁ ∷ [])  (λ tt₁ st ad → replace-helper ⦃ {!!} ⦄ ⦃ {!!} ⦄  (bt-node ⦃ {!!} ⦄ ⦃ {!!} ⦄ ⦃ {!!} ⦄ ⦃ {!!} ⦄  d (bt-leaf ⦃ 0 ⦄ ⦃ d ⦄ z≤n) (bt-leaf ⦃ {!!} ⦄ ⦃ {!!} ⦄  (≤-reflexive refl)) z≤n   (≤-reflexive refl))   st  (λ tree1 →   find-support ⦃ {!!} ⦄ ⦃ {!!} ⦄  d tree1 [] (λ tt₂ st₁ ad₁ → pickKey {{!!}} {{!!}} {{!!}} {{!!}} ⦃ {!!} ⦄ ⦃ {!!} ⦄  tt₂ ≡ just d)))
    lem-helper = {!!}

insert-lem d (bt-node d₁ tree tree₁ x x₁) | tri> ¬a ¬b c = {!!}