Mercurial > hg > Members > kono > Proof > automaton1

changeset 11:554fa6e5a09d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
closed-in-concat
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 16 Nov 2020 02:52:30 +0900
parents ef43350ea0e2
children c3fa431262fa
files nfa-lib.agda nfa.agda regular-language.agda
diffstat 3 files changed, 50 insertions(+), 34 deletions(-) [+]
line wrap: on
line diff
--- a/nfa-lib.agda	Sun Nov 15 14:36:25 2020 +0900
+++ b/nfa-lib.agda	Mon Nov 16 02:52:30 2020 +0900
@@ -38,6 +38,21 @@
 dect136 s1 q₃ q₂ =  no (λ ())
 dect136 s1 q₃ q₃ =  no (λ ())
 
+FindQ3 : FindQ Q3 exists-in-Q3
+FindQ3 = record { create = create ;  found = found ; exists = exists } where
+    create :  {P : Q3 → Set} (q : Q3) → P q → exists-in-Q3 P
+    create q₁ p = qe1 p
+    create q₂ p = qe2 p
+    create q₃ p = qe3 p
+    found : {P : Q3 → Set} → exists-in-Q3 P → Q3
+    found (qe1 x) = q₁
+    found (qe2 x) = q₂
+    found (qe3 x) = q₃
+    exists : {P : Q3 → Set} (n : exists-in-Q3 P) → P (found n)
+    exists (qe1 x) = x
+    exists (qe2 x) = x
+    exists (qe3 x) = x
+
 open import Data.Empty
 open import Relation.Nullary
 open _∧_
--- a/nfa.agda	Sun Nov 15 14:36:25 2020 +0900
+++ b/nfa.agda	Mon Nov 16 02:52:30 2020 +0900
@@ -3,7 +3,7 @@
 open import Level renaming ( suc to Suc ; zero to Zero )
 
 open import Relation.Binary.PropositionalEquality 
-open import Data.List
+open import Data.List hiding ([_])
 open import Relation.Nullary
 open import automaton
 open import logic
@@ -21,7 +21,7 @@
 naccept {n} {Q} {Σ} Nexists nfa qs (x ∷ input) = 
     naccept Nexists nfa (λ p' → Nexists (λ p → qs p ∧ Nδ nfa p x p' ))  input
 
-qlist : {n : Level} {Q : Set n} → (P : Q → Set ) → ((q : Q) → Dec ( P q))  → List Q → List Q
+qlist : {n : Level} {Q : Set n} → (P : Q → Set ) → ((q : Q) → Dec (P q))  → List Q → List Q
 qlist P dec [] = []
 qlist P dec (q ∷ qs) with dec q
 ... | yes _ = q ∷ qlist P dec qs
@@ -48,21 +48,6 @@
        found  : {P : Q → Set} → Nexists (λ q → P q) → Q
        exists : {P : Q → Set} → (n : Nexists (λ q → P q)) → P (found n)
 
-FindQ3 : FindQ Q3 exists-in-Q3
-FindQ3 = record { create = create ;  found = found ; exists = exists } where
-    create :  {P : Q3 → Set} (q : Q3) → P q → exists-in-Q3 P
-    create q₁ p = qe1 p
-    create q₂ p = qe2 p
-    create q₃ p = qe3 p
-    found : {P : Q3 → Set} → exists-in-Q3 P → Q3
-    found (qe1 x) = q₁
-    found (qe2 x) = q₂
-    found (qe3 x) = q₃
-    exists : {P : Q3 → Set} (n : exists-in-Q3 P) → P (found n)
-    exists (qe1 x) = x
-    exists (qe2 x) = x
-    exists (qe3 x) = x
-
 data transition136 : Q3  → Σ2  → Q3 → Set  where
     d0 : transition136 q₁ s1 q₂ 
     d1 : transition136 q₁ s0 q₁ 
@@ -138,8 +123,11 @@
        nend (case2 q) = F (automaton B) q
        nend (case1 q) = F (automaton A) q ∧ F (automaton B) (astart B) -- empty B case
 
-data state-is {n : Level} {Σ : Set }  (A B : RegularLanguage {n} Σ ) : (q : states A ∨ states B ) → Set where
-   this : state-is A B (case1 (astart A))
+-- data state-is {n : Level} {Σ : Set }  (A B : RegularLanguage {n} Σ ) : (q : states A ∨ states B ) → Set where
+--    this : state-is A B (case1 (astart A))
+
+data state-is {n : Level} {Σ : Set }  (A B : RegularLanguage {n} Σ ) (q : states A ∨ states B ) : (states A ∨ states B ) → Set where
+   this : state-is A B q q
 
 record Split {Σ : Set} (A : List Σ → Set ) ( B : List Σ → Set ) (x :  List Σ ) : Set where
     field
@@ -159,29 +147,41 @@
 closed-in-concat :  {n : Level} {Σ : Set } → (A B : RegularLanguage {n}  Σ ) → ( x : List Σ ) 
    (PA : (states A  → Set)  → Set) (FA : FindQ (states A) PA)
    (PB : (states B  → Set)  → Set) (FB : FindQ (states B) PB)
-   → isRegular (Concat {n} (contain A) (contain B)) x record {states = states A ∨ states B → Set ; astart = λ q → state-is A B q
+   → isRegular (Concat {n} (contain A (astart A)) (contain B (astart B))) x record {states = states A ∨ states B → Set
+         ; astart = λ q → state-is A B (case1 (astart A)) q
          ; automaton = subset-construction (Union-Nexists PA PB) ( Concat-NFA A B )}
 closed-in-concat {n} {Σ} A B x PA FA PB FB =  [ closed-in-concat→ x , closed-in-concat← x ] where
     open FindQ 
-    fa : RegularLanguage  Σ
-    fa = record {states = states A ∨ states B → Set ; astart = λ q → state-is A B q
+    fab : RegularLanguage  Σ
+    fab = record {states = states A ∨ states B → Set ; astart = λ q → state-is A B (case1 (astart A)) q
          ; automaton = subset-construction (Union-Nexists PA PB) ( Concat-NFA A B )}
-    closed-in-concat→ : (x : List Σ) → Concat {n} {Σ} (contain A) (contain B) x → contain fa x
+    acceptA : (x : List Σ) → (qa : states A) → Concat {n} {Σ} (contain A qa) (contain B (astart B)) x → contain fab (state-is A B (case1 qa)) x
+    acceptA = {!!}
+    acceptB : (x : List Σ) → (qb : states B) → contain B qb x → contain fab (state-is A B (case2 qb)) x
+    acceptB [] qb cb = case2 (create FB qb [ this , cb ] )
+    acceptB (x ∷ t) qb cb = subst (λ k → contain fab k t) nextb ( acceptB t (δ (automaton B) qb  x ) cb) where
+        nextb : state-is A B (case2 (δ (automaton B) qb x)) ≡ δ (automaton fab) (state-is A B (case2 qb)) x
+        nextb = {!!}
+    closed-in-concat→ : (x : List Σ) → Concat {n} {Σ} (contain A (astart A)) (contain B (astart B)) x → contain fab (state-is A B (case1 (astart A))) x
     closed-in-concat→ [] c = cc1 c where
-        cc1 : contain A [] ∧ contain B [] → 
-                PA (λ q → astart fa (case1 q) ∧ NF (Concat-NFA A B) (case1 q)) ∨ PB (λ q → astart fa (case2 q) ∧ NF (Concat-NFA A B) (case2 q))
+        cc1 : contain A (astart A) [] ∧ contain B (astart B) [] → 
+                PA (λ q → astart fab (case1 q) ∧ NF (Concat-NFA A B) (case1 q)) ∨ PB (λ q → astart fab (case2 q) ∧ NF (Concat-NFA A B) (case2 q))
         cc1 ctab = case1 (create FA (astart A) [ this , [ proj1 ctab , proj2 ctab ] ] )
     -- fina : (F (automaton A) (astart A) ∧ accept (automaton B) (δ (automaton B) (astart B) x) t) 
-    closed-in-concat→ (x ∷ t) (case1 fina ) = {!!}
+    closed-in-concat→ (x ∷ t) (case1 fina ) = subst (λ k →  contain fab k t) bstart ( acceptB t (δ (automaton B) (astart B) x) (proj2 fina)) where 
+        bstart : state-is A B (case2 (δ (automaton B) (astart B) x)) ≡ δ (automaton fab) (state-is A B (case1 (astart A))) x
+        bstart = {!!}
+        accepta : F (automaton A) (found FA (create FA (astart A) (proj1 fina)))
+        accepta = exists FA {F (automaton A)} ( create FA (astart A) (proj1 fina) )
     -- sp :  split (λ t1 → accept (automaton A) (δ (automaton A) (astart A) x) t1) (λ x₁ → accept (automaton B) (astart B) x₁) t
     closed-in-concat→ (x ∷ t) (case2 sp ) = {!!}
-    closed-in-concat← : (x : List Σ) → contain fa x → Concat {n} {Σ} (contain A) (contain B) x
+    closed-in-concat← : (x : List Σ) → contain fab (state-is A B  (case1 (astart A))) x → Concat {n} {Σ} (contain A (astart A)) (contain B (astart B)) x
     closed-in-concat← [] cn = cc2 cn where
-        cc2 : PA (λ q → astart fa (case1 q) ∧ NF (Concat-NFA A B) (case1 q)) ∨ PB (λ q → astart fa (case2 q) ∧ NF (Concat-NFA A B) (case2 q))
-            →   contain A [] ∧ contain B [] 
+        cc2 : PA (λ q → astart fab (case1 q) ∧ NF (Concat-NFA A B) (case1 q)) ∨ PB (λ q → astart fab (case2 q) ∧ NF (Concat-NFA A B) (case2 q))
+            →   contain A (astart A) [] ∧ contain B (astart B) [] 
         -- ca : PA (λ q → state-is A B (case1 q) ∧ F (automaton A) q ∧ F (automaton B) (astart B))
         cc2 (case1 ca) = [ subst (λ k → accept (automaton A) k [] ) (cc5 _ (proj1 (exists FA ca))) cc3 , proj2 (proj2 (exists FA ca)) ] where
-           cc5 : (q : states A) → state-is A B (case1 q) → q ≡ astart A
+           cc5 : (q : states A) → state-is A B (case1 (astart A)) (case1 q) → q ≡ astart A
            cc5 q this = refl
            cc3 : accept (automaton A) (found FA ca ) []
            cc3 = proj1 (proj2 (exists FA  ca)) 
--- a/regular-language.agda	Sun Nov 15 14:36:25 2020 +0900
+++ b/regular-language.agda	Mon Nov 16 02:52:30 2020 +0900
@@ -28,8 +28,8 @@
       states : Set n
       astart : states 
       automaton : Automaton states Σ
-   contain : List Σ → Set 
-   contain x = accept automaton astart x
+   contain : states → List Σ → Set 
+   contain q x = accept automaton q x
 
 split : {Σ : Set} → (List Σ → Set)
       → ( List Σ → Set) → List Σ → Set
@@ -61,7 +61,7 @@
 
 open RegularLanguage 
 isRegular : {n : Level} {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage {n} Σ ) → Set 
-isRegular A x r = A x ⇔ contain r x 
+isRegular A x r = A x ⇔ contain r (astart r) x 
 
 M-Union : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → RegularLanguage Σ
 M-Union {n} {Σ} A B = record {
@@ -75,7 +75,8 @@
 
 open _∧_
 
-closed-in-union :  {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B )
+closed-in-union :  {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → ( x : List Σ )
+    → isRegular (Union (contain A (astart A)) (contain B (astart B))) x ( M-Union A B )
 closed-in-union A B [] = lemma where
    lemma : (F (automaton A) (astart A) ∨ F (automaton B) (astart B)) ⇔
            (F (automaton A) (astart A) ∨ F (automaton B) (astart B))