The Coq mailing list

[Houda Anoun <anoun AT labri.fr>]

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
    |
=============================