Menu
After proving an existence statement, it is often notationally convenient to introduce a constant symbol for some witness of this theorem.
As a simple example, it is much more simple to write (in typical mathematical notation)
∀x. ∅ ⊆ x.
than it is to write
∀x. ∃y. empty(y) and y ⊆ x.
I am looking to replicate this effect in Coq. Here is the basic scenario I am encountering and my attempt which leads to an error (now in real Coq code):
Variable A:Type.
Hypothesis inhabited: exists x:A, x=x.
Definition inhabitant:A.
destruct inhabited.
(*Error: Case analysis on sort Type is not allowed for inductive definition ex.*)
I am wondering what this error message even means and if there is any way to get around this. Thanks!
224
All that you need is to provide the witness first: Inductive A := X | Y . Definition P (a: A) : bool := match a with X => true | Y => false end. Theorem test : exists a: A, P a = true.
The language of Coq Coq objects are sorted into two categories: the Prop sort and the Type sort: Prop is the sort for propositions, i.e. well-formed propositions are of type Prop. Typical propositions are: ∀ A B : Prop, A /\ B -> B \/ B ∀ x y : Z, x * y = 0 -> x = 0 \/ y = 0.
Your issue is related to the usual Prop vs Type distinction. The existence of your witness lies in Prop (see definition of type ex), so you can't inspect it to build a concrete term, you need to have this fact proved in Type.
You are looking for the sig (or a variation like sigS or sigT) type whose notation is :
Hypothesis inhabited : {x : A | x = x }.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
