问题标签 [coq-extraction]

我正在尝试将 Coq 中使用Z数字的程序提取到 Haskell。我想将 Coq 的 Z 映射到 Haskell 的整数。

我找到了一些针对 OCaml 而不是针对 Haskell 的库。没有图书馆吗？

我需要提取物（在此处找到）：

但瞄准Haskell。

我只想问：怎么办？

但其次，我应该说为什么我不能自己做：

我想我自己想不出这个可能是因为我误解了一些东西，例如：为什么第二个定义中有一个空字符串？的定义Z具有三个构造函数Z0：Zpos和Zneg。我看不出"Big.zero" "" "Big.opp"与此有什么关系。

另外，我不明白最后一个字符串是如何工作的：“......最后一个额外的字符串，指示如何在此归纳类型上执行模式匹配。” （在文档中找到）。

SF 的提取一章说“我们给出了一个 OCaml 表达式，它可以用作类型元素的‘递归’。（想想 Church 数字。）”。

下面的代码如何是递归或模式加工？

在我理解了这些事情之后，我希望我自己可以创造出我可能需要的提取物。

我试图了解证明在 Coq 提取中的作用。我有以下取自此处的整数除以二的示例。对于我的第一次尝试，我使用了Admitted关键字：

当我检查生成的 Haskell 文件时，我发现它确实丢失了：

所以我想OK，让我们证明div_2_even_number：

但我收到以下错误：

这里发生了什么？我显然在这里遗漏了一些东西。

我在理解 Coq 中强规范和弱规范之间的区别时遇到了一些麻烦。例如，如果我想使用强规范方式编写复制函数（给定一个数字 n 和一个值 x，它会创建一个长度为 n 的列表，所有元素都等于 x），我将如何做到这一点? 显然我必须编写函数的归纳“版本”，但如何？

Haskell 中的定义：

弱规范的定义：

用弱规范定义这些函数，然后添加伴随引理。例如，我们定义了一个函数 f : A->B 并证明了一个形式为 ∀ x:A, Rx ( fx ) 的语句，其中 R 是编码函数预期输入/输出行为的关系。

强规范的定义：

给出函数的强说明：这个函数的类型直接说明输入是类型 A 的值 x，输出是类型 B 的值 v 和 v 满足Rxv的证明的组合。这种规范通常依赖于依赖类型。

编辑：我收到了老师的回复，显然我必须做类似的事情，但对于复制案例：

“例如，如果我们想从它的规范中提取一个计算列表长度的函数，我们可以定义一个关系 RelLength 来建立预期输入和输出之间的关系，然后证明它。像这样：

用于证明的函数必须直接使用列表“recursor”（这就是fixpoint 不会显示的原因——它隐藏在list_rect 中）。

所以你不需要编写函数本身，只需要编写关系，因为函数将由证明定义。”

知道了这一点，我如何将其应用于复制功能案例？

抱歉，我是 coq 的新手。我想知道如何使用 coq 证明列表连接不是可交换的？

运行以下代码时遇到错误消息。

我想知道我该如何解决它。谢谢。

我很想了解 Coq 中的类型推断。在给定证明项/对象/程序的情况下，我想要在 Coq 中以一种具体的方式生成类型（定理）。所以给定一个证明项（可能有一个洞，可能没有洞，或者可能是一个证明子项）我可以确定地生成它的类型吗？我想知道 Coq 是否为此提供了这个功能，例如在伪 Coq 中：

Coq 中的正确功能是什么：给定一个证明术语，让我得到它的类型（基本上在 Coq/Gallina 中的类型推断）。

我在玩这个证明，它是证明对象：

一些输出示例：

在等待 Coq、Opam 等安装到我的新计算机时，我使用了非常好的 jsCoq 。