Have problem with unable to use destruct tatic in a Definition

Question

I am working with a definition in coq which need to yield something from a Theorem, but cannot destruct in the definition.

Theorem sp : forall (X : Type) (T : X -> Prop)..... , exists (a : X), T a.
Definition yield_sp : (X : Type) (T : X -> Prop) (H : sp X T .....)..... : X.

When I try to destruct H, coq warns that

Case analysis on sort Type is not allowed for inductive definition ex.

I would like to know the reason for it, and further, how to use definition to yield an element from an "exists" proposition.

Answer 1

You cannot extract the witness out of an existence proof. There are a few options:

• Change the statement of the proof to {x : T | P x}, which behaves more-or-less like the existential quantifier, but supports a projection function proj1_sig : {x : T | P x} -> T.

• Assume a choice axiom, as in https://coq.inria.fr/library/Coq.Logic.ClassicalChoice.html

• If you are quantifying over a countable type and your proposition is decidable, you can use the trick in this question to extract the witness.