The Coq mailing list

[Bas Spitters <spitters AT cs.kun.nl>]

Hugo Herbelin wrote:

>  Dear Bas Spitters,
>
>
> > I want to define a "for some" tactic, which should do the following:
> >     For_Some t (P t)
> > introduces a new variable t and adds (P t) as an hypothesis.
> > When I do this naively:
> >  Assert ( EX t | (P t));Pick t.    [Pick is a previously defined tactic].
> >
> > and I try For_Some t '(P t)  coq complains that t was not defined.
>
>  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


Indeed, it seems that defined tactics do not accept fresh names.

> Isn't "t" in "For_Some t '(P t)" a name (and not a term)?
t is indeed a name, below I was refering to the term [t](P t).

> > So, maybe, I should try doing something like For_Some [t](P t) and use
> > pattern matching to get what I want, but apparently it is not allowed to
> > pass a term to a user-defined tactic.
>
>  Yes, the following definition 
>
>  Tactic Definition For_Some p :=
>    Match Context With
>      [ h : (ex ? p) |- ? ] -> Elim h; Do 2 Intro; Clear h.
>
>  works when called with "[t](P t)" as argument, but then you have no
> control on the name of the witness (actually it will be a name based
> on the radical "x" that is hard-wired in the definition of ex_ind).
Now  I see that I can pass terms to defined tactics, but I can not use 
pattern matching on names.

Is there a good reason NOT to allow fresh names in defined tactics, or 
did it just turn out that way?

Thanks,

Bas