Mercurial > hg > Members > kono > Proof > automaton

changeset 123:f7f0a994daef

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
F2L-iso done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 22 Nov 2019 17:20:12 +0900
parents 8a164a846542
children 0ee5c7f46274
files agda/finiteSet.agda
diffstat 1 files changed, 34 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/agda/finiteSet.agda	Fri Nov 22 15:16:06 2019 +0900
+++ b/agda/finiteSet.agda	Fri Nov 22 17:20:12 2019 +0900
@@ -305,14 +305,24 @@
 ... | no _ = List2Func {Q} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa ) fin t q
 
 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 < 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 {!!})
+F2L-iso {Q} {m} fin x = trans (sym ( F2L=Func2List (List2Func a<sa fin x) a<sa )) (f2l m a<sa x) where
+    F2L : {n  : ℕ } → n < suc m → ( (q : Q) → toℕ (FiniteSet.F←Q fin q ) < n  → Bool ) → Vec Bool n
+    F2L  {zero} _ Q→B = []
+    F2L  {suc n}  (s≤s n<m) Q→B = Q→B (FiniteSet.Q←F fin (fromℕ≤ n<m)) lemma6 ∷ F2L {n} (Data.Nat.Properties.<-trans n<m a<sa ) qb1 where
+       lemma6 : toℕ (FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ≤ n<m))) < suc n
+       lemma6 = subst (λ k → toℕ k < suc n ) (sym (FiniteSet.finiso← fin _ )) (subst (λ k → k < suc n) (sym (toℕ-fromℕ≤ n<m ))  a<sa )
+       qb1 : (q : Q) → toℕ (FiniteSet.F←Q fin q) < n → Bool
+       qb1 q q<n = Q→B q (Data.Nat.Properties.<-trans q<n a<sa)
+    F2L=Func2List : ( qb : Q → Bool )  → {n : ℕ } → ( n<m : n < suc m)  → F2L {n} n<m (λ q _ → qb q ) ≡ Func2List {Q} {n} n<m fin qb
+    F2L=Func2List qb {0} (s≤s z≤n) = refl
+    F2L=Func2List qb {suc n} (s≤s n<m) with qb (FiniteSet.Q←F fin (fromℕ≤ n<m))
+    ... | true = cong ( λ k → true ∷ k ) ( F2L=Func2List qb {n} (Data.Nat.Properties.<-trans n<m a<sa)  )
+    ... | false = cong ( λ k → false ∷ k ) ( F2L=Func2List qb {n} (Data.Nat.Properties.<-trans n<m a<sa)  )
     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 ? where
+    f2l (suc n) (s≤s n<m) (h ∷ t ) = lemma1 lemma2 lemma3 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
@@ -321,13 +331,26 @@
        lemma2 with FiniteSet.F←Q fin (FiniteSet.Q←F fin (fromℕ≤ n<m))  ≟ fromℕ≤ n<m
        lemma2 | yes p = refl
        lemma2 | no ¬p = ⊥-elim ( ¬p lemma )
-       lemma4 : (q : Q ) → List2Func (s≤s n<m) fin (h ∷ t) q ≡ List2Func (Data.Nat.Properties.<-trans n<m a<sa) fin t q
-       lemma4 q with FiniteSet.F←Q fin q ≟ fromℕ≤ n<m 
-       lemma4 q | yes p = {!!}
-       lemma4 q | no ¬p = refl
-       lemma3  : Func2List (Data.Nat.Properties.<-trans n<m a<sa) fin (List2Func (s≤s n<m) fin (h ∷ t)) ≡ t
-       lemma3 = subst (λ k → Func2List (Data.Nat.Properties.<-trans n<m a<sa) fin k ≡ t)
-          (sym (FiniteSet.f-extensionality fin ( λ q → lemma4 q )) ) (f2l n (Data.Nat.Properties.<-trans n<m a<sa ) t)
+       lemma4 : (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → List2Func (s≤s n<m) fin (h ∷ t) q ≡ List2Func (Data.Nat.Properties.<-trans n<m a<sa) fin t q
+       lemma4 q _ with FiniteSet.F←Q fin q ≟ fromℕ≤ n<m 
+       lemma4 q lt | yes p = ⊥-elim ( nat-≡< (toℕ-fromℕ≤ n<m) (lemma5 n lt (cong (λ k → toℕ k) p))) where 
+           lemma5 : {j k : ℕ } → ( n : ℕ) → suc j ≤ n → j ≡ k → k < n
+           lemma5 {zero} (suc n) (s≤s z≤n) refl = s≤s  z≤n
+           lemma5 {suc j} (suc n) (s≤s lt) refl = s≤s (lemma5 {j} n lt refl)
+       lemma4 q _ | no ¬p = refl
+       lemma3 :  F2L (Data.Nat.Properties.<-trans n<m a<sa) (λ q q<n → L2F (s≤s n<m) (h ∷ t) q (Data.Nat.Properties.<-trans q<n a<sa) ) ≡ t
+       lemma3 = begin 
+            F2L (Data.Nat.Properties.<-trans n<m a<sa) (λ q q<n → List2Func (s≤s n<m) fin (h ∷ t) q )
+          ≡⟨ cong (λ k → F2L (Data.Nat.Properties.<-trans n<m a<sa) ( λ q q<n → k q q<n ))
+                 (FiniteSet.f-extensionality fin ( λ q →  
+                 (FiniteSet.f-extensionality fin ( λ q<n →  lemma4 q q<n )))) ⟩
+            F2L (Data.Nat.Properties.<-trans n<m a<sa) (λ q q<n → List2Func (Data.Nat.Properties.<-trans n<m a<sa) fin t q )
+          ≡⟨⟩
+            F2L (Data.Nat.Properties.<-trans n<m a<sa) (L2F (Data.Nat.Properties.<-trans n<m a<sa) t) 
+          ≡⟨ f2l n (Data.Nat.Properties.<-trans n<m a<sa ) t ⟩
+            t
+          ∎  where
+            open ≡-Reasoning
 
 L2F-iso : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q {n}) → (f : Q → Bool ) → (q : Q ) → (List2Func a<sa fin (Func2List a<sa fin f )) q ≡ f q
 L2F-iso {Q} {m} fin f q = l2f m a<sa where