coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proofs with Let constructs

From: Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>
To: Nicolas Magaud <nmagaud AT cse.unsw.edu.au>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Proofs with Let constructs
Date: Mon, 8 Nov 2004 12:47:30 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Nicolas Magaud writes:
> -----------------------------------------------------------------
> Require Export Omega.
>
> Parameter mk_pair : Z -> prod Z Z.
> Parameter P:Z->Prop.
> Parameter Q:Z->Prop.
> Axiom fst_pair : forall v:Z,(P (fst (mk_pair v))).
> Axiom snd_pair : forall v:Z,(Q (snd (mk_pair v))).
>
> Lemma bidon : forall v:Z, let (n1,n2):= mk_pair v in ((P n1)/\(Q n2)).
> intros v.

this works:

generalize (fst_pair v) (snd_pair v); destruct (mk_pair v).

--
Jean-Christophe

[Coq-Club] Proofs with Let constructs, Nicolas Magaud
- Re: [Coq-Club] Proofs with Let constructs, Claudio Sacerdoti Coen
- Re: [Coq-Club] Proofs with Let constructs, Houda Anoun
- Re: [Coq-Club] Proofs with Let constructs, Jean-Christophe Filliatre