# HG changeset patch # User Shinji KONO # Date 1573475404 -32400 # Node ID aca3f1349913c947d61d30da953da409101ce67f # Parent f196e739b4bf9611b61d6de74ef183daa842af9d ... diff -r f196e739b4bf -r aca3f1349913 agda/regular-language.agda --- a/agda/regular-language.agda Mon Nov 11 14:25:42 2019 +0900 +++ b/agda/regular-language.agda Mon Nov 11 21:30:04 2019 +0900 @@ -280,38 +280,54 @@ ∎ where open ≡-Reasoning open Found - lemma13 : (x : List Σ) → (nq : states A ∨ states B → Bool ) → Naccept NFA finab nq x ≡ true - → (qa : states A ) → (nq (case1 qa) ≡ true) → ( (q : states A ∨ states B) → nq q ≡ true → q ≡ case1 qa ) + + contain-B : ( h : Σ) → ( t : List Σ ) → ( nq : states A ∨ states B → Bool ) → (qb : states B) → ( nq (case2 qb) ≡ true ) → + Naccept NFA finab nq (h ∷ t) ≡ true → accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true + contain-B = {!!} + + condition-A : (nq : states A ∨ states B → Bool ) → (qa : states A) → (q : states A ∨ states B) → Set + condition-A nq qa q = ( nq q ≡ true → q ≡ case1 qa ) ∨ ( (nq (case1 qa) /\ aend (automaton A) qa /\ nq (case2 (astart B))) ≡ true ) + + contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → Naccept NFA finab nq x ≡ true + → (qa : states A ) → (nq (case1 qa) ≡ true) → ( (q : states A ∨ states B ) → condition-A nq qa q ) → split (accept (automaton A) qa ) (contain B) x ≡ true - lemma13 [] nq fn qa qat qa=q with found← finab fn - ... | S = lemma16 where - lemma15 : (found-q S) ≡ case1 qa - lemma15 = qa=q (found-q S) (bool-∧→tt-0 (found-p S)) - lemma16 : aend (automaton A) qa /\ aend (automaton B) (astart B) ≡ true - lemma16 with lemma15 - ... | refl = bool-∧→tt-1 (found-p S) - lemma13 (h ∷ t) nq fn qa qat qa=q with bool-≡-? ((aend (automaton A) qa) /\ accept (automaton B) (δ (automaton B) (astart B) h) t ) true + contain-A [] nq fn qa qat cond with found← finab fn + ... | S with cond (found-q S) + ... | case2 end = {!!} + ... | case1 qa=q with qa=q (bool-∧→tt-0 (found-p S)) + ... | refl = bool-∧→tt-1 (found-p S) + contain-A (h ∷ t) nq fn qa qat 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 lemma14 where - lemma11 : (q : states A ∨ states B) + ... | no ne = bool-or-31 (contain-A t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) (nmove (case1 qa) nq qat h) lemma11-1 ) where + lemma11-1 : (q : states A ∨ states B) → condition-A (λ q → exists finab (λ qn → nq qn /\ Nδ NFA qn h q)) (δ (automaton A) qa h) q + lemma11-1 q with cond q + ... | case2 end = {!!} + ... | case1 qa=q = case1 (lemma11 q) where + lemma11 : (q : states A ∨ states B) → exists finab (λ qn → nq qn /\ Nδ NFA qn h q) ≡ true → q ≡ case1 (δ (automaton A) qa h) - lemma11 q ex = lemma17 lemma19 where + lemma11 q ex = lemma17 lemma19 where lemma17 : exists finab (λ qn → nq qn /\ Nδ NFA (case1 qa) h q) ≡ true → q ≡ case1 (δ (automaton A) qa h) lemma17 en with found← finab en - ... | S with found-q S | found-p S | qa=q (found-q S) (bool-∧→tt-0 ( found-p S)) - ... | (case1 qq) | e1 | refl = lemma21 q refl where + ... | S with found-q S | found-p S | {!!} -- qa=q (bool-∧→tt-0 ( found-p S))(found-q S) + ... | (case1 qq) | e1 | eq = lemma21 q refl where lemma20 : nq (case1 qa) /\ Concat-NFA.δnfa A B (case1 qa) h q ≡ true - lemma20 = e1 + lemma20 = {!!} lemma21 : (qq : states A ∨ states B) → qq ≡ q → q ≡ case1 (δ (automaton A) qa h) lemma21 (case1 x) refl = cong ( λ k → case1 k ) (sym lemma23 ) where lemma23 : (δ (automaton A) qa h) ≡ x lemma23 = equal→refl (afin A) ( bool-∧→tt-1 e1) - lemma21 (case2 x) refl = {!!} -- ⊥-elim (ne (bool-∧→tt-1 e1)) + lemma21 (case2 x) refl with bool-≡-? (aend (automaton A) qa) true + ... | no not1 = ⊥-elim ( not1 ( bool-∧→tt-0 ( bool-∧→tt-1 e1))) + ... | yes a-end = ⊥-elim ( ne (bool-and-tt a-end lemma25 ) ) where + lemma24 : aend (automaton A) qa /\ (equal? (afin B) x (δ (automaton B) (astart B) h)) ≡ true + lemma24 = bool-∧→tt-1 e1 + lemma25 : accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true + lemma25 = contain-B h t nq (astart B) {!!} fn lemma18 : (qn : states A ∨ states B) → nq qn /\ Nδ NFA qn h q ≡ true → nq qn /\ Nδ NFA (case1 qa) h q ≡ true lemma18 qn eq = begin nq qn /\ Nδ NFA (case1 qa) h q - ≡⟨ cong ( λ k → nq qn /\ Nδ NFA k h q ) (sym ( qa=q qn (bool-∧→tt-0 eq ) )) ⟩ + ≡⟨ cong ( λ k → nq qn /\ Nδ NFA k h q ) (sym {!!}) ⟩ nq qn /\ Nδ NFA qn h q ≡⟨ eq ⟩ true @@ -321,12 +337,12 @@ fq = found-q ( found← finab ex ) lemma14 : split (λ t1 → accept (automaton A) qa (h ∷ t1)) (contain B) t ≡ true - lemma14 = lemma13 t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) (nmove (case1 qa) nq qat h) lemma11 + lemma14 = contain-A t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) (nmove (case1 qa) nq qat h) lemma11-1 lemma10 : Naccept NFA finab (equal? finab (case1 (astart A))) x ≡ true → split (contain A) (contain B) x ≡ true - lemma10 CC = lemma13 x (Concat-NFA-start A B ) CC (astart A) (equal?-refl finab) lemma12 where - lemma12 : (q : states A ∨ states B) → Concat-NFA-start A B q ≡ true → q ≡ case1 (astart A) - lemma12 q eq = sym ( equal→refl finab eq ) + lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) (equal?-refl finab) lemma12-1 where + lemma12-1 : (q : states A ∨ states B) → condition-A (Concat-NFA-start A B) (astart A) q + lemma12-1 q = case1 (λ eq → sym ( equal→refl finab eq ) ) 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