# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574328862 -32400
# Node ID ee43fecd3f3489e10df3cae307402ea7fdd232c3
# Parent  481691ffc7107876b831db41e5149f414c6a7d15
...

diff -r 481691ffc710 -r ee43fecd3f34 agda/finiteSet.agda
--- a/agda/finiteSet.agda	Wed Nov 20 22:31:54 2019 +0900
+++ b/agda/finiteSet.agda	Thu Nov 21 18:34:22 2019 +0900
@@ -202,8 +202,6 @@
           iso→ (case2 x)  = refl
 fin-∨2 {B} (suc a) {b} fb =  iso-fin (fin-∨1 (fin-∨2 a fb) ) iso
     where
-       fin : FiniteSet (Fin a ∨ B) {a Data.Nat.+ b}
-       fin = fin-∨2 a fb
        iso : ISO (One ∨ (Fin a ∨ B) ) (Fin (suc a) ∨ B)
        ISO.A←B iso (case1 zero) = case1 one
        ISO.A←B iso (case1 (suc f)) = case2 (case1 f)
@@ -226,8 +224,8 @@
 ISO.iso→ (FiniteSet→Fin fin) =  FiniteSet.finiso→ fin
    
 
-fin-∨' : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A ∨ B) {a Data.Nat.+ b}
-fin-∨' {A} {B} {a} {b} fa fb = iso-fin (fin-∨2 a fb ) iso2 where
+fin-∨ : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A ∨ B) {a Data.Nat.+ b}
+fin-∨ {A} {B} {a} {b} fa fb = iso-fin (fin-∨2 a fb ) iso2 where
     ia = FiniteSet→Fin fa
     iso2 : ISO (Fin a ∨ B ) (A ∨ B)
     ISO.A←B iso2 (case1 x) = case1 ( ISO.A←B ia x )
@@ -279,7 +277,7 @@
         finiso→ [] = refl
         finiso← : (f : Fin (exp 2 zero)) → # 0 ≡ f
         finiso← zero = refl
-fin2List {suc n} = subst (λ k → FiniteSet (Vec Bool (suc n)) {k} ) (sym (exp2 n)) ( iso-fin (fin-∨' (fin2List {n}) (fin2List {n})) iso )
+fin2List {suc n} = subst (λ k → FiniteSet (Vec Bool (suc n)) {k} ) (sym (exp2 n)) ( iso-fin (fin-∨ (fin2List {n}) (fin2List {n})) iso )
     where
         QtoR : Vec Bool (suc  n) →  Vec Bool n ∨ Vec Bool n
         QtoR ( true ∷ x ) = case1 x
@@ -301,24 +299,42 @@
 Func2List {Q} {suc n} {m} (s≤s n<m) fin Q→B = Q→B (FiniteSet.Q←F fin (fromℕ≤ n<m)) ∷ Func2List {Q} {n} {m} (Data.Nat.Properties.<-trans n<m a<sa ) fin Q→B
 
 List2Func : { Q : Set } → {n m : ℕ } → n < suc m → FiniteSet Q {m} → Vec Bool n →  Q → Bool 
-List2Func {Q} {zero} _ fin [] q = false
+List2Func {Q} {zero} (s≤s z≤n) fin [] q = false
 List2Func {Q} {suc n} {m} (s≤s n<m) fin (h ∷ t) q with  FiniteSet.F←Q fin q ≟ fromℕ≤ n<m
 ... | yes _ = h
 ... | 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<m : n < suc m )→ (x : Vec Bool n ) → Func2List n<m fin (List2Func n<m fin x ) ≡ x
+    f2l : (n : ℕ ) → (n<m : n < suc m )→ (x : Vec Bool n ) → Func2List n<m fin (List2Func n<m fin x ) ≡ x 
     f2l zero (s≤s z≤n) [] = refl
-    f2l (suc n) (s≤s n<m) (h ∷ t ) with FiniteSet.F←Q fin {!!} ≟ fromℕ≤ n<m
-    ... | yes _ = {!!}
-    ... | no _ = begin
-            Func2List (s≤s n<m) fin (List2Func (s≤s n<m) fin (h ∷ t) )
-       ≡⟨ {!!} ⟩
-            h ∷ t
-       ∎  where open ≡-Reasoning
-    -- with f2l n (Data.Nat.Properties.<-trans n<m a<sa) t 
-    -- ... | tail = {!!}
+    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 = {!!}
+       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
+       lemma1 refl refl = refl
+       lemma2 : List2Func (s≤s n<m) fin (h ∷ t) (FiniteSet.Q←F fin (fromℕ≤ n<m)) ≡ h
+       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)
 
 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 = {!!}
+L2F-iso {Q} {m} fin f q = l2f m a<sa where
+    l2f :  (n : ℕ ) → (n<m : n < suc m )→  (List2Func n<m fin (Func2List n<m fin f )) q ≡ f q
+    l2f zero (s≤s z≤n) = {!!}
+    l2f (suc n) n<m = {!!}
diff -r 481691ffc710 -r ee43fecd3f34 agda/regular-language.agda
--- a/agda/regular-language.agda	Wed Nov 20 22:31:54 2019 +0900
+++ b/agda/regular-language.agda	Thu Nov 21 18:34:22 2019 +0900
@@ -108,7 +108,7 @@
 open import Relation.Binary as B hiding (Decidable)
 
 postulate 
-   fin-∨ : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A ∨ B) {a + b}
+   -- 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}
 
 Concat-NFA :  {Σ : Set} → (A B : RegularLanguage Σ ) → NAutomaton (states A ∨ states B) Σ