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
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
|
Require Export Setoid.
Require Export Bool.
(* Standard library. Export, not Import, because if a file
importing the current file wants to use. e.g.,
Theorem eq_true_or : forall b1 b2 : bool, b1 || b2 <-> b1 \/ b2,
then it needs to know about bool and have a notation ||. *)
Require Export QRewrite.
(*
Contents:
- Coercion from bool to Prop
- Extension of the tactics stepl and stepr
- Extentional properties of predicates, relations and functions
(well-definedness and equality)
- Relations on cartesian product
- Miscellaneous
*)
(** Coercion from bool to Prop *)
Definition eq_bool := (@eq bool).
(*Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.*)
(* This has been added to theories/Datatypes.v *)
Coercion eq_true : bool >-> Sortclass.
Theorem eq_true_unfold_pos : forall b : bool, b <-> b = true.
Proof.
intro b; split; intro H. now inversion H. now rewrite H.
Qed.
Theorem eq_true_unfold_neg : forall b : bool, ~ b <-> b = false.
Proof.
intros b; destruct b; simpl; rewrite eq_true_unfold_pos.
split; intro H; [elim (H (refl_equal true)) | discriminate H].
split; intro H; [reflexivity | discriminate].
Qed.
Theorem eq_true_or : forall b1 b2 : bool, b1 || b2 <-> b1 \/ b2.
Proof.
destruct b1; destruct b2; simpl; tauto.
Qed.
Theorem eq_true_and : forall b1 b2 : bool, b1 && b2 <-> b1 /\ b2.
Proof.
destruct b1; destruct b2; simpl; tauto.
Qed.
Theorem eq_true_neg : forall b : bool, negb b <-> ~ b.
Proof.
destruct b; simpl; rewrite eq_true_unfold_pos; rewrite eq_true_unfold_neg;
split; now intro.
Qed.
Theorem eq_true_iff : forall b1 b2 : bool, b1 = b2 <-> (b1 <-> b2).
Proof.
intros b1 b2; split; intro H.
now rewrite H.
destruct b1; destruct b2; simpl; try reflexivity.
apply -> eq_true_unfold_neg. rewrite H. now intro.
symmetry; apply -> eq_true_unfold_neg. rewrite <- H; now intro.
Qed.
(** Extension of the tactics stepl and stepr to make them
applicable to hypotheses *)
Tactic Notation "stepl" constr(t1') "in" hyp(H) :=
match (type of H) with
| ?R ?t1 ?t2 =>
let H1 := fresh in
cut (R t1' t2); [clear H; intro H | stepl t1; [assumption |]]
| _ => fail 1 ": the hypothesis" H "does not have the form (R t1 t2)"
end.
Tactic Notation "stepl" constr(t1') "in" hyp(H) "by" tactic(r) := stepl t1' in H; [| r].
Tactic Notation "stepr" constr(t2') "in" hyp(H) :=
match (type of H) with
| ?R ?t1 ?t2 =>
let H1 := fresh in
cut (R t1 t2'); [clear H; intro H | stepr t2; [assumption |]]
| _ => fail 1 ": the hypothesis" H "does not have the form (R t1 t2)"
end.
Tactic Notation "stepr" constr(t2') "in" hyp(H) "by" tactic(r) := stepr t2' in H; [| r].
(** Extentional properties of predicates, relations and functions *)
Definition predicate (A : Type) := A -> Prop.
Section ExtensionalProperties.
Variables A B C : Type.
Variable EA : relation A.
Variable EB : relation B.
Variable EC : relation C.
(* "wd" stands for "well-defined" *)
Definition fun_wd (f : A -> B) := forall x y : A, EA x y -> EB (f x) (f y).
Definition fun2_wd (f : A -> B -> C) :=
forall x x' : A, EA x x' -> forall y y' : B, EB y y' -> EC (f x y) (f x' y').
Definition eq_fun : relation (A -> B) :=
fun f f' => forall x x' : A, EA x x' -> EB (f x) (f' x').
(* Note that reflexivity of eq_fun means that every function
is well-defined w.r.t. EA and EB, i.e.,
forall x x' : A, EA x x' -> EB (f x) (f x') *)
Definition eq_fun2 (f f' : A -> B -> C) :=
forall x x' : A, EA x x' -> forall y y' : B, EB y y' -> EC (f x y) (f' x' y').
End ExtensionalProperties.
Implicit Arguments fun_wd [A B].
Implicit Arguments fun2_wd [A B C].
Implicit Arguments eq_fun [A B].
Implicit Arguments eq_fun2 [A B C].
Definition predicate_wd (A : Type) (EA : relation A) := fun_wd EA iff.
Definition rel_wd (A B : Type) (EA : relation A) (EB : relation B) :=
fun2_wd EA EB iff.
Implicit Arguments predicate_wd [A].
Implicit Arguments rel_wd [A B].
Ltac solve_predicate_wd :=
unfold predicate_wd;
let x := fresh "x" in
let y := fresh "y" in
let H := fresh "H" in
intros x y H; qiff x y H.
(* The following tactic uses solve_predicate_wd to solve the goals
relating to well-defidedness that are produced by applying induction.
We declare it to take the tactic that applies the induction theorem
and not the induction theorem itself because the tactic may, for
example, supply additional arguments, as does NZinduct_center in
NZBase.v *)
Ltac induction_maker n t :=
try intros until n;
pattern n; t; clear n;
[solve_predicate_wd | ..].
(** Relations on cartesian product. Used in MiscFunct for defining
functions whose domain is a product of sets by primitive recursion *)
Section RelationOnProduct.
Variables A B : Set.
Variable EA : relation A.
Variable EB : relation B.
Hypothesis EA_equiv : equiv A EA.
Hypothesis EB_equiv : equiv B EB.
Definition prod_rel : relation (A * B) :=
fun p1 p2 => EA (fst p1) (fst p2) /\ EB (snd p1) (snd p2).
Lemma prod_rel_refl : reflexive (A * B) prod_rel.
Proof.
unfold reflexive, prod_rel.
destruct x; split; [apply (proj1 EA_equiv) | apply (proj1 EB_equiv)]; simpl.
Qed.
Lemma prod_rel_symm : symmetric (A * B) prod_rel.
Proof.
unfold symmetric, prod_rel.
destruct x; destruct y;
split; [apply (proj2 (proj2 EA_equiv)) | apply (proj2 (proj2 EB_equiv))]; simpl in *; tauto.
Qed.
Lemma prod_rel_trans : transitive (A * B) prod_rel.
Proof.
unfold transitive, prod_rel.
destruct x; destruct y; destruct z; simpl.
intros; split; [apply (proj1 (proj2 EA_equiv)) with (y := a0) |
apply (proj1 (proj2 EB_equiv)) with (y := b0)]; tauto.
Qed.
Theorem prod_rel_equiv : equiv (A * B) prod_rel.
Proof.
unfold equiv; split; [exact prod_rel_refl | split; [exact prod_rel_trans | exact prod_rel_symm]].
Qed.
End RelationOnProduct.
Implicit Arguments prod_rel [A B].
Implicit Arguments prod_rel_equiv [A B].
(** Miscellaneous *)
Theorem neg_false : forall P : Prop, ~ P <-> (P <-> False).
Proof.
intro P; unfold not; split; intro H; [split; intro H1;
[apply H; assumption | elim H1] | apply (proj1 H)].
Qed.
(* This tactic replaces P in the goal with False.
The goal ~ P should be solvable by "apply H". *)
Ltac rewrite_false P H :=
setoid_replace P with False using relation iff;
[| apply -> neg_false; apply H].
Tactic Notation "symmetry" constr(Eq) :=
lazymatch Eq with
| ?E ?t1 ?t2 => setoid_replace (E t1 t2) with (E t2 t1) using relation iff;
[| split; intro; symmetry; assumption]
| _ => fail Eq "does not have the form (E t1 t2)"
end.
Theorem and_cancel_l : forall A B C : Prop,
(B -> A) -> (C -> A ) -> ((A /\ B <-> A /\ C) <-> (B <-> C)).
Proof.
intros; tauto.
Qed.
Theorem and_cancel_r : forall A B C : Prop,
(B -> A) -> (C -> A ) -> ((B /\ A <-> C /\ A) <-> (B <-> C)).
Proof.
intros; tauto.
Qed.
Theorem or_cancel_l : forall A B C : Prop,
(B -> ~A) -> (C -> ~ A) -> ((A \/ B <-> A \/ C) <-> (B <-> C)).
Proof.
intros; tauto.
Qed.
Theorem or_cancel_r : forall A B C : Prop,
(B -> ~A) -> (C -> ~ A) -> ((B \/ A <-> C \/ A) <-> (B <-> C)).
Proof.
intros; tauto.
Qed.
Theorem or_iff_compat_l : forall A B C : Prop,
(B <-> C) -> (A \/ B <-> A \/ C).
Proof.
intros; tauto.
Qed.
Theorem or_iff_compat_r : forall A B C : Prop,
(B <-> C) -> (B \/ A <-> C \/ A).
Proof.
intros; tauto.
Qed.
Lemma iff_stepl : forall A B C : Prop, (A <-> B) -> (A <-> C) -> (C <-> B).
Proof.
intros; tauto.
Qed.
Declare Left Step iff_stepl.
Declare Right Step iff_trans.
Definition comp_bool (x y : comparison) : bool :=
match x, y with
| Lt, Lt => true
| Eq, Eq => true
| Gt, Gt => true
| _, _ => false
end.
Theorem comp_bool_correct : forall x y : comparison,
comp_bool x y <-> x = y.
Proof.
destruct x; destruct y; simpl; split; now intro.
Qed.
Definition LE_Set : forall A : Set, relation A := (@eq).
Lemma eq_equiv : forall A : Set, equiv A (LE_Set A).
Proof.
intro A; unfold equiv, LE_Set, reflexive, symmetric, transitive.
repeat split; [exact (@trans_eq A) | exact (@sym_eq A)].
(* It is interesting how the tactic split proves reflexivity *)
Qed.
Add Relation (fun A : Set => A) LE_Set
reflexivity proved by (fun A : Set => (proj1 (eq_equiv A)))
symmetry proved by (fun A : Set => (proj2 (proj2 (eq_equiv A))))
transitivity proved by (fun A : Set => (proj1 (proj2 (eq_equiv A))))
as EA_rel.
(*
Local Variables:
tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
End:
*)
|
