Mercurial > hg > Members > kono > Proof > automaton

changeset 108:0117144967bb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
case1 done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 17 Nov 2019 12:02:17 +0900
parents 5431d94a4c82
children 330fa494f0e8
files agda/regular-language.agda
diffstat 1 files changed, 20 insertions(+), 20 deletions(-) [+]
line wrap: on
line diff
--- a/agda/regular-language.agda	Sun Nov 17 10:21:05 2019 +0900
+++ b/agda/regular-language.agda	Sun Nov 17 12:02:17 2019 +0900
@@ -286,10 +286,6 @@
     ab-case (case1 qa') qa x = qa'  ≡ qa
     ab-case (case2 qb) qa x = ¬ (exists (afin B) (λ qb → accept (automaton B) qb x ) ≡ true )
 
-    start-eq  : (q : states A ∨ states B) → Concat-NFA-start A B q ≡ true → exists (afin A) (λ qa → equal? finab q (case1 qa)) ≡ true
-    start-eq q eq with equal→refl finab eq
-    ... | 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 )  → (  (q : states A ∨ states B) → nq q ≡ true → ab-case q qa x )
           → split (accept (automaton A) qa ) (contain B) x ≡ true
@@ -301,22 +297,26 @@
     ... | yes eq = bool-or-41 eq
     ... | no ne = bool-or-31 (contain-A t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) lemma11 ) where
        lemma11 :  (q : states A ∨ states B) → exists finab (λ qn → nq qn /\ Nδ NFA qn h q) ≡ true → ab-case q (δ (automaton A) qa h) t
-       lemma11 q ex with found← finab ex 
-       ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) | q 
-       ... | case1 qa | record { eq = refl } | refl | case1 qa' = lemma14 where
-           lemma15 : q ≡ case1 qa' → nq (case1 qa) /\ Concat-NFA.δnfa A B (case1 qa) h (case1 qa') ≡ true 
-           lemma15 refl = found-p S
-           lemma14 : qa' ≡ δ (automaton A) qa h
-           lemma14 = sym ( equal→refl (afin A)  ( bool-∧→tt-1 (lemma15 {!!} ) ) )
-       ... | case1 qa | record { eq = refl } | refl | case2 qb = {!!} where
-       ... | case2 qb | record { eq = refl } | ab | case1 qa' = {!!} where
-           lemma12 : exists (afin B) (λ qb₁ → accept (automaton B) qb₁ (h ∷ t)) ≡ true → ⊥
-           lemma12 = ab
-       ... | case2 qb | record { eq = refl } | ab | case2 qb' = {!!} where
-           lemma13 : exists (afin B) (λ qb₁ → accept (automaton B) qb₁ (h ∷ t)) ≡ true → ⊥
-           lemma13 = ab
-       
-
+       lemma11 (case1 qa')  ex with found← finab ex 
+       ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) 
+       ... | case1 qa | record { eq = refl } | refl = sym ( equal→refl (afin A)  ( bool-∧→tt-1 (found-p S) ))
+       ... | case2 qb | record { eq = refl } | nb with  bool-∧→tt-1 (found-p S) 
+       ... | ()   -- δnfa (case2 q) i (case1 q₁) is false
+       lemma11 (case2 qb)  ex with found← finab ex 
+       ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) 
+       lemma11 (case2 qb)  ex | S | case2 qb' | record { eq = refl } | nb with equal→refl (afin B) (bool-∧→tt-1 (found-p S))
+       ... | refl = contra-position {!!}  ne where
+           lemma14 : exists1 (afin B) (aℕ B) (lt0 (afin B) (aℕ B)) (λ qb → accept (automaton B) qb t) ≡ true →
+                    aend (automaton A) qa /\ accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true
+           lemma14 = ?
+           lemma12 : exists1 (afin B) (aℕ B) (lt0 (afin B) (aℕ B)) (λ qb → accept (automaton B) qb t) ≡ true → ⊥
+           lemma12 = {!!}
+           lemma13 : aend (automaton A) qa /\ accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true → ⊥
+           lemma13 = ne
+       lemma11 (case2 qb)  ex | S | case1 qa' | record { eq = refl } | nb with bool-∧→tt-1 (found-p S)
+       ... | eee = contra-position  {!!} ne where
+           lemma15 : aend (automaton A) qa' /\ (equal? (afin B) qb (δ (automaton B) (astart B) h)) ≡ true
+           lemma15 = eee
 
     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) lemma15 where