coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club]and_rec, Edsko de Vries
- Re: [Coq-Club]and_rec, jean-francois . monin
- Re: [Coq-Club]and_rec,
Edsko de Vries
- Re: [Coq-Club]and_rec,
Pierre Castéran
- [Coq-Club]Xml and coq8.1, Thery Laurent
- Re: [Coq-Club]and_rec,
Pierre Castéran
- Re: [Coq-Club]and_rec,
Edsko de Vries
- Re: [Coq-Club]and_rec,
Benjamin Werner
- Re: [Coq-Club]and_rec, Edsko de Vries
- Re: [Coq-Club]and_rec, Jean.Duprat
- Re: [Coq-Club]and_rec, jean-francois . monin
Archive powered by MhonArc 2.6.16.