Mercurial > hg > Gears > GearsAgda

changeset 691:ca624203b453

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 01 Dec 2021 11:43:53 +0900
parents a971a954a345
children 9f1ccc8a0e1d
files hoareBinaryTree.agda
diffstat 1 files changed, 8 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Wed Dec 01 11:24:42 2021 +0900
+++ b/hoareBinaryTree.agda	Wed Dec 01 11:43:53 2021 +0900
@@ -404,7 +404,7 @@
 ... | 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
+    ... | 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
         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)
@@ -415,9 +415,10 @@
         ... |  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
+        repl12 : (key ≡ key₁) → replacedTree key value (child-replaced key  tree1  ) (node key₁ value left right )
+        repl12 refl with repl09 
+        ... | refl = subst (λ k → replacedTree key value k (node key₁ value left right )) (sym repl07) r-node
+    ... | s-left  {_} {_} {tree₁} {key₂} {v1} x si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl12 b ; ci = lift tt } where
         repl09 : tree1 ≡ node key₂ v1 tree tree₁ 
         repl09 = si-property1 si
         repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
@@ -428,8 +429,9 @@
         ... |  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 = {!!}
+        repl12 : (key ≡ key₁) → replacedTree key value (child-replaced key  tree1  ) (node key₁ value left right )
+        repl12 refl with repl09 
+        ... | refl = subst (λ k → replacedTree key value k (node key₁ value left right )) (sym repl07) r-node
 ... | 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