-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathpumping.v
More file actions
209 lines (191 loc) · 5.73 KB
/
pumping.v
File metadata and controls
209 lines (191 loc) · 5.73 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
Require Import Coq.Lists.List.
Import List.ListNotations.
Inductive reg_exp {T : Type} : Type :=
| EmptySet
| EmptyStr
| Char (t : T)
| App (r1 r2 : reg_exp)
| Union (r1 r2 : reg_exp)
| Star (r : reg_exp).
Inductive exp_match {T} : list T -> reg_exp -> Prop :=
| MEmpty : exp_match [] EmptyStr
| MChar x : exp_match [x] (Char x)
| MApp s1 re1 s2 re2
(H1 : exp_match s1 re1)
(H2 : exp_match s2 re2) :
exp_match (s1 ++ s2) (App re1 re2)
| MUnionL s1 re1 re2
(H1 : exp_match s1 re1) :
exp_match s1 (Union re1 re2)
| MUnionR re1 s2 re2
(H2 : exp_match s2 re2) :
exp_match s2 (Union re1 re2)
| MStar0 re : exp_match [] (Star re)
| MStarApp s1 s2 re
(H1 : exp_match s1 re)
(H2 : exp_match s2 (Star re)) :
exp_match (s1 ++ s2) (Star re).
Notation "s =~ re" := (exp_match s re) (at level 80).
Lemma MStar1 :
forall T s (re : @reg_exp T) ,
s =~ re ->
s =~ Star re.
Proof.
intros T s re H.
rewrite <- (app_nil_r s).
apply (MStarApp s [] re).
- apply H.
- apply MStar0.
Qed.
Lemma star_app: forall T (s1 s2 : list T) (re : reg_exp),
s1 =~ Star re ->
s2 =~ Star re ->
s1 ++ s2 =~ Star re.
Proof.
intros T s1 s2 re H1.
remember (Star re) as re'.
generalize dependent s2.
induction H1
as [|x'|s1 re1 s2' re2 Hmatch1 IH1 Hmatch2 IH2
|s1 re1 re2 Hmatch IH|re1 s2' re2 Hmatch IH
|re''|s1 s2' re'' Hmatch1 IH1 Hmatch2 IH2].
- (* MEmpty *) discriminate.
- (* MChar *) discriminate Heqre'.
- (* MApp *) discriminate.
- (* MUnionL *) discriminate.
- (* MUnionR *) discriminate.
- (* MStar0 *)
injection Heqre'. intros Heqre'' s H. simpl. apply H.
- (* MStarApp *)
injection Heqre'. intros H0.
intros s2 H1. rewrite <- app_assoc.
apply MStarApp.
+ apply Hmatch1.
+ apply IH2.
* rewrite H0. reflexivity.
* apply H1.
Qed.
Fixpoint pumping_constant {T} (re : @reg_exp T) : nat :=
match re with
| EmptySet => 0
| EmptyStr => 1
| Char _ => 2
| App re1 re2 =>
pumping_constant re1 + pumping_constant re2
| Union re1 re2 =>
pumping_constant re1 + pumping_constant re2
| Star _ => 1
end.
Fixpoint napp {T} (n : nat) (l : list T) : list T :=
match n with
| 0 => []
| S n' => l ++ napp n' l
end.
Lemma napp_plus: forall T (n m : nat) (l : list T),
napp (n + m) l = napp n l ++ napp m l.
Proof.
intros T n m l.
induction n as [|n IHn].
- reflexivity.
- simpl. rewrite IHn, app_assoc. reflexivity.
Qed.
Require Import Coq.omega.Omega.
Require Export Logic.
Lemma sum_le: forall (n1 n2 n3 n4 : nat), n1 + n2 <= n3 + n4 -> n1 <= n3 \/ n2 <= n4.
Proof.
intros n1 n2 n3 n4 H.
omega.
Qed.
Lemma sum_le2: forall (n1 n2 n3 : nat), n1 + n2 <= n3 -> n1 <= n3 /\ n2 <= n3.
Proof.
intros n1 n2 n3 H. split.
- omega.
- omega.
Qed.
Lemma length_le: forall T (s1 s2 : list T), 1 <= length (s1 ++ s2) -> 1 <= length s1 \/ 1 <= length s2.
Proof.
intros T s1 s2 H.
rewrite app_length in H.
omega.
Qed.
Lemma pumping : forall T (re : @reg_exp T) s,
s =~ re ->
pumping_constant re <= length s ->
exists s1 s2 s3,
s = s1 ++ s2 ++ s3 /\
s2 <> [] /\
forall m, s1 ++ napp m s2 ++ s3 =~ re.
Proof.
intros T re s Hmatch.
induction Hmatch
as [ | x | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
| s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
| re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2 ].
- simpl. omega.
- simpl. omega.
- simpl. rewrite app_length. intro H.
apply sum_le in H. destruct H.
+ apply IH1 in H.
destruct H as [x0 [x1 [x2]]].
destruct H as [Hs [Hx Happ]]. clear IH1. clear IH2.
exists x0, x1, (x2 ++ s2). split.
* rewrite Hs. repeat rewrite <- app_assoc. reflexivity.
* split.
** trivial.
** intros m. rewrite app_assoc. rewrite app_assoc. apply MApp.
*** rewrite <- app_assoc. apply Happ.
*** apply Hmatch2.
+ apply IH2 in H.
destruct H as [x0 [x1 [x2]]].
destruct H as [Hs [Hx Happ]]. clear IH1. clear IH2.
exists (s1 ++ x0), x1, x2. split.
* rewrite Hs. repeat rewrite <- app_assoc. trivial.
* split.
** apply Hx.
** intros m. repeat rewrite <- app_assoc. apply MApp.
*** apply Hmatch1.
*** apply Happ.
- simpl. intros H. apply sum_le2 in H. destruct H. apply IH in H. clear IH. clear H0.
destruct H as [x1 [x2 [x3]]].
destruct H as [H0 [H1 H2]].
exists x1, x2, x3. split.
+ apply H0.
+ split.
* apply H1.
* intros m. apply MUnionL. apply H2.
- simpl. intros H. rewrite plus_comm in H. apply sum_le2 in H.
destruct H. apply IH in H. clear IH. clear H0.
destruct H as [x1 [x2 [x3]]].
destruct H as [H0 [H1 H2]].
exists x1, x2, x3. split.
+ apply H0.
+ split.
* apply H1.
* intros m. apply MUnionR.
apply H2.
- simpl. omega.
- simpl in *. intros H. apply length_le in H.
destruct H.
* exists [], s1,s2. split.
** simpl. trivial.
** split.
*** induction s1.
**** inversion H.
**** unfold not. intros HH. inversion HH.
*** intros m. simpl. apply star_app.
**** induction m.
***** simpl. apply MStar0.
***** simpl. apply star_app. apply MStar1. apply Hmatch1. apply IHm.
**** apply Hmatch2.
* apply IH2 in H.
destruct H as [x1 [x2 [x3]]].
destruct H as [H0 [H1 H2]].
exists (s1 ++ x1), x2, x3.
split.
** rewrite H0. repeat rewrite <- app_assoc. trivial.
** split.
*** apply H1.
*** intros m. rewrite <- app_assoc. apply MStarApp.
**** apply Hmatch1.
**** apply H2.
Qed.