The Coq mailing list

[Ian Lynagh <igloo AT earth.li>]

On Mon, Mar 15, 2010 at 04:08:35PM +0100, Guillaume Melquiond wrote:
> Ian Lynagh a écrit :
>> In the (very abstracted example of a) lemma below, is there a way to
>> prove the result without writing "nat" or "x = y"?
>>
>> What I'd like is to be able to write something like
>> specialize (H _).
>>     admit.
>
> There have been several suggestions already, but none that mentioned the
> "refine" tactic. So here it comes. "specialize (H _)" can be written
>
> refine (let v := _ in _ (H v)).

Aha, thanks! I think that

Ltac solveFirstIn hyp := refine (let v := _ in _ (hyp v));
                         [ | clear hyp; intro hyp ].

is what I am looking for.


Thanks
Ian