The Coq mailing list

[Aurore Collomb <aurorecollomb AT chez.com>]

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

--
INRIA - VASY
655 av. de l'Europe
F-38330 Montbonnot Saint-Martin
Tel : 04.76.61.53.37
http://www.inrialpes.fr/vasy/people/Aurore.Collomb/