Mercurial > hg > Gears > GearsAgda

changeset 642:6e319e44271b

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 Thu, 18 Nov 2021 16:24:51 +0900
parents 14244de916f2
children fbd2adb6d9c5
files hoareBinaryTree.agda
diffstat 1 files changed, 23 insertions(+), 7 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Tue Nov 16 12:13:47 2021 +0900
+++ b/hoareBinaryTree.agda	Thu Nov 18 16:24:51 2021 +0900
@@ -151,13 +151,27 @@
 si-property-last t t0 (.t ∷ x ∷ st) (s-left si) with  si-property1 _ _ (x ∷ st) si
 ... | refl = si-property-last 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
+ti-right {_} {_} {.leaf} {_} {key₁} {v1} (t-single .key₁ .v1) = t-leaf
+ti-right {_} {_} {.leaf} {_} {key₁} {v1} (t-right x ti) = ti
+ti-right {_} {_} {.(node _ _ _ _)} {_} {key₁} {v1} (t-left x ti) = t-leaf
+ti-right {_} {_} {.(node _ _ _ _)} {_} {key₁} {v1} (t-node x x₁ ti ti₁) = ti₁
+
+ti-left : {n  : Level} {A : Set n} {tree₁ repl : bt A} → {key₁ : ℕ} → {v1 : A} →  treeInvariant  (node key₁ v1 repl tree₁ ) → treeInvariant repl
+ti-left {_} {_} {.leaf} {_} {key₁} {v1} (t-single .key₁ .v1) = t-leaf
+ti-left {_} {_} {_} {_} {key₁} {v1} (t-right x ti) = t-leaf
+ti-left {_} {_} {_} {_} {key₁} {v1} (t-left x ti) = ti
+ti-left {_} {_} {.(node _ _ _ _)} {_} {key₁} {v1} (t-node x x₁ ti ti₁) = ti
+
 stackTreeInvariant : {n  : Level} {A : Set n} (repl tree : bt A) → (stack : List (bt A))
    →  treeInvariant tree → stackInvariant repl tree stack  → treeInvariant repl
 stackTreeInvariant repl .repl .(repl ∷ []) ti (s-single .repl) = ti
-stackTreeInvariant {_} {A} repl tree (.repl ∷ st) ti (s-right si) = si1 si where
-   si1 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} →  stackInvariant (node key₁ v1 tree₁ repl) tree st → treeInvariant repl
-   si1 si = ?
-stackTreeInvariant repl tree .(repl ∷ _) ti (s-left si) = {!!}
+stackTreeInvariant {_} {A} repl tree (repl ∷ st) ti (s-right si) = ti-right (si1 si) where
+   si1 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} →  stackInvariant (node key₁ v1 tree₁ repl) tree st → treeInvariant  (node key₁ v1 tree₁ repl)
+   si1 {tree₁ }  {key₁ }  {v1 }  si = stackTreeInvariant  (node key₁ v1 tree₁ repl) tree st ti si
+stackTreeInvariant {_} {A} repl tree (repl ∷ st) ti (s-left si) = ti-left ( si2 si ) where
+   si2 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} →  stackInvariant (node key₁ v1 repl tree₁ ) tree st → treeInvariant  (node key₁ v1 repl tree₁ )
+   si2 {tree₁ }  {key₁ }  {v1 }  si = stackTreeInvariant  (node key₁ v1 repl tree₁ ) tree st ti si
 
 rt-property1 :  {n : Level} {A : Set n} (key : ℕ) (value : A) (tree tree1 : bt A ) → replacedTree key value tree tree1 → ¬ ( tree1 ≡ leaf )
 rt-property1 {n} {A} key value .leaf .(node key value leaf leaf) r-leaf ()
@@ -230,9 +244,11 @@
     Pre1 :  treeInvariant tree ∧ stackInvariant repl tree (node key₁ value₁ left right ∷ st) ∧ replacedTree key value tree repl
     Pre1 = Pre
     repleq : repl ≡ node key₁ value₁ left right
-    repleq = {!!}
-    repl1 : treeInvariant (node key₁ value₁ left right)
-    repl1 = {!!}
+    repleq with si-property1 _ _ _ (proj1 (proj2 Pre))
+    ... | refl = refl
+    repl1 : treeInvariant (node key₁ value₁ left right) -- stackInvariant (node key₁ value₁ left right) tree st
+    repl1 = stackTreeInvariant _ _ (node key₁ value₁ left right ∷ st) (proj1 Pre)
+        (subst (λ k → stackInvariant k tree (node key₁ value₁ left right ∷ st)) repleq (proj1 (proj2 Pre)))
     repl3 : replacedTree key value (node key₁ value₁ left right) (node key₁ value left right)
     repl3 = subst (λ k → replacedTree k value (node key₁ value₁ left right) (node key₁ value left right) ) (sym b) r-node
 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) (node key₁ value₁ left repl )st {!!}  ≤-refl