Mercurial > hg > Members > kono > Proof > automaton

changeset 105:a61ad3344754

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... state-A is not necessary?
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 15 Nov 2019 11:51:31 +0900
parents fba1cd54581d
children 29e0d2934a0b
files agda/regular-language.agda
diffstat 1 files changed, 27 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/agda/regular-language.agda	Thu Nov 14 05:13:49 2019 +0900
+++ b/agda/regular-language.agda	Fri Nov 15 11:51:31 2019 +0900
@@ -282,10 +282,13 @@
 
     open Found
 
-    data AB-state (nq : states A ∨ states B → Bool ) (x : List Σ) :  Set (Level.suc Level.zero) where
-       state-A  : ((q : states A ∨ states B ) → nq q ≡ true → (exists (afin A) (λ qa → equal? finab q (case1 qa) ) ≡ true )) → AB-state nq x
-       state-AB : ((q : states A ∨ states B ) → nq q ≡ true → (exists (afin B) (λ qb → equal? finab q (case2 qb) /\ accept (automaton B) qb x ) ≡ true ))
-                → AB-state nq  x
+    ab-case : (q : states A ∨ states B ) → (x : List Σ ) → Set
+    ab-case (case1 qa) x = (qa' : states A ) → qa'  ≡ qa
+    ab-case (case2 qb) x = ¬ (exists (afin B) (λ qb → accept (automaton B) qb x ) ≡ true )
+
+    data AB-state (nq : states A ∨ states B → Bool ) (qa : states A) (x : List Σ) :  Set (Level.suc Level.zero) where
+       state-A  : ((q : states A ∨ states B ) → nq q ≡ true → q ≡ case1 qa ) → AB-state nq qa x
+       state-AB : ((q : states A ∨ states B ) → nq q ≡ true → ab-case q x ) → AB-state nq qa x
 
     open AB-state
 
@@ -294,22 +297,31 @@
     ... | refl =  found (afin A) (astart A) eq
 
     contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA finab nq x ≡ true )
-          → (qa : states A )  → AB-state nq x
+          → (qa : states A )  → AB-state nq qa x
           → split (accept (automaton A) qa ) (contain B) x ≡ true
-    contain-A [] nq fn qa cond with found← finab fn | found-q (found← finab fn) | cond | inspect found-q (found← finab fn)
-    contain-A [] nq fn qa cond | S | s | state-A q=qa | record { eq = refl }  = {!!}
-    -- ... | refl = bool-∧→tt-1 (found-p S)
-    contain-A [] nq fn qa cond | S | s | state-AB cond-b | _ with cond-b (found-q S) (bool-∧→tt-0 (found-p S)) 
-    contain-A [] nq fn qa cond | S | case2 qb | state-AB cond-b | record { eq = refl }   | q=qb = ⊥-elim (lemma11 {!!}) where 
-        lemma11 :  ( {qb : states B } → ((found-q S) ≡ case2 qb) ∧ ((aend (automaton B) qb ) ≡ false)) → ⊥
-        lemma11 q=qb  = ¬-bool (proj2 q=qb ) (bool-∧→tt-1 (found-p S ))
-    contain-A [] nq fn qa cond | S | (case1 qa') | state-AB cond-b | record { eq = refl }   |  q=qb = {!!}
+    contain-A [] nq fn qa (state-A caseA) with found← finab fn 
+    ... | S with found-q S | caseA (found-q S) (bool-∧→tt-0 (found-p S)) 
+    ... | case2 qb | ()
+    ... | case1 qa | refl = lemma11 (caseA (found-q S) (bool-∧→tt-0 (found-p S))) (bool-∧→tt-1 (found-p S)) where
+         lemma11 : found-q S ≡ case1 qa → Concat-NFA.nend A B (found-q S) ≡ true → aend (automaton A) qa /\ aend (automaton B) (astart B) ≡ true
+         lemma11 refl xx = xx
+    contain-A [] nq fn qa (state-AB caseAB) with found← finab fn 
+    ... | S with found-q S | inspect found-q S | caseAB (found-q S) (bool-∧→tt-0 (found-p S))
+    ... | case2 qb | record { eq = refl } | ab = ⊥-elim ( ab (found (afin B) qb (bool-∧→tt-1 (found-p S)) )) where
+    ... | case1 qa' | record { eq = refl } | ab with ab qa
+    ... | refl = bool-∧→tt-1 (found-p S) 
     contain-A (h ∷ t) nq fn qa cond with bool-≡-? ((aend (automaton A) qa) /\  accept (automaton B) (δ (automaton B) (astart B) h) t ) true
     ... | yes eq = bool-or-41 eq
-    ... | no ne = bool-or-31 (contain-A t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h)  {!!} ) where
+    ... | no ne = bool-or-31 (contain-A t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) lemma12 ) where
+       lemma13 : (q : states A ∨ states B ) → exists finab (λ qn → nq qn /\ Nδ NFA qn h q) ≡ true
+           → (q ≡ case1 (δ (automaton A) qa h)) ∨ (¬ (exists (afin B) (λ qb → accept (automaton B) qb x ) ≡ true ))
+       lemma13 (case1 qa') ex = case1 {!!}
+       lemma13 (case2 qb) ex = case2 ?
+       lemma12 : AB-state (λ q → exists finab (λ qn → nq qn /\ Nδ NFA qn h q))  (δ (automaton A) qa h) t
+       lemma12 = state-A ( λ q ex → {!!} ) 
 
     lemma10 : Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true → split (contain A) (contain B) x ≡ true
-    lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) (state-A start-eq )
+    lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) (state-A ( λ qa nq=t → {!!} ))
 
     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