The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I'm pretty sure it's not provable.  Think about program extraction: Coq erases Props when it extracts programs, so there's no way for your OCaml function to know which side to take.

-Jason

On Sun, Dec 8, 2013 at 11:11 AM, Arthur Azevedo de Amorim <arthur.aa AT gmail.com> wrote:

My feeling is that it is not provable. Since proof irrelevance is consistent with coq, such a function would have to return always a p or always a q, which is not valid logically.

On Dec 8, 2013 11:04 AM, "Andrej Bauer" <andrej.bauer AT andrej.com> wrote:

Is this provable in Coq?

Lemma is_this_true : forall p q : Prop, p \/ q -> ~ (p /\ q) -> {p} + {q}.

With kind regards,

Andrej