The Coq mailing list

[Benjamin Werner <werner AT lix.polytechnique.fr>]

On Mon, 12 Jan 2004, Aurore Collomb wrote:
Bonne annee aussi,

> 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.
[..]

A priori, on n'a pas besoin de variables existentielles (cad. de points 
d'interrogation dans les buts) pour cette preuve. Et en pareil cas, autant 
les eviter.

Le moyen standard est de ne pas appliquer R1 directement, mais de dire 
d'abord qui sont c3 et c4.

Donc quelque chose comme :

Elim H; Intros c1 [c2 [h1 h2]].
    (* ou ce qui est equivalent : Elim H ; Intros c1 hc1 ; Elim hc1; 
Intros c2 ..... *)
Exists c1 ; Exists c2 ; Split.
Apply R1 ; Assumption.
Assumption.

Je n'ai pas de Coq V7 sous la main pour verifier mon script, donc une typo 
est possible.



Cordialement,

Benjamin Werner