Mercurial > hg > Gears > GearsAgda

changeset 682:cae136ce7352

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 Mon, 29 Nov 2021 21:41:27 +0900
parents 32fba6ff4d45
children aeddbe37d9fc
files hoareBinaryTree.agda
diffstat 1 files changed, 9 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Mon Nov 29 17:08:10 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 29 21:41:27 2021 +0900
@@ -300,19 +300,20 @@
     ... | s-left x t = {!!}  -- can't happen
     ... | s-right lt si with si-property1 si 
     ... | refl = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = si  ; ri = repl04 ; ci = lift tt } where
+        repl07 : {  key₂ : ℕ } { v1 : A } { tree₁ tree0 : bt A} { st : List (bt A) }  → {lt : key₂ < key }  → 
+            (si1 : stackInvariant key (node key₁ value₁ left right) tree0 (node key₁ value₁ left right ∷ st)) →
+            (si :  stackInvariant key (node key₂ v1 tree₁ (node key₁ value₁ left right)) tree0 st ) → s-right lt si ≡  si1 → 
+                 node key₁ value₁ left right ≡ child-replaced key value st tree1 tree0 {!!}
+        repl07  = {!!}
         repl05 : s-right lt si ≡ replacePR.si Pre → node key₁ value₁ left right ≡ child-replaced key value st tree1 (replacePR.tree0 Pre) si
-        repl05 = {!!}
-        repl06 : child-replaced key value (node key₁ value₁ left right ∷ st ) (node key₁ value₁ left right) (replacePR.tree0 Pre) (replacePR.si Pre) ≡ left
-        repl06 with replacePR.si Pre
-        ... | s-right x t = refl
-        ... | s-left x t = {!!}
+        repl05 eq = repl07 (replacePR.si Pre) si eq 
         repl02 :  node key₁ value₁ (child-replaced key value
              (node key₁ value₁ left right ∷ st )
              (node key₁ value₁ left right) (replacePR.tree0 Pre) (replacePR.si Pre)) right
                  ≡ child-replaced key value st tree1 (replacePR.tree0 Pre) si
-        repl02 with replacePR.si Pre |  si-property1 (replacePR.si Pre)
-        ... | s-right lt si | refl = {!!}
-        ... | s-left lt si | refl = {!!}
+        repl02 with replacePR.si Pre
+        ... | s-right x si = repl07 (s-right x si) si refl
+        ... | s-left x si = {!!}
         repl04 :  replacedTree key value (child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) si) (node key₁ value₁ repl right)
         repl04 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right)) repl02 (r-left a (replacePR.ri Pre))
         repl03 : replacedTree key value (child-replaced key value (node key₁ value₁ left right ∷ st) (node key₁ value₁ left right) (replacePR.tree0 Pre) (replacePR.si Pre)) repl