1

我正在尝试从 coq 命题（或类似的东西......）中提取证人。

我有类似的东西

Parameter atom_fresh_for_list :
    forall (xs : list atom), {x : atom | ~ List.In x xs}.

（后来证明，有一个明确的类型atom：

Lemma atom_fresh_for_list :
    forall (xs : list nat), { n : nat | ~ List.In n xs }.

我如何提取这样的x？ 文档说

从这样的（exist xp）中，我们可以反过来提取它的见证 x:A（使用消除构造，例如 match）

但我不明白这是如何工作的......

它还说

给定 A:Type 和 P:A->Prop，构造 {x:A | P x} 是一个类型

但是如果我尝试类似的东西Parameter C : {x : atom | x \notin xs}，它会给

Error: The term "C" has type "{x : atom | x \notin xs}" which should be Set, Prop or Type.
4

1 回答 1

2

这在以下内容中得到了很好的解释： http ://coq.inria.fr/stdlib/Coq.Init.Specif.html

在“sig 的预测”段落下。（请注意，该段中有一个错字：https ://coq.inria.fr/bugs/show_bug.cgi?id=2767 ）

你想要的就叫proj1_sig我相信。您可以在文档中查看它是如何定义的。

于 2012-07-22T08:12:21.910 回答