The Coq mailing list

[Aaron Bohannon <bohannon AT cis.upenn.edu>]

Hi,

I have found a strange behavior.  Consider this custom tactic:

Tactic Notation "foo" constr(e) constr(e1) :=
  apply e with (1 := e1).

I have a proof state in which "apply lemma with (1 := H)" succeeds as
expected; however "foo lemma H" fails.

The problem revolves around type classes.  "lemma" is parametric in a
type and its typeclass dictionary/proof object (and these arguments
are implicit).  Writing the "apply" tactic inline seems to use the
goal to figure out how to instantiate these implicit arguments.
However, when used in a tactic definition, "apply" seems to just
choose an arbitrary instantiation for the implicit arguments, which in
most cases will not match the goal.

Is this a bug or is it the "expected" behavior?

Actually, this is likely related to typeclass instantiation issues
that come up with "auto", too (and maybe there is a general principle
at work):  "Hint Resolve lemma." seems to be basically useless when
"lemma" has implicit typeclass arguments.  I have found two
workarounds:

1) You can write "Hint Extern ... => apply lemma."

2) You can write "Hint Resolve @lemma." And in addition, add something
like "Hint Extern 1 (MyTypeClass _) => auto using
typeclass_instances." (assuming "lemma" is generic for MyTypeClass).

Now I am wondering which is more "correct".  Although solution (1) has
been working for me, I am now suspicious about that approach, given
the problem I've run into with my tactic definition above.

 - Aaron