# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574427737 -32400
# Node ID a79e2c2e1642269c5e681a56ab513d28b6599669
# Parent  d0dbdc01664db77b79c9a20a81d94c37ff3c340a
finite done

diff -r d0dbdc01664d -r a79e2c2e1642 agda/finiteSet.agda
--- a/agda/finiteSet.agda	Fri Nov 22 19:30:10 2019 +0900
+++ b/agda/finiteSet.agda	Fri Nov 22 22:02:17 2019 +0900
@@ -357,13 +357,50 @@
        lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl = subst ( λ k → suc f ≡ k ) (sym (lemma3 n<m) ) ( cong ( λ k → suc k ) ( lemma12 {n} {m} n<m f refl  ) )
     l2f :  (n : ℕ ) → (n<m : n < suc m ) → (q<n : toℕ (FiniteSet.F←Q fin q ) < n )  →  (L2F n<m fin (F2L n<m  fin (λ q _ → f q))) q q<n ≡ f q
     l2f zero (s≤s z≤n) ()
-    l2f (suc n) (s≤s n<m) (s≤s n<q) with FiniteSet.F←Q fin q ≟ fromℕ≤ n<m
-    l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p with f q
-    l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p | true = refl -- f (FiniteSet.Q←F fin (fromℕ≤ n<m)) !=< true
-    l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p | false = {!!}
-    --         {!!}
-    --      ≡⟨ {!!}  ⟩
-    --        f q
-    --      ∎  where
-    --        open ≡-Reasoning
+    l2f (suc n) (s≤s n<m) (s≤s n<q) with FiniteSet.F←Q fin q ≟ fromℕ≤ n<m 
+    l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p with inspect f q
+    l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p | record { eq = refl } = begin 
+             f (FiniteSet.Q←F fin (fromℕ≤ n<m)) 
+          ≡⟨ cong ( λ k → f (FiniteSet.Q←F fin k )) (sym p)  ⟩
+             f (FiniteSet.Q←F fin ( FiniteSet.F←Q fin q ))
+          ≡⟨ cong ( λ k → f k ) (FiniteSet.finiso→ fin _ ) ⟩
+             f q 
+          ∎  where
+            open ≡-Reasoning
     l2f (suc n) (s≤s n<m) (s≤s n<q) | no ¬p = l2f n (Data.Nat.Properties.<-trans n<m a<sa) (lemma11 n<m ¬p n<q)
+
+fin→ : {A : Set} → { a : ℕ } → FiniteSet A {a} → FiniteSet (A → Bool ) {exp 2 a}
+fin→ {A} {a} fin = iso-fin fin2List iso where
+    iso : ISO (Vec Bool a ) (A → Bool)
+    ISO.A←B iso x = F2L a<sa fin ( λ q _ → x q )
+    ISO.B←A iso x = List2Func a<sa fin x 
+    ISO.iso← iso x  =  F2L-iso fin x 
+    ISO.iso→ iso x = lemma where
+       lemma : List2Func a<sa fin (F2L a<sa fin (λ q _ → x q)) ≡ x
+       lemma = FiniteSet.f-extensionality fin ( λ q → L2F-iso fin x q )
+    
+
+open import Data.Product
+
+fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b}
+fin-× {A} {B} {a} {b} fa fb with FiniteSet→Fin fa
+... | a=f = iso-fin (fin-×-f a ) iso-1 where
+   iso-1 : ISO (Fin a × B) ( A × B )
+   ISO.A←B iso-1 x = ( FiniteSet.F←Q fa (proj₁ x)  , proj₂ x) 
+   ISO.B←A iso-1 x = ( FiniteSet.Q←F fa (proj₁ x)  , proj₂ x) 
+   ISO.iso← iso-1 x  =  lemma  where
+      lemma : (FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj₁ x)) , proj₂ x) ≡ ( proj₁ x , proj₂ x )
+      lemma = cong ( λ k → ( k ,  proj₂ x ) )  (FiniteSet.finiso← fa _ )
+   ISO.iso→ iso-1 x = cong ( λ k → ( k ,  proj₂ x ) )  (FiniteSet.finiso→ fa _ )
+   iso-2 : {a : ℕ } → ISO (B ∨ (Fin a × B)) (Fin (suc a) × B)
+   ISO.A←B iso-2 (zero , b ) = case1 b
+   ISO.A←B iso-2 (suc fst , b ) = case2 ( fst , b )
+   ISO.B←A iso-2 (case1 b) = ( zero , b )
+   ISO.B←A iso-2 (case2 (a , b )) = ( suc a , b )
+   ISO.iso← iso-2 (case1 x) = refl
+   ISO.iso← iso-2 (case2 x) = refl
+   ISO.iso→ iso-2 (zero , b ) = refl
+   ISO.iso→ iso-2 (suc a , b ) = refl
+   fin-×-f : ( a  : ℕ ) → FiniteSet ((Fin a) × B) {a * b}
+   fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () }
+   fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2
diff -r d0dbdc01664d -r a79e2c2e1642 agda/regular-language.agda
--- a/agda/regular-language.agda	Fri Nov 22 19:30:10 2019 +0900
+++ b/agda/regular-language.agda	Fri Nov 22 22:02:17 2019 +0900
@@ -61,8 +61,8 @@
 isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set
 isRegular A x r = A x ≡ contain r x 
 
-postulate 
-   fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b}
+-- postulate 
+--   fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b}
 
 M-Union : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
 M-Union {Σ} A B = record {
@@ -107,9 +107,9 @@
 open import Data.Nat.Properties hiding ( _≟_ )
 open import Relation.Binary as B hiding (Decidable)
 
-postulate 
+--postulate 
    -- fin-∨ : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A ∨ B) {a + b}
-   fin→ : {A : Set} → { a : ℕ } → FiniteSet A {a} → FiniteSet (A → Bool ) {exp 2 a}
+   --fin→ : {A : Set} → { a : ℕ } → FiniteSet A {a} → FiniteSet (A → Bool ) {exp 2 a}
 
 Concat-NFA :  {Σ : Set} → (A B : RegularLanguage Σ ) → NAutomaton (states A ∨ states B) Σ 
 Concat-NFA {Σ} A B = record { Nδ = δnfa ; Nend = nend }