|
141
|
1 module regular-concat where
|
|
|
2
|
|
|
3 open import Level renaming ( suc to Suc ; zero to Zero )
|
|
|
4 open import Data.List
|
|
|
5 open import Data.Nat hiding ( _≟_ )
|
|
|
6 open import Data.Fin hiding ( _+_ )
|
|
|
7 open import Data.Empty
|
|
|
8 open import Data.Unit
|
|
|
9 open import Data.Product
|
|
|
10 -- open import Data.Maybe
|
|
|
11 open import Relation.Nullary
|
|
|
12 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
13 open import logic
|
|
|
14 open import nat
|
|
|
15 open import automaton
|
|
268
|
16 open import regular-language
|
|
141
|
17
|
|
|
18 open import nfa
|
|
|
19 open import sbconst2
|
|
268
|
20 open import finiteSet
|
|
|
21 open import finiteSetUtil
|
|
141
|
22
|
|
268
|
23 open Automaton
|
|
|
24 open FiniteSet
|
|
|
25
|
|
269
|
26 open RegularLanguage
|
|
268
|
27
|
|
|
28 Concat-NFA : {Σ : Set} → (A B : RegularLanguage Σ ) → NAutomaton (states A ∨ states B) Σ
|
|
|
29 Concat-NFA {Σ} A B = record { Nδ = δnfa ; Nend = nend }
|
|
141
|
30 module Concat-NFA where
|
|
|
31 δnfa : states A ∨ states B → Σ → states A ∨ states B → Bool
|
|
268
|
32 δnfa (case1 q) i (case1 q₁) = equal? (afin A) (δ (automaton A) q i) q₁
|
|
|
33 δnfa (case1 qa) i (case2 qb) = (aend (automaton A) qa ) /\
|
|
|
34 (equal? (afin B) qb (δ (automaton B) (astart B) i) )
|
|
|
35 δnfa (case2 q) i (case2 q₁) = equal? (afin B) (δ (automaton B) q i) q₁
|
|
141
|
36 δnfa _ i _ = false
|
|
|
37 nend : states A ∨ states B → Bool
|
|
|
38 nend (case2 q) = aend (automaton B) q
|
|
|
39 nend (case1 q) = aend (automaton A) q /\ aend (automaton B) (astart B) -- empty B case
|
|
|
40
|
|
268
|
41 Concat-NFA-start : {Σ : Set} → (A B : RegularLanguage Σ ) → states A ∨ states B → Bool
|
|
|
42 Concat-NFA-start A B q = equal? (fin-∨ (afin A) (afin B)) (case1 (astart A)) q
|
|
|
43
|
|
|
44 CNFA-exist : {Σ : Set} → (A B : RegularLanguage Σ ) → (states A ∨ states B → Bool) → Bool
|
|
|
45 CNFA-exist A B qs = exists (fin-∨ (afin A) (afin B)) qs
|
|
141
|
46
|
|
268
|
47 M-Concat : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
|
|
|
48 M-Concat {Σ} A B = record {
|
|
141
|
49 states = states A ∨ states B → Bool
|
|
268
|
50 ; astart = Concat-NFA-start A B
|
|
|
51 ; afin = finf
|
|
|
52 ; automaton = subset-construction (CNFA-exist A B) (Concat-NFA A B)
|
|
141
|
53 } where
|
|
268
|
54 fin : FiniteSet (states A ∨ states B )
|
|
|
55 fin = fin-∨ (afin A) (afin B)
|
|
|
56 finf : FiniteSet (states A ∨ states B → Bool )
|
|
|
57 finf = fin→ fin
|
|
141
|
58
|
|
|
59 record Split {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (x : List Σ ) : Set where
|
|
|
60 field
|
|
|
61 sp0 : List Σ
|
|
|
62 sp1 : List Σ
|
|
|
63 sp-concat : sp0 ++ sp1 ≡ x
|
|
|
64 prop0 : A sp0 ≡ true
|
|
|
65 prop1 : B sp1 ≡ true
|
|
|
66
|
|
|
67 open Split
|
|
|
68
|
|
|
69 list-empty++ : {Σ : Set} → (x y : List Σ) → x ++ y ≡ [] → (x ≡ [] ) ∧ (y ≡ [] )
|
|
|
70 list-empty++ [] [] refl = record { proj1 = refl ; proj2 = refl }
|
|
|
71 list-empty++ [] (x ∷ y) ()
|
|
|
72 list-empty++ (x ∷ x₁) y ()
|
|
|
73
|
|
|
74 open _∧_
|
|
|
75
|
|
|
76 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
77
|
|
|
78 c-split-lemma : {Σ : Set} → (A B : List Σ → Bool ) → (h : Σ) → ( t : List Σ ) → split A B (h ∷ t ) ≡ true
|
|
|
79 → ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) )
|
|
|
80 → split (λ t1 → A (h ∷ t1)) B t ≡ true
|
|
|
81 c-split-lemma {Σ} A B h t eq p = sym ( begin
|
|
|
82 true
|
|
|
83 ≡⟨ sym eq ⟩
|
|
|
84 split A B (h ∷ t )
|
|
|
85 ≡⟨⟩
|
|
|
86 A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t
|
|
|
87 ≡⟨ cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (lemma-p p ) ⟩
|
|
|
88 false \/ split (λ t1 → A (h ∷ t1)) B t
|
|
|
89 ≡⟨ bool-or-1 refl ⟩
|
|
|
90 split (λ t1 → A (h ∷ t1)) B t
|
|
|
91 ∎ ) where
|
|
|
92 open ≡-Reasoning
|
|
|
93 lemma-p : ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) ) → A [] /\ B (h ∷ t) ≡ false
|
|
|
94 lemma-p (case1 ¬A ) = bool-and-1 ( ¬-bool-t ¬A )
|
|
|
95 lemma-p (case2 ¬B ) = bool-and-2 ( ¬-bool-t ¬B )
|
|
|
96
|
|
|
97 split→AB : {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → split A B x ≡ true → Split A B x
|
|
|
98 split→AB {Σ} A B [] eq with bool-≡-? (A []) true | bool-≡-? (B []) true
|
|
|
99 split→AB {Σ} A B [] eq | yes eqa | yes eqb =
|
|
|
100 record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = eqa ; prop1 = eqb }
|
|
|
101 split→AB {Σ} A B [] eq | yes p | no ¬p = ⊥-elim (lemma-∧-1 eq (¬-bool-t ¬p ))
|
|
|
102 split→AB {Σ} A B [] eq | no ¬p | t = ⊥-elim (lemma-∧-0 eq (¬-bool-t ¬p ))
|
|
|
103 split→AB {Σ} A B (h ∷ t ) eq with bool-≡-? (A []) true | bool-≡-? (B (h ∷ t )) true
|
|
|
104 ... | yes px | yes py = record { sp0 = [] ; sp1 = h ∷ t ; sp-concat = refl ; prop0 = px ; prop1 = py }
|
|
|
105 ... | no px | _ with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case1 px) )
|
|
|
106 ... | S = record { sp0 = h ∷ sp0 S ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S }
|
|
|
107 split→AB {Σ} A B (h ∷ t ) eq | _ | no px with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case2 px) )
|
|
|
108 ... | S = record { sp0 = h ∷ sp0 S ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S }
|
|
|
109
|
|
|
110 AB→split : {Σ : Set} → (A B : List Σ → Bool ) → ( x y : List Σ ) → A x ≡ true → B y ≡ true → split A B (x ++ y ) ≡ true
|
|
|
111 AB→split {Σ} A B [] [] eqa eqb = begin
|
|
|
112 split A B []
|
|
|
113 ≡⟨⟩
|
|
|
114 A [] /\ B []
|
|
|
115 ≡⟨ cong₂ (λ j k → j /\ k ) eqa eqb ⟩
|
|
|
116 true
|
|
|
117 ∎ where open ≡-Reasoning
|
|
|
118 AB→split {Σ} A B [] (h ∷ y ) eqa eqb = begin
|
|
|
119 split A B (h ∷ y )
|
|
|
120 ≡⟨⟩
|
|
|
121 A [] /\ B (h ∷ y) \/ split (λ t1 → A (h ∷ t1)) B y
|
|
|
122 ≡⟨ cong₂ (λ j k → j /\ k \/ split (λ t1 → A (h ∷ t1)) B y ) eqa eqb ⟩
|
|
|
123 true /\ true \/ split (λ t1 → A (h ∷ t1)) B y
|
|
|
124 ≡⟨⟩
|
|
|
125 true \/ split (λ t1 → A (h ∷ t1)) B y
|
|
|
126 ≡⟨⟩
|
|
|
127 true
|
|
|
128 ∎ where open ≡-Reasoning
|
|
|
129 AB→split {Σ} A B (h ∷ t) y eqa eqb = begin
|
|
|
130 split A B ((h ∷ t) ++ y)
|
|
|
131 ≡⟨⟩
|
|
|
132 A [] /\ B (h ∷ t ++ y) \/ split (λ t1 → A (h ∷ t1)) B (t ++ y)
|
|
|
133 ≡⟨ cong ( λ k → A [] /\ B (h ∷ t ++ y) \/ k ) (AB→split {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ) ⟩
|
|
|
134 A [] /\ B (h ∷ t ++ y) \/ true
|
|
|
135 ≡⟨ bool-or-3 ⟩
|
|
|
136 true
|
|
|
137 ∎ where open ≡-Reasoning
|
|
|
138
|
|
|
139 open NAutomaton
|
|
|
140 open import Data.List.Properties
|
|
|
141
|
|
163
|
142 closed-in-concat : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
|
|
141
|
143 closed-in-concat {Σ} A B x = ≡-Bool-func closed-in-concat→ closed-in-concat← where
|
|
163
|
144 finab = (fin-∨ (afin A) (afin B))
|
|
|
145 NFA = (Concat-NFA A B)
|
|
141
|
146 abmove : (q : states A ∨ states B) → (h : Σ ) → states A ∨ states B
|
|
|
147 abmove (case1 q) h = case1 (δ (automaton A) q h)
|
|
|
148 abmove (case2 q) h = case2 (δ (automaton B) q h)
|
|
|
149 lemma-nmove-ab : (q : states A ∨ states B) → (h : Σ ) → Nδ NFA q h (abmove q h) ≡ true
|
|
268
|
150 lemma-nmove-ab (case1 q) h = equal?-refl (afin A)
|
|
|
151 lemma-nmove-ab (case2 q) h = equal?-refl (afin B)
|
|
141
|
152 nmove : (q : states A ∨ states B) (nq : states A ∨ states B → Bool ) → (nq q ≡ true) → ( h : Σ ) →
|
|
163
|
153 exists finab (λ qn → nq qn /\ Nδ NFA qn h (abmove q h)) ≡ true
|
|
|
154 nmove (case1 q) nq nqt h = found finab (case1 q) ( bool-and-tt nqt (lemma-nmove-ab (case1 q) h) )
|
|
|
155 nmove (case2 q) nq nqt h = found finab (case2 q) ( bool-and-tt nqt (lemma-nmove-ab (case2 q) h) )
|
|
141
|
156 acceptB : (z : List Σ) → (q : states B) → (nq : states A ∨ states B → Bool ) → (nq (case2 q) ≡ true) → ( accept (automaton B) q z ≡ true )
|
|
268
|
157 → Naccept NFA (CNFA-exist A B) nq z ≡ true
|
|
141
|
158 acceptB [] q nq nqt fb = lemma8 where
|
|
163
|
159 lemma8 : exists finab ( λ q → nq q /\ Nend NFA q ) ≡ true
|
|
|
160 lemma8 = found finab (case2 q) ( bool-and-tt nqt fb )
|
|
268
|
161 acceptB (h ∷ t ) q nq nq=q fb = acceptB t (δ (automaton B) q h) (Nmoves NFA (CNFA-exist A B) nq h) (nmove (case2 q) nq nq=q h) fb
|
|
141
|
162
|
|
|
163 acceptA : (y z : List Σ) → (q : states A) → (nq : states A ∨ states B → Bool ) → (nq (case1 q) ≡ true)
|
|
|
164 → ( accept (automaton A) q y ≡ true ) → ( accept (automaton B) (astart B) z ≡ true )
|
|
268
|
165 → Naccept NFA (CNFA-exist A B) nq (y ++ z) ≡ true
|
|
163
|
166 acceptA [] [] q nq nqt fa fb = found finab (case1 q) (bool-and-tt nqt (bool-and-tt fa fb ))
|
|
268
|
167 acceptA [] (h ∷ z) q nq nq=q fa fb = acceptB z nextb (Nmoves NFA (CNFA-exist A B) nq h) lemma70 fb where
|
|
141
|
168 nextb : states B
|
|
|
169 nextb = δ (automaton B) (astart B) h
|
|
163
|
170 lemma70 : exists finab (λ qn → nq qn /\ Nδ NFA qn h (case2 nextb)) ≡ true
|
|
|
171 lemma70 = found finab (case1 q) ( bool-and-tt nq=q (bool-and-tt fa (lemma-nmove-ab (case2 (astart B)) h) ))
|
|
268
|
172 acceptA (h ∷ t) z q nq nq=q fa fb = acceptA t z (δ (automaton A) q h) (Nmoves NFA (CNFA-exist A B) nq h) (nmove (case1 q) nq nq=q h) fa fb
|
|
141
|
173
|
|
|
174 acceptAB : Split (contain A) (contain B) x
|
|
268
|
175 → Naccept NFA (CNFA-exist A B) (equal? finab (case1 (astart A))) x ≡ true
|
|
|
176 acceptAB S = subst ( λ k → Naccept NFA (CNFA-exist A B) (equal? finab (case1 (astart A))) k ≡ true ) ( sp-concat S )
|
|
|
177 (acceptA (sp0 S) (sp1 S) (astart A) (equal? finab (case1 (astart A))) (equal?-refl finab) (prop0 S) (prop1 S) )
|
|
141
|
178
|
|
163
|
179 closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true
|
|
|
180 closed-in-concat→ concat with split→AB (contain A) (contain B) x concat
|
|
|
181 ... | S = begin
|
|
268
|
182 accept (subset-construction (CNFA-exist A B) (Concat-NFA A B) ) (Concat-NFA-start A B ) x
|
|
|
183 ≡⟨ ≡-Bool-func (subset-construction-lemma← (CNFA-exist A B) NFA (equal? finab (case1 (astart A))) x )
|
|
|
184 (subset-construction-lemma→ (CNFA-exist A B) NFA (equal? finab (case1 (astart A))) x ) ⟩
|
|
|
185 Naccept NFA (CNFA-exist A B) (equal? finab (case1 (astart A))) x
|
|
163
|
186 ≡⟨ acceptAB S ⟩
|
|
|
187 true
|
|
|
188 ∎ where open ≡-Reasoning
|
|
|
189
|
|
|
190 open Found
|
|
141
|
191
|
|
|
192 ab-case : (q : states A ∨ states B ) → (qa : states A ) → (x : List Σ ) → Set
|
|
|
193 ab-case (case1 qa') qa x = qa' ≡ qa
|
|
|
194 ab-case (case2 qb) qa x = ¬ ( accept (automaton B) qb x ≡ true )
|
|
|
195
|
|
268
|
196 contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA (CNFA-exist A B) nq x ≡ true )
|
|
141
|
197 → (qa : states A ) → ( (q : states A ∨ states B) → nq q ≡ true → ab-case q qa x )
|
|
|
198 → split (accept (automaton A) qa ) (contain B) x ≡ true
|
|
268
|
199 contain-A [] nq fn qa cond with found← finab fn -- at this stage, A and B must be satisfied with [] (ab-case cond forces it)
|
|
163
|
200 ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S))
|
|
|
201 ... | case1 qa' | record { eq = refl } | refl = bool-∧→tt-1 (found-p S)
|
|
|
202 ... | case2 qb | record { eq = refl } | ab = ⊥-elim ( ab (bool-∧→tt-1 (found-p S)))
|
|
|
203 contain-A (h ∷ t) nq fn qa cond with bool-≡-? ((aend (automaton A) qa) /\ accept (automaton B) (δ (automaton B) (astart B) h) t ) true
|
|
268
|
204 ... | yes eq = bool-or-41 eq -- found A ++ B all end
|
|
|
205 ... | no ne = bool-or-31 (contain-A t (Nmoves NFA (CNFA-exist A B) nq h) fn (δ (automaton A) qa h) lemma11 ) where -- B failed continue with ab-base condtion
|
|
|
206 --- prove ab-ase condition (we haven't checked but case2 b may happen)
|
|
163
|
207 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
|
|
|
208 lemma11 (case1 qa') ex with found← finab ex
|
|
|
209 ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S))
|
|
|
210 ... | case1 qa | record { eq = refl } | refl = sym ( equal→refl (afin A) ( bool-∧→tt-1 (found-p S) )) -- continued A case
|
|
|
211 ... | case2 qb | record { eq = refl } | nb with bool-∧→tt-1 (found-p S) -- δnfa (case2 q) i (case1 q₁) is false
|
|
|
212 ... | ()
|
|
|
213 lemma11 (case2 qb) ex with found← finab ex
|
|
|
214 ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S))
|
|
|
215 lemma11 (case2 qb) ex | S | case2 qb' | record { eq = refl } | nb = contra-position lemma13 nb where -- continued B case should fail
|
|
|
216 lemma13 : accept (automaton B) qb t ≡ true → accept (automaton B) qb' (h ∷ t) ≡ true
|
|
|
217 lemma13 fb = subst (λ k → accept (automaton B) k t ≡ true ) (sym (equal→refl (afin B) (bool-∧→tt-1 (found-p S)))) fb
|
|
|
218 lemma11 (case2 qb) ex | S | case1 qa | record { eq = refl } | refl with bool-∧→tt-1 (found-p S)
|
|
|
219 ... | eee = contra-position lemma12 ne where -- starting B case should fail
|
|
|
220 lemma12 : accept (automaton B) qb t ≡ true → aend (automaton A) qa /\ accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true
|
|
|
221 lemma12 fb = bool-and-tt (bool-∧→tt-0 eee) (subst ( λ k → accept (automaton B) k t ≡ true ) (equal→refl (afin B) (bool-∧→tt-1 eee) ) fb )
|
|
141
|
222
|
|
268
|
223 lemma10 : Naccept NFA (CNFA-exist A B) (equal? finab (case1 (astart A))) x ≡ true → split (contain A) (contain B) x ≡ true
|
|
163
|
224 lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) lemma15 where
|
|
|
225 lemma15 : (q : states A ∨ states B) → Concat-NFA-start A B q ≡ true → ab-case q (astart A) x
|
|
|
226 lemma15 q nq=t with equal→refl finab nq=t
|
|
|
227 ... | refl = refl
|
|
141
|
228
|
|
163
|
229 closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true
|
|
268
|
230 closed-in-concat← C with subset-construction-lemma← (CNFA-exist A B) NFA (equal? finab (case1 (astart A))) x C
|
|
163
|
231 ... | CC = lemma10 CC
|
|
141
|
232
|
|
|
233
|
|
|
234
|
|
|
235
|
