The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

There is also a remark on the difference of behavior of algebraic patterns (my personal name for "conjunctive or disjunctive pattern") as terminal patterns or non-terminal in a sequence:

> Remark: intros p1 … pn is not fully equivalent to intros p1;…; intros pn for the following reasons:
> [...]

This remark mentions that you can use
  Set Bracketing Last Introduction Pattern.

to make all algebraic patterns behave as if they were non-terminal (always introduce all parameters):

Coq < Goal (A /\ B) -> C.

 

  ============================
   A /\ B -> C

Unnamed_thm < intros [].
 
  ============================
   A -> B -> C

Unnamed_thm < Restart.
 
  ============================
   A /\ B -> C

Unnamed_thm < Set Bracketing Last Introduction Pattern.

Unnamed_thm < intros [].
 
  H : A
  H0 : B
  ============================
   C

I would instead rather recommend always choosing all the names in the pattern. As Dominique says, you can always explicitly ask for name generation with

  intros [? ?].

but you can also use

  intros [**].

(intros [*] will only introduce the named-variables)

Another behavior of "intros" I found when investigating your question, and which I don't see documented, is that 8.4 will happily overshoot in the rest of the goal if you have more variables in a conjunctive pattern than there are arguments:

Coq < Goal A /\ B -> C -> D.
 
  ============================
   A /\ B -> C -> D

Unnamed_thm < intros [a b c].

  a : A
  b : B
  c : C
  ============================
   D

Under 8.5 I get a failure as I expected:

  ============================
   A /\ B -> C -> D

Unnamed_thm0 < intros [a b c].
Toplevel input, characters 12-13:
> intros [a b c].
>             ^
Error: Unexpected name (at most 2 introduction patterns were expected in the
branch).

On Thu, Apr 21, 2016 at 11:34 AM, Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

On 21/04/2016 17:10, Théo Zimmermann wrote:
> Hello,
>
> For a goal of the form A /\ B -> C, using intros [] yields the goal A ->
> B -> C (and does not add anything to the context). I would have rather
> expected that A and B be added to the context (this can be achieved with
> intros [] **).
>
> Is this a wanted behavior? If yes, is it documented somewhere? (I looked
> but did not find any mention of this pattern in the section of the
> manual devoted to intros intro_pattern_list).

See 8.3.2 of the reference manual:

"if the disjunctive pattern is part of a sequence of patterns, then Coq
completes the pattern so that all the arguments of the constructors of
the inductive type are introduced"

which implicitly means that, if the pattern is not part of a sequence
(or rather it is the last one), the arguments are not introduced unless
recursively asked for.

As far as I am concerned, I am fine with this behavior; I dislike it
when Coq invents names in my stead.

Best regards,

Guillaume