[ssr] Refactor/Extend of under to support more relations

(namely, [RewriteRelation]s beyond Equivalence ones)

Thanks to @CohenCyril for suggesting this enhancement

7 files changed, 275 insertions, 81 deletions

diff --git a/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst b/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst
index e9eab0924c..5e005742fd 100644
--- a/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst
+++ b/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst
@@ -1,21 +1,28 @@
 - Generalize tactics :tacn:`under` and :tacn:`over` for any registered
-  setoid equality. More precisely, assume the given context lemma has
-  type `forall f1 f2, .. -> (forall i, R1 (f1 i) (f2 i)) -> R2 f1 f2`.
-  The first step performed by :tacn:`under` (since Coq 8.10) amounts
-  to calling the tactic :tacn:`rewrite <rewrite (ssreflect)>`, which
+  relation. More precisely, assume the given context lemma has type
+  `forall f1 f2, .. -> (forall i, R1 (f1 i) (f2 i)) -> R2 f1 f2`.  The
+  first step performed by :tacn:`under` (since Coq 8.10) amounts to
+  calling the tactic :tacn:`rewrite <rewrite (ssreflect)>`, which
   itself relies on :tacn:`setoid_rewrite` if need be. So this step was
   already compatible with a double implication or setoid equality for
   the conclusion head symbol `R2`. But a further step consists in
   tagging the generated subgoal `R1 (f1 i) (?f2 i)` to protect it from
-  unwanted evar instantiation, and obtain a subgoal displayed as
-  ``'Under[ f1 i ]``. In Coq 8.10, this second (convenience) step was
-  only performed when `R1` was Leibniz' `eq` or `iff`. Now, it is also
-  performed for any relation `R1` which has a ``RewriteRelation``
-  instance as well as a ``RelationClasses.Reflexive`` instance. This
-  generalized support for setoid relations is enabled as soon as we do
-  both ``Require Import ssreflect.`` and ``Require Setoid.`` Finally,
-  a rewrite rule ``UnderE`` has been added if one wants to "unprotect"
-  the evar, and instantiate it manually with another rule than
-  reflexivity (i.e., without using :tacn:`over`). See also Section
+  unwanted evar instantiation, and get `Under_rel _ R1 (f1 i) (?f2 i)`
+  that is displayed as ``'Under[ f1 i ]``. In Coq 8.10, this second
+  (convenience) step was only performed when `R1` was Leibniz' `eq` or
+  `iff`. Now, it is also performed for any relation `R1` which has a
+  ``RewriteRelation`` instance (a `RelationClasses.Reflexive` instance
+  being also needed so :tacn:`over` can discharge the ``'Under[ _ ]``
+  goal by instantiating the hidden evar.) Also, it is now possible to
+  manipulate `Under_rel _ R1 (f1 i) (?f2 i)` subgoals directly if `R1`
+  is a `PreOrder` relation or so, thanks to extra instances proving
+  that `Under_rel` preserves the properties of the `R1` relation.
+  These two features generalizing support for setoid-like relations is
+  enabled as soon as we do both ``Require Import ssreflect.`` and
+  ``Require Setoid.`` Finally, a rewrite rule ``UnderE`` has been
+  added if one wants to "unprotect" the evar, and instantiate it
+  manually with another rule than reflexivity (i.e., without using the
+  :tacn:`over` tactic nor the ``over`` rewrite rule). See also Section
   :ref:`under_ssr` (`#10022 <https://github.com/coq/coq/pull/10022>`_,
-  by Erik Martin-Dorel, with suggestions and review by Enrico Tassi).
+  by Erik Martin-Dorel, with suggestions and review by Enrico Tassi
+  and Cyril Cohen).
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index 4f8986984f..6699252cee 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -77,4 +77,5 @@ plugins/setoid_ring/Rings_Q.v
 plugins/setoid_ring/Rings_R.v
 plugins/setoid_ring/Rings_Z.v
 plugins/setoid_ring/ZArithRing.v
+plugins/ssr/ssrunder.v
 plugins/ssr/ssrsetoid.v
diff --git a/plugins/ssr/ssrclasses.v b/plugins/ssr/ssrclasses.v
index 29486ff4cf..0ae3f8c6a5 100644
--- a/plugins/ssr/ssrclasses.v
+++ b/plugins/ssr/ssrclasses.v
@@ -12,6 +12,9 @@
 
 (** Compatibility layer for [under] and [setoid_rewrite].
 
+ Note: this file does not require [ssreflect]; it is both required by
+ [ssrsetoid] and required by [ssrunder].
+
  Redefine [Coq.Classes.RelationClasses.Reflexive] here, so that doing
  [Require Import ssreflect] does not [Require Import RelationClasses],
  and conversely. **)
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index a19aade6e9..43c091123e 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -531,65 +531,13 @@ Lemma abstract_context T (P : T -> Type) x :
 Proof. by move=> /(_ P); apply. Qed.
 
 (*****************************************************************************)
-(* Constants for under/over, to rewrite under binders using "context lemmas" *)
-
-Require Import ssrclasses.
-
-Module Type UNDER_REL.
-Parameter Under_rel :
-  forall (A : Type) (eqA : A -> A -> Prop), A -> A -> Prop.
-Parameter Under_rel_from_rel :
-  forall (A : Type) (eqA : A -> A -> Prop) (x y : A),
-    @Under_rel A eqA x y -> eqA x y.
-Parameter Under_relE :
-  forall (A : Type) (eqA : A -> A -> Prop) (x y : A),
-    @Under_rel A eqA x y = eqA x y.
-
-(** [Over_rel, over_rel, over_rel_done]: for "by rewrite over_rel" *)
-Parameter Over_rel :
-  forall (A : Type) (eqA : A -> A -> Prop), A -> A -> Prop.
-Parameter over_rel :
-  forall (A : Type) (eqA : A -> A -> Prop) (x y : A),
-    @Under_rel A eqA x y = @Over_rel A eqA x y.
-Parameter over_rel_done :
-  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
-    @Over_rel A eqA x x.
-Hint Extern 0 (@Over_rel _ _ _ _) =>
-  solve [ apply: over_rel_done ] : core.
-Hint Resolve over_rel_done : core.
-
-(** [under_rel_done]: for Ltac-style over *)
-Parameter under_rel_done :
-  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
-    @Under_rel A eqA x x.
-Notation "''Under[' x ]" := (@Under_rel _ _ x _)
-  (at level 8, format "''Under['  x  ]", only printing).
-End UNDER_REL.
-
-Module Export Under_rel : UNDER_REL.
-Definition Under_rel (A : Type) (eqA : A -> A -> Prop) :=
-  eqA.
-Lemma Under_rel_from_rel :
-  forall (A : Type) (eqA : A -> A -> Prop) (x y : A),
-    @Under_rel A eqA x y -> eqA x y.
-Proof. by []. Qed.
-Lemma Under_relE (A : Type) (eqA : A -> A -> Prop) (x y : A) :
-  @Under_rel A eqA x y = eqA x y.
-Proof. by []. Qed.
-Definition Over_rel := Under_rel.
-Lemma over_rel :
-  forall (A : Type) (eqA : A -> A -> Prop) (x y : A),
-    @Under_rel A eqA x y = @Over_rel A eqA x y.
-Proof. by []. Qed.
-Lemma over_rel_done :
-  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
-    @Over_rel A eqA x x.
-Proof. by rewrite /Over_rel. Qed.
-Lemma under_rel_done :
-  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
-    @Under_rel A eqA x x.
-Proof. by []. Qed.
-End Under_rel.
+(* Material for under/over (to rewrite under binders using "context lemmas") *)
+
+Require Export ssrunder.
+
+Hint Extern 0 (@Under_rel.Over_rel _ _ _ _) =>
+  solve [ apply: Under_rel.over_rel_done ] : core.
+Hint Resolve Under_rel.over_rel_done : core.
 
 Register Under_rel.Under_rel as plugins.ssreflect.Under_rel.
 Register Under_rel.Under_rel_from_rel as plugins.ssreflect.Under_rel_from_rel.
@@ -607,6 +555,8 @@ Ltac over :=
     them in another way than with reflexivity. *)
 Definition UnderE := Under_relE.
 
+(*****************************************************************************)
+
 (** An interface for non-Prop types; used to avoid improper instantiation
     of polymorphic lemmas with on-demand implicits when they are used as views.
     For example: Some_inj {T} : forall x y : T, Some x = Some y -> x = y.
diff --git a/plugins/ssr/ssrsetoid.v b/plugins/ssr/ssrsetoid.v
index 75653be0c5..609c9d5ab8 100644
--- a/plugins/ssr/ssrsetoid.v
+++ b/plugins/ssr/ssrsetoid.v
@@ -12,22 +12,111 @@
 
 (** Compatibility layer for [under] and [setoid_rewrite].
 
- This file is intended to be required by [Require Import Setoid] or so
- in order to reconcile [Coq.Classes.RelationClasses.Reflexive] with
- [Coq.ssr.ssrclasses.Reflexive].
+ This file is intended to be required by [Require Import Setoid].
 
- We can thus use the [under] tactic with other relations than [eq],
- such as [iff] or a [RewriteRelation], by doing:
+ In particular, we can use the [under] tactic with other relations
+ than [eq] or [iff], e.g. a [RewriteRelation], by doing:
  [Require Import ssreflect. Require Setoid.]
 
+ This file's instances have priority 12 > other stdlib instances
+ and each [Under_rel] instance comes with a [Hint Cut] directive
+ (otherwise Ring_polynom.v won't compile because of unbounded search).
+
  (Note: this file could be skipped when porting [under] to stdlib2.)
  *)
 
 Require Import ssrclasses.
+Require Import ssrunder.
 Require Import RelationClasses.
+Require Import Relation_Definitions.
+
+(** Reconcile [Coq.Classes.RelationClasses.Reflexive] with
+    [Coq.ssr.ssrclasses.Reflexive] *)
 
 Instance compat_Reflexive :
-  forall {A} {R : A -> A -> Prop},
+  forall {A} {R : relation A},
     RelationClasses.Reflexive R ->
-    ssrclasses.Reflexive R.
+    ssrclasses.Reflexive R | 12.
 Proof. now trivial. Qed.
+
+(** Add instances so that ['Under[ F i ]] terms,
+    that is, [Under_rel T R (F i) (?G i)] terms,
+    can be manipulated with rewrite/setoid_rewrite with lemmas on [R].
+    Note that this requires that [R] is a [Prop] relation, otherwise
+    a [bool] relation may need to be "lifted": see the [TestPreOrder]
+    section in test-suite/ssr/under.v *)
+
+Instance Under_subrelation {A} (R : relation A) : subrelation R (Under_rel _ R) | 12.
+Proof. now rewrite Under_relE. Qed.
+
+(* see also Morphisms.trans_co_eq_inv_impl_morphism *)
+
+Instance Under_Reflexive {A} (R : relation A) :
+  RelationClasses.Reflexive R ->
+  RelationClasses.Reflexive (Under_rel.Under_rel A R) | 12.
+Proof. now rewrite Under_rel.Under_relE. Qed.
+
+Hint Cut [_* Under_Reflexive Under_Reflexive] : typeclass_instances.
+
+(* These instances are a bit off-topic given that (Under_rel A R) will
+   typically be reflexive, to be able to trigger the [over] terminator
+
+Instance under_Irreflexive {A} (R : relation A) :
+  RelationClasses.Irreflexive R ->
+  RelationClasses.Irreflexive (Under_rel.Under_rel A R) | 12.
+Proof. now rewrite Under_rel.Under_relE. Qed.
+
+Hint Cut [_* Under_Irreflexive Under_Irreflexive] : typeclass_instances.
+
+Instance under_Asymmetric {A} (R : relation A) :
+  RelationClasses.Asymmetric R ->
+  RelationClasses.Asymmetric (Under_rel.Under_rel A R) | 12.
+Proof. now rewrite Under_rel.Under_relE. Qed.
+
+Hint Cut [_* Under_Asymmetric Under_Asymmetric] : typeclass_instances.
+
+Instance under_StrictOrder {A} (R : relation A) :
+  RelationClasses.StrictOrder R ->
+  RelationClasses.StrictOrder (Under_rel.Under_rel A R) | 12.
+Proof. now rewrite Under_rel.Under_relE. Qed.
+
+Hint Cut [_* Under_Strictorder Under_Strictorder] : typeclass_instances.
+ *)
+
+Instance Under_Symmetric {A} (R : relation A) :
+  RelationClasses.Symmetric R ->
+  RelationClasses.Symmetric (Under_rel.Under_rel A R) | 12.
+Proof. now rewrite Under_rel.Under_relE. Qed.
+
+Hint Cut [_* Under_Symmetric Under_Symmetric] : typeclass_instances.
+
+Instance Under_Transitive {A} (R : relation A) :
+  RelationClasses.Transitive R ->
+  RelationClasses.Transitive (Under_rel.Under_rel A R) | 12.
+Proof. now rewrite Under_rel.Under_relE. Qed.
+
+Hint Cut [_* Under_Transitive Under_Transitive] : typeclass_instances.
+
+Instance Under_PreOrder {A} (R : relation A) :
+  RelationClasses.PreOrder R ->
+  RelationClasses.PreOrder (Under_rel.Under_rel A R) | 12.
+Proof. now rewrite Under_rel.Under_relE. Qed.
+
+Hint Cut [_* Under_PreOrder Under_PreOrder] : typeclass_instances.
+
+Instance Under_PER {A} (R : relation A) :
+  RelationClasses.PER R ->
+  RelationClasses.PER (Under_rel.Under_rel A R) | 12.
+Proof. now rewrite Under_rel.Under_relE. Qed.
+
+Hint Cut [_* Under_PER Under_PER] : typeclass_instances.
+
+Instance Under_Equivalence {A} (R : relation A) :
+  RelationClasses.Equivalence R ->
+  RelationClasses.Equivalence (Under_rel.Under_rel A R) | 12.
+Proof. now rewrite Under_rel.Under_relE. Qed.
+
+Hint Cut [_* Under_Equivalence Under_Equivalence] : typeclass_instances.
+
+(* Don't handle Antisymmetric and PartialOrder classes for now,
+   as these classes depend on two relation symbols... *)
diff --git a/plugins/ssr/ssrunder.v b/plugins/ssr/ssrunder.v
new file mode 100644
index 0000000000..7c529a6133
--- /dev/null
+++ b/plugins/ssr/ssrunder.v
@@ -0,0 +1,75 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** #<style> .doc { font-family: monospace; white-space: pre; } </style># **)
+
+(** Constants for under/over, to rewrite under binders using "context lemmas"
+
+ Note: this file does not require [ssreflect]; it is both required by
+ [ssrsetoid] and *exported* by [ssrunder].
+
+ This preserves the following feature: we can use [Setoid] without
+ requiring [ssreflect] and use [ssreflect] without requiring [Setoid].
+*)
+
+Require Import ssrclasses.
+
+Module Type UNDER_REL.
+Parameter Under_rel :
+  forall (A : Type) (eqA : A -> A -> Prop), A -> A -> Prop.
+Parameter Under_rel_from_rel :
+  forall (A : Type) (eqA : A -> A -> Prop) (x y : A),
+    @Under_rel A eqA x y -> eqA x y.
+Parameter Under_relE :
+  forall (A : Type) (eqA : A -> A -> Prop),
+    @Under_rel A eqA = eqA.
+
+(** [Over_rel, over_rel, over_rel_done]: for "by rewrite over_rel" *)
+Parameter Over_rel :
+  forall (A : Type) (eqA : A -> A -> Prop), A -> A -> Prop.
+Parameter over_rel :
+  forall (A : Type) (eqA : A -> A -> Prop) (x y : A),
+    @Under_rel A eqA x y = @Over_rel A eqA x y.
+Parameter over_rel_done :
+  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
+    @Over_rel A eqA x x.
+
+(** [under_rel_done]: for Ltac-style over *)
+Parameter under_rel_done :
+  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
+    @Under_rel A eqA x x.
+Notation "''Under[' x ]" := (@Under_rel _ _ x _)
+  (at level 8, format "''Under['  x  ]", only printing).
+End UNDER_REL.
+
+Module Export Under_rel : UNDER_REL.
+Definition Under_rel (A : Type) (eqA : A -> A -> Prop) :=
+  eqA.
+Lemma Under_rel_from_rel :
+  forall (A : Type) (eqA : A -> A -> Prop) (x y : A),
+    @Under_rel A eqA x y -> eqA x y.
+Proof. now trivial. Qed.
+Lemma Under_relE (A : Type) (eqA : A -> A -> Prop) :
+  @Under_rel A eqA = eqA.
+Proof. now trivial. Qed.
+Definition Over_rel := Under_rel.
+Lemma over_rel :
+  forall (A : Type) (eqA : A -> A -> Prop) (x y : A),
+    @Under_rel A eqA x y = @Over_rel A eqA x y.
+Proof. now trivial. Qed.
+Lemma over_rel_done :
+  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
+    @Over_rel A eqA x x.
+Proof. now unfold Over_rel. Qed.
+Lemma under_rel_done :
+  forall (A : Type) (eqA : A -> A -> Prop) (EeqA : Reflexive eqA) (x : A),
+    @Under_rel A eqA x x.
+Proof. now trivial. Qed.
+End Under_rel.
diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
index 821683ca6d..c12491138a 100644
--- a/test-suite/ssr/under.v
+++ b/test-suite/ssr/under.v
@@ -311,3 +311,72 @@ under [here in Rel _ here]rel2_gen.
 - reflexivity.
 Qed.
 End TestGeneric2.
+
+Section TestPreOrder.
+(* inspired by https://github.com/coq/coq/pull/10022#issuecomment-530101950
+   but without needing to do [rewrite UnderE] manually. *)
+
+Require Import Morphisms.
+
+(** Tip to tell rewrite that the LHS of [leq' x y (:= leq x y = true)]
+    is x, not [leq x y] *)
+Definition rel_true {T} (R : rel T) x y := is_true (R x y).
+Definition leq' : nat -> nat -> Prop := rel_true leq.
+
+Parameter leq_add :
+  forall m1 m2 n1 n2 : nat, m1 <= n1 -> m2 <= n2 -> m1 + m2 <= n1 + n2.
+Parameter leq_mul :
+ forall m1 m2 n1 n2 : nat, m1 <= n1 -> m2 <= n2 -> m1 * m2 <= n1 * n2.
+
+Local Notation "+%N" := addn (at level 0, only parsing).
+
+(** Context lemma (could *)
+Lemma leq'_big : forall I (F G : I -> nat) (r : seq I),
+    (forall i : I, leq' (F i) (G i)) ->
+    (leq' (\big[+%N/0%N]_(i <- r) F i) (\big[+%N/0%N]_(i <- r) G i)).
+Proof.
+red=> F G m n HFG.
+apply: (big_ind2 leq _ _ (P := xpredT) (op1 := addn) (op2 := addn)) =>//.
+move=> *; exact: leq_add.
+move=> *; exact: HFG.
+Qed.
+
+(** Instances for [setoid_rewrite] *)
+Instance leq'_rr : RewriteRelation leq' := {}.
+
+Instance leq'_proper_addn : Proper (leq' ==> leq' ==> leq') addn.
+Proof. move=> a1 b1 le1 a2 b2 le2; exact/leq_add. Qed.
+
+Instance leq'_proper_muln : Proper (leq' ==> leq' ==> leq') muln.
+Proof. move=> a1 b1 le1 a2 b2 le2; exact/leq_mul. Qed.
+
+
+Instance leq'_preorder : PreOrder leq'.
+(** encompasses [Reflexive] *)
+Proof. rewrite /leq' /rel_true; split =>// ??? A B; exact: leq_trans A B. Qed.
+
+Instance leq'_reflexive : Reflexive leq'.
+Proof. by rewrite /leq' /rel_true. Qed.
+
+Parameter leq_add2l :
+  forall p m n : nat, (p + m <= p + n) = (m <= n).
+
+Lemma test : forall n : nat,
+  (1 + 2 * (\big[+%N/0]_(i < n) (3 + i)) * 4 + 5 <= 6 + 24 * n + 8 * n * n)%N.
+Proof.
+move=> n; rewrite -[is_true _]/(rel_true _ _ _) -/leq'.
+have lem : forall (i : nat), i < n -> leq' (3 + i) (3 + n).
+{ by move=> i Hi; rewrite /leq' /rel_true leq_add2l; apply/ltnW. }
+
+under leq'_big => i.
+{
+  (* The "magic" is here: instantiate the evar with the bound "3 + n" *)
+  rewrite lem ?ltn_ord //. over.
+}
+cbv beta.
+
+now_show (leq' (1 + 2 * \big[+%N/0]_(i < n) (3 + n) * 4 + 5) (6 + 24 * n + 8 * n * n)).
+(* uninteresting end of proof, omitted *)
+Abort.
+
+End TestPreOrder.