Mercurial > hg > Members > Moririn

comparison hoareBinaryTree.agda @ 683:aeddbe37d9fc

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 Mon, 29 Nov 2021 22:45:33 +0900
parents cae136ce7352
children 33bd83e5168f
comparison
equal deleted inserted replaced
682:cae136ce7352 683:aeddbe37d9fc
291 ... | s-single = refl 291 ... | s-single = refl
292 repl01 : replacedTree key value (replacePR.tree0 Pre) repl 292 repl01 : replacedTree key value (replacePR.tree0 Pre) repl
293 repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre) 293 repl01 with si-property1 (replacePR.si Pre) | si-property-last _ _ _ _ (replacePR.si Pre)
294 repl01 | refl | refl = subst (λ k → replacedTree key value k repl) repl06 (replacePR.ri Pre) 294 repl01 | refl | refl = subst (λ k → replacedTree key value k repl) repl06 (replacePR.ri Pre)
295 replaceP {n} {_} {A} key value {tree} repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen 295 replaceP {n} {_} {A} key value {tree} repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen
296 replaceP {n} {_} {A} key value {tree} repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit with <-cmp key key₁ | si-property1 (replacePR.si Pre) 296 replaceP {n} {_} {A} key value {tree} repl (node key₁ value₁ left right ∷ st@(tree1 ∷ st1)) Pre next exit with <-cmp key key₁
297 ... | tri< a ¬b ¬c | refl = next key value (node key₁ value₁ repl right ) st Post ≤-refl where 297 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st Post ≤-refl where
298 Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤) 298 Post : replacePR key value tree1 (node key₁ value₁ repl right ) st (λ _ _ _ → Lift n ⊤)
299 Post with replacePR.si Pre 299 Post with replacePR.si Pre
300 ... | s-left x t = {!!} -- can't happen 300 ... | s-left x t = {!!} -- can't happen
301 ... | s-right lt si with si-property1 si 301 ... | s-right {_} {_} {tree₁} {key₂} {v1} lt si = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = repl10 ; ri = repl11 ; ci = lift tt } where
302 ... | refl = record { tree0 = replacePR.tree0 Pre ; ti = replacePR.ti Pre ; si = si ; ri = repl04 ; ci = lift tt } where 302 repl09 : tree1 ≡ node key₂ v1 tree₁ (node key₁ value₁ left right)
303 repl07 : { key₂ : ℕ } { v1 : A } { tree₁ tree0 : bt A} { st : List (bt A) } → {lt : key₂ < key } → 303 repl09 = si-property1 si
304 (si1 : stackInvariant key (node key₁ value₁ left right) tree0 (node key₁ value₁ left right ∷ st)) → 304 repl10 : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1)
305 (si : stackInvariant key (node key₂ v1 tree₁ (node key₁ value₁ left right)) tree0 st ) → s-right lt si ≡ si1 → 305 repl10 with si-property1 si
306 node key₁ value₁ left right ≡ child-replaced key value st tree1 tree0 {!!} 306 ... | refl = si
307 repl07 = {!!} 307 repl07 : (si : stackInvariant key tree1 (replacePR.tree0 Pre) (tree1 ∷ st1) )
308 repl05 : s-right lt si ≡ replacePR.si Pre → node key₁ value₁ left right ≡ child-replaced key value st tree1 (replacePR.tree0 Pre) si 308 → node key₁ value₁ (child-replaced key value (node key₁ value₁ left right ∷ tree1 ∷ st1)
309 repl05 eq = repl07 (replacePR.si Pre) si eq 309 (node key₁ value₁ left right) (replacePR.tree0 Pre) (replacePR.si Pre)) right
310 repl02 : node key₁ value₁ (child-replaced key value 310 ≡ child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) si
311 (node key₁ value₁ left right ∷ st ) 311 repl07 s-single = {!!}
312 (node key₁ value₁ left right) (replacePR.tree0 Pre) (replacePR.si Pre)) right 312 repl07 (s-right x si) = refl
313 ≡ child-replaced key value st tree1 (replacePR.tree0 Pre) si 313 repl07 (s-left x si) = {!!}
314 repl02 with replacePR.si Pre 314 repl11 : replacedTree key value (child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) repl10 ) (node key₁ value₁ repl right)
315 ... | s-right x si = repl07 (s-right x si) si refl 315 repl11 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right)) (repl07 repl10) ( r-left a (replacePR.ri Pre))
316 ... | s-left x si = {!!} 316 ... | tri≈ ¬a b ¬c = next key value {{!!}} (node key₁ value left right ) st {!!} ≤-refl -- can't happen
317 repl04 : replacedTree key value (child-replaced key value (tree1 ∷ st1) tree1 (replacePR.tree0 Pre) si) (node key₁ value₁ repl right) 317 ... | tri> ¬a ¬b c = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl
318 repl04 = subst (λ k → replacedTree key value k (node key₁ value₁ repl right)) repl02 (r-left a (replacePR.ri Pre))
319 repl03 : replacedTree key value (child-replaced key value (node key₁ value₁ left right ∷ st) (node key₁ value₁ left right) (replacePR.tree0 Pre) (replacePR.si Pre)) repl
320 repl03 = replacePR.ri Pre
321 ... | tri≈ ¬a b ¬c | refl = next key value {{!!}} (node key₁ value left right ) st {!!} ≤-refl -- can't happen
322 ... | tri> ¬a ¬b c | refl = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl
323 318
324 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) 319 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
325 → (r : Index) → (p : Invraiant r) 320 → (r : Index) → (p : Invraiant r)
326 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t 321 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t
327 TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r) 322 TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r)