Mercurial > hg > Members > kono > Proof > galois

comparison FLutil.agda @ 199:6c81c3d535d1

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 Mon, 30 Nov 2020 10:13:22 +0900
parents c93a60686dce
children b5b4ee29cbe4
comparison
equal deleted inserted replaced
198:c93a60686dce 199:6c81c3d535d1
320 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) ))
321 (fromℕ<-toℕ _ _) ( AnyFList1 (suc n) (toℕ x) a<sa (∀Flist fmax) (∀Flist fmax) fin<n fin<n (AnyFList y)) where 321 (fromℕ<-toℕ _ _) ( AnyFList1 (suc n) (toℕ x) a<sa (∀Flist fmax) (∀Flist fmax) fin<n fin<n (AnyFList y)) where
322 AnyFList1 : (i x : ℕ) → (i<n : i < suc (suc n) ) → (L L1 : FList (suc n) ) → (x<n : x < suc (suc n) ) → x < suc i → Any (y ≡_ ) L 322 AnyFList1 : (i x : ℕ) → (i<n : i < suc (suc n) ) → (L L1 : FList (suc n) ) → (x<n : x < suc (suc n) ) → x < suc i → Any (y ≡_ ) L
323 → Any (((fromℕ< x<n) :: y) ≡_ ) (Flist i i<n L L1) 323 → Any (((fromℕ< x<n) :: y) ≡_ ) (Flist i i<n L L1)
324 AnyFList1 zero x i<n [] L1 (s≤s x<i) _ () 324 AnyFList1 zero x i<n [] L1 (s≤s x<i) _ ()
325 AnyFList1 zero zero i<n (cons a L xr) L1 x<n (s≤s z≤n) (here refl) = x∈FLins (zero :: a) (Flist 0 i<n L L1) 325 AnyFList1 zero zero i<n (cons y L xr) L1 x<n (s≤s z≤n) (here refl) = x∈FLins (zero :: y) (Flist 0 i<n L L1)
326 AnyFList1 zero zero i<n (cons a L xr) L1 x<n (s≤s z≤n) (there wh) with AnyFList1 zero zero i<n L L1 x<n (s≤s z≤n) wh 326 AnyFList1 zero zero i<n (cons a L xr) L1 x<n (s≤s z≤n) (there wh) = insAny _ (AnyFList1 zero zero i<n L L1 x<n (s≤s z≤n) wh)
327 ... | t = {!!} 327 AnyFList1 (suc i) x (s≤s i<n) (cons y L x₁) L1 x<n (s≤s x<i) (here refl) with <-fcmp (fromℕ< x<n) (fromℕ< (s≤s i<n))
328 AnyFList1 (suc i) x i<n L L1 x<n x<i wh = {!!} 328 ... | tri< a ¬b ¬c = insAny _ af1 where
329 af1 : Any (_≡_ (fromℕ< x<n :: y)) (Flist (suc i) (s≤s i<n) L L1)
330 af1 = AnyFList1 (suc i) x (s≤s i<n) L L1 x<n (s≤s x<i) {!!}
331 ... | tri≈ ¬a b ¬c = subst (λ k → Any (_≡_ (fromℕ< x<n :: y)) (FLinsert k (Flist (suc i) (s≤s i<n) L L1) )) (cong (λ k → k :: y) b)
332 (x∈FLins (fromℕ< x<n :: y) (Flist (suc i) (s≤s i<n) L L1))
333 ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> x<i (subst₂ (λ j k → suc (suc k) ≤ j ) (toℕ-fromℕ< _) (toℕ-fromℕ< _) c) )
334 AnyFList1 (suc i) x i<n (cons a L x₁) L1 x<n (s≤s x<i) (there wh) = {!!}
329 335
330 -- FLinsert membership 336 -- FLinsert membership
331 337
332 module FLMB { n : ℕ } where 338 module FLMB { n : ℕ } where
333 339