# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1638325482 -32400
# Node ID a971a954a345eeb90812d12c0ecc18c4de8d7fbe
# Parent  25f89e4bc1608fc67bbcf33bb3698d6384536acb
...

diff -r 25f89e4bc160 -r a971a954a345 hoareBinaryTree.agda
--- a/hoareBinaryTree.agda	Wed Dec 01 09:18:42 2021 +0900
+++ b/hoareBinaryTree.agda	Wed Dec 01 11:24:42 2021 +0900
@@ -65,12 +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 repl [] next exit = exit repl    -- can't happen
-replace key value repl (leaf ∷ []) next exit = exit repl    -- can't happen
+replace key value repl (leaf ∷ []) next exit = exit repl    
 replace key value repl (node key₁ value₁ left right ∷ []) next exit with <-cmp key key₁
 ... | tri< a ¬b ¬c = exit (node key₁ value₁ repl right ) 
 ... | tri≈ ¬a b ¬c = exit (node key₁ value  left right ) 
 ... | tri> ¬a ¬b c = exit (node key₁ value₁ left repl ) 
-replace key value repl (leaf ∷ st) next exit = next key value repl st    -- can't happen
+replace key value repl (leaf ∷ st) next exit = next key value repl st    
 replace key value repl (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁
 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st
 ... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right ) st
@@ -158,13 +158,6 @@
 si-property1 (s-right _  si) = refl
 si-property1 (s-left _  si) = refl
 
-si-property2 :  {n : Level} {A : Set n} {key : ℕ} {tree tree0 : bt A} → {stack  : List (bt A)} →  stackInvariant key tree tree0 (leaf ∷ stack ) → stack ≡ []
-si-property2 s-single = refl
-si-property2 (s-right x s-single) = {!!}
-si-property2 (s-right x (s-right x₁ si)) = {!!}
-si-property2 (s-right x (s-left x₁ si)) = {!!}
-si-property2 (s-left x si) = {!!}
-
 si-property-last :  {n : Level} {A : Set n}  (key : ℕ) (tree tree0 : bt A) → (stack  : List (bt A)) →  stackInvariant key tree tree0 stack
    → stack-last stack ≡ just tree0
 si-property-last key t t0 (t ∷ [])  (s-single )  = refl
@@ -201,6 +194,9 @@
 rt-property1 {n} {A} key value .(node _ _ _ _) _ (r-right x rt) = λ ()
 rt-property1 {n} {A} key value .(node _ _ _ _) _ (r-left x rt) = λ ()
 
+rt-property-leaf : {n : Level} {A : Set n} {key : ℕ} {value : A} {repl : bt A} → replacedTree key value leaf repl → repl ≡ node key value leaf leaf
+rt-property-leaf r-leaf = refl
+
 depth-1< : {i j : ℕ} →   suc i ≤ suc (i Data.Nat.⊔ j )
 depth-1< {i} {j} = s≤s (m≤m⊔n _ j)
 
@@ -324,7 +320,35 @@
         ... | tri< a ¬b ¬c = ⊥-elim ( ¬c c)
         ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c c)
         ... | tri> ¬a ¬b c = refl 
-replaceP {n} {_} {A} key value  {tree}  repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen
+replaceP {n} {_} {A} key value  {tree}  repl (leaf ∷ st@(tree1 ∷ st1)) Pre next exit = next key value repl st Post ≤-refl where
+    Post :  replacePR key value tree1 repl (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 ; ci = lift tt } where
+        repl09 : tree1 ≡ node key₂ v1 tree₁ leaf
+        repl09 = si-property1 si
+        repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
+        repl10 with si-property1 si
+        ... | refl = si
+        repl07 : child-replaced key (node key₂ v1 tree₁ leaf) ≡ leaf
+        repl07 with <-cmp key key₂ 
+        ... |  tri< a ¬b ¬c = ⊥-elim (¬c x)
+        ... |  tri≈ ¬a b ¬c = ⊥-elim (¬c x)
+        ... |  tri> ¬a ¬b c = refl
+        repl12 : replacedTree key value (child-replaced key  tree1  ) repl
+        repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07 ) ) (sym (rt-property-leaf (replacePR.ri Pre))) r-leaf
+    ... | s-left  {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
+        repl09 : tree1 ≡ node key₂ v1 leaf tree₁ 
+        repl09 = si-property1 si
+        repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
+        repl10 with si-property1 si
+        ... | refl = si
+        repl07 : child-replaced key (node key₂ v1 leaf tree₁ ) ≡ leaf
+        repl07 with <-cmp key key₂ 
+        ... |  tri< a ¬b ¬c = refl
+        ... |  tri≈ ¬a b ¬c = ⊥-elim (¬a x)
+        ... |  tri> ¬a ¬b c = ⊥-elim (¬a x)
+        repl12 : replacedTree key value (child-replaced key  tree1  ) repl
+        repl12 = subst₂ (λ j k → replacedTree key value j k ) (sym (subst (λ k → child-replaced key k ≡ leaf) (sym repl09) repl07 ) ) (sym (rt-property-leaf (replacePR.ri Pre))) r-leaf
 replaceP {n} {_} {A} key value {tree}  repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit  with <-cmp key key₁ 
 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st Post ≤-refl where
     Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤) 
@@ -377,8 +401,86 @@
             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 {!!} ≤-refl -- can't happen
-... | tri> ¬a ¬b c = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl
+... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right ) st Post ≤-refl where -- can't happen
+    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 ; ci = lift tt } where
+        repl09 : tree1 ≡ node key₂ v1 tree₁ tree -- (node key₁ value₁  left right)
+        repl09 = si-property1 si
+        repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
+        repl10 with si-property1 si
+        ... | refl = si
+        repl07 : child-replaced key (node key₂ v1 tree₁ tree) ≡ tree
+        repl07 with <-cmp key key₂ 
+        ... |  tri< a ¬b ¬c = ⊥-elim (¬c x)
+        ... |  tri≈ ¬a b ¬c = ⊥-elim (¬c x)
+        ... |  tri> ¬a ¬b c = refl
+        repl12 : replacedTree key value (child-replaced key  tree1  ) (node key₁ value left right )
+        repl12 = {!!}
+    ... | s-left  {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
+        repl09 : tree1 ≡ node key₂ v1 tree tree₁ 
+        repl09 = si-property1 si
+        repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
+        repl10 with si-property1 si
+        ... | refl = si
+        repl07 : child-replaced key (node key₂ v1 tree tree₁ ) ≡ tree
+        repl07 with <-cmp key key₂ 
+        ... |  tri< a ¬b ¬c = refl
+        ... |  tri≈ ¬a b ¬c = ⊥-elim (¬a x)
+        ... |  tri> ¬a ¬b c = ⊥-elim (¬a x)
+        repl12 : replacedTree key value (child-replaced key  tree1  ) (node key₁ value left right )
+        repl12 = {!!}
+... | tri> ¬a ¬b c = next key value (node key₁ value₁ left repl ) st Post ≤-refl where
+    Post : replacePR key value tree1 (node key₁ value₁ left repl ) st (λ _ _ _ → Lift n ⊤) 
+    Post with replacePR.si Pre 
+    ... | s-right {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
+        repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right) 
+        repl09 = si-property1 si
+        repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
+        repl10 with si-property1 si
+        ... | refl = si
+        repl03 : child-replaced key (node key₁ value₁ left right) ≡ right
+        repl03 with <-cmp key key₁ 
+        ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c)
+        ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c)
+        ... | tri> ¬a ¬b c = refl 
+        repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right
+        repl02 with repl09 | <-cmp key key₂
+        ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt)
+        ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt)
+        ... | refl | tri> ¬a ¬b c = refl
+        repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1
+        repl04  = begin
+            node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩
+            node key₁ value₁ left right ≡⟨ sym repl02 ⟩
+            child-replaced key  (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
+            child-replaced key tree1 ∎  where open ≡-Reasoning
+        repl12 : replacedTree key value (child-replaced key  tree1  ) (node key₁ value₁ left repl)
+        repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ left repl) ) repl04 (r-right c (replacePR.ri Pre)) 
+    ... | s-left {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 ; ci = lift tt } where
+        repl09 : tree1 ≡ node key₂ v1 (node key₁ value₁ left right) tree₁  
+        repl09 = si-property1 si
+        repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
+        repl10 with si-property1 si
+        ... | refl = si
+        repl03 : child-replaced key (node key₁ value₁ left right) ≡ right
+        repl03 with <-cmp key key₁ 
+        ... | tri< a1 ¬b ¬c = ⊥-elim (¬c c)
+        ... | tri≈ ¬a b ¬c = ⊥-elim (¬c c)
+        ... | tri> ¬a ¬b c = refl 
+        repl02 : child-replaced key (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡ node key₁ value₁ left right
+        repl02 with repl09 | <-cmp key key₂
+        ... | refl | tri< a ¬b ¬c = refl
+        ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬a lt)
+        ... | refl | tri> ¬a ¬b c = ⊥-elim (¬a lt)
+        repl04 : node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡ child-replaced key tree1
+        repl04  = begin
+            node key₁ value₁ left (child-replaced key (node key₁ value₁ left right)) ≡⟨ cong (λ k → node key₁ value₁ left k ) repl03 ⟩
+            node key₁ value₁ left right ≡⟨ sym repl02 ⟩
+            child-replaced key  (node key₂ v1 (node key₁ value₁ left right) tree₁) ≡⟨ cong (λ k → child-replaced key k ) (sym repl09) ⟩
+            child-replaced key tree1 ∎  where open ≡-Reasoning
+        repl12 : replacedTree key value (child-replaced key  tree1  ) (node key₁ value₁ left repl)
+        repl12 = subst (λ k → replacedTree key value k (node key₁ value₁ left repl) ) repl04  (r-right c (replacePR.ri Pre)) 
 
 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
    → (r : Index) → (p : Invraiant r)