The Coq mailing list

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

  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. Isn't "t" in "For_Some t '(P t)" a name (and not a term)?

> 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).

  Regards,

  Hugo