Mercurial > hg > Gears > GearsAgda
changeset 657:f7090788789b
s-left0
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 21 Nov 2021 14:40:55 +0900 |
parents | 30690aed1819 |
children | be2fd2884eef |
files | hoareBinaryTree.agda |
diffstat | 1 files changed, 10 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree.agda Sun Nov 21 14:36:55 2021 +0900 +++ b/hoareBinaryTree.agda Sun Nov 21 14:40:55 2021 +0900 @@ -105,9 +105,9 @@ 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-right0 : {tree tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } - → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) (node key₁ v1 tree₁ tree) [] → stackInvariant key tree (node key₁ v1 tree₁ tree) (tree ∷ (node key₁ v1 tree₁ tree) ∷ []) + → key₁ < key → stackInvariant key (node key₁ v1 tree₁ tree) (node key₁ v1 tree₁ tree) [] → stackInvariant key tree tree (tree ∷ []) s-left0 : {tree₁ tree : bt A} → {key₁ : ℕ } → {v1 : A } - → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) (node key₁ v1 tree₁ tree) [] → stackInvariant key tree₁ (node key₁ v1 tree₁ tree) (tree₁ ∷ (node key₁ v1 tree₁ tree) ∷ []) + → key < key₁ → stackInvariant key (node key₁ v1 tree₁ tree) (node key₁ v1 tree₁ tree) [] → stackInvariant key tree₁ tree₁ (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)} @@ -151,7 +151,7 @@ stack-last (x ∷ s) = stack-last s stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] ) -stackInvariantTest1 = s-right0 (add< 2) s-nil +stackInvariantTest1 = s-right (add< 2) (s-right0 (add< 2) s-nil) (λ ()) si-nil : {n : Level} {A : Set n} {key : ℕ} {tree tree0 : bt A} → (si : stackInvariant key tree tree0 []) → tree ≡ tree0 si-nil s-nil = refl @@ -159,16 +159,16 @@ si-property1 : {n : Level} {A : Set n} (key : ℕ) (tree tree0 : bt A) → (stack : List (bt A)) → ¬ (stack ≡ []) → 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-right0 _ _) = refl -si-property1 key t t0 (t ∷ _ ∷ []) ne (s-left0 _ _) = refl +si-property1 key t t0 (t ∷ []) ne (s-right0 _ _) = refl +si-property1 key t t0 (t ∷ []) ne (s-left0 _ _) = 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 → 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-left0 _ _) = {!!} -si-property-last key t t0 (t ∷ _ ∷ []) _ (s-right0 _ _) = {!!} +si-property-last key t t0 (t ∷ []) _ (s-left0 _ _) = {!!} +si-property-last key t t0 (t ∷ []) _ (s-right0 _ _) = {!!} 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 @@ -191,8 +191,8 @@ 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-left0 _ _) = {!!} -stackTreeInvariant {_} {A} key sub tree (sub ∷ _ ∷ []) ti (s-right0 _ _) = {!!} +stackTreeInvariant {_} {A} key sub tree (sub ∷ []) ti (s-left0 _ _) = {!!} +stackTreeInvariant {_} {A} key sub tree (sub ∷ []) ti (s-right0 _ _) = {!!} 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 @@ -248,7 +248,7 @@ ⟪ 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 (x ∷ st) si = s-left a si (λ ()) - findP1 a [] s-nil = {!!} + findP1 a [] s-nil = ? -- s-left0 a 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₁)