Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Proofs with Let constructs

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Proofs with Let constructs


chronological Thread 
  • 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       |
|  e-mail 
:anoun AT labri.fr
    |
=============================







Archive powered by MhonArc 2.6.16.

Top of Page