1 files changed, 12 insertions, 140 deletions

diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index 95d8b366..468b0613 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -8,9 +8,9 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-(*i $Id: NumPrelude.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
+(*i $Id$ i*)
 
-Require Export Setoid.
+Require Export Setoid Morphisms.
 
 Set Implicit Arguments.
 (*
@@ -91,85 +91,31 @@ end.
 
 Tactic Notation "stepr" constr(t2') "in" hyp(H) "by" tactic(r) := stepr t2' in H; [| r].
 
-(** Extentional properties of predicates, relations and functions *)
+(** Predicates, relations, functions *)
 
 Definition predicate (A : Type) := A -> Prop.
 
-Section ExtensionalProperties.
-
-Variables A B C : Type.
-Variable Aeq : relation A.
-Variable Beq : relation B.
-Variable Ceq : relation C.
-
-(* "wd" stands for "well-defined" *)
-
-Definition fun_wd (f : A -> B) := forall x y : A, Aeq x y -> Beq (f x) (f y).
-
-Definition fun2_wd (f : A -> B -> C) :=
-  forall x x' : A, Aeq x x' -> forall y y' : B, Beq y y' -> Ceq (f x y) (f x' y').
-
-Definition fun_eq : relation (A -> B) :=
-  fun f f' => forall x x' : A, Aeq x x' -> Beq (f x) (f' x').
-
-(* Note that reflexivity of fun_eq means that every function
-is well-defined w.r.t. Aeq and Beq, i.e.,
-forall x x' : A, Aeq x x' -> Beq (f x) (f x') *)
-
-Definition fun2_eq (f f' : A -> B -> C) :=
-  forall x x' : A, Aeq x x' -> forall y y' : B, Beq y y' -> Ceq (f x y) (f' x' y').
-
-End ExtensionalProperties.
-
-(* The following definitions instantiate Beq or Ceq to iff; therefore, they
-have to be outside the ExtensionalProperties section *)
-
-Definition predicate_wd (A : Type) (Aeq : relation A) := fun_wd Aeq iff.
-
-Definition relation_wd (A B : Type) (Aeq : relation A) (Beq : relation B) :=
-  fun2_wd Aeq Beq iff.
-
-Definition relations_eq (A B : Type) (R1 R2 : A -> B -> Prop) :=
-  forall (x : A) (y : B), R1 x y <-> R2 x y.
-
-Theorem relations_eq_equiv :
-  forall (A B : Type), equiv (A -> B -> Prop) (@relations_eq A B).
-Proof.
-intros A B; unfold equiv. split; [| split];
-unfold reflexive, symmetric, transitive, relations_eq.
-reflexivity.
-intros R1 R2 R3 H1 H2 x y; rewrite H1; apply H2.
-now symmetry.
-Qed.
-
-Add Parametric Relation (A B : Type) : (A -> B -> Prop) (@relations_eq A B)
-  reflexivity proved by (proj1 (relations_eq_equiv A B))
-  symmetry proved by (proj2 (proj2 (relations_eq_equiv A B)))
-  transitivity proved by (proj1 (proj2 (relations_eq_equiv A B)))
-as relations_eq_rel.
-
-Add Parametric Morphism (A : Type) : (@well_founded A) with signature (@relations_eq A A) ==> iff as well_founded_wd.
+Instance well_founded_wd A :
+ Proper (@relation_equivalence A ==> iff) (@well_founded A).
 Proof.
-unfold relations_eq, well_founded; intros R1 R2 H;
-split; intros H1 a; induction (H1 a) as [x H2 H3]; constructor;
-intros y H4; apply H3; [now apply <- H | now apply -> H].
+intros R1 R2 H.
+split; intros WF a; induction (WF a) as [x _ WF']; constructor;
+intros y Ryx; apply WF'; destruct (H y x); auto.
 Qed.
 
-(* solve_predicate_wd solves the goal [predicate_wd P] for P consisting of
-morhisms and quatifiers *)
+(** [solve_predicate_wd] solves the goal [Proper (?==>iff) P]
+    for P consisting of morphisms and quantifiers *)
 
 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; setoid_rewrite H; reflexivity.
 
-(* solve_relation_wd solves the goal [relation_wd R] for R consisting of
-morhisms and quatifiers *)
+(** [solve_relation_wd] solves the goal [Proper (?==>?==>iff) R]
+    for R consisting of morphisms and quantifiers *)
 
 Ltac solve_relation_wd :=
-unfold relation_wd, fun2_wd;
 let x1 := fresh "x" in
 let y1 := fresh "y" in
 let H1 := fresh "H" in
@@ -191,77 +137,3 @@ Ltac induction_maker n t :=
   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 Aeq : relation A.
-Variable Beq : relation B.
-
-Hypothesis EA_equiv : equiv A Aeq.
-Hypothesis EB_equiv : equiv B Beq.
-
-Definition prod_rel : relation (A * B) :=
-  fun p1 p2 => Aeq (fst p1) (fst p2) /\ Beq (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_sym : 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_sym]].
-Qed.
-
-End RelationOnProduct.
-
-Implicit Arguments prod_rel [A B].
-Implicit Arguments prod_rel_equiv [A B].
-
-(** Miscellaneous *)
-
-(*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.*)
-
-Lemma eq_equiv : forall A : Set, equiv A (@eq A).
-Proof.
-intro A; unfold equiv, 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.*)