The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

On Wed, Nov 02, 2005 at 08:00:58PM +0100, Ledoux Damien wrote:

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

Au niveau logique informelle, l'élimination de H implémente l'étape
"soit x un habitant de E tel que P x", qui est possible puisqu'il en
existe un.

À niveau plus technique, le type "ex" (derrière le "exists") a un seul
constructeur:

 Inductive ex (A : Type) (P : A -> Prop) : Prop :=
    ex_intro : forall x : A, P x -> ex P

H a donc forcément été construit avec ce constructeur, dont les
arguments ont forcément été fournis et ces arguments sont ... "forall
x, P x". Voilà d'où vient ce forall.

-- 
Lionel