Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree.agda @ 646:83ba41589564

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
.......>>>>>>>>..............>>>>>..........ZZ
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 19 Nov 2021 16:59:44 +0900
parents 6340956f143e
children 7b24e17e1441
comparison
equal deleted inserted replaced
645:6340956f143e 646:83ba41589564
241 → (next : ℕ → A → {tree0 tree1 : bt A } (repl : bt A) → (stack1 : List (bt A)) 241 → (next : ℕ → A → {tree0 tree1 : bt A } (repl : bt A) → (stack1 : List (bt A))
242 → treeInvariant tree0 ∧ stackInvariant key tree1 tree0 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t) 242 → treeInvariant tree0 ∧ stackInvariant key tree1 tree0 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t)
243 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t 243 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
244 replaceP key value {tree0} {tree} repl [] Pre next exit with proj1 (proj2 Pre) 244 replaceP key value {tree0} {tree} repl [] Pre next exit with proj1 (proj2 Pre)
245 ... | () 245 ... | ()
246 replaceP key value {tree0} {tree} repl (leaf ∷ st) Pre next exit = {!!} 246 replaceP key value {tree0} {tree} repl (leaf ∷ st) Pre next exit =
247 exit tree0 repl ⟪ proj1 Pre , subst (λ k → replacedTree key value k repl ) (si-property0 (proj1 (proj2 Pre))) (proj2 (proj2 Pre)) ⟫
247 replaceP key value {tree0} {tree} repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ 248 replaceP key value {tree0} {tree} repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁
248 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right ) st {!!} ≤-refl 249 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right ) st {!!} ≤-refl
249 ... | tri≈ ¬a b ¬c = next key value (node key value left right ) st {!!} ≤-refl where -- this case won't happen 250 ... | tri≈ ¬a b ¬c = next key value (node key value left right ) st {!!} ≤-refl where -- this case won't happen
250 repleq : tree0 ≡ node key₁ value₁ left right 251 repleq : tree0 ≡ node key₁ value₁ left right
251 repleq with si-property1 _ _ _ _ (proj1 (proj2 Pre)) 252 repleq with si-property1 _ _ _ _ (proj1 (proj2 Pre))