Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club]and_rec

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]and_rec


chronological Thread 
  • From: jean-francois.monin AT imag.fr
  • To: Edsko de Vries <devriese AT cs.tcd.ie>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club]and_rec
  • Date: Tue, 6 Mar 2007 14:51:52 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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.

Hope this helps,

-- 
Jean-François Monin           Univ. Joseph Fourier, GRENOBLE
VERIMAG - Centre Equation     http://www-verimag.imag.fr/~monin/
2 avenue de Vignate           tel (+33 | 0) 4 56 52 04 39
F-38610 GIERES                fax (+33 | 0) 4 56 52 04 46





Archive powered by MhonArc 2.6.16.

Top of Page