Mercurial > hg > Members > kono > Proof > automaton

changeset 76:7b357b295272

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 Fri, 08 Nov 2019 13:40:25 +0900
parents c10a8347581a
children faf6fcd36018
files agda/finiteSet.agda agda/logic.agda agda/regular-language.agda
diffstat 3 files changed, 61 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/agda/finiteSet.agda	Thu Nov 07 17:15:22 2019 +0900
+++ b/agda/finiteSet.agda	Fri Nov 08 13:40:25 2019 +0900
@@ -3,6 +3,7 @@
 open import Data.Nat hiding ( _≟_ )
 open import Data.Fin renaming ( _<_ to _<<_ )
 open import Data.Fin.Properties
+open import Data.Empty
 open import Relation.Nullary
 open import Relation.Binary.Core
 open import Relation.Binary.PropositionalEquality
@@ -24,15 +25,40 @@
      lt2 {zero} lt = z≤n
      lt2 {suc m} {zero} ()
      lt2 {suc m} {suc n} (s≤s lt) = s≤s (lt2 lt)
+     exists1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Bool
+     exists1  zero  _ _ = false
+     exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) \/ exists1 m (lt2 m<n) p
      exists : ( Q → Bool ) → Bool
-     exists p = exists1 n (lt0 n) p where
-         exists1 : (m : ℕ ) → m Data.Nat.≤ n  → ( Q → Bool ) → Bool
-         exists1  zero  _ _ = false
-         exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) \/ exists1 m (lt2 m<n) p
+     exists p = exists1 n (lt0 n) p 
      equal? : Q → Q → Bool
      equal? q0 q1 with F←Q q0 ≟ F←Q q1
      ... | yes p = true
      ... | no ¬p = false
+     not-found : { p : Q → Bool } → ( (q : Q ) → p q ≡ false ) → exists p ≡ false
+     not-found {p} pn = not-found2 n (lt0 n) where
+         not-found2 : (m : ℕ ) → (m<n : m Data.Nat.≤ n ) → exists1 m m<n p ≡ false
+         not-found2  zero  _ = refl
+         not-found2 ( suc m ) m<n with pn (Q←F (fromℕ≤ {m} {n} m<n))
+         not-found2 (suc m) m<n | eq = begin
+                  p (Q←F (fromℕ≤ m<n)) \/ exists1 m (lt2 m<n) p 
+              ≡⟨ cong (λ k → k \/ exists1 m (lt2 m<n) p ) eq ⟩
+                  false \/ exists1 m (lt2 m<n) p 
+              ≡⟨ bool-or-1 refl  ⟩
+                  exists1 m (lt2 m<n) p 
+              ≡⟨ not-found2 m (lt2 m<n)  ⟩
+                  false
+              ∎  where open ≡-Reasoning
+     not-found1 : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false 
+     not-found1 {p} ne q =  not-found3 n (lt0 n) where
+         not-found3 : (m : ℕ ) → (m<n : m Data.Nat.≤ n ) → p q ≡ false 
+         not-found3  zero  _ = {!!}
+         not-found3 ( suc m ) m<n = {!!}
+     found : { p : Q → Bool } → {q : Q } → p q ≡ true → exists p ≡ true
+     found {p} {q} pt with bool-≡-? (exists p) true
+     ... | yes eq1 = eq1
+     ... | no ne = ⊥-elim ( contra-position not-found1 notall (¬-bool-t ne) ) where
+         notall : ¬ ((q1 : Q) → p q1 ≡ false)
+         notall ne = ¬-bool (ne q) pt 
 
 fless : {n : ℕ} → (f : Fin n ) → toℕ f < n
 fless zero = s≤s z≤n
--- a/agda/logic.agda	Thu Nov 07 17:15:22 2019 +0900
+++ b/agda/logic.agda	Fri Nov 08 13:40:25 2019 +0900
@@ -92,6 +92,9 @@
 ¬-bool-f {true} ne = refl
 ¬-bool-f {false} ne = ⊥-elim ( ne refl )
 
+¬-bool : {a : Bool} →  a ≡ false  → a ≡ true → ⊥
+¬-bool refl ()
+
 lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥
 lemma-∧-0 {true} {true} refl ()
 lemma-∧-0 {true} {false} ()
--- a/agda/regular-language.agda	Thu Nov 07 17:15:22 2019 +0900
+++ b/agda/regular-language.agda	Fri Nov 08 13:40:25 2019 +0900
@@ -238,28 +238,40 @@
 
 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
-    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
+    finav = (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 = {!!}
+    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
+    lemma6 [] q nq _ fb = lemma8 where
+        lemma8 : exists finav ( λ q → nq q /\ Nend NFA 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 )
+    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 
+    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 (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
+        → Naccept NFA finav nq (y ++ z)  ≡ true
+    lemma7 [] z q nq nq=q fa fb = lemma6 z (astart B) nq {!!} fb
+    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)) )
+    lemma9 | yes refl = refl
+    lemma9 | no ¬p = ⊥-elim ( ¬p refl )
     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) )
+        → 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
     ... | 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
+          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
        ≡⟨ lemma5 S ⟩
          true
        ∎  where open ≡-Reasoning