Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree.agda @ 643:fbd2adb6d9c5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 18 Nov 2021 17:16:07 +0900
parents 6e319e44271b
children a3fb9ffa3d60
comparison
equal deleted inserted replaced
642:6e319e44271b 643:fbd2adb6d9c5
239 replaceP key value tree repl (leaf ∷ st) Pre next exit with si-property1 _ _ _ (proj1 (proj2 Pre)) | rt-property1 _ _ _ _ (proj2 (proj2 Pre)) 239 replaceP key value tree repl (leaf ∷ st) Pre next exit with si-property1 _ _ _ (proj1 (proj2 Pre)) | rt-property1 _ _ _ _ (proj2 (proj2 Pre))
240 ... | refl | t1 = ⊥-elim ( t1 refl ) 240 ... | refl | t1 = ⊥-elim ( t1 refl )
241 replaceP key value tree repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ 241 replaceP key value tree repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁
242 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) (node key₁ value₁ repl right ) st {!!} ≤-refl 242 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) (node key₁ value₁ repl right ) st {!!} ≤-refl
243 ... | tri≈ ¬a b ¬c = exit (node key₁ value₁ left right ) (node key₁ value left right ) ⟪ repl1 , repl3 ⟫ where 243 ... | tri≈ ¬a b ¬c = exit (node key₁ value₁ left right ) (node key₁ value left right ) ⟪ repl1 , repl3 ⟫ where
244 Pre1 : treeInvariant tree ∧ stackInvariant repl tree (node key₁ value₁ left right ∷ st) ∧ replacedTree key value tree repl
245 Pre1 = Pre
246 repleq : repl ≡ node key₁ value₁ left right 244 repleq : repl ≡ node key₁ value₁ left right
247 repleq with si-property1 _ _ _ (proj1 (proj2 Pre)) 245 repleq with si-property1 _ _ _ (proj1 (proj2 Pre))
248 ... | refl = refl 246 ... | refl = refl
249 repl1 : treeInvariant (node key₁ value₁ left right) -- stackInvariant (node key₁ value₁ left right) tree st 247 repl1 : treeInvariant (node key₁ value₁ left right) -- stackInvariant (node key₁ value₁ left right) tree st
250 repl1 = stackTreeInvariant _ _ (node key₁ value₁ left right ∷ st) (proj1 Pre) 248 repl1 = stackTreeInvariant _ _ (node key₁ value₁ left right ∷ st) (proj1 Pre)
251 (subst (λ k → stackInvariant k tree (node key₁ value₁ left right ∷ st)) repleq (proj1 (proj2 Pre))) 249 (subst (λ k → stackInvariant k tree (node key₁ value₁ left right ∷ st)) repleq (proj1 (proj2 Pre)))
252 repl3 : replacedTree key value (node key₁ value₁ left right) (node key₁ value left right) 250 repl3 : replacedTree key value (node key₁ value₁ left right) (node key₁ value left right)
253 repl3 = subst (λ k → replacedTree k value (node key₁ value₁ left right) (node key₁ value left right) ) (sym b) r-node 251 repl3 = subst (λ k → replacedTree k value (node key₁ value₁ left right) (node key₁ value left right) ) (sym b) r-node
254 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) (node key₁ value₁ left repl )st {!!} ≤-refl 252 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) (node key₁ value₁ left repl ) st ⟪ repl2 , ⟪ repl4 , repl5 ⟫ ⟫ ≤-refl where
255 253 Pre1 : treeInvariant tree ∧ stackInvariant repl tree (node key₁ value₁ left right ∷ st) ∧ replacedTree key value tree repl
254 Pre1 = Pre
255 repleq : repl ≡ node key₁ value₁ left right
256 repleq with si-property1 _ _ _ (proj1 (proj2 Pre))
257 ... | refl = refl
258 repl2 : treeInvariant (node key₁ value₁ left tree)
259 repl2 = stackTreeInvariant _ _ (node key₁ value₁ left right ∷ st) (proj1 Pre)
260 (subst (λ k → stackInvariant k tree (node key₁ value₁ left right ∷ st)) {!!} (proj1 (proj2 Pre)))
261 repl4 : stackInvariant (node key₁ value₁ left repl) (node key₁ value₁ left tree) st
262 repl4 = ?
263 repl5 : replacedTree key value (node key₁ value₁ left tree) (node key₁ value₁ left repl)
264 repl5 with r-left c (proj2 (proj2 Pre))
265 ... | t = {!!}
256 open import Relation.Binary.Definitions 266 open import Relation.Binary.Definitions
257 267
258 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ 268 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
259 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x 269 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
260 lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥ 270 lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥