Mercurial > hg > Members > kono > Proof > automaton

changeset 87:217ef727574a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reverse direction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 Nov 2019 17:15:18 +0900
parents 4c950a6ad6ce
children e7b3a2856ccb
files agda/finiteSet.agda agda/regular-language.agda
diffstat 2 files changed, 69 insertions(+), 46 deletions(-) [+]
line wrap: on
line diff
--- a/agda/finiteSet.agda	Sat Nov 09 14:44:38 2019 +0900
+++ b/agda/finiteSet.agda	Sat Nov 09 17:15:18 2019 +0900
@@ -42,6 +42,10 @@
      equal? q0 q1 with F←Q q0 ≟ F←Q q1
      ... | yes p = true
      ... | no ¬p = false
+     equal?-refl : {q : Q} → equal? q q ≡ true
+     equal?-refl {q} with F←Q q ≟ F←Q q
+     ... | yes p = refl
+     ... | no ne = ⊥-elim (ne refl)
      fin<n : {n : ℕ} {f : Fin n} → toℕ f < n
      fin<n {_} {zero} = s≤s z≤n
      fin<n {suc n} {suc f} = s≤s (fin<n {n} {f})
--- a/agda/regular-language.agda	Sat Nov 09 14:44:38 2019 +0900
+++ b/agda/regular-language.agda	Sat Nov 09 17:15:18 2019 +0900
@@ -48,13 +48,13 @@
 Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
 Star {Σ} A = split A ( Star {Σ} A )
 
-test-split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ (
+test-AB→split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ (
        ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/ 
        ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/ 
        ( A ( i0 ∷ i1 ∷ [] ) /\ B ( i0 ∷ [] ) ) \/
        ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) /\ B  []  ) 
    )
-test-split {_} {A} {B} = refl
+test-AB→split {_} {A} {B} = refl
 
 open RegularLanguage 
 isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set
@@ -115,12 +115,12 @@
    module Concat-NFA where
        δnfa : states A ∨ states B → Σ → states A ∨ states B → Bool
        δnfa (case1 q) i (case1 q₁) = equal? (afin A) (δ (automaton A) q i) q₁
-       δnfa (case1 qa) i (case2 qb) = (aend (automaton A) qa ) /\ (equal? (afin B) qb (astart B) )
+       δnfa (case1 qa) i (case2 qb) = (aend (automaton A) qa ) /\ (equal? (afin B) qb (δ (automaton B) (astart B) i) )
        δnfa (case2 q) i (case2 q₁) = equal? (afin B) (δ (automaton B) q i) q₁
        δnfa _ i _ = false
        nend : states A ∨ states B → Bool
        nend (case2 q) = aend (automaton B) q
-       nend _ = false
+       nend (case1 q) = aend (automaton A) q
 
 -- 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)
@@ -187,28 +187,28 @@
       split (λ t1 → A (h ∷ t1)) B t
   ∎ ) where open ≡-Reasoning
 
-c-split :  {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → split A B x ≡ true → Split A B x
-c-split {Σ} A B [] eq with bool-≡-? (A []) true | bool-≡-? (B []) true 
-c-split {Σ} A B [] eq | yes eqa | yes eqb = 
+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 }
-c-split {Σ} A B [] eq | yes p | no ¬p = ⊥-elim (lemma-∧-1 eq (¬-bool-t ¬p ))
-c-split {Σ} A B [] eq | no ¬p | t = ⊥-elim (lemma-∧-0 eq (¬-bool-t ¬p ))
-c-split {Σ} A B (h ∷ t ) eq with bool-≡-? (A []) true | bool-≡-? (B (h ∷ t )) true
+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 c-split (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case1 px) )
+... | 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 }
-c-split {Σ} A B (h ∷ t ) eq  | _ | no px with c-split (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case2 px) )
+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 }
 
-split++ :  {Σ : Set} → (A B : List Σ → Bool ) → ( x y : List Σ ) → A x ≡ true → B y ≡ true → split A B (x ++ y ) ≡ true
-split++ {Σ} A B [] [] eqa eqb = begin
+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
-split++ {Σ} A B [] (h ∷ y ) eqa eqb = begin
+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
@@ -219,13 +219,13 @@
      ≡⟨⟩
       true
      ∎  where open ≡-Reasoning
-split++ {Σ} A B (h ∷ t) y eqa eqb = begin
+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 ) ( begin
           split (λ t1 → A (h ∷ t1)) B (t ++ y) 
-        ≡⟨ split++ {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ⟩
+        ≡⟨ AB→split {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ⟩
           true 
         ∎ ) ⟩
        A [] /\ B (h ∷ t ++ y) \/ true
@@ -238,58 +238,77 @@
 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
-    finav = (fin-∨ (afin A) (afin B))
+closed-in-concat {Σ} A B x = ≡-Bool-func closed-in-concat→ closed-in-concat← where
+    finab = (fin-∨ (afin A) (afin B))
     NFA = (Concat-NFA A B)
     abmove : (q : states A ∨ states B) → (h : Σ ) → states A ∨ states B
     abmove (case1 q) h = case1 (δ (automaton A) q h)
     abmove (case2 q) h = case2 (δ (automaton B) q h)
     nmove : (q : states A ∨ states B) (nq : states A ∨ states B → Bool ) → (nq q ≡ true) → ( h : Σ ) →
-       exists finav (λ qn → nq qn /\ Nδ NFA qn h (abmove q h)) ≡ true
-    nmove (case1 q) nq nqt h = found finav {_} {(case1 q)} ( bool-and-tt nqt lemma-nmove-a )  where
+       exists finab (λ qn → nq qn /\ Nδ NFA qn h (abmove q h)) ≡ true
+    nmove (case1 q) nq nqt h = found finab {_} {(case1 q)} ( bool-and-tt nqt lemma-nmove-a )  where
         lemma-nmove-a : Nδ NFA (case1 q) h (abmove (case1 q) h) ≡ true
         lemma-nmove-a with F←Q (afin A) (δ (automaton A) q h) ≟ F←Q (afin A) (δ (automaton A) q h)
         lemma-nmove-a | yes refl = refl
         lemma-nmove-a | no ne = ⊥-elim (ne refl)
-    nmove (case2 q) nq nqt h = found finav {_} {(case2 q)} ( bool-and-tt nqt lemma-nmove ) where
+    nmove (case2 q) nq nqt h = found finab {_} {(case2 q)} ( bool-and-tt nqt lemma-nmove ) where
         lemma-nmove : Nδ NFA (case2 q) h (abmove (case2 q) h) ≡ true
         lemma-nmove with F←Q (afin B) (δ (automaton B) q h) ≟ F←Q (afin B) (δ (automaton B) q h)
         lemma-nmove | yes refl = refl
         lemma-nmove | no ne = ⊥-elim (ne refl)
     lemma6 : (z : List Σ) → (q : states B) → (nq : states A ∨ states B → Bool ) → (nq (case2 q) ≡ true) → ( accept (automaton B) q z ≡ true ) 
-        → Naccept NFA finav nq z  ≡ true
+        → Naccept NFA finab nq z  ≡ true
     lemma6 [] q nq nqt fb = lemma8 where
-        lemma8 : exists finav ( λ q → nq q /\ Nend NFA q ) ≡ true
-        lemma8 = found finav {_} {case2 q} ( bool-and-tt nqt fb )
-    lemma6 (h ∷ t ) q nq nq=q fb = lemma6 t (δ (automaton B) q h) (Nmoves NFA finav nq h) (nmove (case2 q) nq nq=q h) fb 
+        lemma8 : exists finab ( λ q → nq q /\ Nend NFA q ) ≡ true
+        lemma8 = found finab {_} {case2 q} ( bool-and-tt nqt fb )
+    lemma6 (h ∷ t ) q nq nq=q fb = lemma6 t (δ (automaton B) q h) (Nmoves NFA finab nq h) (nmove (case2 q) nq nq=q h) fb 
     lemma7 : (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 finav nq (y ++ z)  ≡ true
-    lemma7 [] z q nq nq=q fa fb = lemma6 z (astart B) nq lemma71 fb where
-         lemma71 : nq (case2 (astart B)) ≡ true
-         lemma71 = {!!}
-         lemma-nq=q : (nq (case1 q) ≡ true)
-         lemma-nq=q = nq=q
-    lemma7 (h ∷ t) z q nq nq=q fa fb = lemma7 t z (δ (automaton A) q h) (Nmoves NFA finav nq h) (nmove (case1 q) nq nq=q h)  fa fb where
-    lemma9 : equal? finav (case1 (astart A)) (case1 (astart A)) ≡ true
-    lemma9 with Data.Fin._≟_ (F←Q finav (case1 (astart A))) ( F←Q finav (case1 (astart A)) )
+        → Naccept NFA finab nq (y ++ z)  ≡ true
+    lemma7 [] [] q nq nqt fa fb = found finab {_} {case1 q} ( bool-and-tt nqt fa )
+    lemma7 [] (h ∷ z)  q nq nq=q fa fb = lemma6 z nextb (Nmoves NFA finab nq h) lemma70 fb where
+         nextb : states B
+         nextb = δ (automaton B) (astart B) h
+         lemma71 : Nδ NFA (case1 q) h (case2 nextb) ≡ true
+         lemma71 with F←Q (afin B) (δ (automaton B) (astart B) h) ≟ F←Q (afin B) (δ (automaton B) (astart B) h)
+         lemma71 | yes refl = bool-and-tt fa refl
+         lemma71 | no ne = ⊥-elim (ne refl)
+         lemma70 : exists finab (λ qn → nq qn /\ Nδ NFA qn h (case2 nextb)) ≡ true
+         lemma70 = found finab {_} {case1 q} ( bool-and-tt nq=q lemma71 )
+    lemma7 (h ∷ t) z q nq nq=q fa fb = lemma7 t z (δ (automaton A) q h) (Nmoves NFA finab nq h) (nmove (case1 q) nq nq=q h)  fa fb where
+    lemma9 : equal? finab (case1 (astart A)) (case1 (astart A)) ≡ true
+    lemma9 with Data.Fin._≟_ (F←Q finab (case1 (astart A))) ( F←Q finab (case1 (astart A)) )
     lemma9 | yes refl = refl
     lemma9 | no ¬p = ⊥-elim ( ¬p refl )
     lemma5 : Split (contain A) (contain B) x
-        → Naccept NFA finav (equal? finav (case1 (astart A))) x  ≡ true
-    lemma5 S = subst ( λ k → Naccept NFA finav (equal? finav (case1 (astart A))) k  ≡ true  ) ( sp-concat S )
-        (lemma7 (sp0 S) (sp1 S)  (astart A) (equal? finav (case1 (astart A))) lemma9 (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
+        → Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true
+    lemma5 S = subst ( λ k → Naccept NFA finab (equal? finab (case1 (astart A))) k  ≡ true  ) ( sp-concat S )
+        (lemma7 (sp0 S) (sp1 S)  (astart A) (equal? finab (case1 (astart A))) lemma9 (prop0 S) (prop1 S) )
+
+    closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true
+    closed-in-concat→ concat with split→AB (contain A) (contain B) x concat
     ... | S = begin
-          accept (subset-construction finav NFA (case1 (astart A))) (Concat-NFA-start A B ) x 
-       ≡⟨ ≡-Bool-func (subset-construction-lemma← finav NFA (case1 (astart A)) x ) 
-          (subset-construction-lemma→ finav NFA (case1 (astart A)) x ) ⟩
-          Naccept NFA finav (equal? finav (case1 (astart A))) x
+          accept (subset-construction finab NFA (case1 (astart A))) (Concat-NFA-start A B ) x 
+       ≡⟨ ≡-Bool-func (subset-construction-lemma← finab NFA (case1 (astart A)) x ) 
+          (subset-construction-lemma→ finab NFA (case1 (astart A)) x ) ⟩
+          Naccept NFA finab (equal? finab (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 ?)
+
+    lemma11 : (x y : List Σ) → (q : states A) → (nq : states A ∨ states B → Bool ) → (nq (case1 q) ≡ true)
+       → split (contain A) (contain B) (x ++ y) ≡ true
+    lemma11 x [] q nq nqt = {!!}
+    lemma11 x (h ∷ t) q nq nqt = {!!}
+
+    lemma10 : Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true → split (contain A) (contain B) x ≡ true
+    lemma10 = {!!}
+
+    closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true
+    closed-in-concat← C with subset-construction-lemma← finab NFA (case1 (astart A)) x C
+    ... | CC = lemma10 CC
+
+    -- AB→split (accept (automaton A) {!!} ) (accept (automaton B) {!!} ) {!!} {!!} {!!} {!!}
 
 
+