The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Saturday, September 10, 2011 08:20:13 AM Guillaume Brunerie wrote:
> Hi,
> I often want to use the [assert] tactic:
> 
> assert (x : T)
>     [proof of T]
> [other proof using T]
> 
> The problem is that after T has been proven, the proof is hidden: the new
> element in the context is [x : T] and I cannot use the structure of the
> proof of T I have given (and if I wanted to construct a dependent pair
> whose first element is [x], I can’t).
> How can I have [x := [proof term I just constructed] : T] in the context
> instead?
> (note that I want to construct x using tactics, I do not want to write the
> term explicitely).

This isn't a complete answer, but you could use something like:

let H:=fresh in refine (let H:=_ in let pair:=exist (fun x => P x) x H in _).

That way you let Coq know about the important parts of the top-level 
structure 
of your object, while you get the convenience that it can often automatically 
infer the types of the other parts.

Another alternative would be to specify a property of the object you're 
constructing in the assert:

assert ({pair:{x:X | P x} | proj1_sig pair = x}) as pair_sig.
    assert (P x) as H.
    [proof of P x]
    exists (exist _ x H).

destruct pair_sig as [[x' ?] ?].
...

or: assert ({pair:{x:X | P x} | exists Px:_, pair = exist _ x Px}) as 
pair_sig.
...
-- 
Daniel Schepler