Mercurial > hg > Gears > GearsAgda

changeset 683:aeddbe37d9fc

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 22:45:33 +0900
parents cae136ce7352
children 33bd83e5168f
files hoareBinaryTree.agda
diffstat 1 files changed, 19 insertions(+), 24 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Mon Nov 29 21:41:27 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 29 22:45:33 2021 +0900
@@ -293,33 +293,28 @@
     repl01 with si-property1 (replacePR.si Pre) | si-property-last  _ _ _ _  (replacePR.si Pre)   
     repl01 | refl | refl = subst (λ k → replacedTree key value k repl) repl06 (replacePR.ri Pre)
 replaceP {n} {_} {A} key value  {tree}  repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen
-replaceP {n} {_} {A} key value {tree}  repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit  with <-cmp key key₁ | si-property1 (replacePR.si Pre)
-... | tri< a ¬b ¬c | refl = next key value (node key₁ value₁ repl right ) st Post ≤-refl where
+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 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 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
-        ... | 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
-        repl03 = replacePR.ri Pre
-... | tri≈ ¬a b ¬c | refl = next key value {{!!}} (node key₁ value  left right ) st {!!} ≤-refl -- can't happen
-... | tri> ¬a ¬b c | refl = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl
+    ... | s-right {_} {_} {tree₁} {key₂} {v1} lt si = 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)
+        repl10 with si-property1 si
+        ... | refl = si
+        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 s-single = {!!}
+        repl07 (s-right x si) = refl
+        repl07 (s-left x si) = {!!}
+        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))
+... | 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
 
 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
    → (r : Index) → (p : Invraiant r)