Mercurial > hg > Members > kono > Proof > automaton
changeset 122:8a164a846542
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 22 Nov 2019 15:16:06 +0900 |
| parents | ee43fecd3f34 |
| children | f7f0a994daef |
| files | agda/finiteSet.agda |
| diffstat | 1 files changed, 6 insertions(+), 10 deletions(-) [+] |
line wrap: on
line diff
--- a/agda/finiteSet.agda Thu Nov 21 18:34:22 2019 +0900 +++ b/agda/finiteSet.agda Fri Nov 22 15:16:06 2019 +0900 @@ -306,17 +306,13 @@ F2L-iso : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q {n}) → (x : Vec Bool n ) → Func2List a<sa fin (List2Func a<sa fin x ) ≡ x F2L-iso {Q} {m} fin x = f2l m a<sa x where - f2l : (n : ℕ ) → (n<m : n < suc m )→ (x : Vec Bool n ) → Func2List n<m fin (List2Func n<m fin x ) ≡ x + F2L : {n : ℕ } → n < suc m → ( (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → Bool ) → Vec Bool n + F2L {n} n<m qf = Func2List n<m fin (λ q → qf q {!!}) + L2F : {n : ℕ } → n < suc m → Vec Bool n → (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → Bool + L2F n<m x q q<n = List2Func n<m fin x q + f2l : (n : ℕ ) → (n<m : n < suc m )→ (x : Vec Bool n ) → F2L n<m (λ q q<n → L2F n<m x q q<n ) ≡ x f2l zero (s≤s z≤n) [] = refl - f2l (suc n) (s≤s n<m) (h ∷ t ) = lemma1 lemma2 lemma3 where - lemma0 : (h : Bool ) → (t : Vec Bool n ) → (q : Q ) → Set - lemma0 h t q with FiniteSet.F←Q fin q ≟ fromℕ≤ n<m - ... | yes p = List2Func (s≤s n<m ) fin ( h ∷ t ) q ≡ h - ... | no ¬p = List2Func (s≤s n<m ) fin ( h ∷ t ) q ≡ List2Func (Data.Nat.Properties.<-trans n<m a<sa) fin t q - lemma00 : (q : Q ) → lemma0 h t q - lemma00 q with FiniteSet.F←Q fin q ≟ fromℕ≤ n<m - ... | yes p = {!!} - ... | no ¬p = {!!} + f2l (suc n) (s≤s n<m) (h ∷ t ) = lemma1 lemma2 ? where lemma : FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ≤ n<m)) ≡ fromℕ≤ n<m lemma = FiniteSet.finiso← fin _ lemma1 : {n : ℕ } → {h h1 : Bool } → {t t1 : Vec Bool n } → h ≡ h1 → t ≡ t1 → h ∷ t ≡ h1 ∷ t1