Mercurial > hg > Gears > GearsAgda

changeset 667:eb3721179793

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, 22 Nov 2021 15:14:16 +0900
parents f344e6b254d8
children d009198364dc
files hoareBinaryTree.agda
diffstat 1 files changed, 11 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Mon Nov 22 14:50:09 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 22 15:14:16 2021 +0900
@@ -271,10 +271,18 @@
          → treeInvariant tree0 ∧ stackInvariant key tree-st tree0 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t)
      → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
 replaceP key value {tree0} {tree} {tree-st} repl [] Pre next exit = ⊥-elim ( si-property0 (proj1 (proj2 Pre)) refl ) -- can't happen
-replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ []) Pre next exit =
-       exit tree0 (node key value leaf leaf) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!}  r-leaf ⟫
+replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ []) Pre next exit with  si-property-last  _ _ _ _  (proj1 (proj2 Pre)) -- tree0 ≡ leaf
+... | refl =  exit tree0 (node key value leaf leaf) ⟪ proj1 Pre ,  r-leaf ⟫
 replaceP key value {tree0} {tree} {tree-st} repl (node key₁ value₁ left right ∷ []) Pre next exit  with <-cmp key key₁
-... | tri< a ¬b ¬c = exit tree0 (node key₁ value₁ tree right ) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!} (r-left a (proj2 (proj2 Pre)) ) ⟫
+... | tri< a ¬b ¬c = exit tree0 (node key₁ value₁ tree right )
+    ⟪ proj1 Pre , subst₂ (λ j k → replacedTree key value j k ) repl03 repl04 (r-left a (proj2 (proj2 Pre)) ) ⟫ where
+      repl02 : node key₁ value₁ left right ≡ tree-st
+      repl02 = si-property1 (proj1 (proj2 Pre)) 
+      repl03 : node key₁ value₁ tree right ≡ tree0
+      repl03 with si-property-last  _ _ _ _ (proj1 (proj2 Pre))
+      ... | refl = {!!}
+      repl04 : node key₁ value₁ repl right ≡ node key₁ value₁ tree right
+      repl04 = {!!}
 ... | tri≈ ¬a refl ¬c = exit tree0 (node key₁ value  left right ) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!} r-node ⟫
 ... | tri> ¬a ¬b c = exit tree0 (node key₁ value₁ left tree ) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!} {!!}  ⟫
 replaceP {n} {_} {A} key value {tree0} {tree} {tree-st} repl (leaf ∷ st@(_ ∷ _)) Pre next exit =