-
Notifications
You must be signed in to change notification settings - Fork 2
/
cfl.v
168 lines (139 loc) · 3.87 KB
/
cfl.v
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
(* ---------------------------------------------------------------------
This file contains definitions and proof scripts related to
(i) closure operations for context-free grammars,
(ii) context-free grammars simplification
(iii) context-free grammar Chomsky normalization and
(iv) pumping lemma for context-free languages.
More information can be found in the paper "Formalization of the
Pumping Lemma for Context-Free Languages", submitted to JFR.
Marcus Vinícius Midena Ramos
--------------------------------------------------------------------- *)
(* --------------------------------------------------------------------- *)
(* CONTEXT FREE LANGUAGES *)
(* --------------------------------------------------------------------- *)
Require Import List.
Require Import Ring.
Require Import Omega.
Require Import misc_arith.
Require Import misc_list.
Require Import cfg.
Require Import emptyrules.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import ListNotations.
Open Scope list_scope.
(* --------------------------------------------------------------------- *)
(* CONTEXT-FREE LANGUAGES - DEFINITIONS *)
(* --------------------------------------------------------------------- *)
Section ContextFreeLanguages_Definitions.
Variables non_terminal terminal: Type.
Notation sentence:= (list terminal).
Definition lang := sentence -> Prop.
Definition lang_of_g (g: cfg non_terminal terminal): lang :=
fun w: sentence => produces g w.
Definition lang_eq (l k: lang) :=
forall w, l w <-> k w.
Definition contains_empty (l: lang): Prop:=
l [].
Definition contains_non_empty (l: lang): Prop:=
exists w: sentence,
l w /\ w <> [].
End ContextFreeLanguages_Definitions.
Infix "==" := lang_eq (at level 80).
Definition cfl (terminal: Type) (l: lang terminal): Prop:=
exists non_terminal: Type,
exists g: cfg non_terminal terminal,
l == lang_of_g g.
(* --------------------------------------------------------------------- *)
(* CONTEXT-FREE LANGUAGES - LEMMAS *)
(* --------------------------------------------------------------------- *)
Section ContextFreeLanguages_Lemma.
Variables non_terminal non_terminal' terminal: Type.
Lemma produces_empty_equiv_contains_empty:
forall g: cfg non_terminal terminal,
produces_empty g <-> contains_empty (lang_of_g g).
Proof.
intros g.
unfold produces_empty.
unfold contains_empty.
unfold lang_of_g.
split; auto.
Qed.
Lemma produces_non_empty_equiv_contains_non_empty:
forall g: cfg non_terminal terminal,
produces_non_empty g <-> contains_non_empty (lang_of_g g).
Proof.
intros g.
unfold produces_non_empty.
unfold contains_non_empty.
unfold lang_of_g.
split; auto.
Qed.
Lemma g_equiv_lang_eq:
forall g: cfg non_terminal terminal,
forall g': cfg non_terminal' terminal,
g_equiv g' g -> lang_of_g g' == lang_of_g g.
Proof.
unfold g_equiv.
unfold lang_of_g.
unfold lang_eq.
intros g g' H1.
split.
- intros H2.
apply H1.
exact H2.
- intros H2.
apply H1.
exact H2.
Qed.
Lemma lang_eq_sym:
forall l1 l2: lang terminal,
l1 == l2 ->
l2 == l1.
Proof.
unfold lang_eq.
intros l1 l2 H1 w.
split.
- intros H2.
apply H1.
exact H2.
- intros H2.
apply H1.
exact H2.
Qed.
Lemma lang_eq_trans:
forall l1 l2 l3: lang terminal,
l1 == l2 ->
l2 == l3 ->
l1 == l3.
Proof.
unfold lang_eq.
intros l1 l2 l3 H1 H3 w.
split.
- intros H4.
apply H3.
apply H1.
exact H4.
- intros H4.
apply H1.
apply H3.
exact H4.
Qed.
Lemma lang_eq_change_g:
forall l: lang terminal,
forall g: cfg non_terminal terminal,
forall g': cfg non_terminal' terminal,
l == lang_of_g g ->
g_equiv g' g ->
l == lang_of_g g'.
Proof.
intros l g g' H1 H2.
apply g_equiv_lang_eq in H2.
apply lang_eq_trans with (l2 := lang_of_g g).
- exact H1.
- apply lang_eq_sym.
exact H2.
Qed.
End ContextFreeLanguages_Lemma.