Mercurial > hg > Gears > GearsAgda
changeset 652:8c7446829b99
new stack invariant
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 21 Nov 2021 07:23:08 +0900 |
| parents | 7b9d35f7c033 |
| children | a8e7d1f20ce6 |
| files | hoareBinaryTree.agda |
| diffstat | 1 files changed, 45 insertions(+), 25 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree.agda Sat Nov 20 14:24:22 2021 +0900 +++ b/hoareBinaryTree.agda Sun Nov 21 07:23:08 2021 +0900 @@ -102,12 +102,15 @@ → treeInvariant (node key₂ value₂ t₃ t₄) → treeInvariant (node key₁ value₁ (node key value t₁ t₂) (node key₂ value₂ t₃ t₄)) -data stackInvariant {n : Level} {A : Set n} (key : ℕ) : (tree tree0 : bt A) → (stack : List (bt A)) → Set n where - s-single : (tree : bt A) → stackInvariant key tree tree (tree ∷ [] ) - s-right : {tree0 tree tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} - → key₁ < key → stackInvariant key (node key₁ v1 tree tree₁) tree0 st → stackInvariant key tree₁ tree0 (tree₁ ∷ st) - s-left : {tree0 tree tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} - → key < key₁ → stackInvariant key (node key₁ v1 tree tree₁) tree0 st → stackInvariant key tree tree0 (tree ∷ st) +data stackInvariant {n : Level} {A : Set n} (key : ℕ) : (top orig : bt A) → (stack : List (bt A)) → Set n where + s-right0 : {tree₁ tree : bt A} → {key₁ : ℕ } → {v1 : A } + → key₁ > key → stackInvariant key (node key₁ v1 tree tree₁) (node key₁ v1 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₁) (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 → stackInvariant key tree₁ tree0 (tree₁ ∷ st) + s-left : {tree tree0 tree₁ : bt A} → {key₁ : ℕ } → {v1 : A } → {st : List (bt A)} + → key > key₁ → stackInvariant key (node key₁ v1 tree₁ tree) tree0 st → stackInvariant key tree tree0 (tree ∷ st) data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree tree1 : bt A ) → Set n where r-leaf : replacedTree key value leaf (node key value leaf leaf) @@ -117,6 +120,18 @@ r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A} → k > key → replacedTree key value t1 t2 → replacedTree key value (node k v1 t1 t) (node k v1 t2 t) +replFromStack : {n : Level} {A : Set n} {key : ℕ} {top orig : bt A} → {stack : List (bt A)} → stackInvariant key top orig stack → bt A +replFromStack (s-right0 {tree} x) = tree +replFromStack (s-left0 {tree} x) = tree +replFromStack (s-right {tree} x st) = tree +replFromStack (s-left {tree} x st) = tree + +stackInvariant-leaf : {n : Level} {A : Set n} {key : ℕ} {top orig : bt A} → {stack : List (bt A)} → stackInvariant key top orig stack → ¬ (orig ≡ leaf) +stackInvariant-leaf {_} {_} {_} {_} {_} (s-right0 x) () +stackInvariant-leaf {_} {_} {_} {_} {_} (s-left0 x) () +stackInvariant-leaf {_} {_} {_} {_} {_} (s-right x st) eq = stackInvariant-leaf st eq +stackInvariant-leaf {_} {_} {_} {_} {_} (s-left x st) eq = stackInvariant-leaf st eq + add< : { i : ℕ } (j : ℕ ) → i < suc i + j add< {i} j = begin suc i ≤⟨ m≤m+n (suc i) j ⟩ @@ -139,18 +154,20 @@ stack-last (x ∷ []) = just x stack-last (x ∷ s) = stack-last s -stackInvariantTest1 : stackInvariant 2 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] ) -stackInvariantTest1 = s-right (add< 0) (s-single treeTest1 ) +stackInvariantTest1 : stackInvariant 4 treeTest2 treeTest1 ( treeTest2 ∷ treeTest1 ∷ [] ) +stackInvariantTest1 = s-left (add< 2) (s-left0 (add< 2)) 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 (x ∷ .[]) (s-single .x) = refl +si-property1 key t t0 (t ∷ st) (s-right0 _ ) = refl +si-property1 key t t0 (t ∷ st) (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)) → stackInvariant key tree tree0 stack → stack-last stack ≡ just tree0 -si-property-last key t t0 (x ∷ []) (s-single .x) = refl +si-property-last key t t0 (.t ∷ []) (s-right0 _ ) = refl +si-property-last key t t0 (.t ∷ []) (s-left0 _ ) = {!!} 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 @@ -170,11 +187,10 @@ stackTreeInvariant : {n : Level} {A : Set n} (key : ℕ) (repl tree : bt A) → (stack : List (bt A)) → treeInvariant tree → stackInvariant key repl tree stack → treeInvariant repl -stackTreeInvariant key repl .repl .(repl ∷ []) ti (s-single .repl) = ti -stackTreeInvariant {_} {A} key repl tree (repl ∷ st) ti (s-right _ si) = ti-right (si1 si) where +stackTreeInvariant {_} {A} key repl tree (repl ∷ st) ti (s-right _ si) = ti-right (si1 {!!}) where si1 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} → stackInvariant key (node key₁ v1 tree₁ repl) tree st → treeInvariant (node key₁ v1 tree₁ repl) si1 {tree₁ } {key₁ } {v1 } si = stackTreeInvariant key (node key₁ v1 tree₁ repl) tree st ti si -stackTreeInvariant {_} {A} key repl tree (repl ∷ st) ti (s-left _ si) = ti-left ( si2 si ) where +stackTreeInvariant {_} {A} key repl tree (repl ∷ st) ti (s-left _ si) = ti-left ( si2 {!!} ) where si2 : {tree₁ : bt A} → {key₁ : ℕ} → {v1 : A} → stackInvariant key (node key₁ v1 repl tree₁ ) tree st → treeInvariant (node key₁ v1 repl tree₁ ) si2 {tree₁ } {key₁ } {v1 } si = stackTreeInvariant key (node key₁ v1 repl tree₁ ) tree st ti si @@ -224,8 +240,8 @@ findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n tree0 st Pre (case2 refl) findP 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 (proj2 Pre) ⟫ depth-1< where findP1 : key < key₁ → stackInvariant key (node key₁ v1 tree tree₁) tree0 st → stackInvariant key tree tree0 (tree ∷ st) - findP1 a 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< + findP1 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) , {!!} ⟫ 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₁) @@ -260,33 +276,37 @@ replaceP key value {tree0} {tree} {tree-st} repl [] Pre next exit with proj1 (proj2 Pre) ... | () replaceP {_} {_} {A} key value {tree0} {tree} {tree-st} repl (leaf ∷ []) Pre next exit = - exit tree0 repl ⟪ proj1 Pre , subst (λ k → replacedTree key value k repl ) (repl4 (proj1 (proj2 Pre))) {!!} ⟫ where + exit tree0 repl ⟪ proj1 Pre , subst (λ k → replacedTree key value k repl ) {!!} {!!} ⟫ where repl41 : tree-st ≡ tree repl41 = {!!} - repl4 : stackInvariant key tree-st tree0 (leaf ∷ []) → tree-st ≡ tree0 - repl4 (s-single .leaf) = refl replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ leaf ∷ st) Pre next exit = ⊥-elim ( repl3 (proj1 (proj2 Pre))) where -- can't happen repl3 : stackInvariant key tree-st tree0 (leaf ∷ leaf ∷ st) → ⊥ - repl3 (s-right x ()) - repl3 (s-left x ()) + repl3 = {!!} replaceP {_} {_} {A} key value {tree0} {tree} {tree-st} repl (leaf ∷ node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ ... | 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 (s-right x si) with si-property1 _ _ _ _ si - ... | refl = ⊥-elim (nat-<> a x) - repl5 (s-left x si) with si-property1 _ _ _ _ si -- stackInvariant key (node key₁ value₁ leaf right) tree0 (node key₁ value₁ leaf right ∷ st) + repl5 = {!!} + -- ... | refl = ⊥-elim (nat-<> a x) + -- repl5 (s-left x si) with si-property1 _ _ _ _ si -- stackInvariant key (node key₁ value₁ leaf right) tree0 (node key₁ value₁ leaf right ∷ st) -- stackInvariant key (node key₁ value₁ tree right) tree0 (node key₁ value₁ tree right ∷ st) - ... | refl = {!!} -- tree ≡ leaf + -- ... | refl = {!!} -- tree ≡ leaf ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right) st {!!} depth-3< ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right) st {!!} depth-3< replaceP key value {tree0} {tree} {tree-st} repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right ) st {!!} ≤-refl ... | tri≈ ¬a b ¬c = next key value (node key value left right ) st {!!} ≤-refl where -- this case won't happen ... | tri< a ¬b ¬c with proj1 (proj2 Pre) -... | s-single .(node key₁ value₁ left right) = {!!} ... | s-right x si1 = {!!} ... | s-left x si1 = next key value (node key₁ value₁ repl right ) st ⟪ proj1 Pre , ⟪ si1 , r-left a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl +-- = next key value (node key₁ value₁ repl right ) st ⟪ proj1 Pre , ⟪ repl2 (proj1 (proj2 Pre)) , r-left a {!!} ⟫ ⟫ ≤-refl where +-- repl2 : stackInvariant key tree tree0 (node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ left right) tree0 st +-- repl2 (s-single .(node key₁ value₁ left right)) = {!!} +-- repl2 (s-right {_} {_} {_} {key₂} {v1} x si) with si-property1 _ _ _ _ si +-- ... | eq = {!!} +-- repl2 (s-left x si) with si-property1 _ _ _ _ (s-left x si) +-- ... | refl = {!!} + TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) → (r : Index) → (p : Invraiant r)