在Coq中使用存在证明定义常量 [英] 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.

比写

∀x. ∃y. empty(y) and y ⊆ x.

我希望在Coq中复制这种效果。这是我遇到的基本场景，并且尝试导致错误（现在在真实的Coq代码中）：

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!

推荐答案

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

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.

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

You are looking for the sig (or a variation like sigS or sigT) type whose notation is :

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

这篇关于在Coq中使用存在证明定义常量的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！