# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1638144391 -32400
# Node ID 681577b60c35bf4fe7cb15fe0810f2cf236f28bc
# Parent  49f1c24842cbd654c62eba3bb86c21a30b99a3e4
child-replaced

diff -r 49f1c24842cb -r 681577b60c35 hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Tue Nov 23 20:13:02 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 29 09:06:31 2021 +0900
@@ -114,13 +114,13 @@
     s-left :  {tree₁ tree0 tree : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} 
         → key  < key₁ →  stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree₁ tree0 (tree₁ ∷ st)
 
-data replacedTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (tree tree1 : bt A ) → Set n where
+data replacedTree  {n : Level} {A : Set n} (key : ℕ) (value : A)  : (before after : bt A ) → Set n where
     r-leaf : replacedTree key value leaf (node key value leaf leaf)
     r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁) 
     r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
-          → k < key →  replacedTree key value t t2 →  replacedTree key value (node k v1 t1 t) t
+          → k < key →  replacedTree key value t2 t →  replacedTree key value (node k v1 t1 t2) (node k v1 t1 t) 
     r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
-          → k > key →  replacedTree key value t t2 →  replacedTree key value (node k v1 t t1) t 
+          → k > key →  replacedTree key value t1 t →  replacedTree key value (node k v1 t1 t2) (node k v1 t t2) 
 
 add< : { i : ℕ } (j : ℕ ) → i < suc i + j
 add<  {i} j = begin
@@ -191,8 +191,8 @@
 rt-property1 :  {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf )
 rt-property1 {n} {A} key value .leaf .(node key value leaf leaf) r-leaf ()
 rt-property1 {n} {A} key value .(node key _ _ _) .(node key value _ _) r-node ()
-rt-property1 {n} {A} key value .(node _ _ _ _) _ (r-right x rt) = ?
-rt-property1 {n} {A} key value .(node _ _ _ _) _ (r-left x rt) = ?
+rt-property1 {n} {A} key value .(node _ _ _ _) _ (r-right x rt) = λ ()
+rt-property1 {n} {A} key value .(node _ _ _ _) _ (r-left x rt) = λ ()
 
 depth-1< : {i j : ℕ} →   suc i ≤ suc (i Data.Nat.⊔ j )
 depth-1< {i} {j} = s≤s (m≤m⊔n _ j)
@@ -255,12 +255,19 @@
 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥
 lemma5 (s≤s z≤n) ()
 
+child-replaced :  {n : Level} {A : Set n} (key : ℕ) (value : A) (stack : List (bt A)) (tree tree0 : bt A) → stackInvariant key tree tree0 stack  → bt A
+child-replaced key value .(tree ∷ []) tree .tree s-single = tree
+child-replaced key value .(leaf ∷ _) leaf tree0 (s-right x si) = leaf
+child-replaced key value .(node key₁ value₁ tree tree₁ ∷ _) (node key₁ value₁ tree tree₁) tree0 (s-right x si) = tree
+child-replaced key value .(leaf ∷ _) leaf tree0 (s-left x si) = leaf
+child-replaced key value .(node key₁ value₁ tree tree₁ ∷ _) (node key₁ value₁ tree tree₁) tree0 (s-left x si) = tree₁
+
 record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A ) (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where
    field
      tree0 : bt A
      ti : treeInvariant tree0
      si : stackInvariant key tree tree0 stack
-     ri : replacedTree key value tree repl
+     ri : replacedTree key value (child-replaced key value stack tree tree0 si) repl
      ci : C tree repl stack     -- data continuation
    
 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A)
@@ -277,11 +284,11 @@
      → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
 replaceP key value {tree}  repl [] Pre next exit = ⊥-elim ( si-property0 (replacePR.si Pre) refl ) -- can't happen
 replaceP key value {tree}  repl (leaf ∷ []) Pre next exit with  si-property-last  _ _ _ _  (replacePR.si Pre)-- tree0 ≡ leaf
-... | eq =  exit (replacePR.tree0 Pre) (node key value leaf leaf) ⟪ replacePR.ti Pre ,  {!!} ⟫
+... | refl  =  exit (replacePR.tree0 Pre) (node key value leaf leaf) ⟪ replacePR.ti Pre ,  r-leaf ⟫
 replaceP key value {tree}  repl (node key₁ value₁ left right ∷ []) Pre next exit  with <-cmp key key₁
-... | tri< a ¬b ¬c = exit (replacePR.tree0 Pre) (node key₁ value₁ repl right ) ⟪ replacePR.ti Pre , {!!} ⟫ where
-    repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ repl right)
-    repl01 = {!!}
+... | tri< a ¬b ¬c = exit (replacePR.tree0 Pre) repl ⟪ replacePR.ti Pre , repl01 ⟫ where
+    repl01 : replacedTree key value (replacePR.tree0 Pre) repl
+    repl01 = subst (λ k → replacedTree key value k _) {!!} (  replacePR.ri Pre )
 ... | tri≈ ¬a b ¬c = exit {!!} (node key₁ value  left right )  ⟪ {!!} , {!!} ⟫ -- can't happen
 ... | tri> ¬a ¬b c = exit {!!} (node key₁ value₁ left repl )  ⟪ {!!} , {!!} ⟫
 replaceP {n} {_} {A} key value  {tree}  repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen