Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree.agda @ 650:11388cab162f

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 Sat, 20 Nov 2021 08:34:59 +0900
parents cc62eb4758b0
children 7b9d35f7c033
comparison
equal deleted inserted replaced
649:cc62eb4758b0 650:11388cab162f
111 111
112 data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree tree1 : bt A ) → Set n where 112 data replacedTree {n : Level} {A : Set n} (key : ℕ) (value : A) : (tree tree1 : bt A ) → Set n where
113 r-leaf : replacedTree key value leaf (node key value leaf leaf) 113 r-leaf : replacedTree key value leaf (node key value leaf leaf)
114 r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁) 114 r-node : {value₁ : A} → {t t₁ : bt A} → replacedTree key value (node key value₁ t t₁) (node key value t t₁)
115 r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A} 115 r-right : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
116 → k > key → replacedTree key value t1 t2 → replacedTree key value (node k v1 t t1) (node k v1 t t2) 116 → k < key → replacedTree key value t1 t2 → replacedTree key value (node k v1 t t1) (node k v1 t t2)
117 r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A} 117 r-left : {k : ℕ } {v1 : A} → {t t1 t2 : bt A}
118 → k < key → replacedTree key value t1 t2 → replacedTree key value (node k v1 t1 t) (node k v1 t2 t) 118 → k > key → replacedTree key value t1 t2 → replacedTree key value (node k v1 t1 t) (node k v1 t2 t)
119 119
120 add< : { i : ℕ } (j : ℕ ) → i < suc i + j 120 add< : { i : ℕ } (j : ℕ ) → i < suc i + j
121 add< {i} j = begin 121 add< {i} j = begin
122 suc i ≤⟨ m≤m+n (suc i) j ⟩ 122 suc i ≤⟨ m≤m+n (suc i) j ⟩
123 suc i + j ∎ where open ≤-Reasoning 123 suc i + j ∎ where open ≤-Reasoning
186 186
187 depth-1< : {i j : ℕ} → suc i ≤ suc (i Data.Nat.⊔ j ) 187 depth-1< : {i j : ℕ} → suc i ≤ suc (i Data.Nat.⊔ j )
188 depth-1< {i} {j} = s≤s (m≤m⊔n _ j) 188 depth-1< {i} {j} = s≤s (m≤m⊔n _ j)
189 189
190 depth-2< : {i j : ℕ} → suc i ≤ suc (j Data.Nat.⊔ i ) 190 depth-2< : {i j : ℕ} → suc i ≤ suc (j Data.Nat.⊔ i )
191 depth-2< {i} {j} = s≤s (m≤n⊔m _ i) 191 depth-2< {i} {j} = s≤s (m≤n⊔m j i)
192 192
193 depth-3< : {i : ℕ } → suc i ≤ suc (suc i) 193 depth-3< : {i : ℕ } → suc i ≤ suc (suc i)
194 depth-3< {zero} = s≤s ( z≤n ) 194 depth-3< {zero} = s≤s ( z≤n )
195 depth-3< {suc i} = s≤s (depth-3< {i} ) 195 depth-3< {suc i} = s≤s (depth-3< {i} )
196 196
236 236
237 open import Relation.Binary.Definitions 237 open import Relation.Binary.Definitions
238 238
239 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ 239 nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥
240 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x 240 nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x
241 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
242 nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
241 lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥ 243 lemma3 : {i j : ℕ} → 0 ≡ i → j < i → ⊥
242 lemma3 refl () 244 lemma3 refl ()
243 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥ 245 lemma5 : {i j : ℕ} → i < 1 → j < i → ⊥
244 lemma5 (s≤s z≤n) () 246 lemma5 (s≤s z≤n) ()
245 247
264 replaceP key value {tree0} {tree} repl (leaf ∷ leaf ∷ st) Pre next exit = ⊥-elim ( repl3 (proj1 (proj2 Pre))) where -- can't happen 266 replaceP key value {tree0} {tree} repl (leaf ∷ leaf ∷ st) Pre next exit = ⊥-elim ( repl3 (proj1 (proj2 Pre))) where -- can't happen
265 repl3 : stackInvariant key tree tree0 (leaf ∷ leaf ∷ st) → ⊥ 267 repl3 : stackInvariant key tree tree0 (leaf ∷ leaf ∷ st) → ⊥
266 repl3 (s-right x ()) 268 repl3 (s-right x ())
267 repl3 (s-left x ()) 269 repl3 (s-left x ())
268 replaceP {_} {_} {A} key value {tree0} {tree} repl (leaf ∷ node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ 270 replaceP {_} {_} {A} key value {tree0} {tree} repl (leaf ∷ node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁
269 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ left repl ) (node key₁ value₁ left tree ∷ st) 271 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) (node key₁ value₁ tree right ∷ st)
270 ⟪ proj1 Pre , ⟪ repl5 (proj1 (proj2 Pre)) , r-right a (proj2 (proj2 Pre)) ⟫ ⟫ {!!} where 272 ⟪ proj1 Pre , ⟪ repl5 (proj1 (proj2 Pre)) , r-left a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl where
271 repl5 : stackInvariant key tree tree0 (leaf ∷ node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ left tree) tree0 (node key₁ value₁ left tree ∷ st ) 273 repl5 : stackInvariant key tree tree0 (leaf ∷ node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ tree right) tree0 (node key₁ value₁ tree right ∷ st )
272 repl5 (s-right x si) with si-property1 _ _ _ _ si 274 repl5 (s-right x si) with si-property1 _ _ _ _ si
273 ... | refl = ⊥-elim ( nat-≤> a {!!} ) 275 ... | refl = ⊥-elim (nat-<> a x)
274 repl5 (s-left x si) with si-property1 _ _ _ _ si 276 repl5 (s-left x si) with si-property1 _ _ _ _ si
275 ... | refl = {!!} -- suc key ≤ key₁ , suc key ≤ key₁ 277 ... | refl = si
276 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right) st {!!} depth-3< 278 ... | tri≈ ¬a b ¬c = next key value (node key₁ value left right) st {!!} depth-3<
277 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right) st {!!} depth-3< 279 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right) st {!!} depth-3<
278 replaceP key value {tree0} {tree} repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁ 280 replaceP key value {tree0} {tree} repl (node key₁ value₁ left right ∷ st) Pre next exit with <-cmp key key₁
279 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right ) st {!!} ≤-refl 281 ... | tri> ¬a ¬b c = next key value (node key₁ value₁ repl right ) st {!!} ≤-refl
280 ... | tri≈ ¬a b ¬c = next key value (node key value left right ) st {!!} ≤-refl where -- this case won't happen 282 ... | tri≈ ¬a b ¬c = next key value (node key value left right ) st {!!} ≤-refl where -- this case won't happen
281 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ left repl) st ⟪ proj1 Pre , ⟪ repl2 (proj1 (proj2 Pre)) , r-right a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl where 283 ... | tri< a ¬b ¬c = next key value (node key₁ value₁ repl right ) st ⟪ proj1 Pre , ⟪ repl2 (proj1 (proj2 Pre)) , r-left a (proj2 (proj2 Pre)) ⟫ ⟫ ≤-refl where
282 repl2 : stackInvariant key tree tree0 (node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ left tree) tree0 st 284 repl2 : stackInvariant key tree tree0 (node key₁ value₁ left right ∷ st) → stackInvariant key (node key₁ value₁ tree right) tree0 st
283 repl2 (s-single .(node key₁ value₁ left right)) = {!!} 285 repl2 (s-single .(node key₁ value₁ left right)) = {!!}
284 repl2 (s-right _ si) = {!!} 286 repl2 (s-right x si) with si-property1 _ _ _ _ si
285 repl2 (s-left _ si) = {!!} 287 ... | eq = {!!}
288 repl2 (s-left x si) with si-property1 _ _ _ _ si
289 ... | eq = ?
286 290
287 291
288 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ) 292 TerminatingLoopS : {l m : Level} {t : Set l} (Index : Set m ) → {Invraiant : Index → Set m } → ( reduce : Index → ℕ)
289 → (r : Index) → (p : Invraiant r) 293 → (r : Index) → (p : Invraiant r)
290 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t 294 → (loop : (r : Index) → Invraiant r → (next : (r1 : Index) → Invraiant r1 → reduce r1 < reduce r → t ) → t) → t