问题标签 [coq]

为什么 Coq 不接受这个？

我正在尝试定义一个提供身份和组合的类。除了其他有用的实例（带有 nil 和连接的列表；与身份和组合的关系 ;-) ），我想要一个函数实例。

给定

我希望能够定义类似的东西

但是 Coq 中的操作符不是这样工作的。首先我假设->是一个符号，但Locate "_ -> _".声称这是一个Unknown notation. 使用fun a b => a -> b有点工作，但之后的类型看起来很有趣。

（同样适用Eval compute in，似乎它并没有简化类型。）我更喜欢更具可读性的identity nat : nat -> nat. （目前，对于我正在做的事情，这些类型变得不可读。）

有没有办法得到“原始”->或至少说服 Coq 给我更好的类型？

旁注：我正在构建很多Inductive表示评估语义的 s，我的目标是将“普通”编程语言的子集映射到 Coq 上并返回，转移安全约束并发挥作用。我被迫用不同的构造函数一遍又一遍地证明同样的事情，并希望这能让我一次又一次地证明东西。我相信类别是抽象这一点的正确方法。如果我错了，我会在此处包含此注释，也许有更好的方法可以回避整个->问题。

在我当前的项目中，我们使用 Java 和 Coq。我们使用 maven 设置了持续集成。我们想检查 coq 文件作为其中的一部分。即我们需要：

• 如果未安装 coq，请在本地下载并安装它（就像 maven 对 gwt 等框架所做的那样）
• 检查 coq 文件是否正确

有人尝试设置这个吗？如何才能做到这一点？

我试图证明P ?x, whereP : A -> Prop和?x : A是一个存在变量。我可以证明forall a:A, P a，所以我需要推广P ?x到forall a:A, P a。

如果 ?x 是一个实例化变量 x，我可以简单地使用generalize x来生成forall x:A, P x. 然而，当我尝试generalize ?x时，Coq 返回一个语法错误。

这可能吗？我已经检查过了，Coq 似乎没有提供一种直观的方式来概括关于存在变量的陈述。

任何帮助将不胜感激。

现在问题出在哪里，我需要 p (a, a, a) -> p (fa, a, fa) 从所有 x, all y, all z, p (x, y, z) 中很明显 - > p (fx, y, fz) 只需要实例化 x,y 和 z = a，但我做不到。我所做的任何事情在这里都不被接受。

给我错误：战术失败：（论证不是一个普遍量化的公式或不符合目标）。

如果我尝试 all_e (all x, all y, all z, p (x, y, z) -> p (fx, y, fz))。错误：战术失败：（论点不是普遍的量化）。

你能帮忙吗？我已经全面挖掘 Coq 信息，打印 PDF，一直在尝试但仍然无法掌握 Coq 的语法和逻辑流程，我仍然非常迷失其中。

提前感谢您的任何指点！

找到的解决方案：

我在 Coq 中有以下定理：Theorem T : exists x:A, P x.我希望能够在后续证明中使用这个值。IE 我想说这样的话：“让o代表一个这样的值P o。我知道它o是由定理存在的T......”

我该怎么做？提前致谢！

我的证明脚本给了我愚蠢的类型等式，比如nat = bool我 nat = list unit需要用来解决相互矛盾的目标。

在正常的数学中，这将是微不足道的。给定集合bool := { true, false }， nat := { 0, 1, 2, ... }我知道true ∈ bool，但是true ∉ nat，因此bool ≠ nat。在 Coq 中，我什至不知道如何表述true :̸ nat。

问题

有没有办法证明这些等式是错误的？或者，这不可能吗？

（Ed.：删除了一长串失败的尝试，仍然可以在历史记录中查看。）

在简单类型的 lambda 演算中类型推导是唯一的证明在纸上是微不足道的。我熟悉的证明是通过对类型推导的完全归纳来进行的。但是，我无法证明通过类型派生类型表示的类型派生是唯一的。在这里，如果变量的类型为 environment ，则谓词dec Γ x τ为真。类型谓词像往常一样定义，只需读取简单类型 lambda 演算的类型规则：xτΓJ

J在证明类型派生是唯一的时，我无法暴露类型术语的结构。例如，我可以对以下引理中的任何一个d1或d2在其中进行归纳，但不能对d1then destruct进行归纳d2，反之亦然。Coq 给出的错误消息（对术语进行抽象会导致输入错误的术语）有点模糊，并且 Coq wiki 没有提供任何帮助。作为参考，这是我试图证明的引理：

在归纳术语时我没有问题，例如，在证明类型是唯一的时。

编辑：我添加了最少数量的定义来说明我遇到问题的结果。作为对 huitseeker 评论的回应，之所以选择这种类型J是因为我想将派生类型作为结构化对象进行推理，以便执行提取等操作并证明唯一性等结果，这是我以前在 Coq 中没有做过的。

针对评论的第一部分，我可以执行inductionor d1，d2但执行后induction我不能使用destruct, case, orinduction剩下的术语。这意味着我不能公开两者的结构，d1并且无法d2对这两个证明树进行推理。当我尝试这样做时收到的错误表明，对剩余术语进行抽象会导致术语输入错误。

我已经尝试过从库中获得dependent induction一些结果Coq.Logic，但没有成功。推导是独一无二的，这似乎是一个容易证明的命题。

我有一个函数“ HF”在部分内有类型S

我想写一个引理：

在哪里

当我在 section 中有这个功能时就可以了S。

但我想incl_fl在节外写函数S。这里是HF外节的类型S。

我在“”处遇到错误HF：

我试图找到一个地方arity在这个函数中添加“ HF”，但我没有成功。你能帮我incl_fl在节外写引理“”S吗？非常感谢。

我有一种列表，其头部和尾部必须在某种意义上“兼容”：

但是，我不太喜欢这段代码，原因如下：

1. 它不是模块化的：ad-hoc 列表数据构造器本质上与头部和尾部兼容的证明 - 标记相结合。
2. 它不利于代码重用：我被迫重新定义通常的列表函数（例如列表连接）并重新证明通常的列表定理（例如列表连接的关联性）。

我想到了一种不同的方法，它包括三个步骤：

1. 定义单一类型的标记元素（而不是一系列标记类型的元素）：

   /li>

2. 定义标记元素的任意（即有效或无效）列表的类型：

   /li>

3. 将标记元素的有效列表定义为元组，其元素是标记元素的任意列表，并证明元素与相邻元素兼容。

   /li>

我将如何在 Coq 中执行第三步？