Mercurial > hg > Members > Moririn

comparison hoareBinaryTree.agda @ 664:1f702351fd1f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
findP done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 Nov 2021 08:24:21 +0900
parents cf5095488bbd
children 1708fe988ac5
comparison
equal deleted inserted replaced
663:cf5095488bbd 664:1f702351fd1f
63 replaceNode k v1 leaf next = next (node k v1 leaf leaf) 63 replaceNode k v1 leaf next = next (node k v1 leaf leaf)
64 replaceNode k v1 (node key value t t₁) next = next (node k v1 t t₁) 64 replaceNode k v1 (node key value t t₁) next = next (node k v1 t t₁)
65 65
66 replace : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → List (bt A) → (next : ℕ → A → bt A → List (bt A) → t ) → (exit : bt A → t) → t 66 replace : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (value : A) → bt A → List (bt A) → (next : ℕ → A → bt A → List (bt A) → t ) → (exit : bt A → t) → t
67 replace key value tree [] next exit = exit tree 67 replace key value tree [] next exit = exit tree
68 replace key value tree (leaf ∷ _) next exit = exit (node key value leaf leaf) 68 replace key value tree (leaf ∷ []) next exit = exit (node key value leaf leaf)
69 replace key value tree (node key₁ value₁ left right ∷ []) next exit with <-cmp key key₁
70 ... | tri< a ¬b ¬c = exit (node key₁ value₁ tree right )
71 ... | tri≈ ¬a b ¬c = exit (node key₁ value left right )
72 ... | tri> ¬a ¬b c = exit (node key₁ value₁ left tree )
73 replace key value tree (leaf ∷ st) next exit = next key value (node key value leaf leaf) st
69 replace key value tree (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁ 74 replace key value tree (node key₁ value₁ left right ∷ st) next exit with <-cmp key key₁
70 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) st 75 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ tree right ) st
71 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st 76 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right ) st
72 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) st 77 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ left tree ) st
73 78
212 treeRightDown {n} {A} {_} {v1} .leaf .leaf (t-single _ .v1) = t-leaf 217 treeRightDown {n} {A} {_} {v1} .leaf .leaf (t-single _ .v1) = t-leaf
213 treeRightDown {n} {A} {_} {v1} .leaf .(node _ _ _ _) (t-right x ti) = ti 218 treeRightDown {n} {A} {_} {v1} .leaf .(node _ _ _ _) (t-right x ti) = ti
214 treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .leaf (t-left x ti) = t-leaf 219 treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .leaf (t-left x ti) = t-leaf
215 treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node x x₁ ti ti₁) = ti₁ 220 treeRightDown {n} {A} {_} {v1} .(node _ _ _ _) .(node _ _ _ _) (t-node x x₁ ti ti₁) = ti₁
216 221
222 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
223 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
224 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
225 nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
217 226
218 open _∧_ 227 open _∧_
219 228
220 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A)) 229 findP : {n m : Level} {A : Set n} {t : Set m} → (key : ℕ) → (tree tree0 : bt A ) → (stack : List (bt A))
221 → treeInvariant tree ∧ stackInvariant key tree tree0 stack 230 → treeInvariant tree ∧ stackInvariant key tree tree0 stack
223 → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack 232 → (exit : (tree1 tree0 : bt A) → (stack : List (bt A)) → treeInvariant tree1 ∧ stackInvariant key tree1 tree0 stack
224 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t 233 → (tree1 ≡ leaf ) ∨ ( node-key tree1 ≡ just key ) → t ) → t
225 findP key leaf tree0 st Pre _ exit = exit leaf tree0 st Pre (case1 refl) 234 findP key leaf tree0 st Pre _ exit = exit leaf tree0 st Pre (case1 refl)
226 findP key (node key₁ v1 tree tree₁) tree0 st Pre next exit with <-cmp key key₁ 235 findP key (node key₁ v1 tree tree₁) tree0 st Pre next exit with <-cmp key key₁
227 findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n tree0 st Pre (case2 refl) 236 findP key n tree0 st Pre _ exit | tri≈ ¬a refl ¬c = exit n tree0 st Pre (case2 refl)
228 findP {n} {_} {A} key nd@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (tree ∷ st) 237 findP {n} {_} {A} key (node key₁ v1 tree tree₁) tree0 st Pre next _ | tri< a ¬b ¬c = next tree tree0 (tree ∷ st)
229 ⟪ treeLeftDown tree tree₁ (proj1 Pre) , findP1 a st (proj2 Pre) ⟫ depth-1< where 238 ⟪ treeLeftDown tree tree₁ (proj1 Pre) , findP1 a st (proj2 Pre) ⟫ depth-1< where
230 findP1 : key < key₁ → (st : List (bt A)) → stackInvariant key (node key₁ v1 tree tree₁) tree0 st → stackInvariant key tree tree0 (tree ∷ st) 239 findP1 : key < key₁ → (st : List (bt A)) → stackInvariant key (node key₁ v1 tree tree₁) tree0 st → stackInvariant key tree tree0 (tree ∷ st)
231 findP1 a .(node key₁ v1 tree tree₁ ∷ []) s-single = {!!} 240 findP1 a (x ∷ st) si = s-left a si
232 findP1 a .(node key₁ v1 tree tree₁ ∷ _) (s-right x si) = {!!}
233 findP1 a .(node key₁ v1 tree tree₁ ∷ _) (s-left x si) = {!!}
234 findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (tree₁ ∷ st) ⟪ treeRightDown tree tree₁ (proj1 Pre) , s-right c (proj2 Pre) ⟫ depth-2< 241 findP key n@(node key₁ v1 tree tree₁) tree0 st Pre next _ | tri> ¬a ¬b c = next tree₁ tree0 (tree₁ ∷ st) ⟪ treeRightDown tree tree₁ (proj1 Pre) , s-right c (proj2 Pre) ⟫ depth-2<
235 242
236 replaceTree1 : {n : Level} {A : Set n} {t t₁ : bt A } → ( k : ℕ ) → (v1 value : A ) → treeInvariant (node k v1 t t₁) → treeInvariant (node k value t t₁) 243 replaceTree1 : {n : Level} {A : Set n} {t t₁ : bt A } → ( k : ℕ ) → (v1 value : A ) → treeInvariant (node k v1 t t₁) → treeInvariant (node k value t t₁)
237 replaceTree1 k v1 value (t-single .k .v1) = t-single k value 244 replaceTree1 k v1 value (t-single .k .v1) = t-single k value
238 replaceTree1 k v1 value (t-right x t) = t-right x t 245 replaceTree1 k v1 value (t-right x t) = t-right x t
239 replaceTree1 k v1 value (t-left x t) = t-left x t 246 replaceTree1 k v1 value (t-left x t) = t-left x t
240 replaceTree1 k v1 value (t-node x x₁ t t₁) = t-node x x₁ t t₁ 247 replaceTree1 k v1 value (t-node x x₁ t t₁) = t-node x x₁ t t₁
241 248
242 open import Relation.Binary.Definitions 249 open import Relation.Binary.Definitions
243 250
244 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
245 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
246 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
247 nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
248 lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥ 251 lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥
249 lemma3 refl () 252 lemma3 refl ()
250 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥ 253 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥
251 lemma5 (s≤s z≤n) () 254 lemma5 (s≤s z≤n) ()
252 255
260 → (key : ℕ) → (value : A) → {tree0 tree tree-st : bt A} ( repl : bt A) 263 → (key : ℕ) → (value : A) → {tree0 tree tree-st : bt A} ( repl : bt A)
261 → (stack : List (bt A)) → treeInvariant tree0 ∧ stackInvariant key tree-st tree0 stack ∧ replacedTree key value tree repl 264 → (stack : List (bt A)) → treeInvariant tree0 ∧ stackInvariant key tree-st tree0 stack ∧ replacedTree key value tree repl
262 → (next : ℕ → A → {tree0 tree1 tree-st : bt A } (repl : bt A) → (stack1 : List (bt A)) 265 → (next : ℕ → A → {tree0 tree1 tree-st : bt A } (repl : bt A) → (stack1 : List (bt A))
263 → treeInvariant tree0 ∧ stackInvariant key tree-st tree0 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t) 266 → treeInvariant tree0 ∧ stackInvariant key tree-st tree0 stack1 ∧ replacedTree key value tree1 repl → length stack1 < length stack → t)
264 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t 267 → (exit : (tree1 repl : bt A) → treeInvariant tree1 ∧ replacedTree key value tree1 repl → t) → t
265 replaceP key value {tree0} {tree} {tree-st} repl [] Pre next exit with proj1 (proj2 Pre) 268 replaceP key value {tree0} {tree} {tree-st} repl [] Pre next exit = {!!} -- can't happen
266 ... | t = {!!} 269 replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ []) Pre next exit = exit tree0 (node key value leaf leaf) ?
267 replaceP {_} {_} {A} key value {tree0} {tree} {tree-st} repl (leaf ∷ []) Pre next exit with proj1 (proj2 Pre) 270 replaceP key value {tree0} {tree} {tree-st} repl (node key₁ value₁ left right ∷ []) Pre next exit with <-cmp key key₁
268 ... | s-single = {!!} 271 ... | tri< a ¬b ¬c = exit tree0 (node key₁ value₁ tree right ) ?
269 ... | s-right x t = {!!} 272 ... | tri≈ ¬a b ¬c = exit tree0 (node key₁ value left right ) ?
270 ... | s-left x t = {!!} 273 ... | tri> ¬a ¬b c = exit tree0 (node key₁ value₁ left tree ) ?
271 replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ leaf ∷ st) Pre next exit with proj1 (proj2 Pre) 274 replaceP key value {tree0} {tree} {tree-st} repl (leaf ∷ st@(_ ∷ _)) Pre next exit = {!!} -- exit (node key value leaf leaf)
272 ... | s-right x t = {!!} 275 replaceP key value {tree0} {tree} {tree-st} repl (node key₁ value₁ left right ∷ st@(_ ∷ _)) Pre next exit with <-cmp key key₁
273 ... | s-left x t = {!!} 276 ... | tri< a ¬b ¬c = next key value {tree0} (node key₁ value₁ tree right ) st ? ≤-refl
274 replaceP {_} {_} {A} key value {tree0} {tree} {tree-st} repl (leaf ∷ node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ 277 ... | tri≈ ¬a b ¬c = next key value {tree0} (node key₁ value left right ) st ? ≤-refl
275 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) (node key₁ value₁ tree right ∷ st) 278 ... | tri> ¬a ¬b c = next key value {tree0} (node key₁ value₁ left tree ) st ? ≤-refl
276 ⟪ proj1 Pre , ⟪ repl5 (proj1 (proj2 Pre)) , r-left a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl where
277 repl5 : stackInvariant key tree-st tree0 (leaf ∷ node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ tree right) tree0 (node key₁ value₁ tree right ∷ st )
278 repl5 si with si-property1 _ _ _ {!!} si
279 repl5 (s-right x si ) | refl = s-left a {!!}
280 repl5 (s-left x si ) | refl = s-left a {!!}
281 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right) st {!!} depth-3<
282 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right) st {!!} depth-3<
283 replaceP key value {tree0} {tree} {tree-st} repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁
284 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right ) st {!!} ≤-refl
285 ... | tri≈ ¬a b ¬c = next key value (node key value left right ) st {!!} ≤-refl where -- this case won't happen
286 ... | tri< a ¬b ¬c with proj1 (proj2 Pre)
287 ... | s-single = {!!}
288 ... | s-right x si1 = {!!}
289 ... | s-left x si1 = next key value (node key₁ value₁ repl right ) st ⟪ proj1 Pre , ⟪ si1 , r-left a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl
290 -- = next key value (node key₁ value₁ repl right ) st ⟪ proj1 Pre , ⟪ repl2 (proj1 (proj2 Pre)) , r-left a {!!} ⟫ ⟫ ≤-refl where
291 -- repl2 : stackInvariant key tree tree0 (node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ left right) tree0 st
292 -- repl2 (s-single .(node key₁ value₁ left right)) = {!!}
293 -- repl2 (s-right {_} {_} {_} {key₂} {v1} x si) with si-property1 _ _ _ _ si
294 -- ... | eq = {!!}
295 -- repl2 (s-left x si) with si-property1 _ _ _ _ (s-left x si)
296 -- ... | refl = {!!}
297
298 279
299 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) 280 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
300 → (r : Index) → (p : Invraiant r) 281 → (r : Index) → (p : Invraiant r)
301 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t 282 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t
302 TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r) 283 TerminatingLoopS {_} {_} {t} Index {Invraiant} reduce r p loop with <-cmp 0 (reduce r)