The Coq mailing list

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

  Hi,

> >  Can you give more details on your implementation of Pick and
> >For_Some please? To my knowledge, defined tactic does not accept fresh
> >names as argument. 
> >
> I defined:
> Tactic Definition Pick x H := Case H;Intro x;Intro;Clear H.
> Tactic Definition For_Some t H:= Assert for_some:(EX t |H); Auto; Pick t 
> for_some.
> 
> Lemma test:(P:nat->Prop)(EX t | (P t))->(EX t | (P t)).
> Intros.
> (* Assert for_some:(EX t | (P t)).    <-  This works.
> Auto.
> Pick t for_some. *)
> For_Some t '(P t).
> 
> But this gives:
> Error: The reference t was not found in the current environment

  Actually the problem is that when building the argument of Assert,
the tactic language does not "see" that "H" in "(EX t|H)" (which is
syntax for "(ex ? [t]H)") is under a binder called "t" (which moreover
is a parameter of the tactique). Otherwise said, "t" is free when
type-checking the value "(P t)" bound to "H". But I don't know what
should be right to do.

  Regards,

  Hugo