The Coq mailing list

[Johannes Kloos <jkloos AT unix-ag.uni-kl.de>]

On Fri, Feb 07, 2014 at 11:55:48AM +0000, Terrell, Jeffrey wrote:
> Is there a tactic that would take a proof of P t1 for some P : T -> Prop 
> and t1 : T, to a proof of exists t : T, P t?

I don't think there's a specific tactic for that.
Assuming that the proof of "P t1" is named H,
you could just write
  pose (ex_intro P _ H) as Hex.

This gives:

  H : 2 >= 1
  P := fun x : nat => 2 >= x : nat -> Prop
  ============================
   ...

Unnamed_thm < pose (ex_intro P _ H) as Hex.
1 subgoal
  
  H : 2 >= 1
  P := fun x : nat => 2 >= x : nat -> Prop
  Hex := ex_intro P 1 H : exists x, P x
  ============================
   ...


Regards,
Johannes

> 
> Thanks.
> 
> Regards,
> Jeff.