在Coq中使用存在证明定义常量

Question

在证明存在性陈述之后，为该定理的某些见证者引入一个常数符号通常在符号上很方便。

作为一个简单的例子，编写起来要简单得多（以典型的数学符号表示）

?x. ? ? x.

比写

?x. ?y. empty(y) and y ? x.

我希望在Coq中复制这种效果。这是我遇到的基本情况以及导致错误的尝试（现在在真实的Coq代码中）：

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

我想知道此错误消息的含义，以及是否有任何方法可以解决此问题。谢谢！

Answer 1

您的问题与通常的Prop vs Type区别有关。见证人的存在在于Prop（请参阅类型的定义ex），因此您无法检查它来建立具体的用语，您需要在中证明这一事实Type。

您正在寻找符号为sig（或类似sigS或的变体sigT）的类型：

Hypothesis inhabited : {x : A | x = x }.