Mercurial > hg > Gears > GearsAgda

changeset 685:01c16d4d6d8c

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 Tue, 30 Nov 2021 05:52:13 +0900
parents 33bd83e5168f
children 4efb74d28d6a
files hoareBinaryTree.agda
diffstat 1 files changed, 14 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Mon Nov 29 23:12:56 2021 +0900
+++ b/hoareBinaryTree.agda	Tue Nov 30 05:52:13 2021 +0900
@@ -296,9 +296,9 @@
 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 ⊤) 
-    Post with replacePR.si Pre
-    ... | s-left x t = {!!}  -- can't happen
-    ... | s-right {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl11 ; ci = lift tt } where
+    Post with replacePR.si Pre | inspect replacePR.si Pre
+    ... | s-left x t | record { eq = eq} = {!!}  -- can't happen
+    ... | s-right {_} {_} {tree₁} {key₂} {v1} lt si | record { eq = refl } = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl11 ; 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)
@@ -306,15 +306,23 @@
         ... | refl = si
         repl03 : s-right {_} {_} {_} {_} {_} {tree₁} {key₂} {v1} lt si ≡ replacePR.si Pre
             → child-replaced key value (node key₁ value₁ left right ∷ tree1 ∷ st1) (node key₁ value₁ left right) (replacePR.tree0 Pre) (replacePR.si Pre) ≡ left
-        repl03 = {!!}
-        repl04 : (si : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) ) → child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) si ≡  node key₁ value₁ left right 
-        repl04 = {!!}
+        repl03 refl = refl
+        repl04 : (si : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) )
+            → tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right)  → child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) si ≡  node key₁ value₁ left right 
+        repl04 s-single refl = {!!}
+        repl04 (s-right lt2 si2) refl = {!!}
+        repl04 (s-left lt2 si2) refl = refl
         repl07 : (si : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) )
            →  node key₁ value₁ (child-replaced key value (node key₁ value₁ left right ∷ tree1 ∷ st1) (node key₁ value₁ left right) (replacePR.tree0 Pre) (replacePR.si Pre)) right
                     ≡ child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) si
         repl07 = {!!}
         repl11 : replacedTree key value (child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) repl10 ) (node key₁ value₁ repl right)
         repl11 =  subst (λ k →  replacedTree key value k (node key₁ value₁ repl right)) (repl07 repl10) ( r-left a (replacePR.ri Pre))
+        repl12 : replacedTree key value (child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) repl10 ) (node key₁ value₁ repl right)
+        repl12 with repl09 | repl10 
+        ... | refl | s-single = {!!}
+        ... | refl | s-right lt2 si2 = {!!}
+        ... | refl | s-left lt2 si2 = r-left a (subst (λ k → replacedTree key value k repl ) (repl03 refl) (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