问题标签 [coq]

免责声明：这是一个家庭作业

我是一个 coq 菜鸟，所以我希望这不是一个重复的问题。我/已经/看过这个问题，但我的问题似乎仍然没有答案。

我有以下前提：

我需要证明：

到目前为止我的coq代码：

当我尝试执行该行时出现以下错误Goal P.：

错误：在当前环境中找不到引用 P。

这些是我能够提出的解决方案：

1. 替换Variables Q : Prop.为Variables P Q : Prop.。问题在于，这P将被假定为前提，但事实并非如此
2. Variables P.在目标声明之前添加。这会导致语法错误。

我错过了什么吗？我似乎无法弄清楚这一点。

我试图将 coq 用作具有依赖类型的编程语言。我创建了以下小程序：

我为非空列表定义了一个类型，并创建了一个函数，该函数获取此类列表的第一个元素，前提是有证据证明它不为空。我很好地处理了头项目由两个项目组成的情况，但我无法处理空列表的不可能情况。我怎样才能在 coq 中做到这一点？

我想到目前为止，我已经阅读了标记为coq的 81 个问题（如果不是全部的话）的大部分内容。作为 coq 的新手，我无法找到这个非常简单的问题的答案（我相当肯定没有在 SO 上问过这个问题，因为它非常基础）。

我正在做一个家庭作业，为此我需要使用 coq 来证明：

• 给定：P/Q。～问
• 证明：P

这是我在纸上做的一个足够简单的证明，但我似乎无法让 coq 为我做这件事。

我的策略是假设每个P和Q，显示P并因此得出结论P必须成立：

1. P / Q [前提]

2. ～Q【前提】

   1. P [假设]

   2. P [复制上一行]

      ---

   3. 问 [假设]

   4. ~Q [复制上一行]
   5. [矛盾]
   6. P【矛盾消除】
3. P [消除\/]

鉴于这是我在纸上证明它的方式，我能够想出以下 coq 代码在 coq 中证明它。可悲的是，我努力假设P,Q或~P没有通过：

这是我对下一行的尝试，以及它们产生的错误：

我很感激这方面的任何帮助，因为我已经用尽了我能想到的一切。

我有一堆规则，它们本质上意味着某些命题 P 永远不会为真。我现在必须使用 Coq 证明 P 是错误的。为了在纸面上这样做，我会假设 P 成立，然后得出矛盾，从而证明 P 不能成立。

我不太确定如何假设 P 支持这个证明，这就是我寻求帮助的原因。我当前的代码：

有人可以确认我是否以正确的方式进行此操作（否则，我应该怎么做？）？

我试图用 tatics [intro]、[apply]、[assumption]、[destruct]、[left]、[right]、[split] 来证明这个引理，但失败了。谁能教我如何证明？

通常，如何证明简单的命题，例如 false->P、P/~P 等？

我正在学习 COQ，但我被困在书中的一个练习中。这本书没有给我一个解决方案，所以我不知道该怎么做。虽然我已经完成了第一个。我必须将这些语句转换为谓词逻辑：

代码：

.

你能帮忙吗？非常感谢！

为了尽可能地隔离这个问题，假设我开始一个 Coq 会话，如下所示。

从这里开始，我想将一个函数定义为始终为真的f : A -> B唯一函数。P a (f a)

我怎样才能做到这一点？我可以这样做吗？显然我应该从类似的东西开始

...但是我如何根据这些假设实际编写函数？

我必须证明这一点：

到目前为止，我已经完成了：

然后我必须证明 False。我不知道该怎么做。这是不可证明的吗？你能把我引向正确的方向吗？或者我在这里错过了什么？

编辑：Ptival，你帮了大忙……我注意到问题上有一个错误，当我尝试编辑问题时，我不小心点击了删除按钮，惊慌失措并按下退格键。:(

你如何证明：forall m n : Z, m < n -> m -n < O在 Coq 中？非常感谢！

假设以下定义（前两个取自http://www.cis.upenn.edu/~bcpierce/sf/Basics.html）：

我想证明以下几点：

我能做的最远的事情就是证明blt_nat_flip假设blt_nat_flip0。我花了很多时间，我快到了，但总的来说，它似乎比它应该的要复杂。有人对如何证明这两个引理有更好的想法吗？

到目前为止，这是我的尝试：