Mercurial > hg > Members > kono > Proof > galois
comparison FLutil.agda @ 197:57188c35ea1a
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 30 Nov 2020 00:36:01 +0900 |
| parents | 03d40f6e98b1 |
| children | c93a60686dce |
comparison
equal
deleted
inserted
replaced
| 196:ca656da4d484 | 197:57188c35ea1a |
|---|---|
| 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) | |
| 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 | |
| 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) | |
| 311 ... | tri< a₁ ¬b ¬c | [] | record { eq = eq } = ? | |
| 312 ... | tri< a₁ ¬b ¬c | cons a₂ t x₁ | record { eq = eq } = subst (λ k → Any (_≡_ x) k ) {!!} (there {_} {_} {_} {{!!}} {{!!}} {{!!}} any) | |
| 313 ... | tri≈ ¬a b ¬c | t | record { eq = eq }= subst (λ k → Any (_≡_ x) k ) {!!} (here refl) | |
| 314 insAny {suc n} {x} {h} (cons a [] xr) any | tri> ¬a ¬b c | t | record { eq = eq } = {!!} | |
| 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 {!!}) | |
| 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 | |
| 307 AnyFList : {n : ℕ } → (x : FL n ) → Any (x ≡_ ) (∀Flist fmax) | 318 AnyFList : {n : ℕ } → (x : FL n ) → Any (x ≡_ ) (∀Flist fmax) |
| 308 AnyFList {zero} f0 = here refl | 319 AnyFList {zero} f0 = here refl |
| 309 AnyFList {suc zero} (zero :: f0) = here refl | 320 AnyFList {suc zero} (zero :: f0) = here refl |
| 310 AnyFList {suc (suc n)} (x :: y) = subst (λ k → Any (_≡_ (k :: y)) (Flist (suc n) a<sa (∀Flist fmax) (∀Flist fmax) )) | 321 AnyFList {suc (suc n)} (x :: y) = subst (λ k → Any (_≡_ (k :: y)) (Flist (suc n) a<sa (∀Flist fmax) (∀Flist fmax) )) |
| 311 (fromℕ<-toℕ _ _) ( AnyFList1 (suc n) (toℕ x) a<sa (∀Flist fmax) (∀Flist fmax) fin<n fin<n (AnyFList y)) where | 322 (fromℕ<-toℕ _ _) ( AnyFList1 (suc n) (toℕ x) a<sa (∀Flist fmax) (∀Flist fmax) fin<n fin<n (AnyFList y)) where |