Deprecate Relation_definitions, remove from supported files

.nix/rocq-overlays/stdlib-subcomponents/default.nix

@@ -11,7 +11,7 @@ let
     "logic" = [ ];
     "relations" = [ "corelib-wrapper" ];
     "program" = [ "corelib-wrapper" "logic" ];
-    "classes" = [ "program" "relations" ];
+    "classes" = [ "program" ];
     "bool" = [ "classes" ];
     "structures" = [ "bool" ];
     "arith-base" = [ "structures" ];
@@ -34,7 +34,7 @@ let
     "classical-logic" = [ "arith" ];
     "sets" = [ "classical-logic" ];
     "vectors" = [ "lists" ];
-    "sorting" = [ "lia" "sets" "vectors" ];
+    "sorting" = [ "lia" "sets" "vectors" "relations" ];
     "orders-ex" = [ "strings" "sorting" ];
     "unicode" = [ ];
     "primitive-int" = [ "unicode" "zarith" ];
@@ -45,7 +45,7 @@ let
     "fmaps-fsets-msets" = [ "orders-ex" "zarith" ];
     "extraction" = [ "primitive-string" "primitive-array" "primitive-floats" ];
     "funind" = [ "arith-base" ];
-    "wellfounded" = [ "lists" ];
+    "wellfounded" = [ "relations" "lists" ];
     "streams" = [ "logic" ];
     "rtauto" = [ "positive" "lists" ];
     "compat" = [ "rtauto" "fmaps-fsets-msets" "funind" "extraction" "reals" "zmod" "wellfounded" "streams" ];

doc/changelog/01-changed/162-deprecate-relations.rst

@@ -0,0 +1,6 @@
+- in `Wellfounded`
+
+  + Changed definitions to use `RelationClasses` instead of `Relations`
+    (`#162 <https://github.com/coq/stdlib/pull/162>`_,
+    by Andres Erbsen).
+

doc/changelog/05-deprecated/162-deprecate-relations.rst

@@ -0,0 +1,18 @@
+- in `Relation_Definitions`
+
+  + Everything except `relation`, in favor of `RelationClasses`
+    (`#162 <https://github.com/coq/stdlib/pull/162>`_,
+    by Andres Erbsen).
+
+- in `Relations`
+
+  + All uses of `Relations`, adding `RelationClasses` versions
+    (`#162 <https://github.com/coq/stdlib/pull/162>`_,
+    by Andres Erbsen).
+
+- in `Operators_Properties`
+
+  + All uses of `Relation_Definitions`, adding `RelationClasses` versions
+    (`#162 <https://github.com/coq/stdlib/pull/162>`_,
+    by Andres Erbsen).
+

doc/stdlib/depends.dot

@@ -9,7 +9,8 @@ digraph stdlib_deps {
 	];
 	bool -> classes;
 	classes -> program;
-	classes -> relations;
+	wellfounded -> relations;
+	sorting -> relations;
 	program -> "corelib-wrapper";
 	program -> logic;
 	strings -> arith;

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/Operators_Properties.v

@@ -29,8 +29,6 @@ Section Properties.
   Arguments clos_trans [A] R x _.
   Arguments clos_trans_1n [A] R x _.
   Arguments clos_trans_n1 [A] R x _.
-  Arguments inclusion [A] R1 R2.
-  Arguments preorder [A] R.
 
   Variable A : Type.
   Variable R : relation A.
@@ -43,56 +41,88 @@ Section Properties.
 
     (** Correctness of the reflexive-transitive closure operator *)
 
-    Lemma clos_rt_is_preorder : preorder R*.
+    #[export] Instance PreOrder_clos_rt : PreOrder R*.
     Proof.
+      split.
+      - exact (rt_refl A R).
+      - exact (rt_trans A R).
+    Qed.
+
+    #[deprecated(since="9.1", use=PreOrder_clos_rt)]
+    #[warning="-deprecated"]
+    Lemma clos_rt_is_preorder : preorder _ R*.
+    Proof.
+      #[warning="-deprecated"]
       apply Build_preorder.
       - exact (rt_refl A R).
       - exact (rt_trans A R).
     Qed.
 
     (** Idempotency of the reflexive-transitive closure operator *)
 
-    Lemma clos_rt_idempotent : inclusion (R*)* R*.
+    #[export] Instance subrelation_clos_rt_idemp : subrelation (R*)* R*.
     Proof.
-      red.
       induction 1 as [x y H|x|x y z H IH H0 IH0]; auto with sets.
       apply rt_trans with y; auto with sets.
     Qed.
 
+    #[deprecated(since="9.1", use=subrelation_clos_rt_idemp)]
+    #[warning="-deprecated"]
+    Lemma clos_rt_idempotent : inclusion _ (R*)* R*.
+    Proof. apply subrelation_clos_rt_idemp. Qed.
+
   End Clos_Refl_Trans.
 
   Section Clos_Refl_Sym_Trans.
 
     (** Reflexive-transitive closure is included in the
         reflexive-symmetric-transitive closure *)
 
-    Lemma clos_rt_clos_rst :
-      inclusion (clos_refl_trans R) (clos_refl_sym_trans R).
+    #[export] Instance subrelation_clos_rt_clos_rst :
+      subrelation (clos_refl_trans R) (clos_refl_sym_trans R).
     Proof.
       red.
       induction 1 as [x y H|x|x y z H IH H0 IH0]; auto with sets.
       apply rst_trans with y; auto with sets.
     Qed.
 
+    #[deprecated(since="9.1", use=subrelation_clos_rt_clos_rst)]
+    #[warning="-deprecated"]
+    Lemma clos_rt_clos_rst :
+      inclusion _ (clos_refl_trans R) (clos_refl_sym_trans R).
+    Proof. apply subrelation_clos_rt_clos_rst. Qed.
+
     (** Reflexive closure is included in the
         reflexive-transitive closure *)
 
-    Lemma clos_r_clos_rt :
-      inclusion (clos_refl R) (clos_refl_trans R).
+    #[export] Instance subrelation_clos_r_clos_rt :
+      subrelation (clos_refl R) (clos_refl_trans R).
     Proof.
       induction 1 as [? ?| ].
       - constructor; auto.
       - constructor 2.
     Qed.
 
-    Lemma clos_t_clos_rt :
-      inclusion (clos_trans R) (clos_refl_trans R).
+    #[deprecated(since="9.1", use=subrelation_clos_r_clos_rt)]
+    #[warning="-deprecated"]
+    Lemma clos_r_clos_rt :
+      inclusion _ (clos_refl R) (clos_refl_trans R).
+    Proof. apply subrelation_clos_r_clos_rt. Qed.
+
+    #[export] Instance subrelation_clos_t_clos_rt :
+      subrelation (clos_trans R) (clos_refl_trans R).
     Proof.
       induction 1 as [? ?| ].
       - constructor. auto.
       - econstructor 3; eassumption.
     Qed.
 
+    #[deprecated(since="9.1", use=subrelation_clos_t_clos_rt)]
+    #[warning="-deprecated"]
+    Lemma clos_t_clos_rt :
+      inclusion _ (clos_trans R) (clos_refl_trans R).
+    Proof. apply subrelation_clos_t_clos_rt. Qed.
+
     Lemma clos_rt_t : forall x y z,
       clos_refl_trans R x y -> clos_trans R y z ->
       clos_trans R x z.
@@ -104,25 +134,42 @@ Section Properties.
 
     (** Correctness of the reflexive-symmetric-transitive closure *)
 
+    #[export] Instance Equivalence_clos_rst_is : Equivalence (clos_refl_sym_trans R).
+    Proof.
+      split.
+      - exact (rst_refl A R).
+      - exact (rst_sym A R).
+      - exact (rst_trans A R).
+    Qed.
+
+    #[deprecated(since="9.1", use=Equivalence_clos_rst_is)]
+    #[warning="-deprecated"]
     Lemma clos_rst_is_equiv : equivalence A (clos_refl_sym_trans R).
     Proof.
-      apply Build_equivalence.
+      split.
       - exact (rst_refl A R).
       - exact (rst_trans A R).
       - exact (rst_sym A R).
     Qed.
 
     (** Idempotency of the reflexive-symmetric-transitive closure operator *)
 
-    Lemma clos_rst_idempotent :
-      inclusion (clos_refl_sym_trans (clos_refl_sym_trans R))
+    #[export] Instance subrelation_clos_rst_idemp :
+      subrelation (clos_refl_sym_trans (clos_refl_sym_trans R))
       (clos_refl_sym_trans R).
     Proof.
       red.
       induction 1 as [x y H|x|x y H IH|x y z H IH H0 IH0]; auto with sets.
       apply rst_trans with y; auto with sets.
     Qed.
 
+    #[deprecated(since="9.1", use=subrelation_clos_rst_idemp)]
+    #[warning="-deprecated"]
+    Lemma clos_rst_idempotent :
+      inclusion _ (clos_refl_sym_trans (clos_refl_sym_trans R))
+      (clos_refl_sym_trans R).
+    Proof. apply subrelation_clos_rst_idemp. Qed.
+
   End Clos_Refl_Sym_Trans.
 
   Section Equivalences.
@@ -424,33 +471,57 @@ End Properties.
 
 (* begin hide *)
 (* Compatibility *)
+#[deprecated(since="2009", use=clos_trans_tn1)]
 Notation trans_tn1 := clos_trans_tn1 (only parsing).
+#[deprecated(since="2009", use=clos_tn1_trans)]
 Notation tn1_trans := clos_tn1_trans (only parsing).
+#[deprecated(since="2009", use=clos_trans_tn1_iff)]
 Notation tn1_trans_equiv := clos_trans_tn1_iff (only parsing).
 
+#[deprecated(since="2009", use=clos_trans_t1n)]
 Notation trans_t1n := clos_trans_t1n (only parsing).
+#[deprecated(since="2009", use=clos_t1n_trans)]
 Notation t1n_trans := clos_t1n_trans (only parsing).
+#[deprecated(since="2009", use=clos_trans_t1n_iff)]
 Notation t1n_trans_equiv := clos_trans_t1n_iff (only parsing).
 
+#[deprecated(since="2009", use=clos_rtn1_step)]
 Notation R_rtn1 := clos_rtn1_step (only parsing).
+#[deprecated(since="2009", use=clos_rt_rt1n)]
 Notation trans_rt1n := clos_rt_rt1n (only parsing).
+#[deprecated(since="2009", use=clos_rt1n_rt)]
 Notation rt1n_trans := clos_rt1n_rt (only parsing).
+#[deprecated(since="2009", use=clos_rt_rt1n_iff)]
 Notation rt1n_trans_equiv := clos_rt_rt1n_iff (only parsing).
 
+#[deprecated(since="2009", use=clos_rt1n_step)]
 Notation R_rt1n := clos_rt1n_step (only parsing).
+#[deprecated(since="2009", use=clos_rt_rtn1)]
 Notation trans_rtn1 := clos_rt_rtn1 (only parsing).
+#[deprecated(since="2009", use=clos_rtn1_rt)]
 Notation rtn1_trans := clos_rtn1_rt (only parsing).
+#[deprecated(since="2009", use=clos_rt_rtn1_iff)]
 Notation rtn1_trans_equiv := clos_rt_rtn1_iff (only parsing).
 
+#[deprecated(since="2009", use=clos_rst1n_rst)]
 Notation rts1n_rts := clos_rst1n_rst (only parsing).
+#[deprecated(since="2009", use=clos_rst1n_trans)]
 Notation rts_1n_trans := clos_rst1n_trans (only parsing).
+#[deprecated(since="2009", use=clos_rst1n_sym)]
 Notation rts1n_sym := clos_rst1n_sym (only parsing).
+#[deprecated(since="2009", use=clos_rst_rst1n)]
 Notation rts_rts1n := clos_rst_rst1n (only parsing).
+#[deprecated(since="2009", use=clos_rst_rst1n_iff)]
 Notation rts_rts1n_equiv := clos_rst_rst1n_iff (only parsing).
 
+#[deprecated(since="2009", use=clos_rstn1_rst)]
 Notation rtsn1_rts := clos_rstn1_rst (only parsing).
+#[deprecated(since="2009", use=clos_rstn1_trans)]
 Notation rtsn1_trans := clos_rstn1_trans (only parsing).
+#[deprecated(since="2009", use=clos_rstn1_sym)]
 Notation rtsn1_sym := clos_rstn1_sym (only parsing).
+#[deprecated(since="2009", use=clos_rst_rstn1)]
 Notation rts_rtsn1 := clos_rst_rstn1 (only parsing).
+#[deprecated(since="2009", use=clos_rst_rstn1_iff)]
 Notation rts_rtsn1_equiv := clos_rst_rstn1_iff (only parsing).
 (* end hide *)

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/Heap.v

@@ -7,6 +7,7 @@
 (*         *     GNU Lesser General Public License Version 2.1          *)
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
+Local Set Warnings "-deprecated".
 
 (** This file is deprecated, for a tree on list, use [Mergesort.v]. *)
 

theories/Sorting/PermutEq.v

@@ -7,6 +7,7 @@
 (*         *     GNU Lesser General Public License Version 2.1          *)
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
+Local Set Warnings "-deprecated".
 
 From Stdlib Require Import Relations Setoid SetoidList List Multiset PermutSetoid Permutation.
 

theories/Sorting/PermutSetoid.v

@@ -7,6 +7,7 @@
 (*         *     GNU Lesser General Public License Version 2.1          *)
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
+Local Set Warnings "-deprecated".
 
 From Stdlib Require Import Lia Relations Multiset SetoidList.