[ssr] under: Fix the defective form ("=> [*|*]" implied) and its doc

* Add tests accordingly.

5 files changed, 75 insertions, 18 deletions

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index 0df0f937a6..c32788c9da 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -3737,17 +3737,13 @@ involves the following steps:
    bound variables as the identifers provided in the first
    intro pattern branch (here, ``i``).
 
-Notes:
+Note:
 
 + For the steps 3. and 4. above, the :tacn:`under` tactic also
   supports subgoals of the form ``some_expr(i) <-> ?Goal i``, which
   are "protected" in the form ``Under_iff (some_expr i) (?Goal i)``,
   itself pretty-printed as ``'Under_iff[ some_expr i ]``.
 
-+ If the intro pattern is omitted, the Ltac expression:
-  :n:`under {@occ_switch}[@r_pattern]@term.` defaults to:
-  :n:`under {@occ_switch}[@r_pattern]@term => *.`
-
 Two equivalent facilities (a terminator and a lemma) are provided to
 close intermediate subgoal ``Under[ … ]`` and instantiate the
 corresponding evar:
@@ -3790,17 +3786,25 @@ The Ltac expression:
 can be viewed as a shorter form for the following Ltac expression:
 :n:`under {@occ_switch}[@r_pattern]@term => [i|j|]; [tac1; over | tac2; over | cbv beta iota].`
 
-Here, the ``beta-iota`` reduction is useful to get rid of the beta
-redexes that could be introduced after the substitution of the evars
-by the :tacn:`under` tactic.
+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 (e.g., ``tac1``) can just as well
+  involve other :tacn:`under` tactics. See below for a typical example
+  involving the `bigop` theory from the Mathematical Components library.
 
-Note that the provided tactics (e.g., ``tac1``) can just 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 are optional, i.e.:
+  :n:`under @term => [i] do [tac1]` is equivalent to:
+  :n:`under @term => i do tac1.` and that shorter form should be
+  preferred.
 
-If there is only one tactic, the brackets are optional, i.e.:
-:n:`under @term => i do [tac1]` can be
-shortened to: :n:`under @term => i do tac1.`
++ If the ``do`` clause is provided but the intro pattern is omitted,
+  the Ltac expression:
+  :n:`under {@occ_switch}[@r_pattern]@term do [tac1|tac2]` defaults to:
+  :n:`under {@occ_switch}[@r_pattern]@term => [*|*] do [tac1|tac2].`
 
 .. example::
 
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 2bac69b5b7..d60e3857b1 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -406,7 +406,15 @@ let check_numgoals ?(minus = 0) nh =
   else
     Proofview.tclUNIT ()
 
-let undertac ist ipats ((dir,_),_ as rule) hint =
+let rec ncons n e = match n with
+  | 0 -> []
+  | n when n > 0 -> e :: ncons (n - 1) e
+  | _ -> failwith "ncons"
+
+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
@@ -426,7 +434,11 @@ let undertac ist ipats ((dir,_),_ as rule) hint =
   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
@@ -457,7 +469,6 @@ let undertac ist ipats ((dir,_),_ as rule) hint =
       Proofview.tclUNIT ()
     else
       let betaiota = Tactics.reduct_in_concl (Reductionops.nf_betaiota, DEFAULTcast) in
-      let nh = List.length (snd hint) + (if hint = nullhint then 2 else 1) 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 *)
diff --git a/plugins/ssr/ssrfwd.mli b/plugins/ssr/ssrfwd.mli
index 6f7cc6d445..6dd01ca6fc 100644
--- a/plugins/ssr/ssrfwd.mli
+++ b/plugins/ssr/ssrfwd.mli
@@ -57,7 +57,13 @@ 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
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index 2c46947658..4286ace519 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -2690,9 +2690,9 @@ TACTIC EXTEND under
     check_under_arg arg;
     Ssrfwd.undertac ist (Some ipats) arg h
     }
-  | [ "under" ssrrwarg(arg) "do" ssrhintarg(h) ] -> { (* implicit "=> *" *)
+  | [ "under" ssrrwarg(arg) "do" ssrhintarg(h) ] -> { (* implicit "=> [*|*]" *)
     check_under_arg arg;
-    Ssrfwd.undertac ist (Some [IPatAnon All]) arg h
+    Ssrfwd.undertac ~pad_intro:true ist (Some [IPatAnon All]) arg h
     }
 END
 
diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
index 1e3b0f678b..ba3aa9d621 100644
--- a/test-suite/ssr/under.v
+++ b/test-suite/ssr/under.v
@@ -104,6 +104,42 @@ under eq_bigr => i Hi do under eq_big => [j|j Hj] do [rewrite muln1 | rewrite ad
 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 [move=> ? (* due to delta-head-cst *); 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.