The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon Ledoux Damien 
<dam.ledoux AT gmail.com>:

> Bonjour,
>
> Je découvre cette année coq, dans le cadre de mes études.
> J'aimerai savoir si vous aviez des polys ou des liens intéressant sur coq?
> Je cherche en priorité les réglès d'inférences associées aux tactiques
> de
> coq.
> Surtout concernant, la tactique elim.
>
> exemple:
> j'ai ça :
>
>    H : exists x : E, P x
>    ============================
>     ~ (forall x : E, ~ P x)
>
> après elim H.
>
>    H : exists x : E, P x
>    ============================
>     forall x : E, P x -> ~ (forall x0 : E, ~ P x0)
>
> Je ne comprends pas pourquoi le "exists" est devenu "forall".

Hello Damien,

 The best way to understand this "forall" is to use two introductions
one for some arbitrary y, the other for an assumption (P y). This
implements the usual "existential elimination rule"




 intros y Hy.

 y : E
 Hy : P y
 =============
 ~ (forall x0 : E, ~ P x0).

 red; intro H1 ; elim (H1 y);auto.
Qed.

There is a Tutorial, available on Coq's site coq.inria.fr,
look at "documentation".

Pierre





>
>
> Merci d'avance pour vos réponses.
> Codialement
> Damien
> --------------------------------------------------------
> 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
>


-- 
Pierre Casteran

http://www.labri.fr/Perso/~casteran/

(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.