Mercurial > hg > Members > kono > Proof > automaton

changeset 88:e7b3a2856ccb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 10 Nov 2019 10:55:25 +0900
parents 217ef727574a
children e919e82e95a2
files agda/finiteSet.agda agda/regular-language.agda
diffstat 2 files changed, 24 insertions(+), 54 deletions(-) [+]
line wrap: on
line diff
--- a/agda/finiteSet.agda	Sat Nov 09 17:15:18 2019 +0900
+++ b/agda/finiteSet.agda	Sun Nov 10 10:55:25 2019 +0900
@@ -66,8 +66,8 @@
               m<n=i i eq m<n = i=j (fromℕ≤ m<n) i (subst (λ k → k ≡ toℕ i) (sym (toℕ-fromℕ≤ m<n)) eq )
      first-end :  ( p : Q → Bool ) → End n p
      first-end p i i>n = ⊥-elim (nat-≤> i>n (fin<n {n} {i}) )
-     found : { p : Q → Bool } → {q : Q } → p q ≡ true → exists p ≡ true
-     found {p} {q} pt = found1 n  (lt0 n) ( first-end p ) where
+     found : { p : Q → Bool } → (q : Q ) → p q ≡ true → exists p ≡ true
+     found {p} q pt = found1 n  (lt0 n) ( first-end p ) where
          found1 : (m : ℕ ) (m<n : m Data.Nat.≤ n ) → ((i : Fin n) → m ≤ toℕ i → p (Q←F i )  ≡ false ) →  exists1 m m<n p ≡ true
          found1 0 m<n end = ⊥-elim ( ¬-bool (subst (λ k → k ≡ false ) (cong (λ k → p k) (finiso→ q) ) (end (F←Q q) z≤n )) pt )
          found1 (suc m)  m<n end with bool-≡-? (p (Q←F (fromℕ≤ m<n))) true
@@ -104,23 +104,5 @@
          found2 (suc m)  m<n end | no np = 
                found2 m (lt2 m<n) (next-end p end m<n (¬-bool-t np )) 
      not-found← : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false 
-     not-found← {p} ne q = not-found3 n (lt0 n) (first-end p ) ne where
-         not-found3 : (m : ℕ ) (m<n : m Data.Nat.≤ n ) → End m p → exists1 m m<n p ≡ false  →  p q ≡ false
-         not-found3 0 m<n end prev = subst (λ k → p k ≡ false) (finiso→ q) ( end (F←Q q) z≤n ) 
-         not-found3 (suc m)  m<n end prev with bool-≡-? (p (Q←F (fromℕ≤ m<n))) true
-         not-found3 (suc m)  m<n end prev | yes eq =
-             ⊥-elim ( ¬-bool prev (subst (λ k → k \/  exists1 m (lt2 m<n) p ≡ true ) (sym eq) (bool-or-4 {exists1 m (lt2 m<n) p}) )) 
-         not-found3 (suc m)  m<n end prev | no np = 
-              not-found3 m (lt2 m<n) (next-end p end m<n (¬-bool-t np )) ( begin
-                     exists1 m (lt2 m<n) p 
-                  ≡⟨ sym (bool-or-1 (¬-bool-t np )) ⟩
-                     p (Q←F (fromℕ≤ m<n))  \/ exists1 m (lt2 m<n) p 
-                  ≡⟨ prev ⟩
-                     false 
-                  ∎ ) where open ≡-Reasoning
-             
+     not-found← {p} np q = ¬-bool-t ( contra-position {_} {_} {_} {exists p ≡ true} (found q) (λ ep → ¬-bool np ep ) )
 
-fless : {n : ℕ} → (f : Fin n ) → toℕ f < n
-fless zero = s≤s z≤n
-fless (suc f) = s≤s ( fless f )
-
--- a/agda/regular-language.agda	Sat Nov 09 17:15:18 2019 +0900
+++ b/agda/regular-language.agda	Sun Nov 10 10:55:25 2019 +0900
@@ -115,12 +115,13 @@
    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 (δ (automaton B) (astart B) i) )
+       δ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 (case1 q) = aend (automaton A) q
+       nend (case1 q) = aend (automaton A) q /\ aend (automaton B) (astart B) -- empty B case
 
 -- 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)
@@ -244,46 +245,33 @@
     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)
+    lemma-nmove-ab : (q : states A ∨ states B) → (h : Σ ) → Nδ NFA q h (abmove q h) ≡ true
+    lemma-nmove-ab (case1 q) _ = equal?-refl (afin A)
+    lemma-nmove-ab (case2 q) _ = equal?-refl (afin B)
     nmove : (q : states A ∨ states B) (nq : states A ∨ states B → Bool ) → (nq q ≡ true) → ( h : Σ ) →
        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 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 ) 
+    nmove (case1 q) nq nqt h = found finab (case1 q) ( bool-and-tt nqt (lemma-nmove-ab (case1 q)  h) )  
+    nmove (case2 q) nq nqt h = found finab (case2 q) ( bool-and-tt nqt (lemma-nmove-ab (case2 q) h) ) where
+    acceptB : (z : List Σ) → (q : states B) → (nq : states A ∨ states B → Bool ) → (nq (case2 q) ≡ true) → ( accept (automaton B) q z ≡ true ) 
         → Naccept NFA finab nq z  ≡ true
-    lemma6 [] q nq nqt fb = lemma8 where
+    acceptB [] q nq nqt fb = lemma8 where
         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)
+        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
-    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
+    acceptA [] [] q nq nqt fa fb = found finab (case1 q) (bool-and-tt nqt (bool-and-tt fa fb )) 
+    acceptA [] (h ∷ z)  q nq nq=q fa fb = acceptB 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
+         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
-    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) )
+    acceptAB S = subst ( λ k → Naccept NFA finab (equal? finab (case1 (astart A))) k  ≡ true  ) ( sp-concat S )
+        (acceptA (sp0 S) (sp1 S)  (astart A) (equal? finab (case1 (astart A))) (equal?-refl finab) (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
@@ -292,7 +280,7 @@
        ≡⟨ ≡-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 ⟩
+       ≡⟨ acceptAB S ⟩
          true
        ∎  where open ≡-Reasoning