# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1574042431 -32400
# Node ID ed0a2dad62f4b2e2323de9953fcc7ecd1b15c590
# Parent  795850729aaafacdce66d65da538884bcc6890c5
finite

diff -r 795850729aaa -r ed0a2dad62f4 agda/finiteSet.agda
--- a/agda/finiteSet.agda	Sun Nov 17 18:07:47 2019 +0900
+++ b/agda/finiteSet.agda	Mon Nov 18 11:00:31 2019 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 module finiteSet  where
 
 open import Data.Nat hiding ( _≟_ )
@@ -128,3 +129,65 @@
      not-found← : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false 
      not-found← {p} np q = ¬-bool-t ( contra-position {_} {_} {_} {exists p ≡ true} (found q) (λ ep → ¬-bool np ep ) )
 
+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 = record {
+        Q←F = Q←F  
+      ; F←Q =  F←Q  
+      ; finiso→ = finiso→ 
+      ; finiso← = finiso← 
+   } where
+        n : ℕ
+        n = a Data.Nat.+ b
+        Q : Set 
+        Q = A ∨ B
+        Q←F : Fin n → Q
+        Q←F f with Data.Nat.Properties.<-cmp (toℕ f) a
+        Q←F f | tri< lt ¬b ¬c = case1 (FiniteSet.Q←F fa (fromℕ≤ lt )) 
+        Q←F f | tri≈ ¬a eq ¬c = case2 (FiniteSet.Q←F fb (fromℕ≤ 0<b )) where
+            0<b : 0 < b
+            0<b = {!!}
+        Q←F f | tri> ¬a ¬b c = case2 (FiniteSet.Q←F fb (fromℕ≤ f-a<b )) where
+            f-a : ℕ
+            f-a = {!!}
+            f-a<b : f-a < b
+            f-a<b = {!!} 
+        F←Q : Q → Fin n
+        F←Q (case1 qa) = inject+ b (FiniteSet.F←Q fa qa)
+        F←Q (case2 qb) = raise a (FiniteSet.F←Q fb qb)
+        finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
+        finiso→ = {!!}
+        finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
+        finiso← = {!!}
+
+import Data.Nat.DivMod
+import Data.Nat.Properties
+
+fin→' : {A : Set} → { a : ℕ } → FiniteSet A {a} → FiniteSet (A → Bool ) {exp 2 a}
+fin→' {A} {a} fin = record {
+        Q←F = Q←F  
+      ; F←Q =  F←Q  
+      ; finiso→ = finiso→ 
+      ; finiso← = finiso← 
+   } where
+        n : ℕ
+        n = exp 2 a
+        shift : (n : ℕ) →  ℕ ∧ Bool
+        shift n with (n Data.Nat.DivMod.mod 2) ≟ (# 0)
+        shift n | yes p = record { proj1 = n Data.Nat.DivMod.div 2 ; proj2 = true }
+        shift n | no ¬p = record { proj1 = n Data.Nat.DivMod.div 2 ; proj2 = false }
+        Q←F-shift : (n : ℕ) → A → Bool
+        Q←F-shift zero = {!!}
+        Q←F-shift (suc n) = {!!}
+        Q : Set 
+        Q = A → Bool
+        Q←F : Fin n → Q
+        Q←F f = λ qa → {!!}
+        F←Q : Q → Fin n
+        F←Q fq = {!!}
+        finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q
+        finiso→ = {!!}
+        finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f
+        finiso← = {!!}
+
+
+
diff -r 795850729aaa -r ed0a2dad62f4 agda/regular-language.agda
--- a/agda/regular-language.agda	Sun Nov 17 18:07:47 2019 +0900
+++ b/agda/regular-language.agda	Mon Nov 18 11:00:31 2019 +0900
@@ -162,28 +162,21 @@
 c-split-lemma : {Σ : Set} → (A B : List Σ → Bool ) → (h : Σ) → ( t : List Σ ) → split A B (h ∷ t ) ≡ true
    → ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) )
    → split (λ t1 → A (h ∷ t1)) B t ≡ true
-c-split-lemma {Σ} A B h t eq (case1 ¬p ) = sym ( begin
+c-split-lemma {Σ} A B h t eq p = sym ( begin
       true
   ≡⟨  sym eq  ⟩
       split A B (h ∷ t ) 
   ≡⟨⟩
       A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t
-  ≡⟨  cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (bool-and-1 (¬-bool-t ¬p)) ⟩
+  ≡⟨  cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (lemma-p p ) ⟩
       false \/ split (λ t1 → A (h ∷ t1)) B t
   ≡⟨ bool-or-1 refl ⟩
       split (λ t1 → A (h ∷ t1)) B t
-  ∎ ) where open ≡-Reasoning
-c-split-lemma {Σ} A B h t eq (case2 ¬p ) = sym ( begin
-      true
-  ≡⟨  sym eq  ⟩
-      split A B (h ∷ t ) 
-  ≡⟨⟩
-      A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t
-  ≡⟨  cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (bool-and-2 (¬-bool-t ¬p)) ⟩
-      false \/ split (λ t1 → A (h ∷ t1)) B t
-  ≡⟨ bool-or-1 refl ⟩
-      split (λ t1 → A (h ∷ t1)) B t
-  ∎ ) where open ≡-Reasoning
+  ∎ ) where
+     open ≡-Reasoning 
+     lemma-p : ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) ) → A [] /\ B (h ∷ t) ≡ false
+     lemma-p (case1 ¬A ) = bool-and-1 ( ¬-bool-t ¬A )
+     lemma-p (case2 ¬B ) = bool-and-2 ( ¬-bool-t ¬B )
 
 split→AB :  {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → split A B x ≡ true → Split A B x
 split→AB {Σ} A B [] eq with bool-≡-? (A []) true | bool-≡-? (B []) true 
@@ -221,11 +214,7 @@
        split A B ((h ∷ t) ++ y)  
      ≡⟨⟩
        A [] /\ B (h ∷ t ++ y) \/ split (λ t1 → A (h ∷ t1)) B (t ++ y)
-     ≡⟨ cong ( λ k →  A [] /\ B (h ∷ t ++ y) \/ k ) ( begin
-          split (λ t1 → A (h ∷ t1)) B (t ++ y) 
-        ≡⟨ AB→split {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ⟩
-          true 
-        ∎ ) ⟩
+     ≡⟨ cong ( λ k →  A [] /\ B (h ∷ t ++ y) \/ k ) (AB→split {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ) ⟩
        A [] /\ B (h ∷ t ++ y) \/ true
      ≡⟨ bool-or-3 ⟩
       true
@@ -254,6 +243,7 @@
         lemma8 : exists finab ( λ q → nq q /\ Nend NFA q ) ≡ true
         lemma8 = found finab (case2 q) ( bool-and-tt nqt fb )
     acceptB (h ∷ t ) q nq nq=q fb = acceptB t (δ (automaton B) q h) (Nmoves NFA finab nq h) (nmove (case2 q) nq nq=q h) fb 
+
     acceptA : (y z : List Σ) → (q : states A) → (nq : states A ∨ states B → Bool ) → (nq (case1 q) ≡ true)
         → ( accept (automaton A) q y ≡ true ) → ( accept (automaton B) (astart B) z ≡ true ) 
         → Naccept NFA finab nq (y ++ z)  ≡ true
@@ -264,6 +254,7 @@
          lemma70 : exists finab (λ qn → nq qn /\ Nδ NFA qn h (case2 nextb)) ≡ true
          lemma70 = found finab (case1 q) ( bool-and-tt nq=q (bool-and-tt fa (lemma-nmove-ab (case2 (astart B)) h) ))
     acceptA (h ∷ t) z q nq nq=q fa fb = acceptA t z (δ (automaton A) q h) (Nmoves NFA finab nq h) (nmove (case1 q) nq nq=q h)  fa fb where
+
     acceptAB : Split (contain A) (contain B) x
         → Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true
     acceptAB S = subst ( λ k → Naccept NFA finab (equal? finab (case1 (astart A))) k  ≡ true  ) ( sp-concat S )
@@ -299,17 +290,16 @@
        lemma11 :  (q : states A ∨ states B) → exists finab (λ qn → nq qn /\ Nδ NFA qn h q) ≡ true → ab-case q (δ (automaton A) qa h) t
        lemma11 (case1 qa')  ex with found← finab ex 
        ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) 
-       ... | case1 qa | record { eq = refl } | refl = sym ( equal→refl (afin A)  ( bool-∧→tt-1 (found-p S) ))
-       ... | case2 qb | record { eq = refl } | nb with  bool-∧→tt-1 (found-p S) 
-       ... | ()   -- δnfa (case2 q) i (case1 q₁) is false
+       ... | case1 qa | record { eq = refl } | refl = sym ( equal→refl (afin A)  ( bool-∧→tt-1 (found-p S) ))  -- continued A case
+       ... | case2 qb | record { eq = refl } | nb with  bool-∧→tt-1 (found-p S) -- δnfa (case2 q) i (case1 q₁) is false
+       ... | ()   
        lemma11 (case2 qb)  ex with found← finab ex 
        ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) 
-       lemma11 (case2 qb)  ex | S | case2 qb' | record { eq = refl } | nb =
-               contra-position lemma13 nb where
+       lemma11 (case2 qb)  ex | S | case2 qb' | record { eq = refl } | nb = contra-position lemma13 nb where -- continued B case should fail
            lemma13 :  accept (automaton B) qb t ≡ true → accept (automaton B) qb' (h ∷ t) ≡ true
            lemma13 fb = subst (λ k → accept (automaton B) k t ≡ true ) (sym (equal→refl (afin B) (bool-∧→tt-1 (found-p S)))) fb  
        lemma11 (case2 qb)  ex | S | case1 qa | record { eq = refl } | refl with bool-∧→tt-1 (found-p S)
-       ... | eee = contra-position lemma12 ne where
+       ... | eee = contra-position lemma12 ne where -- starting B case should fail
            lemma12 : accept (automaton B) qb t ≡ true → aend (automaton A) qa /\ accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true
            lemma12 fb = bool-and-tt (bool-∧→tt-0 eee) (subst ( λ k → accept (automaton B) k t ≡ true ) (equal→refl (afin B) (bool-∧→tt-1 eee) ) fb )