Coq-从命题中提取证人 [英] Coq - Extract witness from Proposition

问题描述

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

I'm trying to extract a witness from a coq proposition (or something like that...).

我有类似

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 ？
The文档说

从这样的（存在xp）我们可以反过来提取其见证人x：A（使用消除构造）例如比赛）

From such a (exist x p) we may in turn extract its witness x:A (using an elimination construct such as match)

但我不知道它是如何工作的...。

but i don't get how this works....

它也说

给出A：Type和P：A-> Prop，构造{x：A | P x}是类型

Given A:Type and P:A->Prop, the construct {x:A | P x} is a Type

但是如果我尝试类似的参数C：{x：atom | x ＼ ＼notin xs} ，它给出

But if i try something like Parameter C : {x : atom | x \notin xs}, it gives

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

推荐答案

以下内容对此进行了很好的解释：
http：/ /coq.inria.fr/stdlib/Coq.Init.Specif.html

This is explained quite well in: http://coq.inria.fr/stdlib/Coq.Init.Specif.html

在 sig的投影段落下。
（注意该段中有错字： https://coq.inria.fr/ bugs / show_bug.cgi？id = 2767 ）

Under the paragraph "Projections of sig". (Note that there is a typo in that paragraph: https://coq.inria.fr/bugs/show_bug.cgi?id=2767 )

您想要的称为 proj1_sig 您可以在文档中查看其定义。

What you want is called proj1_sig I believe. You can see how it's defined in the documentation.

这篇关于Coq-从命题中提取证人的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！