Mercurial > hg > Members > kono > Proof > automaton

comparison agda/finiteSet.agda @ 135:2d70f90565c6

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 Sun, 24 Nov 2019 15:40:37 +0900
parents 14cf0e1c8d91
children 7c8460329f27
comparison
equal deleted inserted replaced
134:14cf0e1c8d91 135:2d70f90565c6
380 lemma = FiniteSet.f-extensionality fin ( λ q → L2F-iso fin x q ) 380 lemma = FiniteSet.f-extensionality fin ( λ q → L2F-iso fin x q )
381 381
382 382
383 open import Data.Product 383 open import Data.Product
384 384
385 Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n) {n}
386 Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl }
387
388 data f-1 { n m : ℕ } { A : Set } (n<m : n < m ) (fa : FiniteSet A {m}) : Set where
389 elm1 : (elm : A ) → toℕ (FiniteSet.F←Q fa elm ) < n → f-1 n<m fa
390
391 -- f-1-cong : { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m})
392 -- → ( elm s ≡ elm t) → ( elm<n s ≅ elm<n t ) → elm1 e0 e0<n ≡ elm1 e1 e1<n
393 -- f-1-<-cong n<m fa _ _ refl HE.refl = refl
394
395 fin-<' : {A : Set} → { n m : ℕ } → (n<m : n < m ) → (fa : FiniteSet A {m}) → FiniteSet (f-1 n<m fa) {n}
396 fin-<' {A} {n} {m} n<m fa = iso-fin (Fin2Finite n) iso where
397 iso : ISO (Fin n) (f-1 n<m fa)
398 ISO.A←B iso (elm1 elm x) = fromℕ≤ x
399 ISO.B←A iso x = elm1 (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans x<n n<m ))) to<n where
400 x<n : toℕ x < n
401 x<n = toℕ<n x
402 to<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans x<n n<m)))) < n
403 to<n = subst (λ k → toℕ k < n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k < n ) (sym ( toℕ-fromℕ≤ (Data.Nat.Properties.<-trans x<n n<m) )) x<n )
404 ISO.iso← iso x = lemma2 where
405 lemma2 : fromℕ≤ (subst (λ k → toℕ k < n) (sym
406 (FiniteSet.finiso← fa (fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n)
407 (sym (toℕ-fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n x) n<m))) (toℕ<n x))) ≡ x
408 lemma2 = {!!}
409 ISO.iso→ iso (elm1 elm x) = lemma1 where
410 lemma : FiniteSet.Q←F fa (fromℕ≤ (Data.Nat.Properties.<-trans (toℕ<n (ISO.A←B iso (elm1 elm x))) n<m)) ≡ elm
411 lemma = {!!}
412 lemma1 : ISO.B←A iso (ISO.A←B iso (elm1 elm x)) ≡ elm1 elm x
413 lemma1 with lemma
414 ... | eq = {!!}
415
416
385 record Fin-< { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m}) : Set where 417 record Fin-< { n m : ℕ } (n<m : n < m ) { A : Set } (fa : FiniteSet A {m}) : Set where
386 field 418 field
387 elm : A 419 elm : A
388 elm<n : toℕ (FiniteSet.F←Q fa elm ) < n 420 elm<n : toℕ (FiniteSet.F←Q fa elm ) < n
389 421