CODEWITHSUNDEEP
coq
user4614475
user4614475

Reputation: 133

Defining constants using existence proofs in Coq

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!

Upvotes: 5

Views: 552

Answers (1)

Vinz
Vinz

Reputation: 6057

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

Upvotes: 5

Related Questions