The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

Note that the flag "Set Bracketing Last Introduction Pattern" is on by
default in the development version, so that "algebraic patterns"
behave regularly, independently of whether they are in last position
of a sequence or not.

Of course, it is still possible to give names by hand, so, in my
opinion, this regular behavior is optimal for "algebraic patterns" in
the sense that it allows both a light and convenient mode where one
does not have to care about names and the possibility of a robust
controlled mode where one can give names explicitly.

The situation is of course different for tactics like intuition, or
more generally with programmed tactics. I feel that a generic "as
... by ..." clause could be made available in this situation, the "as"
for naming and the "by" to deal with side conditions.

Best,

Hugo

On Thu, Apr 21, 2016 at 11:44:06AM -0400, Gabriel Scherer wrote:
> 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
> 
>