# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1637537061 -32400
# Node ID 1f702351fd1f76a75d1dc89cef757683ccc537eb
# Parent  cf5095488bbddb9759fa367fc67652037257392b
findP done

diff -r cf5095488bbd -r 1f702351fd1f hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Sun Nov 21 22:10:16 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 22 08:24:21 2021 +0900
@@ -65,7 +65,12 @@
 
 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 ∷ _) next exit = exit (node key value leaf leaf)
+replace key value tree (leaf ∷ []) next exit = exit  (node key value leaf leaf)
+replace key value tree (node key₁ value₁ left right ∷ []) next exit with <-cmp key key₁
+... | tri< a ¬b ¬c = exit (node key₁ value₁ tree right ) 
+... | tri≈ ¬a b ¬c = exit (node key₁ value  left right ) 
+... | tri> ¬a ¬b c = exit (node key₁ value₁ left tree ) 
+replace key value tree (leaf ∷ st) next exit = next key value (node key value leaf leaf) st
 replace key value tree (node key₁ value₁ left right ∷ st) 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
@@ -214,6 +219,10 @@
 treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .leaf (t-left x ti) = t-leaf
 treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node x x₁ ti ti₁) = ti₁
 
+nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
+nat-≤>  (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
+nat-<> : { x y : ℕ } → x < y → y < x → ⊥
+nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
 
 open _∧_
 
@@ -225,12 +234,10 @@
 findP key leaf tree0 st Pre _ exit = exit leaf tree0 st Pre (case1 refl)
 findP key (node key₁ v1 tree tree₁) tree0 st Pre next exit with <-cmp key key₁
 findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n tree0 st Pre (case2 refl)
-findP {n} {_} {A} key nd@(node key₁ v1 tree tree₁) tree0 st  Pre next _ | tri< a ¬b ¬c = next tree tree0 (tree ∷ st)
+findP {n} {_} {A} key (node key₁ v1 tree tree₁) tree0 st  Pre next _ | tri< a ¬b ¬c = next tree tree0 (tree ∷ st)
        ⟪ treeLeftDown tree tree₁ (proj1 Pre)  , findP1 a st (proj2 Pre) ⟫ depth-1< where
    findP1 : key < key₁ → (st : List (bt A)) →  stackInvariant key (node key₁ v1 tree tree₁) tree0 st → stackInvariant key tree tree0 (tree ∷ st)
-   findP1 a .(node key₁ v1 tree tree₁ ∷ []) s-single = {!!}
-   findP1 a .(node key₁ v1 tree tree₁ ∷ _) (s-right x si) = {!!}
-   findP1 a .(node key₁ v1 tree tree₁ ∷ _) (s-left x si) = {!!}
+   findP1 a (x ∷ st) si = s-left a si
 findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (tree₁ ∷ st) ⟪ treeRightDown tree tree₁ (proj1 Pre) , s-right c (proj2 Pre) ⟫ depth-2<
 
 replaceTree1 : {n  : Level} {A : Set n} {t t₁ : bt A } → ( k : ℕ ) → (v1 value : A ) →  treeInvariant (node k v1 t t₁) → treeInvariant (node k value t t₁)
@@ -241,10 +248,6 @@
 
 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
-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 → ⊥
@@ -262,39 +265,17 @@
      → (next : ℕ → A → {tree0 tree1 tree-st : bt A } (repl : bt A) → (stack1 : List (bt A))
          → treeInvariant tree0 ∧ stackInvariant key tree-st tree0 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t)
      → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
-replaceP key value {tree0} {tree} {tree-st} repl [] Pre next exit with proj1 (proj2 Pre)
-... | t = {!!} 
-replaceP {_} {_} {A} key value {tree0} {tree} {tree-st} repl (leaf ∷ []) Pre next exit with proj1 (proj2 Pre)
-... | s-single   = {!!}
-... | s-right x t  = {!!}
-... | s-left x t  = {!!}
-replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ leaf ∷ st) Pre next exit with proj1 (proj2 Pre)
-... | s-right x t  = {!!}
-... | s-left x t  = {!!}
-replaceP {_} {_} {A} key value {tree0} {tree} {tree-st} repl (leaf ∷ node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁
-... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) (node key₁ value₁ tree right ∷ st)
-                  ⟪ proj1 Pre , ⟪ repl5 (proj1 (proj2 Pre)) , r-left a (proj2 (proj2 Pre))  ⟫ ⟫ ≤-refl where
-    repl5 :  stackInvariant key tree-st tree0 (leaf ∷ node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ tree right) tree0 (node key₁ value₁ tree right ∷ st )
-    repl5 si with si-property1  _ _ _ {!!} si
-    repl5 (s-right x si ) | refl = s-left a {!!} 
-    repl5 (s-left x si ) | refl = s-left a {!!} 
-... | tri≈ ¬a b ¬c = next key value (node key₁ value left right) st {!!} depth-3<
-... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right) st {!!} depth-3<
-replaceP key value {tree0} {tree} {tree-st} repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁
-... | tri> ¬a ¬b c = next key value  (node key₁ value₁ repl right ) st {!!}  ≤-refl
-... | tri≈ ¬a b ¬c = next key value  (node key value left right ) st {!!}  ≤-refl where -- this case won't happen
-... | tri< a ¬b ¬c with proj1 (proj2 Pre)
-... | s-single = {!!}
-... | s-right x si1  = {!!}
-... | s-left x si1  = next key value (node key₁ value₁ repl right )  st ⟪ proj1 Pre , ⟪ si1 ,  r-left a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl   
--- = next key value (node key₁ value₁ repl right )  st ⟪ proj1 Pre , ⟪ repl2 (proj1 (proj2 Pre)) ,  r-left a {!!}  ⟫ ⟫ ≤-refl   where
---    repl2 : stackInvariant key tree tree0 (node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ left right) tree0 st
---    repl2 (s-single .(node key₁ value₁ left right)) = {!!}
---    repl2 (s-right {_} {_} {_} {key₂} {v1} x si) with si-property1 _ _ _ _ si 
---    ... | eq = {!!}
---    repl2 (s-left x si) with si-property1 _ _ _ _ (s-left x si)
---    ... | refl = {!!}
-
+replaceP key value {tree0} {tree} {tree-st} repl [] Pre next exit = {!!} -- can't happen
+replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ []) Pre next exit =  exit tree0 (node key value leaf leaf) ?
+replaceP key value {tree0} {tree} {tree-st} repl (node key₁ value₁ left right ∷ []) Pre next exit  with <-cmp key key₁
+... | tri< a ¬b ¬c = exit tree0 (node key₁ value₁ tree right ) ?
+... | tri≈ ¬a b ¬c = exit tree0 (node key₁ value  left right ) ?
+... | tri> ¬a ¬b c = exit tree0 (node key₁ value₁ left tree ) ?
+replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ st@(_ ∷ _)) Pre next exit =  {!!} -- exit (node key value leaf leaf)
+replaceP key value {tree0} {tree} {tree-st} repl (node key₁ value₁ left right ∷ st@(_ ∷ _)) Pre next exit  with <-cmp key key₁
+... | tri< a ¬b ¬c = next key value {tree0} (node key₁ value₁ tree right ) st ? ≤-refl
+... | tri≈ ¬a b ¬c = next key value {tree0} (node key₁ value  left right ) st ? ≤-refl
+... | tri> ¬a ¬b c = next key value {tree0} (node key₁ value₁ left tree ) st ? ≤-refl
 
 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
    → (r : Index) → (p : Invraiant r)