The Coq mailing list

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

On Tue, Mar 06, 2007 at 02:51:52PM +0100, 
jean-francois.monin AT imag.fr
 wrote:
> Hi,
> 
> I did'nt read the complicated part, but at least:
> > I would think if if I have a proof of type A /\ B, I must be able to
> > show that the structure of that proof must be conj _ _; and hence, I
> > should be able to simplify my and_rec, above. But I don't seem to be
> > able to prove the following lemma:
> > 
> > Lemma and_conj : forall (A B:Prop) (pf : A /\ B), 
> >   exists pa : A, exists pb : B, pf = conj pa pb.
> 
> intros. case pf. intros a b.
> exists a. exists b.
> reflexivity.
> Qed.

Aaargh. Okay. That was easy :) Thanks! I had tried both (elim pf) and
(inversion pf), but neither worked; I hadn't tried (case pf). I don't
really understand why (case pf) works, but the other two don't. I guess
it's back to Coq'Art for me :)

Thanks!

Edsko