The Coq mailing list

[Viktor Vafeiadis <viktor AT mpi-sws.org>]

Require Import ClassicalEpsilon.

Inductive sum (A B : Type) : Type :=
  | leftT : A ->  sum A B
  | rightT : B ->  sum A B.

Lemma foo : forall A : Type, sum A (A ->  False).
intros; destruct (excluded_middle_informative (exists x : A, True)) as [M|]; 
eauto using sum.
left; eapply constructive_indefinite_description in M; destruct M; auto.
Qed.


On 2 Jul 2013, at 21:44, Chris Casinghino wrote:

> Hi Adam,
> 
> Thanks for the quick response.  You're certainly right, and I should
> have been a little clearer.  I'm interested specifically in logical
> consistency, and am not concerned about extraction or the fact that
> the axiom will get in the way of reduction.
> 
> --Chris
> 
>> Such an axiom certainly breaks extraction, since it has no natural
>> computational interpretation, but perhaps you don't care about extraction.
>> It also makes Gallina "computation" highly non-computational, which also
>> might not bother you, depending on the application.  I don't know if it's
>> logically consistent.