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

Reviewed-by: gares

4 files changed, 44 insertions, 3 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