The Coq mailing list

[Sean Wilson <sean.wilson AT ed.ac.uk>]

On Thursday 05 March 2009 19:00:23 you wrote:
> Hello.
>
> Could I interactively construct witnesses of sig types?
>
...
> and I want to use (x, x0) as a witness by interactively proving
> that (x, x0) inhabits the sig type.
>
> I am aware that I can complete the rest of the proof with:
>
>   apply (satisfy_intro
>   (Build_spec
>   ({x: prod (index p1) (index p2) |
>     eq (gen p1 (fst x))  (gen p2 (snd x))})
>   (fun x => match x with exist (n, _) _ => gen p1 n end))
>   (@exist (prod (index p1) (index p2))
>                 (fun x => eq (gen p1 (fst x)) (gen p2 (snd x)))
>                 (x, x0) (eq_trans _ _ _ H (eq_sym _ _ H0))) n).
>   simpl. apply H.

You can use the "assert" tactic to state what type of term you want to 
construct and use "exists" to make use of (x, x0). You can then interactively 
construct the proof part of your term:

assert {x: prod (index p1) (index p2) | eq (gen p1 (fst x))  (gen p2 (snd 
x))}.
exists (x, x0).
simpl.
eapply eq_trans.
apply H.
apply eq_sym.
apply H0.
...

Regards,

Sean