Mercurial > hg > Gears > GearsAgda

changeset 689:25f89e4bc160

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 Wed, 01 Dec 2021 09:18:42 +0900
parents c916adcfd3be
children a971a954a345
files hoareBinaryTree.agda
diffstat 1 files changed, 39 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Wed Dec 01 06:47:47 2021 +0900
+++ b/hoareBinaryTree.agda	Wed Dec 01 09:18:42 2021 +0900
@@ -158,6 +158,13 @@
 si-property1 (s-right _  si) = refl
 si-property1 (s-left _  si) = refl
 
+si-property2 :  {n : Level} {A : Set n} {key : ℕ} {tree tree0 : bt A} → {stack  : List (bt A)} →  stackInvariant key tree tree0 (leaf ∷ stack ) → stack ≡ []
+si-property2 s-single = refl
+si-property2 (s-right x s-single) = {!!}
+si-property2 (s-right x (s-right x₁ si)) = {!!}
+si-property2 (s-right x (s-left x₁ si)) = {!!}
+si-property2 (s-left x si) = {!!}
+
 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
@@ -285,12 +292,38 @@
 replaceP key value {tree}  repl [] Pre next exit = ⊥-elim ( si-property0 (replacePR.si Pre) refl ) -- can't happen
 replaceP key value {tree}  repl (leaf ∷ []) Pre next exit with  si-property-last  _ _ _ _  (replacePR.si Pre)-- tree0 ≡ leaf
 ... | refl  =  exit (replacePR.tree0 Pre) (node key value leaf leaf) ⟪ replacePR.ti Pre ,  r-leaf ⟫
-replaceP key value {tree}  repl (node key₁ value₁ left right ∷ []) Pre next exit = exit (replacePR.tree0 Pre) repl ⟪ replacePR.ti Pre , repl01 ⟫ where
-    repl06 : child-replaced key  tree  ≡ node key₁ value₁ left right
-    repl06 = {!!}
+replaceP key value {tree}  repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁
+... | tri< a ¬b ¬c = exit (replacePR.tree0 Pre) (node key₁ value₁ repl right ) ⟪ replacePR.ti Pre , repl01 ⟫ where
+    repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ repl right )
+    repl01 with si-property1 (replacePR.si Pre) | si-property-last  _ _ _ _  (replacePR.si Pre)   
+    repl01 | refl | refl = subst (λ k → replacedTree key value  (node key₁ value₁ k right ) (node key₁ value₁ repl right )) repl02 (r-left a repl03) where
+        repl03 : replacedTree key value ( child-replaced key (node key₁ value₁ left right)) repl
+        repl03 = replacePR.ri Pre
+        repl02 : child-replaced key (node key₁ value₁ left right) ≡ left
+        repl02 with <-cmp key key₁
+        ... | tri< a ¬b ¬c = refl 
+        ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a a)
+        ... | tri> ¬a ¬b c = ⊥-elim ( ¬a a)
+... | tri≈ ¬a b ¬c = exit (replacePR.tree0 Pre) repl ⟪ replacePR.ti Pre , repl01 ⟫ where
     repl01 : replacedTree key value (replacePR.tree0 Pre) repl  
     repl01 with si-property1 (replacePR.si Pre) | si-property-last  _ _ _ _  (replacePR.si Pre)   
-    repl01 | refl | refl = subst (λ k → replacedTree key value k repl) repl06 (replacePR.ri Pre)
+    repl01 | refl | refl = subst (λ k → replacedTree key value k repl) repl02 (replacePR.ri Pre) where
+        repl02 : child-replaced key (node key₁ value₁ left right) ≡ node key₁ value₁ left right
+        repl02 with <-cmp key key₁
+        ... | tri< a ¬b ¬c = ⊥-elim ( ¬b b)
+        ... | tri≈ ¬a b ¬c = refl
+        ... | tri> ¬a ¬b c = ⊥-elim ( ¬b b)
+... | tri> ¬a ¬b c = exit (replacePR.tree0 Pre) (node key₁ value₁ left repl  ) ⟪ replacePR.ti Pre , repl01 ⟫ where
+    repl01 : replacedTree key value (replacePR.tree0 Pre) (node key₁ value₁ left repl )
+    repl01 with si-property1 (replacePR.si Pre) | si-property-last  _ _ _ _  (replacePR.si Pre)   
+    repl01 | refl | refl = subst (λ k → replacedTree key value  (node key₁ value₁ left k ) (node key₁ value₁ left repl )) repl02 (r-right c repl03) where
+        repl03 : replacedTree key value ( child-replaced key (node key₁ value₁ left right)) repl
+        repl03 = replacePR.ri Pre
+        repl02 : child-replaced key (node key₁ value₁ left right) ≡ right
+        repl02 with <-cmp key key₁
+        ... | tri< a ¬b ¬c = ⊥-elim ( ¬c c)
+        ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬c c)
+        ... | tri> ¬a ¬b c = refl 
 replaceP {n} {_} {A} key value  {tree}  repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen
 replaceP {n} {_} {A} key value {tree}  repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit  with <-cmp key key₁ 
 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st Post ≤-refl where
@@ -310,7 +343,7 @@
         repl02 : child-replaced key (node key₂ v1 tree₁ (node key₁ value₁ left right) ) ≡ node key₁ value₁ left right
         repl02 with repl09 | <-cmp key key₂
         ... | refl | tri< a ¬b ¬c = ⊥-elim (¬c lt)
-        ... | refl | tri≈ ¬a b ¬c = {!!}
+        ... | refl | tri≈ ¬a b ¬c = ⊥-elim (¬c lt)
         ... | refl | tri> ¬a ¬b c = refl
         repl04 : node key₁ value₁ (child-replaced key (node key₁ value₁ left right)) right ≡ child-replaced key tree1
         repl04  = begin
@@ -407,7 +440,7 @@
 findPP {_} {_} {A} key n@(node key₁ v1 tree tree₁) st Pre next exit | tri< a ¬b ¬c =
           next tree (n ∷ st) (record {ti = findPR.ti Pre  ; si = findPP2 st (findPR.si Pre) ; ci = lift tt} ) findPP1 where 
     tree0 =  findPR.tree0 Pre 
-    findPP2 : (st : List (bt A)) → stackInvariant key {!!} tree0 st →  stackInvariant key {!!} tree0 (node key₁ v1 tree tree₁ ∷ st)
+    findPP2 : (st : List (bt A)) → stackInvariant key (node key₁ v1 tree tree₁) tree0 st →  stackInvariant key tree tree0 (node key₁ v1 tree tree₁ ∷ st)
     findPP2 = {!!}
     findPP1 : suc ( bt-depth tree ) ≤ suc (bt-depth tree Data.Nat.⊔ bt-depth tree₁)
     findPP1 =  depth-1<