port Wellfounded and Sorting to RelationClasses

andres-erbsen · andres-erbsen · commit a8316834a534 · 2025-06-03T01:30:25.000-04:00
diff --git a/theories/Relations/Operators_Properties.v b/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 *)
diff --git a/theories/Sorting/Heap.v b/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]. *)
 
diff --git a/theories/Sorting/PermutEq.v b/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.
 
diff --git a/theories/Sorting/PermutSetoid.v b/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.
 
diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v
@@ -11,12 +11,13 @@
 (** Author: Bruno Barras *)
 
 From Stdlib Require Import Relation_Definitions.
+From Stdlib Require Import RelationClasses.
 
 Section WfInclusion.
   Variable A : Type.
   Variables R1 R2 : A -> A -> Prop.
 
-  Lemma Acc_incl : inclusion A R1 R2 -> forall z:A, Acc R2 z -> Acc R1 z.
+  Lemma Acc_incl : subrelation R1 R2 -> forall z:A, Acc R2 z -> Acc R1 z.
   Proof.
     induction 2.
     apply Acc_intro; auto with sets.
@@ -25,7 +26,7 @@ Section WfInclusion.
   #[local]
   Hint Resolve Acc_incl : core.
 
-  Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1.
+  Theorem wf_incl : subrelation R1 R2 -> well_founded R2 -> well_founded R1.
   Proof.
     unfold well_founded; auto with sets.
   Qed.
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -94,7 +94,7 @@ Section Wf_Lexicographic_Exponentiation.
       apply Forall_app. split; [easy|].
       constructor; [|easy].
       eapply rt_trans.
-      + apply clos_r_clos_rt. eassumption.
+      + apply subrelation_clos_r_clos_rt. eassumption.
       + apply Forall_app in IH as [_ IH].
         destruct l as [|? l].
         * now apply rt_refl.
@@ -204,7 +204,7 @@ Section Wf_Lexicographic_Exponentiation.
           intros. eapply clos_rt_t; [|apply t_step]; eassumption. }
         rewrite <-(app_nil_r (a :: l1)).
         apply (clos_trans_list_ext_app_l _ _ _ _ [b]); [assumption|].
-        destruct l2; [apply rt_refl|apply clos_t_clos_rt].
+        destruct l2; [apply rt_refl|apply subrelation_clos_t_clos_rt].
         now apply clos_trans_list_ext_nil_l.
       + apply (dist_Desc_concat [a]) in Hl1 as [_ ?].
         apply (dist_Desc_concat [a]) in Hl2 as [_ ?].
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v
@@ -19,7 +19,7 @@ Section Wf_Transitive_Closure.
 
   Notation trans_clos := (clos_trans A R).
 
-  Lemma incl_clos_trans : inclusion A R trans_clos.
+  Lemma incl_clos_trans : subrelation R trans_clos.
     red; auto with sets.
   Qed.
 
diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v
@@ -20,13 +20,16 @@ Section WfUnion.
 
   Notation Union := (union A R1 R2).
 
+  Local Definition commut (R1 R2:relation A) : Prop :=
+    forall x y:A, R1 y x -> forall z:A, R2 z y ->  exists2 y' : A, R2 y' x & R1 z y'.
+  Context (H : commut R1 R2).
+
   Remark strip_commut :
-    commut A R1 R2 ->
     forall x y:A,
       clos_trans A R1 y x ->
       forall z:A, R2 z y ->  exists2 y' : A, R2 y' x & clos_trans A R1 z y'.
   Proof.
-    induction 2 as [x y| x y z H0 IH1 H1 IH2]; intros.
+    induction 1 as [x y| x y z H0 IH1 H1 IH2]; intros.
     - elim H with y x z; auto with sets; intros x0 H2 H3.
       exists x0; auto with sets.
 
@@ -38,10 +41,9 @@ Section WfUnion.
 
 
   Lemma Acc_union :
-    commut A R1 R2 ->
     (forall x:A, Acc R2 x -> Acc R1 x) -> forall a:A, Acc R2 a -> Acc Union a.
   Proof.
-    induction 3 as [x H1 H2].
+    induction 2 as [x H1 H2].
     apply Acc_intro; intros.
     elim H3; intros; auto with sets.
     cut (clos_trans A R1 y x); auto with sets.
@@ -65,7 +67,7 @@ Section WfUnion.
 
 
   Theorem wf_union :
-    commut A R1 R2 -> well_founded R1 -> well_founded R2 -> well_founded Union.
+    well_founded R1 -> well_founded R2 -> well_founded Union.
   Proof.
     unfold well_founded.
     intros.
