The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

Alternatively,

assert (Hex := ex_intro P _ H).

hides the body of the proof, and is often more convenient and more readable.
Although I hardly see the point in turning "P t" into "exists t, P t" which loses some information.

2014-02-07 13:15 GMT+01:00 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.

--
.../Sedrikov\...