The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

On Tue, Mar 06, 2007 at 03:05:08PM +0100, Benjamin Werner wrote:
> I suggest the following. Prove:
> 
> 
> Lemma pia1 : forall A B, A/\B -> A.
> intros A B [a _]; trivial.
> Defined.
> 
> 
> Lemma pia2 : forall A B, A/\B -> B.
> intros A B [_ b]; trivial.
> Defined.
> 
> Lemma surj_conj : forall A B, forall c : A/\B,
>                 c = (conj (pia1 _ _ c)(pia2 _ _ c)).
> intros A B [a b]; trivial.
> Qed.
> 
> 
> Then each time you are stuck, you simply have to do
>  rewrite (surj_conj c)
> where c is the proof of the conjunction.

Thanks! That is quite elegant, and works very nicely. I also didn't know
about the syntax you are using (intro [a b]) - is there an implied case
analysis there? Good to know! Using intro [a b] gets me a conj _ _
straight away, which is the bit I couldn't get working..

Thanks again,

Edsko