coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Houda Anoun <anoun AT labri.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, 08 Nov 2004 12:39:04 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi,
Here is a script that proofs your lemma, you need to destruct (mk_pair v) ...
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)).
intro v.
cut (P (fst (mk_pair v)) /\ Q (snd (mk_pair v))).
elim (mk_pair v).
simpl.
auto.
split.
apply fst_pair.
apply snd_pair.
Qed.
Hope this helps
Houda
Hi,
I am stuck with the following strange proof. I have a function (mk_pair)
building pairs and I know a property P (resp. Q) holds for the first (resp. second) element of a pair built using mk_pair.
Now I want to prove the following theorem: forall v:Z, let (n1,n2):= mk_pair v in ((P n1)/\(Q n2)).
My attempt was to make a pattern (n1,n2) appear in the ((P n1)/\(Q n2)).
It yields something like ((P (fst (pair n1 n2)))/\(Q (snd (pair n1 n2)))))
by convertibility. At this stage, I would like to be able to do some sort
of reduction (of the let construct) to get "mk_pair v" instead of "(pair n1 n2)"
in the goal.
So far I didn't manage to do that. Has someone any suggestions about
the point I missed ?
Thanks in advance,
Nicolas Magaud
PS: It seems to be related to Jasper Stein's message "Some questions on reduction tactics"
sent last month to the list, but it doesn't help me solve my problem...
-----------------------------------------------------------------
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.
change (let (n1,n2):= mk_pair v in ((P (fst (pair n1 n2)))/\(Q (snd (pair n1 n2))))).
--------------------------------------------------------
Bug reports: http://coq.inria.fr/bin/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
--
==============================
| Houda ANOUN |
| LaBRI |
| 351 Cours de la libération |
| 33405 Talence |
| phone: 0540002489 |
:anoun AT labri.fr
|
=============================
- [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
Archive powered by MhonArc 2.6.16.