# HG changeset patch # User Shinji KONO # Date 1637473015 -32400 # Node ID 30690aed181902492f3189f370a6ebd5ecb751cb # Parent d0394c191d844c4712b76e1066561c1368458f4a ... diff -r d0394c191d84 -r 30690aed1819 hoareBinaryTree.agda --- a/hoareBinaryTree.agda Sun Nov 21 10:54:13 2021 +0900 +++ b/hoareBinaryTree.agda Sun Nov 21 14:36:55 2021 +0900 @@ -104,7 +104,10 @@ 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-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) ∷ []) + 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) ∷ []) 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)} @@ -120,7 +123,8 @@ replFromStack : {n : Level} {A : Set n} {key : ℕ} {top orig : bt A} → {stack : List (bt A)} → stackInvariant key top orig stack → bt A replFromStack (s-nil {tree} ) = tree -replFromStack (s-single {tree} _ ) = tree +replFromStack (s-right0 {tree} _ _ ) = tree +replFromStack (s-left0 {tree} _ _ ) = tree replFromStack (s-right {tree} x _ st) = tree replFromStack (s-left {tree} x _ st) = tree @@ -147,25 +151,31 @@ stack-last (x ∷ s) = stack-last s stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] ) -stackInvariantTest1 = s-right (add< 2) (s-single s-nil) (λ ()) +stackInvariantTest1 = 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 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-single _) = 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-single _) = 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-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 ... | 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 + 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 ti-right {_} {_} {.leaf} {_} {key₁} {v1} (t-right x ti) = ti @@ -181,7 +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-single _) = 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 ∷ 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 @@ -233,10 +244,11 @@ 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 +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) + findP1 a (x ∷ st) si = s-left a si (λ ()) findP1 a [] s-nil = {!!} - findP1 a (x ∷ st) si = s-left a 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₁)