-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathEx.v
163 lines (148 loc) · 6.1 KB
/
Ex.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
Require Export Pump.
Require Import Arith.
Require Import Coq.Arith.Arith.
Definition exp_equiv {T} (ss : list (list T)) (re : reg_exp T) : Prop :=
forall s, In s ss <-> exp_match s re.
Lemma empty_equiv :
forall (T: Type), exp_equiv [] EmptySet (T := T).
Proof.
intros. unfold exp_equiv.
intros. split.
- (* In s [] -> s =~ EmptySet *)
intro.
inversion H. (* Discriminate In s [] *)
- (* s =~ EmptySet -> In s [] *)
intro.
inversion H. (* Discriminate s =~ EmptySet *)
Qed.
Lemma list_equiv {T} (l1 l2 l3 l4: list T) :
l1 ++ l2 = l3 ++ l4 -> length l1 = length l3 -> l1 = l3 /\ l2 = l4.
Proof.
intros.
apply app_eq_app in H.
do 2 destruct H.
- destruct H. rewrite H in H0. rewrite app_length in H0.
rewrite plus_n_O in H0. apply Nat.add_cancel_l in H0.
destruct x.
+ simpl in *. rewrite app_nil_r in H. auto.
+ inversion H0.
- destruct H. rewrite H in H0. rewrite app_length in H0.
rewrite (plus_n_O (length l1)) in H0 at 1. apply Nat.add_cancel_l in H0.
destruct x.
+ simpl in *. rewrite app_nil_r in H. auto.
+ inversion H0.
Qed.
Lemma napp_zero_one_equiv (p q r s: nat) :
napp p [0] ++ napp q [1] = napp r [0] ++ napp s [1] -> p = r /\ q = s.
Proof.
intros.
(* We divide the cases as `p <= r` or `r <= p` to induce contradiction from the head of lists *)
specialize (Nat.le_ge_cases p r). intro.
(* We first prove a lemma that will solve both cases at once *)
assert (Hl: forall a b c d, napp a [0] ++ napp b [1] = napp c [0] ++ napp d [1] -> a <= c -> a = c /\ b = d). {
intros.
apply Arith_prebase.le_plus_minus_r_stt in H2 as H2'.
rewrite <- H2' in H1. rewrite napp_plus in H1. rewrite <- app_assoc in H1.
apply list_equiv in H1.
- destruct H1. clear H1 H2'.
(*
napp b [1] = napp (c - a) [0] ++ napp d [1]
We destruct `c - a` to earn `b = d` when `c = a`. The leftover case is discriminated.
*)
destruct (c - a) eqn:Hca.
+ simpl in *. apply Nat.sub_0_le in Hca. split.
* apply Nat.le_antisymm; auto.
* assert (length (napp b [1]) = length (napp d [1])). f_equal. auto.
repeat rewrite napp_length in H1. simpl in H1. repeat rewrite Nat.mul_1_r in H1. auto.
+ simpl in H3. destruct b.
* simpl in H3. discriminate.
* simpl in H3. discriminate.
- auto.
}
destruct H0.
(* After destruction, we simply apply the above assertion *)
- apply Hl; auto.
- symmetry in H. apply (Hl r s p q) in H; try auto.
destruct H. split; auto.
Qed.
(* A list definition of the string 0^n1^n *)
Definition zero_n_one_n (n : nat) : list nat :=
napp n [0] ++ napp n [1].
(* A set of all 0^n1^ns *)
Definition zero_n_one_n_lang (ss : list (list nat)): Prop :=
forall s, In s ss <-> exists m, s = zero_n_one_n m.
(* A proof that `zero_n_one_n_lang` is not a regular language *)
Theorem zero_n_one_n_lang_not_regular :
forall (ss : list (list nat)), zero_n_one_n_lang ss -> ~(exists re, exp_equiv ss re).
Proof.
(* We first assume an equivalent regular expression `re` *)
intros. intro. destruct H0 as [re H0].
unfold exp_equiv in H0.
unfold zero_n_one_n_lang in H.
(* We now set up the string 0^t1^t to induce a contradiction in the pumping theorem *)
remember (pumping_constant re) as t.
remember (zero_n_one_n t) as xyz.
(* Step 1. We first show that xyz =~ re *)
assert (exists m : nat, xyz = zero_n_one_n m). exists t. auto.
apply H in H1. apply H0 in H1 as Hre. (* Hre : xyz =~ re *)
(* Step 2. Apply pumping theorem to xyz *)
apply pumping in Hre.
(* Now we induce contradiction from the existence of x, y, z in the pumping theorem *)
destruct Hre as [x [y [z Hre]]].
(* Hre : xyz = x ++ y ++ z /\ y <> [] /\ length x + length y <= pumping_constant re
/\ (forall m : nat, x ++ napp m y ++ z =~ re) *)
destruct Hre as [Hp1 [Hp2 [Hp3 Hp4]]].
rewrite <- Heqt in Hp3.
(* We will use x ++ napp 0 y ++ z = x ++ z *)
specialize (Hp4 0).
simpl in Hp4. remember (x ++ z) as xz.
(* The reverse process of proving xyz =~ re *)
apply H0 in Hp4. apply H in Hp4.
(* Hp4 : exists m : nat, xz = zero_n_one_n m *)
assert (xyz = napp (length x) [0] ++ napp (length y) [0] ++ napp (t - (length x + length y)) [0] ++ napp t [1]). {
rewrite Heqxyz.
rewrite (app_assoc (napp (length x) [0]) _ _).
rewrite <- (napp_plus (nat) (length x) (length y) [0]).
rewrite (app_assoc _ _ (napp t [1])).
rewrite <- napp_plus.
unfold zero_n_one_n.
repeat f_equal.
(* Now the goal shrinks to t = length x + length y + (t - (length x + length y)) *)
symmetry.
rewrite Nat.add_comm. apply Nat.sub_add. auto.
}
rewrite Hp1 in H2.
apply list_equiv in H2.
{
destruct H2. apply list_equiv in H3. destruct H3.
(* We now have x = napp (length x) [0] and z = napp (t - (length x + length y)) [0] ++ napp t [1] *)
rewrite Heqxz in Hp4.
rewrite H2 in Hp4. rewrite H4 in Hp4.
unfold zero_n_one_n in Hp4.
rewrite app_assoc in Hp4.
rewrite <- (napp_plus nat (length x) _ [0]) in Hp4.
destruct Hp4 as [m Hp4].
apply napp_zero_one_equiv in Hp4.
destruct Hp4. rewrite <- H6 in H5.
(* We now have H5 : length x + (t - (length x + length y)) = t *)
rewrite Nat.add_sub_assoc in H5.
rewrite <- Arith_prebase.minus_plus_simpl_l_reverse_stt in H5.
apply Nat.add_sub_eq_nz in H5.
(* H5 : length y + t = t *)
rewrite Nat.add_comm in H5. rewrite plus_n_O in H5.
rewrite Nat.add_cancel_l in H5.
(* H5 : length y = 0. This is contradictory with Hp2: y <> []! *)
destruct y eqn:Hy. contradiction. discriminate.
(* The core proof process is over since we created a contradiction.
We now take care of the side-effect goals made during some `apply`s.
Most are derived almost directly from the assumptions. *)
- rewrite Heqt. intro. apply pumping_constant_0_false in H7. auto.
- auto.
- rewrite napp_length. simpl. rewrite Nat.mul_1_r. auto.
}
- rewrite napp_length. simpl. rewrite Nat.mul_1_r. auto.
- rewrite <- Heqt. rewrite Heqxyz.
unfold zero_n_one_n. rewrite app_length.
repeat rewrite napp_length. simpl.
repeat rewrite Nat.mul_1_r. apply Nat.le_add_r.
Qed.