1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
8
(* Evgeny Makarov, INRIA, 2007 *)
9
(************************************************************************)
11
(*i $Id: NumPrelude.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
13
Require Export Setoid.
15
Set Implicit Arguments.
18
- Coercion from bool to Prop
19
- Extension of the tactics stepl and stepr
20
- Extentional properties of predicates, relations and functions
21
(well-definedness and equality)
22
- Relations on cartesian product
26
(** Coercion from bool to Prop *)
28
(*Definition eq_bool := (@eq bool).*)
30
(*Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.*)
31
(* This has been added to theories/Datatypes.v *)
32
(*Coercion eq_true : bool >-> Sortclass.*)
34
(*Theorem eq_true_unfold_pos : forall b : bool, b <-> b = true.
36
intro b; split; intro H. now inversion H. now rewrite H.
39
Theorem eq_true_unfold_neg : forall b : bool, ~ b <-> b = false.
41
intros b; destruct b; simpl; rewrite eq_true_unfold_pos.
42
split; intro H; [elim (H (refl_equal true)) | discriminate H].
43
split; intro H; [reflexivity | discriminate].
46
Theorem eq_true_or : forall b1 b2 : bool, b1 || b2 <-> b1 \/ b2.
48
destruct b1; destruct b2; simpl; tauto.
51
Theorem eq_true_and : forall b1 b2 : bool, b1 && b2 <-> b1 /\ b2.
53
destruct b1; destruct b2; simpl; tauto.
56
Theorem eq_true_neg : forall b : bool, negb b <-> ~ b.
58
destruct b; simpl; rewrite eq_true_unfold_pos; rewrite eq_true_unfold_neg;
62
Theorem eq_true_iff : forall b1 b2 : bool, b1 = b2 <-> (b1 <-> b2).
64
intros b1 b2; split; intro H.
66
destruct b1; destruct b2; simpl; try reflexivity.
67
apply -> eq_true_unfold_neg. rewrite H. now intro.
68
symmetry; apply -> eq_true_unfold_neg. rewrite <- H; now intro.
71
(** Extension of the tactics stepl and stepr to make them
72
applicable to hypotheses *)
74
Tactic Notation "stepl" constr(t1') "in" hyp(H) :=
75
match (type of H) with
78
cut (R t1' t2); [clear H; intro H | stepl t1; [assumption |]]
79
| _ => fail 1 ": the hypothesis" H "does not have the form (R t1 t2)"
82
Tactic Notation "stepl" constr(t1') "in" hyp(H) "by" tactic(r) := stepl t1' in H; [| r].
84
Tactic Notation "stepr" constr(t2') "in" hyp(H) :=
85
match (type of H) with
88
cut (R t1 t2'); [clear H; intro H | stepr t2; [assumption |]]
89
| _ => fail 1 ": the hypothesis" H "does not have the form (R t1 t2)"
92
Tactic Notation "stepr" constr(t2') "in" hyp(H) "by" tactic(r) := stepr t2' in H; [| r].
94
(** Extentional properties of predicates, relations and functions *)
96
Definition predicate (A : Type) := A -> Prop.
98
Section ExtensionalProperties.
100
Variables A B C : Type.
101
Variable Aeq : relation A.
102
Variable Beq : relation B.
103
Variable Ceq : relation C.
105
(* "wd" stands for "well-defined" *)
107
Definition fun_wd (f : A -> B) := forall x y : A, Aeq x y -> Beq (f x) (f y).
109
Definition fun2_wd (f : A -> B -> C) :=
110
forall x x' : A, Aeq x x' -> forall y y' : B, Beq y y' -> Ceq (f x y) (f x' y').
112
Definition fun_eq : relation (A -> B) :=
113
fun f f' => forall x x' : A, Aeq x x' -> Beq (f x) (f' x').
115
(* Note that reflexivity of fun_eq means that every function
116
is well-defined w.r.t. Aeq and Beq, i.e.,
117
forall x x' : A, Aeq x x' -> Beq (f x) (f x') *)
119
Definition fun2_eq (f f' : A -> B -> C) :=
120
forall x x' : A, Aeq x x' -> forall y y' : B, Beq y y' -> Ceq (f x y) (f' x' y').
122
End ExtensionalProperties.
124
(* The following definitions instantiate Beq or Ceq to iff; therefore, they
125
have to be outside the ExtensionalProperties section *)
127
Definition predicate_wd (A : Type) (Aeq : relation A) := fun_wd Aeq iff.
129
Definition relation_wd (A B : Type) (Aeq : relation A) (Beq : relation B) :=
132
Definition relations_eq (A B : Type) (R1 R2 : A -> B -> Prop) :=
133
forall (x : A) (y : B), R1 x y <-> R2 x y.
135
Theorem relations_eq_equiv :
136
forall (A B : Type), equiv (A -> B -> Prop) (@relations_eq A B).
138
intros A B; unfold equiv. split; [| split];
139
unfold reflexive, symmetric, transitive, relations_eq.
141
intros R1 R2 R3 H1 H2 x y; rewrite H1; apply H2.
145
Add Parametric Relation (A B : Type) : (A -> B -> Prop) (@relations_eq A B)
146
reflexivity proved by (proj1 (relations_eq_equiv A B))
147
symmetry proved by (proj2 (proj2 (relations_eq_equiv A B)))
148
transitivity proved by (proj1 (proj2 (relations_eq_equiv A B)))
151
Add Parametric Morphism (A : Type) : (@well_founded A) with signature (@relations_eq A A) ==> iff as well_founded_wd.
153
unfold relations_eq, well_founded; intros R1 R2 H;
154
split; intros H1 a; induction (H1 a) as [x H2 H3]; constructor;
155
intros y H4; apply H3; [now apply <- H | now apply -> H].
158
(* solve_predicate_wd solves the goal [predicate_wd P] for P consisting of
159
morhisms and quatifiers *)
161
Ltac solve_predicate_wd :=
163
let x := fresh "x" in
164
let y := fresh "y" in
165
let H := fresh "H" in
166
intros x y H; setoid_rewrite H; reflexivity.
168
(* solve_relation_wd solves the goal [relation_wd R] for R consisting of
169
morhisms and quatifiers *)
171
Ltac solve_relation_wd :=
172
unfold relation_wd, fun2_wd;
173
let x1 := fresh "x" in
174
let y1 := fresh "y" in
175
let H1 := fresh "H" in
176
let x2 := fresh "x" in
177
let y2 := fresh "y" in
178
let H2 := fresh "H" in
179
intros x1 y1 H1 x2 y2 H2;
180
rewrite H1; setoid_rewrite H2; reflexivity.
182
(* The following tactic uses solve_predicate_wd to solve the goals
183
relating to well-defidedness that are produced by applying induction.
184
We declare it to take the tactic that applies the induction theorem
185
and not the induction theorem itself because the tactic may, for
186
example, supply additional arguments, as does NZinduct_center in
189
Ltac induction_maker n t :=
191
pattern n; t; clear n;
192
[solve_predicate_wd | ..].
194
(** Relations on cartesian product. Used in MiscFunct for defining
195
functions whose domain is a product of sets by primitive recursion *)
197
Section RelationOnProduct.
200
Variable Aeq : relation A.
201
Variable Beq : relation B.
203
Hypothesis EA_equiv : equiv A Aeq.
204
Hypothesis EB_equiv : equiv B Beq.
206
Definition prod_rel : relation (A * B) :=
207
fun p1 p2 => Aeq (fst p1) (fst p2) /\ Beq (snd p1) (snd p2).
209
Lemma prod_rel_refl : reflexive (A * B) prod_rel.
211
unfold reflexive, prod_rel.
212
destruct x; split; [apply (proj1 EA_equiv) | apply (proj1 EB_equiv)]; simpl.
215
Lemma prod_rel_sym : symmetric (A * B) prod_rel.
217
unfold symmetric, prod_rel.
218
destruct x; destruct y;
219
split; [apply (proj2 (proj2 EA_equiv)) | apply (proj2 (proj2 EB_equiv))]; simpl in *; tauto.
222
Lemma prod_rel_trans : transitive (A * B) prod_rel.
224
unfold transitive, prod_rel.
225
destruct x; destruct y; destruct z; simpl.
226
intros; split; [apply (proj1 (proj2 EA_equiv)) with (y := a0) |
227
apply (proj1 (proj2 EB_equiv)) with (y := b0)]; tauto.
230
Theorem prod_rel_equiv : equiv (A * B) prod_rel.
232
unfold equiv; split; [exact prod_rel_refl | split; [exact prod_rel_trans | exact prod_rel_sym]].
235
End RelationOnProduct.
237
Implicit Arguments prod_rel [A B].
238
Implicit Arguments prod_rel_equiv [A B].
242
(*Definition comp_bool (x y : comparison) : bool :=
250
Theorem comp_bool_correct : forall x y : comparison,
251
comp_bool x y <-> x = y.
253
destruct x; destruct y; simpl; split; now intro.
256
Lemma eq_equiv : forall A : Set, equiv A (@eq A).
258
intro A; unfold equiv, reflexive, symmetric, transitive.
259
repeat split; [exact (@trans_eq A) | exact (@sym_eq A)].
260
(* It is interesting how the tactic split proves reflexivity *)
263
(*Add Relation (fun A : Set => A) LE_Set
264
reflexivity proved by (fun A : Set => (proj1 (eq_equiv A)))
265
symmetry proved by (fun A : Set => (proj2 (proj2 (eq_equiv A))))
266
transitivity proved by (fun A : Set => (proj1 (proj2 (eq_equiv A))))
added
removed
theories/Numbers/NumPrelude.v
