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

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

8 files changed, 397 insertions, 49 deletions

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         *)