The Coq mailing list

["Randy Pollack" <rap AT dcs.ed.ac.uk>]

Dear Christine,

> One thing could be to adapt the Apply tactic such that it performs
> expansion in order to succeed (as in LEGO if I remember correctly)
> I would like to know what is your feeling on that point.

Yes, LEGO "Refine" tries to use the applied lemma with 0 subgoals,
then with 1 subgoal, with 2 subgoals, ....  It will expand definitions
if necessary to get another product in the applied lemma to create
another subgoal.  This finds the best match possible, and is
convenient for users.  It is not very expensive as long as the
attempted unification is not expensive.

LEGO also expands definitions (on both sides) in the attempt to unify,
until a unifier is found, or, eventually, beta-iota-delta normal form
is reached.  This expansion during unification can be very expensive.

Since Coq does not automatically expand constants in the goal, Apply
can see what head constant it is intended to solve, and could expand
in the applied lemma searching for that constant.  Then the user
specifies what s/he intends by putting the goal in shape, while the
system does a tiny bit of search through the applied lemma.

> A more explicit way would be to have a tactic 
>   Apply lemma [reduction_tactic]
> which performs expansion of the type of lemma following the expansion
> strategy indicated by the reduction_tactic before performing
> application.

Hugo suggested something like this too.  I also liked Freek's
suggestion to be able to specify what head constant a Hint is intended
to solve.  Maybe this idea, along with the ability to use
reduction_tactics on the applied lemma as well as on the goal, will be
useful.

Best wishes,
Randy