# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1638713918 -32400
# Node ID fa0feb3c7adf6c2d4293e5ceca69cc2b4f066611
# Parent  aad148b5037d18dbb0bc1ac837685c90ac58d8bc
...

diff -r aad148b5037d -r fa0feb3c7adf hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Sun Dec 05 18:57:23 2021 +0900
+++ b/hoareBinaryTree.agda	Sun Dec 05 23:18:38 2021 +0900
@@ -242,22 +242,22 @@
 treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node x x₁ ti ti₁) = ti₁
 
 
-record findCond {n  : Level} {A : Set n} {C : ℕ → bt A → Set n} ( key : ℕ ) (tree : bt A) : Set (suc n) where
+record FindCond {n  : Level} {A : Set n} (C : ℕ → bt A → Set n)   : Set (Level.suc n) where
    field
-      c1 : {key₁ : ℕ} } {v1 : A } { tree₀ tree₁ : bt A } → C key (node key₁ v1 tree tree₁) → key < key₁  → C key tree
-      c2 : {key₁ : ℕ} } {v1 : A } { tree₀ tree₁ : bt A } → C key (node key₁ v1 tree tree₁) → key > key₁  → C key tree
+      c1 : {key key₁ : ℕ}  {v1 : A } { tree tree₁ : bt A } → C key (node key₁ v1 tree tree₁) → key < key₁  → C key tree
+      c2 : {key key₁ : ℕ}  {v1 : A } { tree tree₁ : bt A } → C key (node key₁ v1 tree tree₁) → key > key₁  → C key tree₁
 
 
 findP0 : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
-           →  {C : ℕ → bt A → Set n} → C key tree
+           →  {C : ℕ → bt A → Set n} → C key tree → FindCond C
            → (next : (tree1 : bt A) → (stack : List (bt A)) → C key tree1 → bt-depth tree1 < bt-depth tree   → t )
            → (exit : (tree1 : bt A) → (stack : List (bt A)) → C key tree1 
                  → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key )  → t ) → t
-findP0 key leaf st Pre _ exit = exit leaf st Pre (case1 refl)
-findP0 key (node key₁ v1 tree tree₁) st Pre next exit with <-cmp key key₁
-findP0 key n st Pre _ exit | tri≈ ¬a refl ¬c = exit n st Pre (case2 refl)
-findP0 {n} {_} {A} key (node key₁ v1 tree tree₁) st  Pre next _ | tri< a ¬b ¬c = next tree (tree ∷ st) {!!}  depth-1< 
-findP0 key n@(node key₁ v1 tree tree₁) st Pre next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st) {!!} depth-2<
+findP0 key leaf st Pre _ _ exit = exit leaf st Pre (case1 refl)
+findP0 key (node key₁ v1 tree tree₁) st Pre _ next exit with <-cmp key key₁
+findP0 key n st Pre e _ exit | tri≈ ¬a refl ¬c = exit n st Pre (case2 refl)
+findP0 {n} {_} {A} key (node key₁ v1 tree tree₁) st  Pre e next _ | tri< a ¬b ¬c = next tree (tree ∷ st) (FindCond.c1 e Pre a) depth-1< 
+findP0 key n@(node key₁ v1 tree tree₁) st Pre e next _ | tri> ¬a ¬b c = next tree₁ (tree₁ ∷ st) (FindCond.c2 e Pre c) depth-2<
 
 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
            →  treeInvariant tree ∧ stackInvariant key tree tree0 stack  
@@ -271,7 +271,6 @@
        ⟪ 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 (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₁ (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₁)
@@ -438,7 +437,7 @@
             child-replaced key tree1 ∎  where open ≡-Reasoning
         repl12 : replacedTree key value (child-replaced key  tree1  ) (node key₁ value₁ repl right)
         repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right) ) repl04  (r-left a (replacePR.ri Pre)) 
-... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right ) st Post ≤-refl where -- can't happen
+... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right ) st Post ≤-refl where 
     Post :  replacePR key value tree1 (node key₁ value left right ) (tree1 ∷ st1) (λ _ _ _ → Lift n ⊤)
     Post with replacePR.si Pre 
     ... | s-right  {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 b ; ci = lift tt } where
@@ -628,7 +627,7 @@
 findPP key (node key₁ v1 tree tree₁) st Pre _ next exit with <-cmp key key₁
 findPP key n st Pre _ _ exit | tri≈ ¬a refl ¬c = exit n st Pre (case2 refl)
 findPP {n} {_} {A} key (node key₁ v1 tree tree₁) st  Pre e next _ | tri< a ¬b ¬c = next tree (tree ∷ st)
-       record { tree0 = findPR.tree0 Pre ; ti0 = findPR.ti0 Pre ; ti = treeLeftDown tree tree₁ (findPR.ti Pre)  ; si =  findP1 a st (findPR.si Pre) ; ci = findExt.c1 e Pre a } depth-1< where -- findPR key (node key₁ v1 tree tree₁) st C → key < key₁  → C tree (tree ∷ st)
+       record { tree0 = findPR.tree0 Pre ; ti0 = findPR.ti0 Pre ; ti = treeLeftDown tree tree₁ (findPR.ti Pre)  ; si =  findP1 a st (findPR.si Pre) ; ci = findExt.c1 e Pre a } depth-1< where 
    findP1 : key < key₁ → (st : List (bt A)) →  stackInvariant key (node key₁ v1 tree tree₁)
          (findPR.tree0 Pre) st → stackInvariant key tree (findPR.tree0 Pre) (tree ∷ st)
    findP1 a (x ∷ st) si = s-left a si