1 files changed, 10 insertions, 90 deletions

diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v
index ddd1c50c3..290c9b1c2 100644
--- a/theories/Numbers/NumPrelude.v
+++ b/theories/Numbers/NumPrelude.v
@@ -91,75 +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) := Proper (Aeq==>Beq) f.
-
-Definition fun2_wd (f : A -> B -> C) := Proper (Aeq==>Beq==>Ceq) f.
-
-Definition fun_eq : relation (A -> B) := (Aeq==>Beq)%signature.
-
-(* 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) := (Aeq==>Beq==>Ceq)%signature f f'.
-
-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) := Proper (Aeq==>iff).
-
-Definition relation_wd (A B : Type) (Aeq : relation A) (Beq : relation B) :=
-  Proper (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.
-
-Instance relation_eq_equiv A B : Equivalence (@relations_eq A B).
-Proof.
-intros A B; split;
-unfold Reflexive, Symmetric, Transitive, relations_eq.
-reflexivity.
-now symmetry.
-intros R1 R2 R3 H1 H2 x y; rewrite H1; apply H2.
-Qed.
-
-Instance well_founded_wd A : Proper (@relations_eq A A ==> iff) (@well_founded A).
+Instance well_founded_wd A :
+ Proper (@relation_equivalence A ==> iff) (@well_founded A).
 Proof.
-unfold relations_eq, well_founded; intros A 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 A 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
@@ -181,39 +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.
-
-Definition prod_rel : relation (A * B) := (Aeq * Beq)%signature.
-
-Instance prod_rel_equiv `(Equivalence _ Aeq, Equivalence _ Beq) :
- Equivalence prod_rel.
-
-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.*)
-
-