--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/hoareBinaryTree.agda	Wed Dec 04 15:42:47 2019 +0900
@@ -0,0 +1,116 @@
+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)
+
+
+
+data bt {n : Level} {a : Set n} : ℕ → ℕ → Set n where
+  bt-leaf : ⦃ l u : ℕ ⦄ → l ≤ u → bt l u
+  bt-node : ⦃ l l' u u' : ℕ ⦄ → (d : ℕ) →
+             bt {n} {a} l' d → bt {n} {a} d u' → l ≤ l' → u' ≤ u → bt l u
+
+lleaf : {n : Level} {a : Set n} → bt {n} {a} 0 3
+lleaf = (bt-leaf ⦃ 0 ⦄ ⦃ 3 ⦄ z≤n)
+
+rleaf : {n : Level} {a : Set n} → bt {n} {a} 3 4
+rleaf = (bt-leaf ⦃ 3 ⦄ ⦃ 4 ⦄ (n≤1+n 3))
+
+test-node : {n : Level} {a : Set n} → bt {n} {a} 0 4
+test-node {n} {a} = (bt-node ⦃ 0 ⦄ ⦃ 0 ⦄ ⦃ 4 ⦄ ⦃ 4 ⦄ 3 lleaf rleaf z≤n ≤-refl )
+
+
+
+_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₁ }
+
+-- 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} {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
+
+
+-- この辺の 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} l u) → 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} 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} {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 {!!} {!!})
+-- bt が l u の2つの ℕ を受ける、この値はすべてのnodeによって異なるため stack に積むときに型が合わない
+
+-- find-support ⦃ ll' ⦄ ⦃ d ⦄ key L {!!} {!!})
+
+
+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 = {!!}
+
+
+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)
+
+
+
+-- 証明に 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 = ?