Mercurial > hg > Gears > GearsAgda

changeset 663:cf5095488bbd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
stack contains original tree at end always
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 21 Nov 2021 22:10:16 +0900
parents a8959c8340e0
children 1f702351fd1f
files hoareBinaryTree.agda
diffstat 1 files changed, 16 insertions(+), 19 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Sun Nov 21 21:52:03 2021 +0900
+++ b/hoareBinaryTree.agda	Sun Nov 21 22:10:16 2021 +0900
@@ -145,21 +145,19 @@
 stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] )
 stackInvariantTest1 = s-right (add< 2) s-single  
 
-si-property1 :  {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack  : List (bt A)) → ¬ (stack ≡ [])  → stackInvariant key tree tree0 stack
+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 [] ne (s-nil ) = ⊥-elim ( ne refl )
-si-property1 key t t0 (t ∷ []) ne 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 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-property-last :  {n : Level} {A : Set n}  (key : ℕ) (tree tree0 : bt A) → (stack  : List (bt A)) → ¬ (stack ≡ [])   → stackInvariant key tree tree0 stack
+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 [] ne s-nil  = ⊥-elim ( ne refl )
-si-property-last key t t0 (t ∷ [])  _ s-single   = refl
-si-property-last key t t0 (.t ∷ x ∷ st) ne (s-right _ si ) with  si-property1 key _ _ (x ∷ st) (λ ()) si
-... | refl = si-property-last key x t0 (x ∷ st)  (λ ()) si
-si-property-last key t t0 (.t ∷ x ∷ st) ne (s-left _ si ) with  si-property1 key _ _ (x ∷ st)  (λ ()) si
-... | refl = si-property-last key x t0 (x ∷ st)  (λ ()) si
+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
+... | 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
+... | 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
 ti-right {_} {_} {.leaf} {_} {key₁} {v1} (t-single .key₁ .v1) = t-leaf
@@ -228,12 +226,11 @@
 findP key (node key₁ v1 tree tree₁) tree0 st Pre next exit with <-cmp key key₁
 findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n tree0 st Pre (case2 refl)
 findP {n} {_} {A} key nd@(node key₁ v1 tree tree₁) tree0 st  Pre next _ | tri< a ¬b ¬c = next tree tree0 (tree ∷ st)
-       ⟪ treeLeftDown tree tree₁ (proj1 Pre)  , {!!} ⟫ depth-1< where
-   findP1 : key < key₁ → (st : List (bt A)) →  stackInvariant key (node key₁ v1 tree tree₁) tree0 st → stackInvariant key tree tree0 (nd ∷ st)
-   findP1 a (x ∷ st) si = {!!} -- s-left a ? ?    stackInvariant key (node key₁ v1 tree tree₁) tree0 (x ∷ st)
-                                            --  → stackInvariant key tree tree0 (node key₁ v1 tree tree₁ ∷ x ∷ st)
-   findP1 a [] si = {!!} --  stackInvariant key (node key₁ v1 tree tree₁) tree0 []
-                    --     → stackInvariant key tree tree0 (node key₁ v1 tree tree₁ ∷ [])
+       ⟪ treeLeftDown tree tree₁ (proj1 Pre)  , findP1 a st (proj2 Pre) ⟫ depth-1< where
+   findP1 : key < key₁ → (st : List (bt A)) →  stackInvariant key (node key₁ v1 tree tree₁) tree0 st → stackInvariant key tree tree0 (tree ∷ st)
+   findP1 a .(node key₁ v1 tree tree₁ ∷ []) s-single = {!!}
+   findP1 a .(node key₁ v1 tree tree₁ ∷ _) (s-right x si) = {!!}
+   findP1 a .(node key₁ v1 tree tree₁ ∷ _) (s-left x si) = {!!}
 findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (tree₁ ∷ st) ⟪ treeRightDown tree tree₁ (proj1 Pre) , s-right c (proj2 Pre) ⟫ depth-2<
 
 replaceTree1 : {n  : Level} {A : Set n} {t t₁ : bt A } → ( k : ℕ ) → (v1 value : A ) →  treeInvariant (node k v1 t t₁) → treeInvariant (node k value t t₁)
@@ -278,7 +275,7 @@
 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) (node key₁ value₁ tree right ∷ st)
                   ⟪ proj1 Pre , ⟪ repl5 (proj1 (proj2 Pre)) , r-left a (proj2 (proj2 Pre))  ⟫ ⟫ ≤-refl where
     repl5 :  stackInvariant key tree-st tree0 (leaf ∷ node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ tree right) tree0 (node key₁ value₁ tree right ∷ st )
-    repl5 si with si-property1 _ _ _ _ {!!} si
+    repl5 si with si-property1  _ _ _ {!!} si
     repl5 (s-right x si ) | refl = s-left a {!!} 
     repl5 (s-left x si ) | refl = s-left a {!!} 
 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right) st {!!} depth-3<