Mercurial > hg > Gears > GearsAgda

changeset 640:e0bea7a2bb4d

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 Tue, 16 Nov 2021 11:08:59 +0900
parents 5fe23f540726
children 14244de916f2
files hoareBinaryTree.agda
diffstat 1 files changed, 16 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Mon Nov 15 17:04:13 2021 +0900
+++ b/hoareBinaryTree.agda	Tue Nov 16 11:08:59 2021 +0900
@@ -151,6 +151,13 @@
 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
 
+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 repl leaf (.repl ∷ st) ti (s-right si) = {!!}
+stackTreeInvariant repl (node key value tree tree₁) (.repl ∷ st) ti (s-right si) = {!!}
+stackTreeInvariant repl tree (.repl ∷ st) ti (s-left 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 ()
 rt-property1 {n} {A} key value .(node key _ _ _) .(node key value _ _) r-node ()
@@ -218,7 +225,15 @@
 ... | refl | t1 = ⊥-elim ( t1 refl )
 replaceP key value tree repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁
 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) (node key₁ value₁ repl right ) st {!!}  ≤-refl
-... | tri≈ ¬a b ¬c = next key value (node key₁ value  left right )(node key₁ value₁  left right )  st {!!}   ≤-refl
+... | tri≈ ¬a b ¬c = exit (node key₁ value₁  left right ) (node key₁ value  left right )  ⟪ repl1 , repl3 ⟫ where
+    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 = {!!}
+    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
 
 open import Relation.Binary.Definitions