# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1636011311 -32400
# Node ID 79418701a2838e549df3c44a287c326219108ffb
# Parent  8df36383ced09775b331741ac721443ce0c6a6bf
add test and speciication

diff -r 8df36383ced0 -r 79418701a283 hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Wed Nov 03 18:28:31 2021 +0900
+++ b/hoareBinaryTree.agda	Thu Nov 04 16:35:11 2021 +0900
@@ -33,11 +33,11 @@
   node :  (key : ℕ) → (value : A) →
     (left : bt A ) → (write : bt A ) → bt A
 
-bt-length : {n : Level} {A : Set n} → (tree : bt A ) → ℕ
-bt-length leaf = 0
-bt-length (node key value t t₁) = Data.Nat._⊔_ (bt-length t ) (bt-length t₁ )
+bt-depth : {n : Level} {A : Set n} → (tree : bt A ) → ℕ
+bt-depth leaf = 0
+bt-depth (node key value t t₁) = Data.Nat._⊔_ (bt-depth t ) (bt-depth t₁ )
 
-find : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (tree : bt A ) → List (bt A)
+find : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → List (bt A)
            → (next : bt A → List (bt A) → t ) → (exit : bt A → List (bt A) → t ) → t
 find key leaf st _ exit = exit leaf st
 find key (node key₁ v tree tree₁) st next exit with <-cmp key key₁
@@ -46,12 +46,12 @@
 find key n@(node key₁ v tree tree₁) st next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st)
 
 {-# TERMINATING #-}
-find-loop : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → bt A → List (bt A)  → (exit : bt A → List (bt A) → t) → t
-find-loop {_} {A} {t} key tree st exit = find-loop1 tree st where
+find-loop : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → bt A → List (bt A)  → (exit : bt A → List (bt A) → t) → t
+find-loop {_} {_} {A} {t} key tree st exit = find-loop1 tree st where
     find-loop1 : bt A → List (bt A) → t
     find-loop1 tree st = find key tree st find-loop1  exit
 
-replace : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (value : A) → bt A → List (bt A) → (next : ℕ → A → bt A → List (bt A) → t ) → (exit : bt A → t) → t
+replace : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → List (bt A) → (next : ℕ → A → bt A → List (bt A) → t ) → (exit : bt A → t) → t
 replace key value tree [] next exit = exit tree
 replace key value tree (leaf ∷ st) next exit = next key value tree st 
 replace key value tree (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁
@@ -60,12 +60,12 @@
 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) st
 
 {-# TERMINATING #-}
-replace-loop : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (value : A) → bt A → List (bt A)  → (exit : bt A → t) → t
-replace-loop {_} {A} {t} key value tree st exit = replace-loop1 key value tree st where
+replace-loop : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → List (bt A)  → (exit : bt A → t) → t
+replace-loop {_} {_} {A} {t} key value tree st exit = replace-loop1 key value tree st where
     replace-loop1 : (key : ℕ) → (value : A) → bt A → List (bt A) → t
     replace-loop1 key value tree st = replace key value tree st replace-loop1  exit
 
-insertTree : {n : Level} {A : Set n} {t : Set n} → (tree : bt A) → (key : ℕ) → (value : A) → (next : bt A → t ) → t
+insertTree : {n m : Level} {A : Set n} {t : Set m} → (tree : bt A) → (key : ℕ) → (value : A) → (next : bt A → t ) → t
 insertTree tree key value exit = find-loop key tree [] ( λ t st → replace-loop key value t st exit ) 
 
 insertTest1 = insertTree leaf 1 1 (λ x → x )
@@ -93,18 +93,74 @@
 stackInvariant {_} {A} (x ∷ tail @ (node key value left right ∷ _  )) = ( (left ≡ x) ∧ stackInvariant tail) ∨ ( (right ≡ x) ∧ stackInvariant tail)
 stackInvariant {_} {A} s = Lift _ ⊥
 
-findP : {n : Level} {A : Set n} {t : Set n} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
-           →  treeInvariant tree  → stackInvariant stack  
-           → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant stack → bt-length tree1 < bt-length tree   → t )
+findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
+           →  treeInvariant tree ∧ stackInvariant stack  
+           → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant stack → bt-depth tree1 < bt-depth tree   → t )
            → (exit : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant stack → t ) → t
-findP = {!!}
-
-replaceP : {n : Level} {A : Set n} {t : Set n}
-     → (key : ℕ) → (value : A) → (tree : bt A) → (stack : List (bt A)) → treeInvariant tree ∧ stackInvariant stack 
-     → (next : (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant stack → bt-length tree1 < bt-length tree   → t )
-     → (exit : (tree1 : bt A) → treeInvariant tree1 → t) → t
-replaceP = {!!}
+findP key leaf st Pre _ exit = exit leaf st {!!}
+findP key (node key₁ v tree tree₁) st Pre next exit with <-cmp key key₁
+findP key n st Pre _ exit | tri≈ ¬a b ¬c = exit n st {!!}
+findP key n@(node key₁ v tree tree₁) st Pre next _ | tri< a ¬b ¬c = next tree (n ∷ st) {!!} {!!}
+findP key n@(node key₁ v tree tree₁) st Pre next _ | tri> ¬a ¬b c = next tree₁ (n ∷ st) {!!} {!!}
 
 
+replaceP : {n m : Level} {A : Set n} {t : Set m}
+     → (key : ℕ) → (value : A) → (tree : bt A) → (stack : List (bt A)) → treeInvariant tree ∧ stackInvariant stack 
+     → (next : ℕ → A → (tree1 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant stack → bt-depth tree1 < bt-depth tree   → t )
+     → (exit : (tree1 : bt A) → treeInvariant tree1 → t) → t
+replaceP key value tree [] Pre next exit = exit tree {!!}
+replaceP key value tree (leaf ∷ st) Pre next exit = next key value tree st {!!} {!!}
+replaceP key value tree (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁
+... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) st {!!} {!!}
+... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right ) st {!!} {!!}
+... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) st {!!} {!!}
 
+open import Relation.Binary.Definitions
 
+nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
+nat-≤>  (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
+lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥
+lemma3 refl ()
+lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥
+lemma5 (s≤s z≤n) ()
+
+TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
+   → (r : Index) → (p : Invraiant r)  
+   → (loop : (r : Index)  → Invraiant r → (next : (r1 : Index)  → Invraiant r1 → reduce r1 < reduce r  → t ) → t) → t
+TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r)
+... | tri≈ ¬a b ¬c = loop r p (λ r1 p1 lt → ⊥-elim (lemma3 b lt) ) 
+... | tri< a ¬b ¬c = loop r p (λ r1 p1 lt1 → TerminatingLoop1 (reduce r) r r1 (≤-step lt1) p1 lt1 ) where 
+    TerminatingLoop1 : (j : ℕ) → (r r1 : Index) → reduce r1 < suc j  → Invraiant r1 →  reduce r1 < reduce r → t
+    TerminatingLoop1 zero r r1 n≤j p1 lt = loop r1 p1 (λ r2 p1 lt1 → ⊥-elim (lemma5 n≤j lt1)) 
+    TerminatingLoop1 (suc j) r r1  n≤j p1 lt with <-cmp (reduce r1) (suc j)
+    ... | tri< a ¬b ¬c = TerminatingLoop1 j r r1 a p1 lt 
+    ... | tri≈ ¬a b ¬c = loop r1 p1 (λ r2 p2 lt1 → TerminatingLoop1 j r1 r2 (subst (λ k → reduce r2 < k ) b lt1 ) p2 lt1 )
+    ... | tri> ¬a ¬b c =  ⊥-elim ( nat-≤> c n≤j )   
+
+open _∧_
+
+insertTreeP : {n : Level} {A : Set n} {t : Set n} → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → (exit : (tree : bt A) → treeInvariant tree  → t ) → t
+insertTreeP {n} {A} {t} tree key value P exit =
+   TerminatingLoopS (bt A ∧ List (bt A)) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj2 p)} (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫  ⟪ P , lift tt ⟫
+       (λ p P loop → findP key (proj1 p)  (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt )
+       (λ t s P → TerminatingLoopS (bt A ∧ List (bt A)) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj2 p)} (λ p → bt-depth (proj1 p)) ⟪ t , s ⟫　P
+         (λ p P1 loop → replaceP key value (proj1 p) (proj2 p) P1 (λ k v t s P2 lt → loop ⟪ t , s ⟫ P2 lt) exit) 
+       ) )
+
+top-value : {n : Level} {A : Set n} → (tree : bt A) →  Maybe A 
+top-value leaf = nothing
+top-value (node key value tree tree₁) = just value
+
+insertTreeSpec0 : {n : Level} {A : Set n} {t : Set n} → (tree : bt A) → (value : A) → top-value tree ≡ just value → ⊤
+insertTreeSpec0 _ _ _ = tt
+
+insertTreeSpec1 : {n : Level} {A : Set n}  → (tree : bt A) → (key : ℕ) → (value : A) → treeInvariant tree → ⊤
+insertTreeSpec1 {n} {A}  tree key value P =
+         TerminatingLoopS (bt A ∧ List (bt A)) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj2 p)} (λ p → bt-depth (proj1 p)) ⟪ tree , [] ⟫  ⟪ P , lift tt ⟫
+       $ λ p P loop → findP key (proj1 p)  (proj2 p) P (λ t s P1 lt → loop ⟪ t , s ⟫ P1 lt )
+       $ λ t s P → TerminatingLoopS (bt A ∧ List (bt A)) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj2 p)} (λ p → bt-depth (proj1 p)) ⟪ t , s ⟫　P
+       $ λ p P1 loop → replaceP key value (proj1 p) (proj2 p) P1 (λ k v t s P2 lt → loop ⟪ t , s ⟫ P2 lt)
+       $ λ t1 P2 → TerminatingLoopS (bt A ∧ List (bt A)) {λ p → treeInvariant (proj1 p) ∧ stackInvariant (proj2 p)} (λ p → bt-depth (proj1 p)) ⟪ t1 , [] ⟫  ⟪ P2 , lift tt ⟫
+       $ λ p P3 loop → findP key (proj1 p)  (proj2 p) P3 (λ t s P3 lt → loop ⟪ t , s ⟫ P3 lt )
+       $ λ t2 s1 P4 → insertTreeSpec0 t2 value {!!}
+
diff -r 8df36383ced0 -r 79418701a283 logic.agda
--- a/logic.agda	Wed Nov 03 18:28:31 2021 +0900
+++ b/logic.agda	Thu Nov 04 16:35:11 2021 +0900
@@ -14,6 +14,7 @@
     false : Bool
 
 record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   constructor ⟪_,_⟫
    field
       proj1 : A
       proj2 : B