Merge PR #9651: [ssr] Add tactics under and over

Reviewed-by: CohenCyril
Ack-by: Zimmi48
Ack-by: erikmd
Ack-by: gares
Ack-by: jfehrle

16 files changed, 1026 insertions, 53 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 9a292562ed..2f58bfb825 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -293,12 +293,22 @@ Misc
 
 SSReflect
 
+- New tactic `under` to rewrite under binders, given an extensionality lemma:
+  - interactive mode: `under lem`, associated terminator: `over`
+  - one-liner mode: `under lem do [tac1 | ...]`
+
+  It can take occurrence switches, contextual patterns, and intro patterns:
+  `under {2}[in RHS]eq_big => [i|i ?] do ...`.
+
+  See the reference manual for the actual documentation.
+
 - New intro patterns:
   - temporary introduction: `=> +`
   - block introduction: `=> [^ prefix ] [^~ suffix ]`
   - fast introduction: `=> >`
   - tactics as views: `=> /ltac:mytac`
   - replace hypothesis: `=> {}H`
+
   See the reference manual for the actual documentation.
 
 - Clear discipline made consistent across the entire proof language.
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index b240cef40c..4e40df6f94 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -1737,9 +1737,8 @@ Intro patterns
   for each :token:`ident`.  Its type has to be fixed later on by using the
   ``abstract`` tactic.  Before then the type displayed is ``<hidden>``.
 
-
 Note that |SSR| does not support the syntax ``(ipat, …, ipat)`` for
-destructing intro-patterns.
+destructing intro patterns.
 
 Clear switch
 ````````````
@@ -3626,7 +3625,7 @@ corresponding new goals will be generated.
   As in :ref:`apply_ssr`, the ``ssrautoprop`` tactic is used to try to
   solve the existential variable.
 
-  .. coqtop:: all
+  .. coqtop:: all abort
 
      Lemma test (x : 'I_2) y (H : y < 2) : Some x = insub 2 y.
      rewrite insubT.
@@ -3637,6 +3636,272 @@ rewriting rule is stated using Leibniz equality (as opposed to setoid
 relations). It will be extended to other rewriting relations in the
 future.
 
+.. _under_ssr:
+
+Rewriting under binders
+~~~~~~~~~~~~~~~~~~~~~~~
+
+Goals involving objects defined with higher-order functions often
+require "rewriting under binders". While setoid rewriting is a
+possible approach in this case, it is common to use regular rewriting
+along with dedicated extensionality lemmas. This may cause some
+practical issues during the development of the corresponding scripts,
+notably as we might be forced to provide the rewrite tactic with
+complete terms, as shown by the simple example below.
+
+.. example::
+
+   .. coqtop:: reset none
+
+      From Coq Require Import ssreflect.
+      Set Implicit Arguments.
+      Unset Strict Implicit.
+      Unset Printing Implicit Defensive.
+
+   .. coqtop:: in
+
+      Axiom subnn : forall n : nat, n - n = 0.
+      Parameter map : (nat -> nat) -> list nat -> list nat.
+      Parameter sumlist : list nat -> nat.
+      Axiom eq_map :
+        forall F1 F2 : nat -> nat,
+        (forall n : nat, F1 n = F2 n) ->
+        forall l : list nat, map F1 l = map F2 l.
+
+   .. coqtop:: all
+
+      Lemma example_map l : sumlist (map (fun m => m - m) l) = 0.
+
+   In this context, one cannot directly use ``eq_map``:
+
+   .. coqtop:: all fail
+
+      rewrite eq_map.
+
+   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 rewrite step one has to
+   provide the term by hand as follows:
+
+   .. coqtop:: all abort
+
+      rewrite (@eq_map _ (fun _ : nat => 0)).
+        by move=> m; rewrite subnn.
+
+   The :tacn:`under` tactic lets one perform the same operation in a more
+   convenient way:
+
+   .. coqtop:: all abort
+
+      Lemma example_map l : sumlist (map (fun m => m - m) l) = 0.
+      under eq_map => m do rewrite subnn.
+
+
+The under tactic
+````````````````
+
+The convenience :tacn:`under` tactic supports the following syntax:
+
+.. tacn:: under {? @r_prefix } @term {? => {+ @i_item}} {? do ( @tactic | [ {*| @tactic } ] ) }
+   :name: under
+
+   Operate under the context proved to be extensional by
+   lemma :token:`term`.
+
+   .. exn:: Incorrect number of tactics (expected N tactics, was given M).
+
+      This error can occur when using the version with a ``do`` clause.
+
+   The multiplier part of :token:`r_prefix` is not supported.
+
+We distinguish two modes,
+:ref:`interactive mode <under_interactive>` without a ``do`` clause, and
+:ref:`one-liner mode <under_one_liner>` with a ``do`` clause,
+which are explained in more detail below.
+
+.. _under_interactive:
+
+Interactive mode
+````````````````
+
+Let us redo the running example in interactive mode.
+
+.. example::
+
+   .. coqtop:: all abort
+
+      Lemma example_map l : sumlist (map (fun m => m - m) l) = 0.
+      under eq_map => m.
+        rewrite subnn.
+        over.
+
+The execution of the Ltac expression:
+
+:n:`under @term => [ @i_item__1 | … | @i_item__n ].`
+
+involves the following steps:
+
+1. It performs a :n:`rewrite @term`
+   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. If so :tacn:`under` puts these n goals in head normal form (using
+   the defective form of the tactic :tacn:`move`), then 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).
+
+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.
+
+7. Interactive editing of the first n goals has to be signalled by
+   using the :tacn:`over` tactic or rewrite rule (see below).
+
+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
+   the intro pattern for the first branch.
+
+.. _over_ssr:
+
+The over tactic
++++++++++++++++
+
+Two equivalent facilities (a terminator and a lemma) are provided to
+close intermediate subgoals generated by :tacn:`under` (i.e. goals
+displayed as ``Under[ … ]``):
+
+.. tacn:: over
+   :name: over
+
+   This terminator tactic allows one to close goals of the form
+   ``'Under[ … ]``.
+
+.. tacv:: by rewrite over
+
+   This is a variant of :tacn:`over` in order to close ``Under[ … ]``
+   goals, relying on the ``over`` rewrite rule.
+
+.. _under_one_liner:
+
+One-liner mode
+``````````````
+
+The Ltac expression:
+
+:n:`under @term => [ @i_item__1 | … | @i_item__n ] do [ @tac__1 | … | @tac__n ].`
+
+can be seen as a shorter form for the following expression:
+
+:n:`(under @term) => [ @i_item__1 | … | @i_item__n | ]; [ @tac__1; over | … | @tac__n; over | cbv beta iota ].`
+
+Notes:
+
++ The ``beta-iota`` reduction here is useful to get rid of the beta
+  redexes that could be introduced after the substitution of the evars
+  by the :tacn:`under` tactic.
+
++ Note that the provided tactics can as well
+  involve other :tacn:`under` tactics. See below for a typical example
+  involving the `bigop` theory from the Mathematical Components library.
+
++ If there is only one tactic, the brackets can be omitted, e.g.:
+  :n:`under @term => i do @tac.` and that shorter form should be
+  preferred.
+
++ If the ``do`` clause is provided and the intro pattern is omitted,
+  then the default :token:`i_item` ``*`` is applied to each branch.
+  E.g., the Ltac expression:
+  :n:`under @term do [ @tac__1 | … | @tac__n ]` is equivalent to:
+  :n:`under @term => [ * | … | * ] do [ @tac__1 | … | @tac__n ]`
+  (and it can be noted here that the :tacn:`under` tactic performs a
+  ``move.`` before processing the intro patterns ``=> [ * | … | * ]``).
+
+.. example::
+
+   .. coqtop:: reset none
+
+      From Coq Require Import ssreflect.
+      Set Implicit Arguments.
+      Unset Strict Implicit.
+      Unset Printing Implicit Defensive.
+
+      Coercion is_true : bool >-> Sortclass.
+
+      Reserved Notation "\big [ op / idx ]_ ( m <= i < n | P ) F"
+        (at level 36, F at level 36, op, idx at level 10, m, i, n at level 50,
+                 format "'[' \big [ op / idx ]_ ( m  <=  i  <  n  |  P )  F ']'").
+      Variant bigbody (R I : Type) : Type :=
+        BigBody : forall (_ : I) (_ : forall (_ : R) (_ : R), R) (_ : bool) (_ : R), bigbody R I.
+
+      Parameter bigop :
+        forall (R I : Type) (_ : R) (_ : list I) (_ : forall _ : I, bigbody R I), R.
+
+      Axiom eq_bigr_ :
+        forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type)
+               (r : list I) (P : I -> bool) (F1 F2 : I -> R),
+          (forall x : I, is_true (P x) -> F1 x = F2 x) ->
+          bigop idx r (fun i : I => BigBody i op (P i) (F1 i)) =
+          bigop idx r (fun i : I => BigBody i op (P i) (F2 i)).
+
+      Axiom eq_big_ :
+        forall (R : Type) (idx : R) (op : R -> R -> R) (I : Type) (r : list I)
+               (P1 P2 : I -> bool) (F1 F2 : I -> R),
+          (forall x : I, P1 x = P2 x) ->
+          (forall i : I, is_true (P1 i) -> F1 i = F2 i) ->
+          bigop idx r (fun i : I => BigBody i op (P1 i) (F1 i)) =
+          bigop idx r (fun i : I => BigBody i op (P2 i) (F2 i)).
+
+      Reserved Notation "\sum_ ( m <= i < n | P ) F"
+        (at level 41, F at level 41, i, m, n at level 50,
+                 format "'[' \sum_ ( m  <=  i  <  n  |  P ) '/  '  F ']'").
+
+      Parameter index_iota : nat -> nat -> list nat.
+
+      Notation "\big [ op / idx ]_ ( m <= i < n | P ) F" :=
+        (bigop idx (index_iota m n) (fun i : nat => BigBody i op P%bool F)).
+
+      Notation "\sum_ ( m <= i < n | P ) F" :=
+        (\big[plus/O]_(m <= i < n | P%bool) F%nat).
+
+      Notation eq_bigr := (fun n m => eq_bigr_ 0 plus (index_iota n m)).
+      Notation eq_big := (fun n m => eq_big_ 0 plus (index_iota n m)).
+
+      Parameter odd : nat -> bool.
+      Parameter prime : nat -> bool.
+
+   .. coqtop:: in
+
+      Parameter addnC : forall m n : nat, m + n = n + m.
+      Parameter muln1 : forall n : nat, n * 1 = n.
+
+   .. coqtop:: all
+
+      Check eq_bigr.
+      Check eq_big.
+
+      Lemma test_big_nested (m n : nat) :
+        \sum_(0 <= a < m | prime a) \sum_(0 <= j < n | odd (j * 1)) (a + j) =
+        \sum_(0 <= i < m | prime i) \sum_(0 <= j < n | odd j) (j + i).
+      under eq_bigr => i prime_i do
+        under eq_big => [ j | j odd_j ] do
+          [ rewrite (muln1 j) | rewrite (addnC i j) ].
+
+   Remark how the final goal uses the name ``i`` (the name given in the
+   intro pattern) rather than ``a`` in the binder of the first summation.
 
 .. _locking_ssr:
 
@@ -5373,7 +5638,15 @@ respectively.
 
 .. tacn:: rewrite {+ @r_step }
 
-   rewrite  (see :ref:`rewriting_ssr`)
+   rewrite (see :ref:`rewriting_ssr`)
+
+.. tacn:: under {? @r_prefix } @term {? => {+ @i_item}} {? do ( @tactic | [ {*| @tactic } ] )}
+
+   under (see :ref:`under_ssr`)
+
+.. tacn:: over
+
+   over (see :ref:`over_ssr`)
 
 .. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } {? : @term } := @term
           have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } : @term {? by @tactic }
diff --git a/ide/coq-ssreflect.lang b/ide/coq-ssreflect.lang
index bd9cb4bfa2..fc7bc64a68 100644
--- a/ide/coq-ssreflect.lang
+++ b/ide/coq-ssreflect.lang
@@ -73,11 +73,13 @@
       <keyword>suffices</keyword>
       <keyword>suff</keyword>
       <keyword>transitivity</keyword>
+      <keyword>under</keyword>
       <keyword>without loss</keyword>
       <keyword>wlog</keyword>
     </context>
     <context id="ssr-endtac" style-ref="endtactic">
       <keyword>by</keyword>
+      <keyword>over</keyword>
       <keyword>exact</keyword>
       <keyword>reflexivity</keyword>
     </context>
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 2a84469af0..a05b1e3d81 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -828,10 +828,12 @@ let view_error s gv =
 open Locus
 (****************************** tactics ***********************************)
 
-let rewritetac dir c =
+let rewritetac ?(under=false) dir c =
   (* Due to the new optional arg ?tac, application shouldn't be too partial *)
+  let open Proofview.Notations in
   Proofview.V82.of_tactic begin
-    Equality.general_rewrite (dir = L2R) AllOccurrences true false c
+      Equality.general_rewrite (dir = L2R) AllOccurrences true false c <*>
+        if under then Proofview.cycle 1 else Proofview.tclUNIT ()
   end
 
 (**********************`:********* hooks ************************************)
@@ -973,7 +975,7 @@ let dependent_apply_error =
  *
  * Refiner.refiner that does not handle metas with a non ground type but works
  * with dependently typed higher order metas. *)
-let applyn ~with_evars ?beta ?(with_shelve=false) n t gl =
+let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t gl =
   if with_evars then
     let refine gl =
       let t, ty, args, gl = pf_saturate ?beta ~bi_types:true gl t n in
@@ -985,8 +987,11 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl =
       pf_partial_solution gl t gs
     in
     Proofview.(V82.of_tactic
-      (tclTHEN (V82.tactic refine)
-        (if with_shelve then shelve_unifiable else tclUNIT ()))) gl
+      (Tacticals.New.tclTHENLIST [
+        V82.tactic refine;
+        (if with_shelve then shelve_unifiable else tclUNIT ());
+        (if first_goes_last then cycle 1 else tclUNIT ())
+        ])) gl
   else
     let t, gl = if n = 0 then t, gl else
       let sigma, si = project gl, sig_it gl in
@@ -1001,21 +1006,17 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl =
           | _ -> assert false
       in loop sigma t [] n in
     pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t));
-    Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t) gl
+    Proofview.(V82.of_tactic
+      (Tacticals.New.tclTHENLIST [
+         V82.tactic (Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t));
+         (if first_goes_last then cycle 1 else tclUNIT ())
+      ])) gl
 
 let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
-  let rec mkRels = function 1 -> [] | n -> mkRel n :: mkRels (n-1) in
   let uct = Evd.evar_universe_context (fst oc) in
-  let n, oc = pf_abs_evars_pirrel gl (fst oc, EConstr.Unsafe.to_constr (snd oc)) in
+  let n, oc = pf_abs_evars_pirrel gl (fst oc, EConstr.to_constr ~abort_on_undefined_evars:false (fst oc) (snd oc)) in
   let gl = pf_unsafe_merge_uc uct gl in
-  let oc = if not first_goes_last || n <= 1 then oc else
-    let l, c = decompose_lam oc in
-    if not (List.for_all_i (fun i (_,t) -> Vars.closedn ~-i t) (1-n) l) then oc else
-    compose_lam (let xs,y = List.chop (n-1) l in y @ xs) 
-      (mkApp (compose_lam l c, Array.of_list (mkRel 1 :: mkRels n)))
-  in
-  pp(lazy(str"after: " ++ Printer.pr_constr_env (pf_env gl) (project gl) oc));
-  try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl
+  try applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc) gl
   with e when CErrors.noncritical e -> raise dependent_apply_error
 
 (* We wipe out all the keywords generated by the grammar rules we defined. *)
@@ -1540,5 +1541,10 @@ let get g =
 
 end
 
+let is_construct_ref sigma c r =
+  EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r
+let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r
+let is_const_ref sigma c r =
+  EConstr.isConst sigma c && GlobRef.equal (ConstRef (fst(EConstr.destConst sigma c))) r
 
 (* vim: set filetype=ocaml foldmethod=marker: *)
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 9662daa7c7..58ce84ecb3 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -312,6 +312,7 @@ val applyn :
            with_evars:bool ->
            ?beta:bool ->
            ?with_shelve:bool ->
+           ?first_goes_last:bool ->
            int ->
            EConstr.t -> v82tac
 exception NotEnoughProducts
@@ -348,7 +349,7 @@ val resolve_typeclasses :
 
 (*********************** Wrapped Coq  tactics *****************************)
 
-val rewritetac : ssrdir -> EConstr.t -> tactic
+val rewritetac : ?under:bool -> ssrdir -> EConstr.t -> tactic
 
 type name_hint = (int * EConstr.types array) option ref
 
@@ -482,3 +483,7 @@ module MakeState(S : StateType) : sig
   val get : Proofview.Goal.t -> S.state
 
 end
+
+val is_ind_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
+val is_construct_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
+val is_const_ref : Evd.evar_map -> EConstr.t -> Names.GlobRef.t -> bool
diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v
index 4721e19a8b..6c74ac1960 100644
--- a/plugins/ssr/ssreflect.v
+++ b/plugins/ssr/ssreflect.v
@@ -500,3 +500,100 @@ Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2.
 Lemma abstract_context T (P : T -> Type) x :
   (forall Q, Q = P -> Q x) -> P 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).
+
+Ltac over :=
+  by [ apply: Under_eq.under_eq_done
+     | apply: Under_iff.under_iff_done
+     | rewrite over
+     ].
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 4433f2fce7..ad20113320 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -19,7 +19,6 @@ open Context
 open Vars
 open Locus
 open Printer
-open Globnames
 open Termops
 open Tacinterp
 
@@ -327,15 +326,15 @@ let rule_id = mk_internal_id "rewrite rule"
 
 exception PRtype_error of (Environ.env * Evd.evar_map * Pretype_errors.pretype_error) option
 
-let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
+let id_map_redex _ sigma ~before:_ ~after = sigma, after
+
+let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
 (*   ppdebug(lazy(str"sigma@pirrel_rewrite=" ++ pr_evar_map None sigma)); *)
   let env = pf_env gl in
   let beta = Reductionops.clos_norm_flags CClosure.beta env sigma in
-  let sigma, p = 
-    let sigma = Evd.create_evar_defs sigma in
-    let (sigma, ev) = Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in
-    (sigma, ev)
-  in
+  let sigma, new_rdx = map_redex env sigma ~before:rdx ~after:new_rdx in
+  let sigma, p = (* The resulting goal *)
+    Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in
   let pred = EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdx_ty pred in
   let elim, gl = 
     let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in
@@ -355,9 +354,10 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
     | Pretype_errors.PretypeError (env, sigma, te) -> raise (PRtype_error (Some (env, sigma, te)))
     | e when CErrors.noncritical e -> raise (PRtype_error None)
   in
-  ppdebug(lazy Pp.(str"pirrel_rewrite proof term of type: " ++ pr_econstr_env env sigma proof_ty));
+  ppdebug(lazy Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof));
+  ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty));
   try refine_with 
-    ~first_goes_last:(not !ssroldreworder) ~with_evars:false (sigma, proof) gl
+    ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof) gl
   with _ -> 
     (* we generate a msg like: "Unable to find an instance for the variable" *)
     let hd_ty, miss = match EConstr.kind sigma c with
@@ -381,11 +381,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
       (Pp.fnl()++str"Rule's type:" ++ spc() ++ pr_econstr_env env sigma hd_ty))
 ;;
 
-let is_construct_ref sigma c r =
-  EConstr.isConstruct sigma c && GlobRef.equal (ConstructRef (fst(EConstr.destConstruct sigma c))) r
-let is_ind_ref sigma c r = EConstr.isInd sigma c && GlobRef.equal (IndRef (fst(EConstr.destInd sigma c))) r
-
-let rwcltac cl rdx dir sr gl =
+let rwcltac ?under ?map_redex cl rdx dir sr gl =
   let sr =
     let sigma, r = sr in
     let sigma = resolve_typeclasses ~where:r ~fail:false (pf_env gl) sigma in
@@ -403,14 +399,14 @@ let rwcltac cl rdx dir sr gl =
       let sigma, c_ty = Typing.type_of env sigma c in
         ppdebug(lazy Pp.(str"c_ty@rwcltac=" ++ pr_econstr_env env sigma c_ty));
       match EConstr.kind_of_type sigma (Reductionops.whd_all env sigma c_ty) with
-      | AtomicType(e, a) when is_ind_ref sigma e c_eq ->
+      | AtomicType(e, a) when Ssrcommon.is_ind_ref sigma e c_eq ->
           let new_rdx = if dir = L2R then a.(2) else a.(1) in
-          pirrel_rewrite cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl
+          pirrel_rewrite ?under ?map_redex cl rdx rdxt new_rdx dir (sigma,c) c_ty, tclIDTAC, gl
       | _ -> 
           let cl' = EConstr.mkApp (EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdxt cl, [|rdx|]) in
           let sigma, _ = Typing.type_of env sigma cl' in
           let gl = pf_merge_uc_of sigma gl in
-          Proofview.V82.of_tactic (convert_concl cl'), rewritetac dir r', gl
+          Proofview.V82.of_tactic (convert_concl cl'), rewritetac ?under dir r', gl
     else
       let dc, r2 = EConstr.decompose_lam_n_assum (project gl) n r' in
       let r3, _, r3t  = 
@@ -421,7 +417,7 @@ let rwcltac cl rdx dir sr gl =
       let cl'' = EConstr.mkNamedProd (make_annot pattern_id Sorts.Relevant) rdxt cl' in
       let itacs = [introid pattern_id; introid rule_id] in
       let cltac = Proofview.V82.of_tactic (Tactics.clear [pattern_id; rule_id]) in
-      let rwtacs = [rewritetac dir (EConstr.mkVar rule_id); cltac] in
+      let rwtacs = [rewritetac ?under dir (EConstr.mkVar rule_id); cltac] in
       apply_type cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], tclTHENLIST (itacs @ rwtacs), gl
   in
   let cvtac' _ =
@@ -439,7 +435,6 @@ let rwcltac cl rdx dir sr gl =
   in
   tclTHEN cvtac' rwtac gl
 
-
 [@@@ocaml.warning "-3"]
 let lz_coq_prod =
   let prod = lazy (Coqlib.build_prod ()) in fun () -> Lazy.force prod
@@ -547,7 +542,7 @@ let rwprocess_rule dir rule gl =
   in
     r_sigma, rules
 
-let rwrxtac occ rdx_pat dir rule gl =
+let rwrxtac ?under ?map_redex occ rdx_pat dir rule gl =
   let env = pf_env gl in
   let r_sigma, rules = rwprocess_rule dir rule gl in
   let find_rule rdx =
@@ -585,7 +580,7 @@ let rwrxtac occ rdx_pat dir rule gl =
   let concl = eval_pattern env0 sigma0 concl0 rdx_pat occ find_R in
   let (d, r), rdx = conclude concl in
   let r = Evd.merge_universe_context (pi1 r) (pi2 r), EConstr.of_constr (pi3 r) in
-  rwcltac (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl
+  rwcltac ?under ?map_redex (EConstr.of_constr concl) (EConstr.of_constr rdx) d r gl
 ;;
 
 let ssrinstancesofrule ist dir arg gl =
@@ -614,7 +609,7 @@ let ssrinstancesofrule ist dir arg gl =
 
 let ipat_rewrite occ dir c gl = rwrxtac occ None dir (project gl, c) gl
 
-let rwargtac ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl =
+let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl =
   let fail = ref false in
   let interp_rpattern gl gc =
     try interp_rpattern gl gc
@@ -628,7 +623,7 @@ let rwargtac ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl =
     (match kind with
     | RWred sim -> simplintac occ rx sim
     | RWdef -> if dir = R2L then foldtac occ rx t else unfoldintac occ rx t gt
-    | RWeq -> rwrxtac occ rx dir t) gl in
+    | RWeq -> rwrxtac ?under ?map_redex occ rx dir t) gl in
   let ctac = old_cleartac (interp_clr (project gl) (oclr, (fst gt, snd (interp gt gl)))) in
   if !fail then ctac gl else tclTHEN (tclMULT mult rwtac) ctac gl
 
@@ -638,8 +633,8 @@ let rwargtac ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl =
 
 (** The "rewrite" tactic *)
 
-let ssrrewritetac ist rwargs =
-  tclTHENLIST (List.map (rwargtac ist) rwargs)
+let ssrrewritetac ?under ?map_redex ist rwargs =
+  tclTHENLIST (List.map (rwargtac ?under ?map_redex ist) rwargs)
 
 (** The "unlock" tactic *)
 
@@ -660,4 +655,3 @@ let unlocktac ist args gl =
     (fun gl -> unfoldtac None None (project gl,locked) xInParens gl); 
     Proofview.V82.of_tactic (Ssrelim.casetac key (fun ?seed:_ k -> k)) ] in
   tclTHENLIST (List.map utac args @ ktacs) gl
-
diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli
index bbcd6b900a..601968d511 100644
--- a/plugins/ssr/ssrequality.mli
+++ b/plugins/ssr/ssrequality.mli
@@ -48,13 +48,15 @@ val ssrinstancesofrule :
   Ssrast.ssrterm ->
   Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
 
+(* map_redex (by default the identity on after) is called on the
+ * redex (before) and its replacement (after). It is used to
+ * "rename" binders by the under tactic *)
 val ssrrewritetac :
+  ?under:bool ->
+  ?map_redex:(Environ.env -> Evd.evar_map ->
+                 before:EConstr.t -> after:EConstr.t -> Evd.evar_map * EConstr.t) ->
   Ltac_plugin.Tacinterp.interp_sign ->
-  ((Ssrast.ssrdir * (int * Ssrast.ssrmmod)) *
-     (((Ssrast.ssrhyps option * Ssrmatching.occ) *
-         Ssrmatching.rpattern option) *
-        (ssrwkind * Ssrast.ssrterm)))
-           list -> Tacmach.tactic
+   ssrrwarg list -> Tacmach.tactic
 
 val ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> Tacmach.tactic
 
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 3cadc92bcc..01d71aa96a 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -319,3 +319,172 @@ let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
     let _,ty,_,uc = pf_interp_ty ist gl c in let gl = pf_merge_uc uc gl in
     basecuttac "ssr_suff" ty gl in
   Tacticals.tclTHENS ctac [htac; Tacticals.tclTHEN (old_cleartac clr) (introstac (binders@simpl))]
+
+open Proofview.Notations
+
+let is_app_evar sigma t =
+  match EConstr.kind sigma t with
+  | Constr.Evar _ -> true
+  | Constr.App(t,_) ->
+      begin match EConstr.kind sigma t with
+      | Constr.Evar _ -> true
+      | _ -> false end
+  | _ -> false
+
+let rec ncons n e = match n with
+  | 0 -> []
+  | n when n > 0 -> e :: ncons (n - 1) e
+  | _ -> failwith "ncons"
+
+let intro_lock ipats =
+  let hnf' = Proofview.numgoals >>= fun ng ->
+             Proofview.tclDISPATCH
+               (ncons (ng - 1) ssrsmovetac @ [Proofview.tclUNIT ()]) in
+  let rec lock_eq () : unit Proofview.tactic = Proofview.Goal.enter begin fun _ ->
+    Proofview.tclORELSE
+      (Ssripats.tclIPAT [Ssripats.IOpTemporay; Ssripats.IOpEqGen (lock_eq ())])
+      (fun _exn -> Proofview.Goal.enter begin fun gl ->
+        let c = Proofview.Goal.concl gl in
+        let sigma = Proofview.Goal.sigma gl in
+        let env = Proofview.Goal.env gl in
+        match EConstr.kind_of_type sigma c with
+        | Term.AtomicType(hd, args) when
+            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|]))
+        | _ ->
+        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|]))
+        | _ ->
+    ppdebug(lazy Pp.(str"under: stop:" ++ pr_econstr_env env sigma t));
+
+            Proofview.tclUNIT ()
+       end)
+    end
+  in
+  hnf' <*> Ssripats.tclIPATssr ipats <*> lock_eq ()
+
+let pretty_rename evar_map term varnames =
+  let rec aux term vars =
+    try
+      match vars with
+      | [] -> term
+      | Names.Name.Anonymous :: varnames ->
+          let name, types, body = EConstr.destLambda evar_map term in
+          let res = aux body varnames in
+          EConstr.mkLambda (name, types, res)
+      | Names.Name.Name _ as name :: varnames ->
+          let { Context.binder_relevance = r }, types, body =
+            EConstr.destLambda evar_map term in
+          let res = aux body varnames in
+          EConstr.mkLambda (Context.make_annot name r, types, res)
+    with DestKO -> term
+  in
+    aux term varnames
+
+let overtac = Proofview.V82.tactic (ssr_n_tac "over" ~-1)
+
+let check_numgoals ?(minus = 0) nh =
+  Proofview.numgoals >>= fun ng ->
+  if nh <> ng then
+    let errmsg =
+      str"Incorrect number of tactics" ++ spc() ++
+        str"(expected "++int (ng - minus)++str(String.plural ng " tactic") ++
+        str", was given "++ int (nh - minus)++str")."
+    in
+    CErrors.user_err errmsg
+  else
+    Proofview.tclUNIT ()
+
+let undertac ?(pad_intro = false) ist ipats ((dir,_),_ as rule) hint =
+
+  (* total number of implied hints *)
+  let nh = List.length (snd hint) + (if hint = nullhint then 2 else 1) in
+
+  let varnames =
+    let rec aux acc = function
+      | IPatId id :: rest -> aux (Names.Name.Name id :: acc) rest
+      | IPatClear _ :: rest -> aux acc rest
+      | IPatSimpl _ :: rest -> aux acc rest
+      | IPatAnon (One _ | Drop) :: rest ->
+          aux (Names.Name.Anonymous :: acc) rest
+      | _ -> List.rev acc in
+    aux [] @@ match ipats with
+              | None -> []
+              | Some (IPatCase(Regular (l :: _)) :: _) -> l
+              | Some l -> l in
+
+  (* If we find a "=> [|]" we add 1 | to get "=> [||]" for the extra
+   * goal (the one that is left once we run over) *)
+  let ipats =
+    match ipats with
+    | None -> [IPatNoop]
+    | Some l when pad_intro -> (* typically, ipats = Some [IPatAnon All] *)
+       let new_l = ncons (nh - 1) l in
+       [IPatCase(Regular (new_l @ [[]]))]
+    | Some (IPatCase(Regular []) :: _ as ipats) -> ipats
+    (* Erik: is the previous line correct/useful? *)
+    | Some (IPatCase(Regular l) :: rest) -> IPatCase(Regular(l @ [[]])) :: rest
+    | Some (IPatCase(Block _) :: _ as l) -> l
+    | Some l -> [IPatCase(Regular [l;[]])] in
+
+  let map_redex env evar_map ~before:_ ~after:t =
+    ppdebug(lazy Pp.(str"under vars: " ++ prlist Names.Name.print varnames));
+
+    let evar_map, ty = Typing.type_of env evar_map t in
+    let new_t = (* pretty-rename the bound variables *)
+      try begin match EConstr.destApp evar_map t with (f, ar) ->
+            let lam = Array.last ar in
+            ppdebug(lazy Pp.(str"under: mapping:" ++
+                             pr_econstr_env env evar_map lam));
+            let new_lam = pretty_rename evar_map lam varnames in
+            let new_ar, len1 = Array.copy ar, pred (Array.length ar) in
+            new_ar.(len1) <- new_lam;
+            EConstr.mkApp (f, new_ar)
+          end with
+      | DestKO ->
+        ppdebug(lazy Pp.(str"under: cannot pretty-rename bound variables with destApp"));
+        t
+    in
+    ppdebug(lazy Pp.(str"under: to:" ++ pr_econstr_env env evar_map new_t));
+    evar_map, new_t
+  in
+  let undertacs =
+    if hint = nohint then
+      Proofview.tclUNIT ()
+    else
+      let betaiota = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in
+      (* Usefulness of check_numgoals: tclDISPATCH would be enough,
+         except for the error message w.r.t. the number of
+         provided/expected tactics, as the last one is implied *)
+      check_numgoals ~minus:1 nh <*>
+        Proofview.tclDISPATCH
+          ((List.map (function None -> overtac
+                             | Some e -> ssrevaltac ist e <*>
+                                           overtac)
+              (if hint = nullhint then [None] else snd hint))
+           @ [betaiota])
+  in
+  let rew =
+    Proofview.V82.tactic
+      (Ssrequality.ssrrewritetac ~under:true ~map_redex ist [rule])
+  in
+  rew <*> intro_lock ipats <*> undertacs
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index 35e89dbcea..6dd01ca6fc 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -57,3 +57,16 @@ val sufftac :
        (bool * Tacinterp.Value.t option list)) ->
   Tacmach.tactic
 
+(* pad_intro (by default false) indicates whether the intro-pattern
+   "=> i..." must be turned into "=> [i...|i...|i...|]" (n+1 branches,
+   assuming there are n provided tactics in the ssrhint argument
+   "do [...|...|...]"; it is useful when the intro-pattern is "=> *").
+   Otherwise, "=> i..." is turned into "=> [i...|]". *)
+val undertac :
+  ?pad_intro:bool ->
+  Ltac_plugin.Tacinterp.interp_sign ->
+  Ssrast.ssripats option -> Ssrequality.ssrrwarg ->
+  Ltac_plugin.Tacinterp.Value.t Ssrast.ssrhint -> unit Proofview.tactic
+
+val overtac :
+  unit Proofview.tactic
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index f44962f213..27a558611e 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -86,6 +86,15 @@ GRAMMAR EXTEND Gram
   ssrtacarg: [[ tac = tactic_expr LEVEL "5" -> { tac } ]];
 END
 
+(* Copy of ssrtacarg with LEVEL "3", useful for: "under ... do ..." *)
+ARGUMENT EXTEND ssrtac3arg TYPED AS tactic PRINTED BY { pr_ssrtacarg env sigma }
+| [ "YouShouldNotTypeThis" ] -> { CErrors.anomaly (Pp.str "Grammar placeholder match") }
+END
+GRAMMAR EXTEND Gram
+  GLOBAL: ssrtac3arg;
+  ssrtac3arg: [[ tac = tactic_expr LEVEL "3" -> { tac } ]];
+END
+
 {
 
 (* Lexically closed tactic for tacticals. *)
@@ -741,15 +750,33 @@ let pushIPatNoop = function
   | pats :: orpat -> (IPatNoop :: pats) :: orpat
   | [] -> []
 
+let test_ident_no_do strm =
+  match Util.stream_nth 0 strm with
+  | Tok.IDENT s when s <> "do" -> ()
+  | _ -> raise Stream.Failure
+
+let test_ident_no_do =
+  Pcoq.Entry.of_parser "test_ident_no_do" test_ident_no_do
+
 }
 
+ARGUMENT EXTEND ident_no_do PRINTED BY { fun _ _ _ -> Names.Id.print }
+| [ "YouShouldNotTypeThis" ident(id) ] -> { id }
+END
+
+
+GRAMMAR EXTEND Gram
+  GLOBAL: ident_no_do;
+  ident_no_do: [ [ test_ident_no_do; id = IDENT -> { Id.of_string id } ] ];
+END
+
 ARGUMENT EXTEND ssripat TYPED AS ssripatrep list PRINTED BY { pr_ssripats }
   INTERPRETED BY { interp_ipats }
   GLOBALIZED BY { intern_ipats }
   | [ "_" ] -> { [IPatAnon Drop] }
   | [ "*" ] -> { [IPatAnon All] }
   | [ ">" ] -> { [IPatFastNondep] }
-  | [ ident(id) ] -> { [IPatId id] }
+  | [ ident_no_do(id) ] -> { [IPatId id] }
   | [ "?" ] -> { [IPatAnon (One None)] }
   | [ "+" ] -> { [IPatAnon Temporary] }
   | [ "++" ] -> { [IPatAnon Temporary; IPatAnon Temporary] }
@@ -1047,6 +1074,13 @@ ARGUMENT EXTEND ssrhintarg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintar
 | [ ssrtacarg(arg) ] -> { mk_hint arg }
 END
 
+(* Copy of ssrhintarg with LEVEL "3", useful for: "under ... do ..." *)
+ARGUMENT EXTEND ssrhint3arg TYPED AS (bool * ssrortacs) PRINTED BY { pr_ssrhintarg env sigma }
+| [ "[" "]" ] -> { nullhint }
+| [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs }
+| [ ssrtac3arg(arg) ] -> { mk_hint arg }
+END
+
 ARGUMENT EXTEND ssrortacarg TYPED AS ssrhintarg PRINTED BY { pr_ssrhintarg env sigma }
 | [ "[" ssrortacs(tacs) "]" ] -> { mk_orhint tacs }
 END
@@ -2652,6 +2686,34 @@ END
 
 {
 
+let check_under_arg ((_dir,mult),((_occ,_rpattern),_rule)) =
+  if mult <> nomult then
+    CErrors.user_err Pp.(str"under does not support multipliers")
+
+}
+
+
+TACTIC EXTEND under
+  | [ "under" ssrrwarg(arg) ] -> {
+    check_under_arg arg;
+    Ssrfwd.undertac ist None arg nohint
+    }
+  | [ "under" ssrrwarg(arg) ssrintros_ne(ipats) ] -> {
+    check_under_arg arg;
+    Ssrfwd.undertac ist (Some ipats) arg nohint
+    }
+  | [ "under" ssrrwarg(arg) ssrintros_ne(ipats) "do" ssrhint3arg(h) ] -> {
+    check_under_arg arg;
+    Ssrfwd.undertac ist (Some ipats) arg h
+    }
+  | [ "under" ssrrwarg(arg) "do" ssrhint3arg(h) ] -> { (* implicit "=> [*|*]" *)
+    check_under_arg arg;
+    Ssrfwd.undertac ~pad_intro:true ist (Some [IPatAnon All]) arg h
+    }
+END
+
+{
+
 (* We wipe out all the keywords generated by the grammar rules we defined. *)
 (* The user is supposed to Require Import ssreflect or Require ssreflect   *)
 (* and Import ssreflect.SsrSyntax to obtain these keywords and as a         *)
diff --git a/test-suite/output/ssr_under.out b/test-suite/output/ssr_under.out
new file mode 100644
index 0000000000..499d25391e
--- /dev/null
+++ b/test-suite/output/ssr_under.out
@@ -0,0 +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
new file mode 100644
index 0000000000..fb7503d902
--- /dev/null
+++ b/test-suite/output/ssr_under.v
@@ -0,0 +1,30 @@
+From Coq Require Import ssreflect.
+
+Axiom subnn : forall n : nat, n - n = 0.
+Parameter G : (nat -> nat) -> nat -> nat.
+Axiom eq_G :
+  forall F1 F2 : nat -> nat,
+    (forall n : nat, F1 n = F2 n) ->
+    forall n : nat, G F1 n = G F2 n.
+
+Ltac show := match goal with [|-?g] => idtac g end.
+
+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/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v
index cb2c56736c..ca360f65a7 100644
--- a/test-suite/prerequisite/ssr_mini_mathcomp.v
+++ b/test-suite/prerequisite/ssr_mini_mathcomp.v
@@ -427,6 +427,8 @@ Lemma leqnSn n : n <= n.+1.             Proof. by elim: n. Qed.
 
 Lemma leq_trans n m p : m <= n -> n <= p -> m <= p.
 Admitted.
+Lemma leq_ltn_trans n m p : m <= n -> n < p -> m < p.
+Admitted.
 Lemma leqW m n : m <= n -> m <= n.+1.
 Admitted.
 Hint Resolve leqnSn.
diff --git a/test-suite/ssr/over.v b/test-suite/ssr/over.v
new file mode 100644
index 0000000000..8232741b0d
--- /dev/null
+++ b/test-suite/ssr/over.v
@@ -0,0 +1,70 @@
+Require Import ssreflect.
+
+Axiom daemon : False. Ltac myadmit := case: daemon.
+
+(** Testing over for the 1-var case *)
+
+Lemma test_over_1_1 : False.
+intros.
+evar (I : Type); evar (R : Type); evar (x2 : I -> R).
+assert (H : forall i : nat, i + 2 * i - i = x2 i).
+  intros i.
+  unfold x2 in *; clear x2;
+  unfold R in *; clear R;
+  unfold I in *; clear I.
+  apply Under_eq_from_eq.
+  Fail done.
+
+  over.
+  myadmit.
+Qed.
+
+Lemma test_over_1_2 : False.
+intros.
+evar (I : Type); evar (R : Type); evar (x2 : I -> R).
+assert (H : forall i : nat, i + 2 * i - i = x2 i).
+  intros i.
+  unfold x2 in *; clear x2;
+  unfold R in *; clear R;
+  unfold I in *; clear I.
+  apply Under_eq_from_eq.
+  Fail done.
+
+  by rewrite over.
+  myadmit.
+Qed.
+
+(** Testing over for the 2-var case *)
+
+Lemma test_over_2_1 : False.
+intros.
+evar (I : Type); evar (J : Type); evar (R : Type); evar (x2 : I -> J -> R).
+assert (H : forall i j, i + 2 * j - i = x2 i j).
+  intros i j.
+  unfold x2 in *; clear x2;
+  unfold R in *; clear R;
+  unfold J in *; clear J;
+  unfold I in *; clear I.
+  apply Under_eq_from_eq.
+  Fail done.
+
+  over.
+  myadmit.
+Qed.
+
+Lemma test_over_2_2 : False.
+intros.
+evar (I : Type); evar (J : Type); evar (R : Type); evar (x2 : I -> J -> R).
+assert (H : forall i j : nat, i + 2 * j - i = x2 i j).
+  intros i j.
+  unfold x2 in *; clear x2;
+  unfold R in *; clear R;
+  unfold J in *; clear J;
+  unfold I in *; clear I.
+  apply Under_eq_from_eq.
+  Fail done.
+
+  rewrite over.
+  done.
+  myadmit.
+Qed.
diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
new file mode 100644
index 0000000000..f285ad138b
--- /dev/null
+++ b/test-suite/ssr/under.v
@@ -0,0 +1,234 @@
+Require Import ssreflect.
+Require Import ssrbool TestSuite.ssr_mini_mathcomp.
+Global Unset SsrOldRewriteGoalsOrder.
+
+(* under <names>: {occs}[patt]<lemma>.
+   under <names>: {occs}[patt]<lemma> by tac1.
+   under <names>: {occs}[patt]<lemma> by [tac1 | ...].
+ *)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Axiom daemon : False. Ltac myadmit := case: daemon.
+
+Module Mocks.
+
+(* Mock bigop.v definitions to test the behavior of under with bigops
+   without requiring mathcomp *)
+
+Definition eqfun :=
+  fun (A B : Type) (f g : forall _ : B, A) => forall x : B, @eq A (f x) (g x).
+
+Section Defix.
+Variables (T : Type) (n : nat) (f : forall _ : T, T) (x : T).
+Fixpoint loop (m : nat) : T :=
+  match m return T with
+  | O => x
+  | S i => f (loop i)
+  end.
+Definition iter := loop n.
+End Defix.
+
+Parameter eq_bigl :
+  forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type)
+         (r : list I) (P1 P2 : pred I) (F : forall _ : I, R) (_ : @eqfun bool I P1 P2),
+    @eq R (@bigop R I idx r (fun i : I => @BigBody R I i op (P1 i) (F i)))
+        (@bigop R I idx r (fun i : I => @BigBody R I i op (P2 i) (F i))).
+
+Parameter eq_big :
+  forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type)
+         (r : list I) (P1 P2 : pred I) (F1 F2 : forall _ : I, R) (_ : @eqfun bool I P1 P2)
+         (_ : forall (i : I) (_ : is_true (P1 i)), @eq R (F1 i) (F2 i)),
+    @eq R (@bigop R I idx r (fun i : I => @BigBody R I i op (P1 i) (F1 i)))
+        (@bigop R I idx r (fun i : I => @BigBody R I i op (P2 i) (F2 i))).
+
+Parameter eq_bigr :
+  forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (I : Type)
+         (r : list I) (P : pred I) (F1 F2 : forall _ : I, R)
+         (_ : forall (i : I) (_ : is_true (P i)), @eq R (F1 i) (F2 i)),
+    @eq R (@bigop R I idx r (fun i : I => @BigBody R I i op (P i) (F1 i)))
+        (@bigop R I idx r (fun i : I => @BigBody R I i op (P i) (F2 i))).
+
+Parameter big_const_nat :
+  forall (R : Type) (idx : R) (op : forall (_ : R) (_ : R), R) (m n : nat) (x : R),
+    @eq R (@bigop R nat idx (index_iota m n) (fun i : nat => @BigBody R nat i op true x))
+        (@iter R (subn n m) (op x) idx).
+
+Delimit Scope N_scope with num.
+Delimit Scope nat_scope with N.
+
+Reserved Notation "\sum_ ( m <= i < n | P ) F"
+  (at level 41, F at level 41, i, m, n at level 50,
+           format "'[' \sum_ ( m  <=  i  <  n  |  P ) '/  '  F ']'").
+Reserved Notation "\sum_ ( m <= i < n ) F"
+  (at level 41, F at level 41, i, m, n at level 50,
+           format "'[' \sum_ ( m  <=  i  <  n ) '/  '  F ']'").
+
+Local Notation "+%N" := addn (at level 0, only parsing).
+
+Notation "\sum_ ( m <= i < n | P ) F" :=
+  (\big[+%N/0%N]_(m <= i < n | P%B) F%N) : (*nat_scope*) big_scope.
+Notation "\sum_ ( m <= i < n ) F" :=
+  (\big[+%N/0%N]_(m <= i < n) F%N) : (*nat_scope*) big_scope.
+
+Parameter iter_addn_0 : forall m n : nat, @eq nat (@iter nat n (addn m) O) (muln m n).
+
+End Mocks.
+
+Import Mocks.
+
+(*****************************************************************************)
+
+Lemma test_big_nested_1 (F G : nat -> nat) (m n : nat) :
+  \sum_(0 <= i < m) \sum_(0 <= j < n | odd (j * 1)) (i + j) =
+  \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i).
+Proof.
+(* in interactive mode *)
+under eq_bigr => i Hi.
+  under eq_big => [j|j Hj].
+  { rewrite muln1. over. }
+  { rewrite addnC. over. }
+  simpl. (* or: cbv beta. *)
+  over.
+by [].
+Qed.
+
+Lemma test_big_nested_2 (F G : nat -> nat) (m n : nat) :
+  \sum_(0 <= i < m) \sum_(0 <= j < n | odd (j * 1)) (i + j) =
+  \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i).
+Proof.
+(* in one-liner mode *)
+under eq_bigr => i Hi do under eq_big => [j|j Hj] do [rewrite muln1 | rewrite addnC ].
+done.
+Qed.
+
+Lemma test_big_2cond_0intro (F : nat -> nat) (m : nat) :
+  \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0.
+Proof.
+(* in interactive mode *)
+under eq_big.
+{ move=> n; rewrite (addnC n 1); over. }
+{ move=> i Hi; rewrite (addnC i 2); over. }
+done.
+Qed.
+
+Lemma test_big_2cond_1intro (F : nat -> nat) (m : nat) :
+  \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0.
+Proof.
+(* in interactive mode *)
+Fail under eq_big => i.
+(* as it amounts to [under eq_big => [i]] *)
+Abort.
+
+Lemma test_big_2cond_all (F : nat -> nat) (m : nat) :
+  \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0.
+Proof.
+(* in interactive mode *)
+Fail under eq_big => *.
+(* as it amounts to [under eq_big => [*]] *)
+Abort.
+
+Lemma test_big_2cond_all_implied (F : nat -> nat) (m : nat) :
+  \sum_(0 <= i < m | odd (i + 1)) (i + 2) >= 0.
+Proof.
+(* in one-liner mode *)
+under eq_big do [rewrite addnC
+                |rewrite addnC].
+(* amounts to [under eq_big => [*|*] do [...|...]] *)
+done.
+Qed.
+
+Lemma test_big_patt1 (F G : nat -> nat) (n : nat) :
+  \sum_(0 <= i < n) (F i + G i) = \sum_(0 <= i < n) (G i + F i) + 0.
+Proof.
+under [in RHS]eq_bigr => i Hi.
+  by rewrite addnC over.
+done.
+Qed.
+
+Lemma test_big_patt2 (F G : nat -> nat) (n : nat) :
+  \sum_(0 <= i < n) (F i + F i) =
+  \sum_(0 <= i < n) 0 + \sum_(0 <= i < n) (F i * 2).
+Proof.
+under [X in _ = _ + X]eq_bigr => i Hi do rewrite mulnS muln1.
+by rewrite big_const_nat iter_addn_0.
+Qed.
+
+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.
+Qed.
+
+(* Solely used, one such renaming is useless in practice, but it works anyway *)
+Lemma test_big_cosmetic (F G : nat -> nat) (m n : nat) :
+  \sum_(0 <= i < m) \sum_(0 <= j < n | odd (j * 1)) (i + j) =
+  \sum_(0 <= i < m) \sum_(0 <= j < n | odd j) (j + i).
+Proof.
+under [RHS]eq_bigr => a A do under eq_bigr => b B do []. (* renaming bound vars *)
+myadmit.
+Qed.
+
+Lemma test_big_andb (F : nat -> nat) (m n : nat) :
+  \sum_(0 <= i < 5 | odd i && (i == 1)) i = 1.
+Proof.
+under eq_bigl => i do [rewrite andb_idl; first by move/eqP->].
+under eq_bigr => i do move/eqP=>{1}->. (* the 2nd occ should not be touched *)
+myadmit.
+Qed.
+
+Lemma test_foo (f1 f2 : nat -> nat) (f_eq : forall n, f1 n = f2 n)
+      (G : (nat -> nat) -> nat)
+      (Lem : forall f1 f2 : nat -> nat,
+          True ->
+          (forall n, f1 n = f2 n) ->
+          False = False ->
+          G f1 = G f2) :
+  G f1 = G f2.
+Proof.
+(*
+under x: Lem.
+- done.
+- rewrite f_eq; over.
+- done.
+ *)
+under Lem => [|x|] do [done|rewrite f_eq|done].
+done.
+Qed.
+
+
+(* Inspired From Coquelicot.Lub. *)
+(* http://coquelicot.saclay.inria.fr/html/Coquelicot.Lub.html#Lub_Rbar_eqset *)
+
+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.
+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.
+by move=> H; split; move=> [x Hx]; exists x; apply H.
+Qed.
+
+Arguments ex_iff [R P1] P2 iffP12.
+
+Require Import Setoid.
+Lemma test_ex_iff (P : nat -> Prop) : (exists x, P x) -> True.
+under ex_iff => n.
+by rewrite over.
+Abort.