The Coq mailing list

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

Hi,

> Ltac so H := solve [H].
> 
> Lemma wtf:
>   false = true -> False.
> Proof.
>  intro. so congruence.  (*fails here*)

The reason why this fails with "congruence" while similar examples do
not fail, e.g. with "auto", is that there is a bug in the mechanism
allowing to interpret as a tactic a reference given as argument of an
ltac function.

The general rule is that, if "f" is an Ltac reference, as "so" is
here, its arguments are parsed by default as terms, as shown here:

  Ltac f x := apply x.
  Ltac S x := intro.
  Goal nat.
  f (S 0).

As explained by Arthur Charguéraud, to provide a tactic argument, the
normal syntax is:

  f ltac:(tactic expression)

so that "so ltac:(congruence)" above works (alternatively, use a
"Tactic Notation" as indicated by Arthur).

There is however an special case when the argument of an Ltac function
is a reference. By default, the reference is interpreted as a term, if
ever possible, as in:

  Ltac f x := apply x.
  Ltac S x := intro.
  Goal nat.
  f S.

but if the reference is not interpretable as a term, there is an
attempt to interpret it as an atomic tactic name.

For tactics with predefined parsing rules, like e.g. "intro" or
"auto", this is done once for all in the system.

For tactics added dynamically to the system, as e.g. "congruence",
"firstorder", "eauto", or any tactics added via a plugin using the
ocaml-level "TACTIC EXTEND" construction, this fallback process is
done mechanically, based on the form of the parsing rules of the
tactic.

Unfortunately, the process did not work correctly in some cases and
"congruence", "firstorder", "eauto" were precisely such tactics for
which it failed. This is now fixed in the development version and this
will be available in 8.4.

Hugo Herbelin

On Fri, Mar 16, 2012 at 05:28:18PM +0100, Arthur Charguéraud wrote:
> 
> 
> >Ltac so H := solve [H].
> >
> >Lemma wtf:
> >  false = true -> False.
> >Proof.
> >  intro. so congruence.  (*fails here*)
> >
> >I do not understand why the above fails. Help please :)
> >
> Hi, I think it's a kind of scoping problem. I usually use "tactic notation" 
> to avoid this issue:
> -------
> Tactic Notation "so" tactic(H) := solve [H].
> 
> Lemma wtf:
>   false = true -> False.
> Proof.
>   intro. so congruence.
> -------
> 
> Alternatively, you can you "ltac:()" to locally change the scope:
> -------
> Ltac so H := solve [H].
> 
> Lemma wtf:
>   false = true -> False.
> Proof.
>   intro. so ltac:(congruence).
> -------
> 
> Best,
> Arthur