The Coq mailing list

[David Nowak <David.Nowak AT irisa.fr>]

Hello,

I do not understand why, in the standard library, the predicate Exists
is defined by :

     Inductive   Exists :  Stream -> Prop :=
        Here    : (x:Stream)(P x) ->(Exists x) |
        Further : (x:Stream)~(P x)->(Exists (tl x))->(Exists x).

More precisely my question is why do we need to prove ~(P x) in the
second case ? It may be that (P x) and ~(P x) are not provable, and then
(Exists x) will not be provable whenever (Exists (tl x)) is provable ;
which is again my again my intuition of the predicate Exists (Maybe it
is not the good intuition).

--
David Nowak

~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
David Nowak                   | phone:  +33 2 99 84 25 03
IRISA / INRIA, EP-ATR project | fax:    +33 2 99 84 25 28
Campus de Beaulieu            | e-mail: 
David.Nowak AT irisa.fr
F-35042 RENNES CEDEX - FRANCE | http://www.irisa.fr/prive/nowak/
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~