The Coq mailing list

[Pierre Casteran <casteran AT labri.fr>]

Bonjour et bonne année.

 Est-ce que c'est bien ce genre de preuve que tu voulais faire ?
Pierre



Parameter P P' Q : nat* nat -> Prop.


Axiom R : forall a b, P (a, b) -> P' (a, b).

Goal (exists c1, (exists c2,  P (c1, c2) /\ Q (c1, c2))) ->
     (exists c3, (exists c4,  P' (c3, c4) /\ Q (c3, c4))).
Proof.
 intro H; case H; intros x Hx.
 case Hx; intros y Hy.
 exists x; exists y.
 generalize R; intuition.
Qed.



Aurore Collomb wrote:
> Bonjour et bonne annee.
>
> Me voila avec l'erreur w_Unify, mais je ne vois pas d'autre chemin pour 
> arriver a construire ma preuve.
>
> Je vous explique :
>
> Au debut j'ai :
>       H : Ex c1 c2 : P(c1,c2) /\ Q(c1,c2)
>       -------------------------
>        Ex c3 c4 :  P'(c3,c4) /\ Q(c3,c4)
>
> Il se trouve que j'ai dans mes definitions qq part une regle qui dit :
> R1 :     P(a,b) ->  P'(a,b)
>
> Mais je n'ai pas reussi a l'appliquer directement. Alors je decompose.
>     EApply ex_intro ; EApply ex_intro ;  Split.
>     EApply R1.
>
> Du coup j'obtiens les buts :
>   b1 :  P(?1 ?2)
>   b2 : Q(?1 ?2)
>
> Y'a-il moyen de faire "unsplit" pour pouvoir appliquer l'hypothese H ?
>
> Sinon moi j'ai essaye :
>   Elim H ; Intros ; Elim H0 ; Intros.  pour obtenir une hypothese Hi : 
> P(a,b) pour le but b1.
> Mais en tapant ensuite : Apply Hi, j'obtiens l'erreur : w_Unify.
>
> Voila, encore desolee de vous embeter avec des questions de 
> manipulations de Coq.
>
> Cordialement,
>
> Aurore Collomb



--
Pierre Casteran,
LaBRI, Universite Bordeaux-I      |
351 Cours de la Liberation        |
F-33405 TALENCE Cedex             |
France                            |
tel : (+ 33) 5 40 00 69 31
fax : (+ 33) 5 40 00 66 69
email: Pierre . Casteran @ labri .  fr  (but whithout white space)
www: http://www.labri.fr/Perso/~casteran