--- a/hoareBinaryTree.agda	Wed Dec 04 15:42:47 2019 +0900
+++ b/hoareBinaryTree.agda	Thu Dec 05 18:11:22 2019 +0900
@@ -30,26 +30,42 @@
 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)
 
 
 
-data bt {n : Level} {a : Set n} : ℕ → ℕ → Set n where
-  bt-leaf : ⦃ l u : ℕ ⦄ → l ≤ u → bt l u
+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)
+
+{--
+  data A B : C → D → Set where の A B と C → D の差は？
+  
+ --}
+data bt {n : Level} {a : Set n} : Set n where
+  bt-leaf : ⦃ l u : ℕ ⦄ → l ≤ u → bt
   bt-node : ⦃ l l' u u' : ℕ ⦄ → (d : ℕ) →
-             bt {n} {a} l' d → bt {n} {a} d u' → l ≤ l' → u' ≤ u → bt l u
+             bt {n} {a}  → bt {n} {a} → l ≤ l' → u' ≤ u → bt 
 
-lleaf : {n : Level} {a : Set n} → bt {n} {a} 0 3
+lleaf : {n : Level} {a : Set n} → bt {n} {a} 
 lleaf = (bt-leaf ⦃ 0 ⦄ ⦃ 3 ⦄ z≤n)
 
-rleaf : {n : Level} {a : Set n} → bt {n} {a} 3 4
+rleaf : {n : Level} {a : Set n} → bt {n} {a} 
 rleaf = (bt-leaf ⦃ 3 ⦄ ⦃ 4 ⦄ (n≤1+n 3))
 
-test-node : {n : Level} {a : Set n} → bt {n} {a} 0 4
+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) )
+
 
 
 _iso_ : {n : Level} {a : Set n} → ℕ → ℕ → Set
@@ -60,12 +76,16 @@
 
 -- 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} l u → (Maybe (Σ ℕ (λ d' → _iso_  {n} {a} d d')) → t ) → t
+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 d L R x x₁) cg with <-cmp key d
-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
+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 を書くときは型を考えるのがやや面倒なので先に動作を書いてから型を ? から補間するとよさそう
@@ -80,7 +100,7 @@
 -- 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} l u) → bt-search ⦃ l ⦄ ⦃ u ⦄ key tree (λ gdata → gdata ≡ gdata)
+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₁
@@ -89,7 +109,7 @@
 
 
 -- bt-find 
-find-support : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → (d : ℕ) → (tree : bt {n} {a} l u) → SingleLinkedStack (bt {n} {a} l u) → ( (bt {n} {a} l u) → SingleLinkedStack (bt {n} {a} l u) → Maybe (Σ ℕ (λ d' → _iso_  {n} {a} d d')) → t ) → t
+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
@@ -97,20 +117,101 @@
 
 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 {!!} {!!})
--- bt が l u の2つの ℕ を受ける、この値はすべてのnodeによって異なるため stack に積むときに型が合わない
+                         (λ 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-support ⦃ ll' ⦄ ⦃ d ⦄ key L {!!} {!!})
+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-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 = {!!}
+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
 
 
-bt-find : {n m : Level} {a : Set n} {t : Set m}  ⦃ l u : ℕ  ⦄ → (d : ℕ) → (tree : bt {n} {a} l u) → SingleLinkedStack (bt {n} {a} l u) → ( (bt {n} {a} l u) → SingleLinkedStack (bt {n} {a} l u) → 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 key tr cst cg)
+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} l u) → bt-search d tree (λ pt →  ) → t
--- bt-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 = {!!}
+