Mercurial > hg > Members > Moririn

comparison hoareBinaryTree.agda @ 671:b5fde9727830

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use record invariant for replace
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Nov 2021 22:59:08 +0900
parents 0022b7ce7c16
children 3676e845d46f 7421e5c7e56c
comparison
equal deleted inserted replaced
670:0022b7ce7c16 671:b5fde9727830
258 lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥ 258 lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥
259 lemma3 refl () 259 lemma3 refl ()
260 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥ 260 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥
261 lemma5 (s≤s z≤n) () 261 lemma5 (s≤s z≤n) ()
262 262
263 record replacePR {n : Level} {A : Set n} (key : ℕ) (value : A) (tree repl : bt A ) (stack : List (bt A)) (C : bt A → bt A → List (bt A) → Set n) : Set n where
264 field
265 tree0 : bt A
266 ti : treeInvariant tree0
267 si : stackInvariant key tree tree0 stack
268 ri : replacedTree key value (replFromStack si) repl
269 ci : C tree repl stack -- data continuation
270
263 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A) 271 replaceNodeP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → (tree : bt A)
264 → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key ) 272 → (tree ≡ leaf ) ∨ ( node-key tree ≡ just key )
265 → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value tree tree1 → t) → t 273 → (treeInvariant tree ) → ((tree1 : bt A) → treeInvariant tree1 → replacedTree key value tree tree1 → t) → t
266 replaceNodeP k v1 leaf C P next = next (node k v1 leaf leaf) (t-single k v1 ) r-leaf 274 replaceNodeP k v1 leaf C P next = next (node k v1 leaf leaf) (t-single k v1 ) r-leaf
267 replaceNodeP k v1 (node .k value t t₁) (case2 refl) P next = next (node k v1 t t₁) (replaceTree1 k value v1 P) r-node 275 replaceNodeP k v1 (node .k value t t₁) (case2 refl) P next = next (node k v1 t t₁) (replaceTree1 k value v1 P) r-node
268 276
269 replaceP : {n m : Level} {A : Set n} {t : Set m} 277 replaceP : {n m : Level} {A : Set n} {t : Set m}
270 → (key : ℕ) → (value : A) → {tree0 tree : bt A} ( repl : bt A) 278 → (key : ℕ) → (value : A) → {tree : bt A} ( repl : bt A)
271 → (stack : List (bt A)) → treeInvariant tree0 ∧ stackInvariant key tree tree0 stack ∧ replacedTree key value tree repl 279 → (stack : List (bt A)) → replacePR key value tree repl stack (λ _ _ _ → Lift n ⊤)
272 → (next : ℕ → A → {tree0 tree1 : bt A } (repl : bt A) → (stack1 : List (bt A)) 280 → (next : ℕ → A → {tree1 : bt A } (repl : bt A) → (stack1 : List (bt A))
273 → treeInvariant tree0 ∧ stackInvariant key tree1 tree0 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t) 281 → replacePR key value tree1 repl stack1 (λ _ _ _ → Lift n ⊤) → length stack1 < length stack → t)
274 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t 282 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
275 replaceP key value {tree0} {tree} repl [] Pre next exit = ⊥-elim ( si-property0 (proj1 (proj2 Pre)) refl ) -- can't happen 283 replaceP key value {tree} repl [] Pre next exit = ⊥-elim ( si-property0 {!!} refl ) -- can't happen
276 replaceP key value {tree0} {tree} repl (leaf ∷ []) Pre next exit with si-property-last _ _ _ _ (proj1 (proj2 Pre)) -- tree0 ≡ leaf 284 replaceP key value {tree} repl (leaf ∷ []) Pre next exit with si-property-last _ _ _ _ {!!} -- tree0 ≡ leaf
277 ... | refl = exit tree0 (node key value leaf leaf) ⟪ proj1 Pre , r-leaf ⟫ 285 ... | eq = exit {!!} (node key value leaf leaf) ⟪ {!!} , r-leaf ⟫
278 replaceP key value {tree0} {tree} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁ 286 replaceP key value {tree} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁
279 ... | tri< a ¬b ¬c = exit tree0 (node key₁ value₁ repl right ) ⟪ proj1 Pre , subst (λ k → replacedTree key value k _ ) repl01 (r-left a (proj2 (proj2 Pre))) ⟫ where 287 ... | tri< a ¬b ¬c = exit {!!} (node key₁ value₁ repl right ) {!!} where
280 repl01 : node key₁ value₁ tree right ≡ tree0 288 repl01 : node key₁ value₁ tree right ≡ {!!}
281 repl01 with si-property-last _ _ _ _ (proj1 (proj2 Pre)) 289 repl01 with si-property-last _ _ _ _ {!!}
282 ... | refl = {!!} 290 ... | eq = {!!}
283 ... | tri≈ ¬a b ¬c = exit tree0 (node key₁ value left right ) ⟪ proj1 Pre , {!!} ⟫ -- can't happen 291 ... | tri≈ ¬a b ¬c = exit {!!} (node key₁ value left right ) ⟪ {!!} , {!!} ⟫ -- can't happen
284 ... | tri> ¬a ¬b c = exit tree0 (node key₁ value₁ left repl ) ⟪ proj1 Pre , {!!} ⟫ 292 ... | tri> ¬a ¬b c = exit {!!} (node key₁ value₁ left repl ) ⟪ {!!} , {!!} ⟫
285 replaceP {n} {_} {A} key value {tree0} {tree} repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen 293 replaceP {n} {_} {A} key value {tree} repl (leaf ∷ st@(x ∷ xs)) Pre next exit = {!!} -- can't happen
286 replaceP key value {tree0} {tree} repl (node key₁ value₁ left right ∷ st@(_ ∷ _)) Pre next exit with <-cmp key key₁ 294 replaceP key value {tree} repl (node key₁ value₁ left right ∷ st@(_ ∷ _)) Pre next exit with <-cmp key key₁
287 ... | tri< a ¬b ¬c = next key value {tree0} (node key₁ value₁ tree right ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫ ⟫ ≤-refl 295 ... | tri< a ¬b ¬c = next key value {{!!}} (node key₁ value₁ tree right ) st {!!} ≤-refl
288 ... | tri≈ ¬a b ¬c = next key value {tree0} (node key₁ value left right ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫ ⟫ ≤-refl 296 ... | tri≈ ¬a b ¬c = next key value {{!!}} (node key₁ value left right ) st {!!} ≤-refl
289 ... | tri> ¬a ¬b c = next key value {tree0} (node key₁ value₁ left tree ) st ⟪ proj1 Pre , ⟪ {!!} , subst (λ k → replacedTree key value k _ ) {!!} {!!} ⟫ ⟫ ≤-refl 297 ... | tri> ¬a ¬b c = next key value {{!!}} (node key₁ value₁ left tree ) st {!!} ≤-refl
290 298
291 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) 299 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
292 → (r : Index) → (p : Invraiant r) 300 → (r : Index) → (p : Invraiant r)
293 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t 301 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t
294 TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r) 302 TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r)