coq - 无法在定义中使用 destruct tatic 的问题

Question

我正在使用 coq 中的定义，它需要从定理中产生一些东西，但不能在定义中破坏。

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.

当我尝试破坏 H 时，coq 会发出警告

归纳定义前不允许对排序类型进行案例分析。

我想知道它的原因，以及如何使用定义从“存在”命题中产生一个元素。

Answer 1

您不能从存在证明中提取证人。有几个选项：

• 将证明的陈述改为{x : T | P x}，其行为或多或少类似于存在量词，但支持投影函数proj1_sig : {x : T | P x} -> T。

• 假设一个选择公理，如https://coq.inria.fr/library/Coq.Logic.ClassicalChoice.html

• 如果您正在对可数类型进行量化并且您的命题是可判定的，则可以使用此问题中的技巧来提取证人。