Mercurial > hg > Members > kono > Proof > galois

comparison FLutil.agda @ 198:c93a60686dce

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
insAny
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 30 Nov 2020 08:07:55 +0900
parents 57188c35ea1a
children 6c81c3d535d1
comparison
equal deleted inserted replaced
197:57188c35ea1a 198:c93a60686dce
302 302
303 nextAny : {n : ℕ} → {x h : FL n } → {L : FList n} → {hr : fresh (FL n) ⌊ _f<?_ ⌋ h L } → Any (x ≡_ ) L → Any (x ≡_ ) (cons h L hr ) 303 nextAny : {n : ℕ} → {x h : FL n } → {L : FList n} → {hr : fresh (FL n) ⌊ _f<?_ ⌋ h L } → Any (x ≡_ ) L → Any (x ≡_ ) (cons h L hr )
304 nextAny (here x₁) = there (here x₁) 304 nextAny (here x₁) = there (here x₁)
305 nextAny (there any) = there (there any) 305 nextAny (there any) = there (there any)
306 306
307 insAny : {n : ℕ} → {x h : FL n } → (L : FList n) → Any (_≡_ x) L → Any (_≡_ x) (FLinsert h L) 307 insAny : {n : ℕ} → {x h : FL n } → (xs : FList n) → Any (x ≡_ ) xs → Any (x ≡_ ) (FLinsert h xs)
308 insAny {zero} {f0} {f0} (cons a L xr) (here refl) = here refl 308 insAny {zero} {f0} {f0} (cons a L xr) (here refl) = here refl
309 insAny {zero} {f0} {f0} (cons a L xr) (there any) = insAny {zero} {f0} {f0} L any 309 insAny {zero} {f0} {f0} (cons a L xr) (there any) = insAny {zero} {f0} {f0} L any
310 insAny {suc n} {x} {h} (cons a L xr) any with FLcmp h x | FLinsert h (cons a L xr) | inspect (FLinsert h) (cons a L xr) 310 insAny {suc n} {x} {h} (cons a L xr) any with FLcmp h a
311 ... | tri< a₁ ¬b ¬c | [] | record { eq = eq } = ? 311 ... | tri< x<a ¬b ¬c = there any
312 ... | tri< a₁ ¬b ¬c | cons a₂ t x₁ | record { eq = eq } = subst (λ k → Any (_≡_ x) k ) {!!} (there {_} {_} {_} {{!!}} {{!!}} {{!!}} any) 312 ... | tri≈ ¬a b ¬c = any
313 ... | tri≈ ¬a b ¬c | t | record { eq = eq }= subst (λ k → Any (_≡_ x) k ) {!!} (here refl) 313 insAny {suc n} {a} {h} (cons a [] (Level.lift tt)) (here refl) | tri> ¬a ¬b c = here refl
314 insAny {suc n} {x} {h} (cons a [] xr) any | tri> ¬a ¬b c | t | record { eq = eq } = {!!} 314 insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (here refl) | tri> ¬a ¬b c = here refl
315 insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (here x₂) | tri> ¬a ¬b c | t | record { eq = eq } = subst (λ k → Any (_≡_ x) k) {!!} (here {!!}) 315 insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (there any) | tri> ¬a ¬b c = there (insAny (cons a₁ L x₁) any)
316 insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (there any) | tri> ¬a ¬b c | t | record { eq = eq } = subst (λ k → Any (_≡_ x) k) {!!} (there {!!})
317 316
318 AnyFList : {n : ℕ } → (x : FL n ) → Any (x ≡_ ) (∀Flist fmax) 317 AnyFList : {n : ℕ } → (x : FL n ) → Any (x ≡_ ) (∀Flist fmax)
319 AnyFList {zero} f0 = here refl 318 AnyFList {zero} f0 = here refl
320 AnyFList {suc zero} (zero :: f0) = here refl 319 AnyFList {suc zero} (zero :: f0) = here refl
321 AnyFList {suc (suc n)} (x :: y) = subst (λ k → Any (_≡_ (k :: y)) (Flist (suc n) a<sa (∀Flist fmax) (∀Flist fmax) )) 320 AnyFList {suc (suc n)} (x :: y) = subst (λ k → Any (_≡_ (k :: y)) (Flist (suc n) a<sa (∀Flist fmax) (∀Flist fmax) ))