[ssr] Define over as a rewrite rule & Merge 'Under[ _ ] notations

as suggested by @gares, and:

* Rename some Under_* terms for better uniformity;
* Update & Improve minor details in the documentation.

6 files changed, 83 insertions, 70 deletions

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 7545e1b8d7..a40dfa486f 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3680,7 +3680,7 @@ complete terms, as shown by the simple example below.
 
    as we need to explicitly provide the non-inferable argument ``F2``,
    which corresponds here to the term we want to obtain *after* the
-   rewriting step. In order to perform the rewrie step one has to
+   rewriting step. In order to perform the rewrite step one has to
    provide the term by hand as follows:
 
    .. coqtop:: all abort
@@ -3742,30 +3742,30 @@ The execution of the Ltac expression:
 involves the following steps:
 
 1. It performs a :n:`rewrite @term`
-   without failing like in the above example with ``eq_map``, but
-   creating evars (see :tacn:`evar`). If :n:`term` is prefixed by
-   a pattern or an occurrence selector, then the modifiers is honoured.
+   without failing like in the first example with ``rewrite eq_map.``,
+   but creating evars (see :tacn:`evar`). If :n:`term` is prefixed by
+   a pattern or an occurrence selector, then the modifiers are honoured.
 
 2. As a n-branches intro pattern is provided :tacn:`under` checks that
    n+1 subgoals have been created. The last one is the main subgoal,
    while the other ones correspond to premises of the rewrite rule (such as
    ``forall n, F1 n = F2 n`` for ``eq_map``).
 
-3. Then :tacn:`under` checks that the first n subgoals
+3. If so :tacn:`under` executes the corresponding
+   intro pattern :n:`@ipat__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).
 
-4. If so :tacn:`under` executes the corresponding
-   intro pattern :n:`@ipat__i` in each goal.
-
-5. Then :tacn:`under` protects these n goals against an
-   accidental instantiation of the evar. These protected goals are displayed
-   using the ``Under[ … ]`` notation (e.g. ``Under[ m - m ]``
-   in the running example).
+5. If so :tacn:`under` protects these n goals against an
+   accidental instantiation of the evar.
+   These protected goals are displayed using the ``Under[ … ]``
+   notation (e.g. ``Under[ m - m ]`` in the running example).
 
 6. The expression inside the ``Under[ … ]`` notation can be
    proved equivalent to the desired expression
-   by using a regular tacn:`rewrite` tactic.
+   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).
@@ -3787,17 +3787,12 @@ displayed as ``Under[ … ]``):
    :name: over
 
    This terminator tactic allows one to close goals of the form
-   ``'Under[ … ]`` or ``'Under_iff[ … ]``.
+   ``'Under[ … ]``.
 
 .. tacv:: by rewrite over
 
    This is a variant of :tacn:`over` in order to close ``Under[ … ]``
-   goals, relying on the ``over`` lemma.
-
-.. tacv:: by rewrite over_iff
-
-   This is a variant of :tacn:`over` in order to close ``Under_iff[ … ]``
-   goals, relying on the ``over_iff`` lemma.
+   goals, relying on the ``over`` rewrite rule.
 
 .. _under_one_liner:
 
@@ -3828,8 +3823,8 @@ Notes:
 
 + If the ``do`` clause is provided and the intro pattern is omitted,
   then the defeault :token:`i_item` ``*`` is applied to each branch.
-  Eg the Ltac expression
-  :n:`under @term do [ @tac__1 | … | @tac__n ]` is equivalent to
+  E.g., the Ltac expression:
+  :n:`under @term do [ @tac__1 | … | @tac__n ]` is equivalent to:
   :n:`under @term => [ * | … | * ] do [ @tac__1 | … | @tac__n ].`
 
 .. example::
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 94e0b2a724..6c74ac1960 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -504,55 +504,55 @@ Proof. by move=> /(_ P); apply. Qed.
 (*****************************************************************************)
 (* Constants for under, to rewrite under binders using "Leibniz eta lemmas". *)
 
-Module Type UNDER.
-Parameter Under :
+Module Type UNDER_EQ.
+Parameter Under_eq :
   forall (R : Type), R -> R -> Prop.
-Parameter Under_from_eq :
-  forall (T : Type) (x y : T), @Under T x y -> x = y.
+Parameter Under_eq_from_eq :
+  forall (T : Type) (x y : T), @Under_eq T x y -> x = y.
 
-(** [Over, over, over_done]: for "by rewrite over" *)
-Parameter Over :
+(** [Over_eq, over_eq, over_eq_done]: for "by rewrite over_eq" *)
+Parameter Over_eq :
   forall (R : Type), R -> R -> Prop.
-Parameter over :
-  forall (T : Type) (x : T) (y : T), @Under T x y = @Over T x y.
-Parameter over_done :
-  forall (T : Type) (x : T), @Over T x x.
+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 _ _ _) => solve [ apply over_done ] : core.
+Hint Extern 0 (@Over_eq _ _ _) => solve [ apply over_eq_done ] : core.
 (* => for [test-suite/ssr/under.v:test_big_patt1] *)
-Hint Resolve over_done : core.
+Hint Resolve over_eq_done : core.
 (* => for [test-suite/ssr/over.v:test_over_1_1] *)
 
-(** [under_done]: for Ltac-style over *)
-Parameter under_done :
-  forall (T : Type) (x : T), @Under T x x.
-Notation "''Under[' x ]" := (@Under _ x _)
-  (at level 8, format "''Under['  x  ]").
-End UNDER.
-
-Module Export Under : UNDER.
-Definition Under := @eq.
-Lemma Under_from_eq (T : Type) (x y : T) :
-  @Under T x y -> x = y.
+(** [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 := Under.
-Lemma over :
-  forall (T : Type) (x : T) (y : T), @Under T x y = @Over T x y.
+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_done :
-  forall (T : Type) (x : T), @Over T x x.
+Lemma over_eq_done :
+  forall (T : Type) (x : T), @Over_eq T x x.
 Proof. by []. Qed.
-Lemma under_done :
-  forall (T : Type) (x : T), @Under T x x.
+Lemma under_eq_done :
+  forall (T : Type) (x : T), @Under_eq T x x.
 Proof. by []. Qed.
-End Under.
+End Under_eq.
 
-Register Under as plugins.ssreflect.Under.
-Register Under_from_eq as plugins.ssreflect.Under_from_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_from_iff : forall x y : Prop, @Under_iff x y -> x <-> y.
+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.
@@ -566,13 +566,13 @@ 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_iff[' x ]" := (@Under_iff x _)
-  (at level 8, format "''Under_iff['  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_from_iff (x y : Prop) :
+Lemma Under_iff_from_iff (x y : Prop) :
   @Under_iff x y -> x <-> y.
 Proof. by []. Qed.
 Definition Over_iff := Under_iff.
@@ -588,11 +588,12 @@ Proof. by []. Qed.
 End Under_iff.
 
 Register Under_iff as plugins.ssreflect.Under_iff.
-Register Under_from_iff as plugins.ssreflect.Under_from_iff.
+Register Under_iff_from_iff as plugins.ssreflect.Under_iff_from_iff.
+
+Definition over := (over_eq, over_iff).
 
 Ltac over :=
-  by [ apply: Under.under_done
-     | rewrite over
+  by [ apply: Under_eq.under_eq_done
      | apply: Under_iff.under_iff_done
-     | rewrite over_iff
+     | rewrite over
      ].
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index d60e3857b1..313b46ddc3 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -347,7 +347,7 @@ let intro_lock ipats =
                let sigma, under_iff =
                  Ssrcommon.mkSsrConst "Under_iff" env sigma in
                let sigma, under_from_iff =
-                 Ssrcommon.mkSsrConst "Under_from_iff" env sigma in
+                 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|]))
@@ -359,9 +359,9 @@ let intro_lock ipats =
             Array.length args = 3 && is_app_evar sigma args.(2) ->
               Tactics.New.refine ~typecheck:true (fun sigma ->
                 let sigma, under =
-                  Ssrcommon.mkSsrConst "Under" env sigma in
+                  Ssrcommon.mkSsrConst "Under_eq" env sigma in
                 let sigma, under_from_eq =
-                  Ssrcommon.mkSsrConst "Under_from_eq" env sigma in
+                  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|]))
diff --git a/test-suite/output/ssr_under.out b/test-suite/output/ssr_under.out
index 8532b62a54..499d25391e 100644
--- a/test-suite/output/ssr_under.out
+++ b/test-suite/output/ssr_under.out
@@ -1,2 +1,4 @@
 'Under[ m - m ]
 (G (fun _ : nat => 0) n >= 0)
+'Under[ r = R0 \/ E r ]
+(Rbar_le Rbar0 (Lub_Rbar (fun r : R => r = R0 \/ E r)))
diff --git a/test-suite/output/ssr_under.v b/test-suite/output/ssr_under.v
index b11dd1509c..7335c87e61 100644
--- a/test-suite/output/ssr_under.v
+++ b/test-suite/output/ssr_under.v
@@ -13,3 +13,18 @@ Lemma example_G (n : nat) : G (fun n => n - n) n >= 0.
 under eq_G => m do show; rewrite subnn.
 show.
 Abort.
+
+Parameters (R Rbar : Set) (R0 : R) (Rbar0 : Rbar).
+Parameter Rbar_le : Rbar -> Rbar -> Prop.
+Parameter Lub_Rbar : (R -> Prop) -> Rbar.
+Parameter Lub_Rbar_eqset :
+  forall E1 E2 : R -> Prop,
+    (forall x : R, E1 x <-> E2 x) ->
+    Lub_Rbar E1 = Lub_Rbar E2.
+
+Lemma test_Lub_Rbar (E : R -> Prop)  :
+  Rbar_le Rbar0 (Lub_Rbar (fun x => x = R0 \/ E x)).
+Proof.
+under Lub_Rbar_eqset => r do show.
+show.
+Abort.
diff --git a/test-suite/ssr/over.v b/test-suite/ssr/over.v
index cd6b196eeb..8232741b0d 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_from_eq.
+  apply Under_eq_from_eq.
   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_from_eq.
+  apply Under_eq_from_eq.
   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_from_eq.
+  apply Under_eq_from_eq.
   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_from_eq.
+  apply Under_eq_from_eq.
   Fail done.
 
   rewrite over.