The Coq mailing list

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

Hi,

> I got a strange error today from trying to do:
> 
> applyFwd f_equal
> 
> in Coq 8.1pl3. (...) Apparently, the strange error
> message was due to f_equal in "applyFwd f_equal" being interpreted as
> meaning the *tactic* called f_equal, not the lemma (f_equal may refer to
> either a tactic or a lemma).
> 
> I would argue that good computer languages (whether for programming,
> proving, or structure data) have the property that if there are
> multiple namespaces, either there is never ambiguity or it's always
> possible to disambiguate which namespace you mean. Apparently this can
> be done using Tactic Notation instead of Ltac, but this still seems
> unsatisfactory - after all, what should one do - never use Ltac?

There is a way to force the parser to consider f_equal as a term
identifier without relying on "Tactic Notation". The syntax is
"applyFwd (f_equal)". 

If the syntax of tactic arguments is ambiguous, it is mainly for
convenience. To force the interpretation of a tactic argument as a
tactic reference, one should use the notation "ltac:id", as in
"applyFwd ltac:f_equal". To force the interpretation as a term
reference, one should use the notation "(id)", as above.

> Can something more be done to avoid this kind of confusing error,
> where a lemma is mistaken for a tactic?

As a matter of fact, the Ltac language has emerged in a rather
empirical way from a few collections of macros like the powerful
"match context with". Some aspects of its semantics and syntax have
been progressively clarified but it still remains some form of
scripting language for which debugging is often not easy.

Hope it helps,

Hugo Herbelin