问题标签 [gallina]

Coq 中的 Gallina 语言是否有一个预定义的运算符来帮助避免像 Haskell's$或 OCaml's这样的括号@@？

如果没有，是否存在人们使用 Notation 定义的传统方法？

我正在使用 Coq 8.10.0。以下证明脚本似乎在 Mac 中工作（忽略警告）：

但是 Linux (Ubuntu) 和 Windows 不接受相同的证明脚本。它抛出以下错误：

（在证明 plus_comm 中）：尝试保存放弃目标的证明。如果这确实是您想要做的，请使用 Admitted 代替 Qed。

知道这里发生了什么吗？

PS：我知道理想情况下，承认的证明应该以 Admitted 而不是 Qed/Defined 结尾。我正在尝试调试证明脚本。

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

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

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

一些输出示例：

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

我正在尝试重新理解intros关键字。假设我们要证明P /\ ~P -> Q。好的，以某种方式intros P Q介绍Pand Q。但是这是什么意思？它是否从要证明的事物中识别P和？Q怎么样P_and_not_P？它是什么？为什么 P 和 Q 使用相同的名称，而P_and_not_Pis 是定义名称？

更新：

看起来它是逐词匹配的：

给

但为什么不not_p等于~P？

最后一个策略rewirte <- sum不起作用。这是目标：

我不知道如何重写n+1为S(n). 我认为这n+1只是一个符号S(n)，对吧？