Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) relation

Reviewed-by: gares

14 files changed, 480 insertions, 120 deletions

diff --git a/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst b/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst
new file mode 100644
index 0000000000..5e005742fd
--- /dev/null
+++ b/doc/changelog/06-ssreflect/10022-ssr-under-setoid.rst
@@ -0,0 +1,28 @@
+- Generalize tactics :tacn:`under` and :tacn:`over` for any registered
+  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 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
+  and Cyril Cohen).
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 75897fec45..04d0503ff4 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3756,8 +3756,11 @@ involves the following steps:
    the corresponding intro pattern :n:`@i_pattern__i` in each goal.
 
 4. Then :tacn:`under` checks that the first n subgoals
-   are (quantified) equalities or double implications between a
-   term and an evar (e.g. ``m - m = ?F2 m`` in the running example).
+   are (quantified) Leibniz equalities, double implications or
+   registered relations (w.r.t. Class ``RewriteRelation``) between a
+   term and an evar, e.g. ``m - m = ?F2 m`` in the running example.
+   (This support for setoid-like relations is enabled as soon as we do
+   both ``Require Import ssreflect.`` and ``Require Setoid.``)
 
 5. If so :tacn:`under` protects these n goals against an
    accidental instantiation of the evar.
@@ -3769,7 +3772,10 @@ involves the following steps:
    by using a regular :tacn:`rewrite` tactic.
 
 7. Interactive editing of the first n goals has to be signalled by
-   using the :tacn:`over` tactic or rewrite rule (see below).
+   using the :tacn:`over` tactic or rewrite rule (see below), which
+   requires that the underlying relation is reflexive. (The running
+   example deals with Leibniz equality, but ``PreOrder`` relations are
+   also supported, for example.)
 
 8. Finally, a post-processing step is performed in the main goal
    to keep the name(s) for the bound variables chosen by the user in
@@ -3795,6 +3801,10 @@ displayed as ``'Under[ … ]``):
    This is a variant of :tacn:`over` in order to close ``'Under[ … ]``
    goals, relying on the ``over`` rewrite rule.
 
+Note that a rewrite rule ``UnderE`` is available as well, if one wants
+to "unprotect" the evar, without closing the goal automatically (e.g.,
+to instantiate it manually with another rule than reflexivity).
+
 .. _under_one_liner:
 
 One-liner mode
diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
index 5b243c8a9e..a2bc90ffc0 100644
--- a/doc/stdlib/hidden-files
+++ b/doc/stdlib/hidden-files
@@ -83,3 +83,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/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index eedd8a3d61..851510b465 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -620,6 +620,7 @@ through the <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     plugins/ssrmatching/ssrmatching.v
+    plugins/ssr/ssrclasses.v
     plugins/ssr/ssreflect.v
     plugins/ssr/ssrbool.v
     plugins/ssr/ssrfun.v
diff --git a/plugins/ssr/ssrclasses.v b/plugins/ssr/ssrclasses.v
new file mode 100644
index 0000000000..0ae3f8c6a5
--- /dev/null
+++ b/plugins/ssr/ssrclasses.v
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*         *   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># **)
+
+(** 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. **)
+
+Section Defs.
+  Context {A : Type}.
+  Class Reflexive (R : A -> A -> Prop) :=
+    reflexivity : forall x : A, R x x.
+End Defs.
+
+Register Reflexive as plugins.ssreflect.reflexive_type.
+Register reflexivity as plugins.ssreflect.reflexive_proof.
+
+Instance eq_Reflexive {A : Type} : Reflexive (@eq A) := @eq_refl A.
+Instance iff_Reflexive : Reflexive iff := iff_refl.
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 9ebdf71329..bc4a57dedd 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -530,102 +530,32 @@ Lemma abstract_context T (P : T -> Type) x :
 Proof. by move=> /(_ P); apply. Qed.
 
 (*****************************************************************************)
-(* Constants for under, to rewrite under binders using "Leibniz eta lemmas". *)
-
-Module Type UNDER_EQ.
-Parameter Under_eq :
-  forall (R : Type), R -> R -> Prop.
-Parameter Under_eq_from_eq :
-  forall (T : Type) (x y : T), @Under_eq T x y -> x = y.
-
-(** [Over_eq, over_eq, over_eq_done]: for "by rewrite over_eq" *)
-Parameter Over_eq :
-  forall (R : Type), R -> R -> Prop.
-Parameter over_eq :
-  forall (T : Type) (x : T) (y : T), @Under_eq T x y = @Over_eq T x y.
-Parameter over_eq_done :
-  forall (T : Type) (x : T), @Over_eq T x x.
-(* We need both hints below, otherwise the test-suite does not pass *)
-Hint Extern 0 (@Over_eq _ _ _) => solve [ apply over_eq_done ] : core.
-(* => for [test-suite/ssr/under.v:test_big_patt1] *)
-Hint Resolve over_eq_done : core.
-(* => for [test-suite/ssr/over.v:test_over_1_1] *)
-
-(** [under_eq_done]: for Ltac-style over *)
-Parameter under_eq_done :
-  forall (T : Type) (x : T), @Under_eq T x x.
-Notation "''Under[' x ]" := (@Under_eq _ x _)
-  (at level 8, format "''Under['  x  ]", only printing).
-End UNDER_EQ.
-
-Module Export Under_eq : UNDER_EQ.
-Definition Under_eq := @eq.
-Lemma Under_eq_from_eq (T : Type) (x y : T) :
-  @Under_eq T x y -> x = y.
-Proof. by []. Qed.
-Definition Over_eq := Under_eq.
-Lemma over_eq :
-  forall (T : Type) (x : T) (y : T), @Under_eq T x y = @Over_eq T x y.
-Proof. by []. Qed.
-Lemma over_eq_done :
-  forall (T : Type) (x : T), @Over_eq T x x.
-Proof. by []. Qed.
-Lemma under_eq_done :
-  forall (T : Type) (x : T), @Under_eq T x x.
-Proof. by []. Qed.
-End Under_eq.
-
-Register Under_eq as plugins.ssreflect.Under_eq.
-Register Under_eq_from_eq as plugins.ssreflect.Under_eq_from_eq.
-
-Module Type UNDER_IFF.
-Parameter Under_iff : Prop -> Prop -> Prop.
-Parameter Under_iff_from_iff : forall x y : Prop, @Under_iff x y -> x <-> y.
-
-(** [Over_iff, over_iff, over_iff_done]: for "by rewrite over_iff" *)
-Parameter Over_iff : Prop -> Prop -> Prop.
-Parameter over_iff :
-  forall (x : Prop) (y : Prop), @Under_iff x y = @Over_iff x y.
-Parameter over_iff_done :
-  forall (x : Prop), @Over_iff x x.
-Hint Extern 0 (@Over_iff _ _) => solve [ apply over_iff_done ] : core.
-Hint Resolve over_iff_done : core.
-
-(** [under_iff_done]: for Ltac-style over *)
-Parameter under_iff_done :
-  forall (x : Prop), @Under_iff x x.
-Notation "''Under[' x ]" := (@Under_iff x _)
-  (at level 8, format "''Under['  x  ]", only printing).
-End UNDER_IFF.
-
-Module Export Under_iff : UNDER_IFF.
-Definition Under_iff := iff.
-Lemma Under_iff_from_iff (x y : Prop) :
-  @Under_iff x y -> x <-> y.
-Proof. by []. Qed.
-Definition Over_iff := Under_iff.
-Lemma over_iff :
-  forall (x : Prop) (y : Prop), @Under_iff x y = @Over_iff x y.
-Proof. by []. Qed.
-Lemma over_iff_done :
-  forall (x : Prop), @Over_iff x x.
-Proof. by []. Qed.
-Lemma under_iff_done :
-  forall (x : Prop), @Under_iff x x.
-Proof. by []. Qed.
-End Under_iff.
-
-Register Under_iff as plugins.ssreflect.Under_iff.
-Register Under_iff_from_iff as plugins.ssreflect.Under_iff_from_iff.
-
-Definition over := (over_eq, over_iff).
+(* 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.
+
+(** Closing rewrite rule *)
+Definition over := over_rel.
+
+(** Closing tactic *)
 Ltac over :=
-  by [ apply: Under_eq.under_eq_done
-     | apply: Under_iff.under_iff_done
+  by [ apply: Under_rel.under_rel_done
      | rewrite over
      ].
 
+(** Convenience rewrite rule to unprotect evars, e.g., to instantiate
+    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/ssreflect_plugin.mlpack b/plugins/ssr/ssreflect_plugin.mlpack
index 824348fee7..46669998b9 100644
--- a/plugins/ssr/ssreflect_plugin.mlpack
+++ b/plugins/ssr/ssreflect_plugin.mlpack
@@ -10,4 +10,3 @@ Ssripats
 Ssrfwd
 Ssrparser
 Ssrvernac
-
diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli
index 43aeeb2dae..baf5288725 100644
--- a/plugins/ssr/ssrequality.mli
+++ b/plugins/ssr/ssrequality.mli
@@ -42,6 +42,9 @@ val mk_rwarg :
 val norwmult : ssrdir * ssrmult
 val norwocc : (Ssrast.ssrclear option * Ssrast.ssrocc) * Ssrmatching.rpattern option
 
+val ssr_is_setoid :
+  Environ.env -> Evd.evar_map -> EConstr.t -> EConstr.t array -> bool
+
 val ssrinstancesofrule :
   Ltac_plugin.Tacinterp.interp_sign ->
   Ssrast.ssrdir ->
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index cca94c8c9b..b0f56c423f 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -340,6 +340,21 @@ let intro_lock ipats =
   let hnf' = Proofview.numgoals >>= fun ng ->
              Proofview.tclDISPATCH
                (ncons (ng - 1) ssrsmovetac @ [Proofview.tclUNIT ()]) in
+  let protect_subgoal env sigma hd args =
+    Tactics.New.refine ~typecheck:true (fun sigma ->
+        let lm2 = Array.length args - 2 in
+        let sigma, carrier =
+          Typing.type_of env sigma args.(lm2) in
+        let rel = EConstr.mkApp (hd, Array.sub args 0 lm2) in
+        let rel_args = Array.sub args lm2 2 in
+        let sigma, under_rel =
+          Ssrcommon.mkSsrConst "Under_rel" env sigma in
+        let sigma, under_from_rel =
+          Ssrcommon.mkSsrConst "Under_rel_from_rel" env sigma in
+        let under_rel_args = Array.append [|carrier; rel|] rel_args in
+        let ty = EConstr.mkApp (under_rel, under_rel_args) in
+        let sigma, t = Evarutil.new_evar env sigma ty in
+        sigma, EConstr.mkApp(under_from_rel,Array.append under_rel_args [|t|])) in
   let rec lock_eq () : unit Proofview.tactic = Proofview.Goal.enter begin fun _ ->
     Proofview.tclORELSE
       (Ssripats.tclIPAT [Ssripats.IOpTemporay; Ssripats.IOpEqGen (lock_eq ())])
@@ -349,30 +364,23 @@ let intro_lock ipats =
         let env = Proofview.Goal.env gl in
         match EConstr.kind_of_type sigma c with
         | Term.AtomicType(hd, args) when
+            Array.length args >= 2 && is_app_evar sigma (Array.last args) &&
+            Ssrequality.ssr_is_setoid env sigma hd args
+            (* if the last condition above [ssr_is_setoid ...] holds
+            then [Coq.Classes.RelationClasses] has been required *)
+            ||
+            (* if this is not the case, the tactic can still succeed
+            when the considered relation is [Coq.Init.Logic.iff] *)
             Ssrcommon.is_const_ref sigma hd (Coqlib.lib_ref "core.iff.type") &&
-           Array.length args = 2 && is_app_evar sigma args.(1) ->
-           Tactics.New.refine ~typecheck:true (fun sigma ->
-               let sigma, under_iff =
-                 Ssrcommon.mkSsrConst "Under_iff" env sigma in
-               let sigma, under_from_iff =
-                 Ssrcommon.mkSsrConst "Under_iff_from_iff" env sigma in
-               let ty = EConstr.mkApp (under_iff,args) in
-               let sigma, t = Evarutil.new_evar env sigma ty in
-               sigma, EConstr.mkApp(under_from_iff,Array.append args [|t|]))
+            Array.length args = 2 && is_app_evar sigma args.(1) ->
+          protect_subgoal env sigma hd args
         | _ ->
         let t = Reductionops.whd_all env sigma c in
         match EConstr.kind_of_type sigma t with
         | Term.AtomicType(hd, args) when
             Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") &&
             Array.length args = 3 && is_app_evar sigma args.(2) ->
-              Tactics.New.refine ~typecheck:true (fun sigma ->
-                let sigma, under =
-                  Ssrcommon.mkSsrConst "Under_eq" env sigma in
-                let sigma, under_from_eq =
-                  Ssrcommon.mkSsrConst "Under_eq_from_eq" env sigma in
-                let ty = EConstr.mkApp (under,args) in
-                let sigma, t = Evarutil.new_evar env sigma ty in
-                sigma, EConstr.mkApp(under_from_eq,Array.append args [|t|]))
+          protect_subgoal env sigma hd args
         | _ ->
     ppdebug(lazy Pp.(str"under: stop:" ++ pr_econstr_env env sigma t));
 
diff --git a/plugins/ssr/ssrsetoid.v b/plugins/ssr/ssrsetoid.v
new file mode 100644
index 0000000000..609c9d5ab8
--- /dev/null
+++ b/plugins/ssr/ssrsetoid.v
@@ -0,0 +1,122 @@
+(************************************************************************)
+(*         *   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># **)
+
+(** Compatibility layer for [under] and [setoid_rewrite].
+
+ This file is intended to be required by [Require Import Setoid].
+
+ 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 : relation A},
+    RelationClasses.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/over.v b/test-suite/ssr/over.v
index 8232741b0d..267d981d05 100644
--- a/test-suite/ssr/over.v
+++ b/test-suite/ssr/over.v
@@ -12,7 +12,7 @@ assert (H : forall i : nat, i + 2 * i - i = x2 i).
   unfold x2 in *; clear x2;
   unfold R in *; clear R;
   unfold I in *; clear I.
-  apply Under_eq_from_eq.
+  apply Under_rel_from_rel.
   Fail done.
 
   over.
@@ -27,7 +27,7 @@ assert (H : forall i : nat, i + 2 * i - i = x2 i).
   unfold x2 in *; clear x2;
   unfold R in *; clear R;
   unfold I in *; clear I.
-  apply Under_eq_from_eq.
+  apply Under_rel_from_rel.
   Fail done.
 
   by rewrite over.
@@ -45,7 +45,7 @@ assert (H : forall i j, i + 2 * j - i = x2 i j).
   unfold R in *; clear R;
   unfold J in *; clear J;
   unfold I in *; clear I.
-  apply Under_eq_from_eq.
+  apply Under_rel_from_rel.
   Fail done.
 
   over.
@@ -61,7 +61,7 @@ assert (H : forall i j : nat, i + 2 * j - i = x2 i j).
   unfold R in *; clear R;
   unfold J in *; clear J;
   unfold I in *; clear I.
-  apply Under_eq_from_eq.
+  apply Under_rel_from_rel.
   Fail done.
 
   rewrite over.
diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
index f285ad138b..c12491138a 100644
--- a/test-suite/ssr/under.v
+++ b/test-suite/ssr/under.v
@@ -160,7 +160,15 @@ Lemma test_big_occs (F G : nat -> nat) (n : nat) :
   \sum_(0 <= i < n) (i * 0) = \sum_(0 <= i < n) (i * 0) + \sum_(0 <= i < n) (i * 0).
 Proof.
 under {2}[in RHS]eq_bigr => i Hi do rewrite muln0.
-by rewrite big_const_nat iter_addn_0.
+by rewrite big_const_nat iter_addn_0 mul0n addn0.
+Qed.
+
+Lemma test_big_occs_inH (F G : nat -> nat) (n : nat) :
+  \sum_(0 <= i < n) (i * 0) = \sum_(0 <= i < n) (i * 0) + \sum_(0 <= i < n) (i * 0) -> True.
+Proof.
+move=> H.
+do [under {2}[in RHS]eq_bigr => i Hi do rewrite muln0] in H.
+by rewrite big_const_nat iter_addn_0 mul0n addn0 in H.
 Qed.
 
 (* Solely used, one such renaming is useless in practice, but it works anyway *)
@@ -218,7 +226,6 @@ under Lub_Rbar_eqset => r.
 by rewrite over.
 Abort.
 
-
 Lemma ex_iff R (P1 P2 : R -> Prop) :
   (forall x : R, P1 x <-> P2 x) -> ((exists x, P1 x) <-> (exists x, P2 x)).
 Proof.
@@ -227,8 +234,149 @@ Qed.
 
 Arguments ex_iff [R P1] P2 iffP12.
 
-Require Import Setoid.
+(** Load the [setoid_rewrite] machinery *)
+Require Setoid.
+
+(** Replay the tactics from [test_Lub_Rbar] in this new environment *)
+Lemma test_Lub_Rbar_again (E : R -> Prop)  :
+  Rbar_le Rbar0 (Lub_Rbar (fun x => x = R0 \/ E x)).
+Proof.
+under Lub_Rbar_eqset => r.
+by rewrite over.
+Abort.
+
 Lemma test_ex_iff (P : nat -> Prop) : (exists x, P x) -> True.
-under ex_iff => n.
+under ex_iff => n. (* this requires [Setoid] *)
 by rewrite over.
+by move=> _.
+Qed.
+
+Section TestGeneric.
+Context {A B : Type} {R : nat -> B -> B -> Prop}
+        `{!forall n : nat, RelationClasses.Equivalence (R n)}.
+Variables (F : (A -> A -> B) -> B).
+Hypothesis ex_gen : forall (n : nat) (P1 P2 : A -> A -> B),
+  (forall x y : A, R n (P1 x y) (P2 x y)) -> (R n (F P1) (F P2)).
+Arguments ex_gen [n P1] P2 relP12.
+Lemma test_ex_gen (P1 P2 : A -> A -> B) (n : nat) :
+  (forall x y : A, P2 x y = P2 y x) ->
+  R n (F P1) (F P2) /\ True -> True.
+Proof.
+move=> P2C.
+under [X in R _ _ X]ex_gen => a b.
+  by rewrite P2C over.
+by move => _.
+Qed.
+End TestGeneric.
+
+Import Setoid.
+(* to expose [Coq.Relations.Relation_Definitions.reflexive],
+   [Coq.Classes.RelationClasses.RewriteRelation], and so on. *)
+
+Section TestGeneric2.
+(* Some toy abstract example with a parameterized setoid type *)
+Record Setoid (m n : nat) : Type :=
+  { car : Type
+  ; Rel : car -> car -> Prop
+  ; refl : reflexive _ Rel
+  ; sym : symmetric _ Rel
+  ; trans : transitive _ Rel
+  }.
+
+Context {m n : nat}.
+Add Parametric Relation (s : Setoid m n) : (car s) (@Rel _ _ s)
+  reflexivity proved by (@refl _ _ s)
+  symmetry proved by (@sym _ _ s)
+  transitivity proved by (@trans _ _ s)
+  as eq_rel.
+
+Context {A : Type} {s1 s2 : Setoid m n}.
+
+Let B := @car m n s1.
+Let C := @car m n s2.
+Variable (F : C -> (A -> A -> B) -> C).
+Hypothesis rel2_gen :
+  forall (c1 c2 : C) (P1 P2 : A -> A -> B),
+    Rel c1 c2 ->
+    (forall a b : A, Rel (P1 a b) (P2 a b)) ->
+    Rel (F c1 P1) (F c2 P2).
+Arguments rel2_gen [c1] c2 [P1] P2 relc12 relP12.
+Lemma test_rel2_gen (c : C) (P : A -> A -> B)
+  (toy_hyp : forall a b, P a b = P b a) :
+  Rel (F c P) (F c (fun a b => P b a)).
+Proof.
+under [here in Rel _ here]rel2_gen.
+- over.
+- by move=> a b; rewrite toy_hyp over.
+- 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.
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 2f8be5de12..ddc9967bfa 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -12,6 +12,8 @@ Require Export Coq.Classes.SetoidTactics.
 
 Export Morphisms.ProperNotations.
 
+Require Coq.ssr.ssrsetoid.
+
 (** For backward compatibility *)
 
 Definition Setoid_Theory := @Equivalence.