The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Adam Chlipala wrote:
> Elvet wrote:
> > How can I represent a propositional function in Coq? Something along the
> > lines of:
> >
> > Ex Q(x)
> > (where E is supposed to be the existential quantifier)
> >
> > I'm sure this is trivial, but I am totally lost!
> >   
>
> Which source (book, etc.) are you using to learn Coq?  Any good 
> introduction will cover this.  (I'm guessing, because your question 
> confuses me, and I'm not sure exactly what you're asking.)
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/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
The trivial answer is :

exists x, Q x

But, most of the time you also have to give type information (what is 
the type over which x can range?)

I believe the tutorial will be the easiest quick link for this kind of 
question (there are explicit sections
for propositional logic and predicate calculus).

http://coq.inria.fr/V8.2/doc/html/tutorial.html

Yves