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.
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.