Mercurial > hg > Gears > GearsAgda
changeset 659:afcccfaea264
stack invariant in findP
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 21 Nov 2021 17:24:40 +0900 |
| parents | be2fd2884eef |
| children | 712e2998c76b |
| files | hoareBinaryTree.agda |
| diffstat | 1 files changed, 10 insertions(+), 7 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree.agda Sun Nov 21 15:53:27 2021 +0900 +++ b/hoareBinaryTree.agda Sun Nov 21 17:24:40 2021 +0900 @@ -104,7 +104,7 @@ data stackInvariant {n : Level} {A : Set n} (key : ℕ) : (top orig : bt A) → (stack : List (bt A)) → Set n where s-nil : {tree : bt A} → stackInvariant key tree tree [] - s-single : {tree : bt A} → stackInvariant key tree tree [] → stackInvariant key tree tree (tree ∷ []) + s-single : {tree tree0 : bt A} → stackInvariant key tree tree0 [] → stackInvariant key tree tree0 (tree ∷ []) s-right : {tree tree0 tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → ¬ (st ≡ []) → stackInvariant key tree tree0 (tree ∷ st) s-left : {tree₁ tree0 tree : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} @@ -162,7 +162,7 @@ si-property-last : {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack : List (bt A)) → ¬ (stack ≡ []) → 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 _) = {!!} +si-property-last key t t0 (t ∷ []) _ (s-single s-nil) = refl si-property-last key t t0 (t ∷ []) _ (s-right _ _ ne) = ⊥-elim ( ne refl ) si-property-last key t t0 (t ∷ []) _ (s-left _ _ ne) = ⊥-elim ( ne refl ) si-property-last key t t0 (.t ∷ x ∷ st) ne (s-right _ si _) with si-property1 key _ _ (x ∷ st) (λ ()) si @@ -185,7 +185,7 @@ stackTreeInvariant : {n : Level} {A : Set n} (key : ℕ) (sub tree : bt A) → (stack : List (bt A)) → treeInvariant tree → stackInvariant key sub tree stack → treeInvariant sub stackTreeInvariant {_} {A} key sub tree [] ti s-nil = ti -stackTreeInvariant {_} {A} key sub tree (sub ∷ []) ti (s-single _ ) = {!!} +stackTreeInvariant {_} {A} key sub tree (sub ∷ []) ti (s-single s-nil ) = ti stackTreeInvariant {_} {A} key sub tree (sub ∷ st) ti (s-right _ si _) = ti-right (si1 si) where si1 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} → stackInvariant key (node key₁ v1 tree₁ sub ) tree st → treeInvariant (node key₁ v1 tree₁ sub ) si1 {tree₁ } {key₁ } {v1 } si = stackTreeInvariant key (node key₁ v1 tree₁ sub ) tree st ti si @@ -237,11 +237,14 @@ findP key leaf tree0 st Pre _ exit = exit leaf tree0 st Pre (case1 refl) 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 {_} {_} {A} key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (tree ∷ st) - ⟪ 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) +findP {n} {_} {A} key (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 + findP0 : key < key₁ → (st : List (bt A)) → stackInvariant key (node key₁ v1 tree tree₁) tree0 st → Set n + findP0 a [] si = stackInvariant key tree0 tree0 (tree0 ∷ []) + findP0 a (x ∷ st) si = stackInvariant key tree tree0 (tree ∷ x ∷ st) + findP1 : (a : key < key₁ ) → (st : List (bt A)) → (si : stackInvariant key (node key₁ v1 tree tree₁) tree0 st) → findP0 a st si findP1 a (x ∷ st) si = s-left a si (λ ()) - findP1 a [] s-nil = {!!} --s-single s-nil + findP1 a [] s-nil = s-single s-nil 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₁)