--- a/automaton-in-agda/src/regular-language.agda	Sun Sep 24 18:02:04 2023 +0900
+++ b/automaton-in-agda/src/regular-language.agda	Wed Nov 08 21:35:54 2023 +0900
@@ -53,6 +53,19 @@
 Star : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool 
 Star {Σ} x y = repeat x y
 
+-- We have to prove definitions of Concat and Star are equivalent to the set theoretic definitions
+
+-- 1.  A ∪ B = { x | x ∈ A \/ x ∈ B }
+-- 2.  A ∘ B = { x | ∃ y ∈ A, z ∈ B, x = y ++ z }
+-- 3.  A* = { x | ∃ n ∈ ℕ, y1, y2, ..., yn ∈ A, x = y1 ++ y2 ++ ... ++ yn }
+
+-- lemma-Union : {Σ : Set} → ( A B : language {Σ} ) → ( x : List Σ ) → Union A B x ≡ ( A x \/ B x )
+-- lemma-Union = ?
+
+-- lemma-Concat : {Σ : Set} → ( A B : language {Σ} ) → ( x : List Σ ) 
+--    → Concat A B x ≡ ( ∃ λ y → ∃ λ z → A y /\ B z /\ x ≡ y ++ z )
+-- lemma-Concat = ?
+
 open import automaton-ex
 
 test-AB→split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ (
@@ -119,3 +132,84 @@
    lemma1 [] qa qb = refl
    lemma1 (h ∷ t ) qa qb = lemma1 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h))
 
+
+       
+record Split {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (x :  List Σ ) : Set where
+    field
+        sp0 sp1 : List Σ
+        sp-concat : sp0 ++ sp1 ≡ x
+        prop0 : A sp0 ≡ true
+        prop1 : B sp1 ≡ true
+
+open Split
+
+list-empty++ : {Σ : Set} → (x y : List Σ) → x ++ y ≡ [] → (x ≡ [] ) ∧ (y ≡ [] )
+list-empty++ [] [] refl = record { proj1 = refl ; proj2 = refl }
+list-empty++ [] (x ∷ y) ()
+list-empty++ (x ∷ x₁) y ()
+
+open _∧_
+
+open import Relation.Binary.PropositionalEquality hiding ( [_] )
+
+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 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 ) (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 
+     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 
+split→AB {Σ} A B [] eq | yes eqa | yes eqb = 
+    record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = eqa ; prop1 = eqb }
+split→AB {Σ} A B [] eq | yes p | no ¬p = ⊥-elim (lemma-∧-1 eq (¬-bool-t ¬p ))
+split→AB {Σ} A B [] eq | no ¬p | t = ⊥-elim (lemma-∧-0 eq (¬-bool-t ¬p ))
+split→AB {Σ} A B (h ∷ t ) eq with bool-≡-? (A []) true | bool-≡-? (B (h ∷ t )) true
+... | yes px | yes py = record { sp0 = [] ; sp1 = h ∷ t ; sp-concat = refl ; prop0 = px ; prop1 = py }
+... | no px | _ with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case1 px) )
+... | S = record { sp0 = h ∷ sp0 S  ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S }
+split→AB {Σ} A B (h ∷ t ) eq  | _ | no px with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case2 px) )
+... | S = record { sp0 = h ∷ sp0 S  ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S }
+
+AB→split :  {Σ : Set} → (A B : List Σ → Bool ) → ( x y : List Σ ) → A x ≡ true → B y ≡ true → split A B (x ++ y ) ≡ true
+AB→split {Σ} A B [] [] eqa eqb = begin
+       split A B [] 
+     ≡⟨⟩
+       A [] /\ B []
+     ≡⟨ cong₂ (λ j k → j /\ k ) eqa eqb ⟩
+      true
+     ∎  where open ≡-Reasoning
+AB→split {Σ} A B [] (h ∷ y ) eqa eqb = begin
+      split A B (h ∷ y )
+     ≡⟨⟩
+      A [] /\ B (h ∷ y) \/ split (λ t1 → A (h ∷ t1)) B y
+     ≡⟨ cong₂ (λ j k → j /\ k \/ split (λ t1 → A (h ∷ t1)) B y ) eqa eqb ⟩
+      true /\ true \/ split (λ t1 → A (h ∷ t1)) B y
+     ≡⟨⟩
+      true \/ split (λ t1 → A (h ∷ t1)) B y
+     ≡⟨⟩
+      true
+     ∎  where open ≡-Reasoning
+AB→split {Σ} A B (h ∷ t) y eqa eqb = begin
+       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 ) (AB→split {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ) ⟩
+       A [] /\ B (h ∷ t ++ y) \/ true
+     ≡⟨ bool-or-3 ⟩
+      true
+     ∎  where open ≡-Reasoning
+