Mercurial > hg > Gears > GearsAgda
changeset 633:119f340c0b10
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 11 Nov 2021 15:57:19 +0900 |
| parents | b58991f8e2e4 |
| children | 189cf03bda5f |
| files | hoareBinaryTree.agda |
| diffstat | 1 files changed, 12 insertions(+), 5 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree.agda Thu Nov 11 15:48:36 2021 +0900 +++ b/hoareBinaryTree.agda Thu Nov 11 15:57:19 2021 +0900 @@ -138,6 +138,17 @@ depth-2< : {i j : ℕ} → suc i ≤ suc (j Data.Nat.⊔ i ) depth-2< {i} {j} = s≤s (m≤n⊔m _ i) +lemma11 : {n : Level} {A : Set n} {v1 : A} → (key key₁ : ℕ) → (tree tree₁ : bt A ) + → key < key₁ + → treeInvariant (node key₁ v1 tree tree₁) + → treeInvariant tree +lemma11 = {!!} + +-- stackInvariant key (node key₁ v1 tree tree₁) tree0 st +-- → stackInvariant key tree tree0 (node key₁ v1 tree tree₁ ∷ st) + +open _∧_ + findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A)) → treeInvariant tree ∧ stackInvariant key tree tree0 stack → (next : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack → bt-depth tree1 < bt-depth tree → t ) @@ -145,12 +156,8 @@ findP key leaf tree0 st Pre _ exit = exit leaf tree0 st Pre 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 b ¬c = exit n tree0 st Pre -findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (n ∷ st) {!!} depth-1< +findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (n ∷ st) ⟪ lemma11 {!!} {!!} {!!} {!!} {!!} (proj1 Pre) , {!!} ⟫ depth-1< findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (n ∷ st) {!!} depth-2< --- Pre : treeInvariant (node key₁ v1 tree tree₁) --- → treeInvariant tree ∧ --- stackInvariant key (node key₁ v1 tree tree₁) tree0 st -- → stackInvariant key tree tree0 (node key₁ v1 tree tree₁ ∷ st) replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A) → (treeInvariant tree )