Mercurial > hg > Gears > GearsAgda

changeset 668:d009198364dc

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 16:04:06 +0900
parents eb3721179793
children 077e2f3e417f
files hoareBinaryTree.agda
diffstat 1 files changed, 16 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Mon Nov 22 15:14:16 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 22 16:04:06 2021 +0900
@@ -265,34 +265,30 @@
 replaceNodeP k v1 (node .k value t t₁) (case2 refl) P next = next (node k v1 t t₁) (replaceTree1 k value v1 P) r-node
 
 replaceP : {n m : Level} {A : Set n} {t : Set m}
-     → (key : ℕ) → (value : A) → {tree0 tree tree-st : bt A} ( repl : bt A)
-     → (stack : List (bt A)) → treeInvariant tree0 ∧ stackInvariant key tree-st tree0 stack ∧ replacedTree key value tree repl
-     → (next : ℕ → A → {tree0 tree1 tree-st : bt A } (repl : bt A) → (stack1 : List (bt A))
-         → treeInvariant tree0 ∧ stackInvariant key tree-st tree0 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t)
+     → (key : ℕ) → (value : A) → {tree0 tree : bt A} ( repl : bt A)
+     → (stack : List (bt A)) → treeInvariant tree0 ∧ stackInvariant key tree tree0 (tree ∷ stack) ∧ replacedTree key value tree repl
+     → (next : ℕ → A → {tree0 tree1 : bt A } (repl : bt A) → (stack1 : List (bt A))
+         → treeInvariant tree0 ∧ stackInvariant key tree1 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 with  si-property-last  _ _ _ _  (proj1 (proj2 Pre)) -- tree0 ≡ leaf
+replaceP key value {tree0} {tree}  repl [] Pre next exit = ⊥-elim ( si-property0 (proj1 (proj2 Pre)) {!!} ) -- can't happen
+replaceP key value {tree0} {tree}  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₂ (λ 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
+replaceP key value {tree0} {tree}  repl (node key₁ value₁ left right ∷ []) Pre next exit  with <-cmp key key₁
+... | tri< a ¬b ¬c = exit tree0 (node key₁ value₁ repl right )
+    ⟪ proj1 Pre , subst (λ k → replacedTree key value k (node key₁ value₁ repl right)) {!!} (r-left a (proj2 (proj2 Pre)) ) ⟫ where
+      repl03 : node key₁ value₁ left right ≡ tree0
       repl03 with si-property-last  _ _ _ _ (proj1 (proj2 Pre))
-      ... | refl = {!!}
-      repl04 : node key₁ value₁ repl right ≡ node key₁ value₁ tree right
-      repl04 = {!!}
+      ... | refl = refl
 ... | 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 =
+replaceP {n} {_} {A} key value {tree0} {tree}  repl (leaf ∷ st@(_ ∷ _)) Pre next exit =
      next key value {tree0} (node key value leaf leaf) st
-         ⟪ proj1 Pre ,  ⟪ repl01 (sym (si-property1 (proj1 (proj2 Pre)))) (proj1 (proj2 Pre))
-             , subst (λ k → replacedTree key value k  (node key value leaf leaf) ) (si-property1 (proj1 (proj2 Pre))) r-leaf ⟫  ⟫  ≤-refl where
-      repl01 : {x : bt A} → { xs : List (bt A)} → tree-st ≡ leaf  → stackInvariant key tree-st tree0 (leaf ∷ x ∷ xs) → stackInvariant key x tree0 (x ∷ xs)
+         ⟪ proj1 Pre ,  ⟪ repl01 (sym (si-property1 (proj1 (proj2 Pre)))) {!!}
+             , subst (λ k → replacedTree key value k  (node key value leaf leaf) ) {!!} r-leaf ⟫  ⟫  ≤-refl where
+      repl01 : {x : bt A} → { xs : List (bt A)} → {!!} → stackInvariant key tree tree0 (leaf ∷ x ∷ xs) → stackInvariant key x tree0 (x ∷ xs)
       repl01 {x} {xs} refl (s-right lt si) = subst (λ k → stackInvariant key k tree0 (x ∷ xs) ) (sym (si-property1 si)) si
       repl01 {x} {xs} refl (s-left lt si) = subst (λ k → stackInvariant key k tree0 (x ∷ xs) ) (sym (si-property1 si)) si
-replaceP key value {tree0} {tree} {tree-st} repl (node key₁ value₁ left right ∷ st@(_ ∷ _)) Pre next exit  with <-cmp key key₁
+replaceP key value {tree0} {tree}  repl (node key₁ value₁ left right ∷ st@(_ ∷ _)) Pre next exit  with <-cmp key key₁
 ... | tri< a ¬b ¬c = next key value {tree0} (node key₁ value₁ tree right ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫  ⟫ ≤-refl
 ... | tri≈ ¬a b ¬c = next key value {tree0} (node key₁ value  left right ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!}  ⟫ ⟫ ≤-refl
 ... | tri> ¬a ¬b c = next key value {tree0} (node key₁ value₁ left tree ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!}  ⟫ ⟫ ≤-refl