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.

I guess a colon is missing after `Theorem sp`? – Bubbler May 22 '19 at 11:40 — Bubbler, May 22 '19 at 11:40
yes, I mess it up with Definition – shrubbroom May 23 '19 at 12:55 — shrubbroom, May 23 '19 at 12:55

score 1 · Accepted Answer · answered May 22 '19 at 15:56

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.

answered May 22 '19 at 15:56

Arthur Azevedo De Amorim

23,012
3
33
39

Is it a syntax of coq that to yield something simply from an exists statement is not allowed? I think that to do so one has to declare that there is a projection function that exactly can **compute** it since arrow means computable relation in coq. – shrubbroom May 24 '19 at 08:12

Have problem with unable to use destruct tatic in a Definition

1 Answers1