deprecate relations; remove usages outside wellfounded, deprecated sorting

Author: andres-erbsen

theories/Classes/RelationPairs.v

@@ -11,7 +11,8 @@
 (** * Relations over pairs *)
 
 
-From Stdlib Require Import Relations Morphisms.
+From Stdlib Require Import Relation_Definitions (relation).
+From Stdlib Require Import Morphisms.
 (* NB: This should be system-wide someday, but for that we need to
     fix the simpl tactic, since "simpl fst" would be refused for
     the moment.

theories/Relations/Relation_Definitions.v

@@ -1 +1,57 @@
-From Corelib Require Export Relation_Definitions.
+From Corelib Require Export RelationClasses.
+From Corelib Require Import Relation_Definitions.
+
+Notation relation := relation (only parsing).
+
+#[deprecated(since="9.1", use=Reflexive)]
+Notation reflexive := reflexive (only parsing).
+#[deprecated(since="9.1", use=Transitive)]
+Notation transitive := transitive (only parsing).
+#[deprecated(since="9.1", use=Symmetric)]
+Notation symmetric := symmetric (only parsing).
+#[deprecated(since="9.1", use=Antisymmetric)]
+Notation antisymmetric := antisymmetric (only parsing).
+#[deprecated(since="9.1", use=Equivalence)]
+Notation equiv := equiv (only parsing).
+#[deprecated(since="9.1", use=PreOrder)]
+Notation preorder := preorder (only parsing).
+#[deprecated(since="9.1", use=Build_PreOrder)]
+Notation Build_preorder := Build_preorder (only parsing).
+#[deprecated(since="9.1", use=PreOrder_Reflexive)]
+Notation preord_refl := preord_refl (only parsing).
+#[deprecated(since="9.1", use=PreOrder_Transitive)]
+Notation preord_trans := preord_trans (only parsing).
+#[deprecated(since="9.1", use=PartialOrder)]
+Notation order := order (only parsing).
+#[deprecated(since="9.1", note="Use RelationClasses.PartialOrder")]
+Notation Build_order := Build_order (only parsing).
+#[deprecated(since="9.1", use=partial_order_antisym)]
+Notation ord_antisym := ord_antisym (only parsing).
+#[deprecated(since="9.1", note="Use RelationClasses.PartialOrder")]
+Notation ord_refl := ord_refl (only parsing).
+#[deprecated(since="9.1", note="Use RelationClasses.PartialOrder")]
+Notation ord_trans := ord_trans (only parsing).
+#[deprecated(since="9.1", use=Equivalence)]
+Notation equivalence := equivalence (only parsing).
+#[deprecated(since="9.1", use=Build_Equivalence)]
+Notation Build_equivalence := Build_equivalence (only parsing).
+#[deprecated(since="9.1", use=Equivalence_Reflexive)]
+Notation equiv_refl := equiv_refl (only parsing).
+#[deprecated(since="9.1", use=Equivalence_Transitive)]
+Notation equiv_trans := equiv_trans (only parsing).
+#[deprecated(since="9.1", use=Equivalence_Symmetric)]
+Notation equiv_sym := equiv_sym (only parsing).
+#[deprecated(since="9.1", use=RelationClasses.PER)]
+Notation PER := PER (only parsing).
+#[deprecated(since="9.1", use=RelationClasses.Build_PER)]
+Notation Build_PER := Build_PER (only parsing).
+#[deprecated(since="9.1", use=RelationClasses.PER_Symmetric)]
+Notation per_sym := per_sym (only parsing).
+#[deprecated(since="9.1", use=RelationClasses.PER_Transitive)]
+Notation per_trans := per_trans (only parsing).
+#[deprecated(since="9.1", use=subrelation)]
+Notation inclusion := inclusion (only parsing).
+#[deprecated(since="9.1", use=relation_equivalence)]
+Notation same_relation := same_relation (only parsing).
+#[deprecated(since="9.1", note="If you would like the standard library to keep this definition, please open an issue")]
+Notation commut := commut (only parsing).

theories/Relations/Relations.v

@@ -7,11 +7,20 @@
 (*         *     GNU Lesser General Public License Version 2.1          *)
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
-
 From Stdlib Require Export Relation_Definitions.
 From Stdlib Require Export Relation_Operators.
 From Stdlib Require Export Operators_Properties.
+From Stdlib Require Export RelationClasses.
+
+Lemma Equivalence_on [A B] (f:A -> B) (r:relation B) :
+    Equivalence r -> Equivalence (fun x y => r (f x) (f y)).
+Proof. intros []; split; red; eauto. Qed.
+
+Lemma Equivalence_eq_on [A B] (f:A -> B) : Equivalence (fun x y => f x = f y).
+Proof. apply Equivalence_on; exact _. Qed.
 
+#[deprecated(since="9.1", use=Equivalence_on)]
+#[warning="-deprecated"]
 Lemma inverse_image_of_equivalence :
   forall (A B:Type) (f:A -> B) (r:relation B),
     equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)).
@@ -20,6 +29,8 @@ Proof.
   intros _ equiv_trans _ x y z H0 H1; apply equiv_trans with (f y); assumption.
 Qed.
 
+#[deprecated(since="9.1", use=Equivalence_eq_on)]
+#[warning="-deprecated"]
 Lemma inverse_image_of_eq :
   forall (A B:Type) (f:A -> B), equivalence A (fun x y:A => f x = f y).
 Proof.

theories/Sorting/Sorted.v

@@ -20,7 +20,7 @@
   The two notions are equivalent if the order is transitive.
 *)
 
-From Stdlib Require Import List Relations Relations_1.
+From Stdlib Require Import List Relation_Definitions Relations_1.
 
 (* Set Universe Polymorphism. *)
 

theories/Structures/Orders.v

@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-From Stdlib Require Export Relations Morphisms Setoid Equalities.
+From Stdlib Require Export Morphisms Setoid Equalities.
 Set Implicit Arguments.
 Unset Strict Implicit.