coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Explication de la tactique Elim

From: "Ledoux Damien" <dam.ledoux AT gmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Explication de la tactique Elim
Date: Wed, 02 Nov 2005 20:00:58 +0100
Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=beta; d=gmail.com; h=received:date:to:subject:from:content-type:mime-version:content-transfer-encoding:message-id:user-agent; b=tOw2wJvAE1aoax6bmuTs+MTYNctBcE51bvR7nfJFoD3oiMunvsB7dRkH8eAepgdzMdsPZpU4MfNJhAOMXdwYKE486aVeYo6zkHyaBgcWANU54dQhpeGc9tuFcB+uK/1OQeXOZ4HTnQnBz5mxBo4FLKhbDRUpTKv/SOU2vegsxQk=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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".

Merci d'avance pour vos réponses.
Codialement
Damien

[Coq-Club] Explication de la tactique Elim, Ledoux Damien
- Re: [Coq-Club] Explication de la tactique Elim, Lionel Elie Mamane
- Re: [Coq-Club] Explication de la tactique Elim, Pierre Casteran