The Coq mailing list

[Ryan Wisnesky <ryan AT cs.harvard.edu>]

Another issue: in addition to excluded middle, FOL and its prenex conversion assumes a non-empty domain of discourse and there are empty Coq types.  

On Sep 4, 2012, at 10:00 AM, Gregory Malecha <gmalecha AT eecs.harvard.edu> wrote:

Hi --

Is this guaranteed when you have dependent types? You could try to pull apart the dependency, but it isn't clear to me that it is always possible.

Inductive IsEven : nat -> Type :=

| Pf : forall n, Even n -> IsEven n.

forall x : nat, Even x -> exists y : IsEven x, True

What would be the prenex form for this? You can't move the existential before the "Even x". It seems like you would need a way to pull dependency out of values, or treat -> as forall (does that defeat the purpose? I don't know).

On Mon, Sep 3, 2012 at 10:08 PM, Ryan Wisnesky <ryan AT cs.harvard.edu> wrote:

Such a conversion could be non-trivial in that to avoid reifying the syntax of Prop, it would probably need to be a tactic (although you could use explicit syntax), and regardless, it would require heavy use of a classical logic axiom or a decidable domain.  It would be pretty useful though, so I hope it exists.

On Sep 3, 2012, at 6:20 PM, Marko Maliković <marko AT ffri.hr> wrote:

> Regards,
>
> Is there module for conversion first-order formulas over the Prop into
> Prenex form. I can not find it.
>
> Great thanks,
>
> -----------------------
> Dr. Sc. Marko Maliković
> Docent
> Filozofski fakultet
> Sveučilište u Rijeci
> ---------------------
> Ph.D. Marko Maliković
> Assistant Professor
> Faculty of Humanities and Social Sciences
> University of Rijeka, Croatia
> -----------------------------
> marko.malikovic AT ffri.hr
> http://www.ffri.hr/~marko
> -------------------------

--
gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/