Mercurial > hg > Gears > GearsAgda

changeset 666:f344e6b254d8

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 14:50:09 +0900
parents 1708fe988ac5
children eb3721179793
files hoareBinaryTree.agda
diffstat 1 files changed, 21 insertions(+), 16 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Mon Nov 22 08:58:59 2021 +0900
+++ b/hoareBinaryTree.agda	Mon Nov 22 14:50:09 2021 +0900
@@ -150,23 +150,23 @@
 stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] )
 stackInvariantTest1 = s-right (add< 2) s-single  
 
-si-property0 :  {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack  : List (bt A)) →  stackInvariant key tree tree0 stack → ¬ ( stack ≡ [] )
-si-property0 key tree .tree .(tree ∷ []) s-single ()
-si-property0 key tree tree0 .(tree ∷ _) (s-right x si) ()
-si-property0 key tree tree0 .(tree ∷ _) (s-left x si) ()
+si-property0 :  {n : Level} {A : Set n} {key : ℕ} {tree tree0 : bt A} → {stack  : List (bt A)} →  stackInvariant key tree tree0 stack → ¬ ( stack ≡ [] )
+si-property0  s-single ()
+si-property0  (s-right x si) ()
+si-property0  (s-left x si) ()
 
-si-property1 :  {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack  : List (bt A)) →  stackInvariant key tree tree0 stack
-   → stack-top stack ≡ just tree
-si-property1 key t t0 (t ∷ []) s-single  = refl
-si-property1 key t t0 (t ∷ st) (s-right _  si) = refl
-si-property1 key t t0 (t ∷ st) (s-left _  si) = refl
+si-property1 :  {n : Level} {A : Set n} {key : ℕ} {tree tree0 tree1 : bt A} → {stack  : List (bt A)} →  stackInvariant key tree tree0 (tree1 ∷ stack)
+   → tree1 ≡ tree
+si-property1 s-single  = refl
+si-property1 (s-right _  si) = refl
+si-property1 (s-left _  si) = refl
 
 si-property-last :  {n : Level} {A : Set n}  (key : ℕ) (tree tree0 : bt A) → (stack  : List (bt A)) →  stackInvariant key tree tree0 stack
    → stack-last stack ≡ just tree0
 si-property-last key t t0 (t ∷ [])  s-single   = refl
-si-property-last key t t0 (.t ∷ x ∷ st) (s-right _ si ) with  si-property1 key _ _ (x ∷ st)  si
+si-property-last key t t0 (.t ∷ x ∷ st) (s-right _ si ) with  si-property1 si
 ... | refl = si-property-last key x t0 (x ∷ st)   si
-si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ si ) with  si-property1 key _ _ (x ∷ st)   si
+si-property-last key t t0 (.t ∷ x ∷ st) (s-left _ si ) with  si-property1  si
 ... | refl = si-property-last key x t0 (x ∷ st)   si
 
 ti-right : {n  : Level} {A : Set n} {tree₁ repl : bt A} → {key₁ : ℕ} → {v1 : A} →  treeInvariant  (node key₁ v1 tree₁ repl) → treeInvariant repl
@@ -270,15 +270,20 @@
      → (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)
      → (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 [] 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 (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 _ ) {!!} {!!}  ⟫
-... | tri≈ ¬a b ¬c = exit tree0 (node key₁ value  left right ) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) {!!} {!!}  ⟫
+... | 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 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 key value {tree0} {tree} {tree-st} repl (leaf ∷ st@(_ ∷ _)) Pre next exit =
-     next key value {tree0} (node key value leaf leaf) st ⟪ proj1 Pre ,  ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫  ⟫  ≤-refl
+replaceP {n} {_} {A} key value {tree0} {tree} {tree-st} 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)
+      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₁
 ... | 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