Mercurial > hg > Members > kono > Proof > automaton

changeset 75:c10a8347581a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 07 Nov 2019 17:15:22 +0900
parents 762d5a6fbe09
children 7b357b295272
files agda/regular-language.agda
diffstat 1 files changed, 32 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/agda/regular-language.agda	Thu Nov 07 13:16:03 2019 +0900
+++ b/agda/regular-language.agda	Thu Nov 07 17:15:22 2019 +0900
@@ -121,9 +121,12 @@
        nend (case2 q) = aend (automaton B) q
        nend _ = false
 
+-- Concat-NFA-start :  {Σ : Set} → (A B : RegularLanguage Σ ) → states A ∨ states B → Bool
+-- Concat-NFA-start A B (case1 q) = equal? (afin A) q (astart A)
+-- Concat-NFA-start _ _ _ = false
+
 Concat-NFA-start :  {Σ : Set} → (A B : RegularLanguage Σ ) → states A ∨ states B → Bool
-Concat-NFA-start A B (case1 q) = equal? (afin A) q (astart A)
-Concat-NFA-start _ _ _ = false
+Concat-NFA-start A B q = equal? (fin-∨ (afin A) (afin B)) (case1 (astart A)) q
 
 M-Concat : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
 M-Concat {Σ} A B = record {
@@ -138,17 +141,6 @@
        finf : FiniteSet (states A ∨ states B → Bool ) 
        finf = fin→ fin 
        
-lemma1 : {Σ : Set} →  ( x y : List Σ )
-    → (A B : RegularLanguage Σ ) 
-    → accept (automaton A) (astart A) x ≡ true
-    → accept (automaton B) (astart B) y ≡ true
-    → Naccept (Concat-NFA A B) (fin-∨ (afin A) (afin B)) (Concat-NFA-start A B) ( x ++ y ) ≡ true
-lemma1 {Σ} x y A B aA aB = lemma2 x (astart A) (Concat-NFA-start A B) aA where
-    lemma2 : (x : List Σ) → (q : states A) → (qab : states A ∨ states B → Bool)
-       → accept (automaton A) q x ≡ true → Naccept (Concat-NFA A B) (fin-∨ (afin A) (afin B)) qab ( x ++ y ) ≡ true
-    lemma2 [] q qab aA = {!!}
-    lemma2 (h ∷ t ) q qab aA  = lemma2 t {!!} {!!} {!!}
-
 record Split {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (x :  List Σ ) : Set where
     field
         sp0 : List Σ
@@ -240,12 +232,37 @@
       true
      ∎  where open ≡-Reasoning
 
+postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n)
+
+open NAutomaton
 
 closed-in-concat :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
-closed-in-concat A B x = ≡-Bool-func lemma3 lemma4 where
+closed-in-concat {Σ} A B x = ≡-Bool-func lemma3 lemma4 where
+    lemma6 : (z : List Σ) → (q : states B) → (nq : states A ∨ states B → Bool ) → ( accept (automaton B) q z ≡ true ) 
+        → Naccept (Concat-NFA A B) (fin-∨ (afin A) (afin B)) nq z  ≡ true
+    lemma6 [] q nq fb = lemma8 where
+        lemma8 : exists (fin-∨ (afin A) (afin B)) ( λ q → nq q /\ Nend (Concat-NFA A B) q ) ≡ true
+        lemma8 = {!!}
+    lemma6 (h ∷ t ) q nq fb = lemma6 t (δ (automaton B) q h) {!!} fb 
+    lemma7 : (y z : List Σ) → (q : states A) → (nq : states A ∨ states B → Bool )
+        → ( accept (automaton A) q y ≡ true ) → ( accept (automaton B) (astart B) z ≡ true ) 
+        → Naccept (Concat-NFA A B) (fin-∨ (afin A) (afin B)) nq (y ++ z)  ≡ true
+    lemma7 [] z q nq fa fb = lemma6 z (astart B) nq fb
+    lemma7 (h ∷ t)  z q fa fb = lemma7 t z (δ (automaton A) q h) {!!} fb
+    lemma5 : Split (contain A) (contain B) x
+        → Naccept (Concat-NFA A B) (fin-∨ (afin A) (afin B)) (equal? (fin-∨ (afin A) (afin B)) (case1 (astart A))) x  ≡ true
+    lemma5 S = subst ( λ k → Naccept (Concat-NFA A B) (fin-∨ (afin A) (afin B)) (equal? (fin-∨ (afin A) (afin B)) (case1 (astart A))) k  ≡ true  ) ( sp-concat S )
+        (lemma7 (sp0 S) (sp1 S)  (astart A) (equal? (fin-∨ (afin A) (afin B)) (case1 (astart A))) (prop0 S) (prop1 S) )
     lemma3 : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true
     lemma3 concat with c-split (contain A) (contain B) x concat
-    ... | S = {!!}
+    ... | S = begin
+          accept (subset-construction (fin-∨ (afin A) (afin B)) (Concat-NFA A B) (case1 (astart A))) (Concat-NFA-start A B ) x 
+       ≡⟨ ≡-Bool-func (subset-construction-lemma← (fin-∨ (afin A) (afin B)) (Concat-NFA A B) (case1 (astart A)) x ) 
+          (subset-construction-lemma→ (fin-∨ (afin A) (afin B)) (Concat-NFA A B) (case1 (astart A)) x ) ⟩
+          Naccept (Concat-NFA A B) (fin-∨ (afin A) (afin B)) (equal? (fin-∨ (afin A) (afin B)) (case1 (astart A))) x
+       ≡⟨ lemma5 S ⟩
+         true
+       ∎  where open ≡-Reasoning
     lemma4 : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true
     lemma4 C = {!!} -- split++ (contain A) (contain B) x y (accept ?) (accept ?)