Coq是一种形式化的证明管理系统，半交互式定理证明器和函数式编程语言。 Coq用于软件验证，编程语言的形式化，数学定理的形式化，教学等。由于Coq的交互性，如果认为合适，我们建议将问题链接到https://x80.org/collacoq/上的可执行示例。
要使用归纳法以一种直接的方式编写，我有下面的代码。归纳T：= | t0 | t1（a b：T）| .. | tk（P：T-> Prop）（t：T）| tn（P：T-> T-> Prop）（t：T）| .. ...
据我了解，然后Coq内置了一阶逻辑https://coq.inria.fr/tutorial/1-basic-predicate-calculus。但是Coq不是定理证明者，Coq是证明助手，这意味着...
编辑：我通过使用子类型解决了这个问题，即将forall（i：nat）更改为forall（i：{n：nat | n length}），但是我仍然想知道为什么程序模块的行为是这样的，如果那里...
编辑：我包括了证明。我将一个证明（从软件基础获取的证明）从一个文件复制到另一个文件。在原始文件中，一切编译正常。在新文件中，错误：Hs ...
我找不到标准库==函数，该函数已重载并返回布尔值（或sumbool或我可以用其计算的东西）。我希望能够做到3 == 5和“ hello” ==“ hello” ...
了解如何从Software Foundations的正则表达式中证明一些引理
我正在通过Software Foundations工作，目前在IndProp部分。注意：我是一个人做的，这不是功课。我仍在努力思考如何使用这些...
CPDT的Ltac章节显示了一种“错误的”策略：定理t1'：forall x：nat，x = x。与|匹配目标[|-forall x，？P] =>平凡的结尾。这本书然后解释了问题是...
comparable.vo包含库Top.comparable，但与库不具有可比性
我对Coq非常陌生。在我们的项目中，我们切换到使用coq_makefile实用程序，并遇到以下问题。单步执行证明脚本将导致此错误：需要导入...
[当我尝试复制粘贴证明代码时，有时会显示[...]（即使我没有复制任何形式的东西），也无法删除它。我必须撤消该副本才能摆脱它。什么...
我正在尝试证明insert_SearchTree，这是一个有关在插入关系后保留二进制搜索树的定理，如下。我不确定如何使用依赖...
如何证明Coq中的a * b * c = a *（b * c）？
我正在尝试证明上述问题。我给了一个归纳的定义：定义nat_ind（p：nat-> Prop）（基础：p 0）（步骤：forall n，pn-> p（S n））：forall ...
给出定义：定义强制转换（a b：Type）（p：a = b）（x：a）：b：=将p与|匹配eq_refl _ => x结束。我希望可以证明以下引理：引理...
我正在尝试通过H2中的apply（list2map_not_in_default [[k，v）] i）找出以下错误的根源。命令。这是list2map_not_in_default类型：list2map_not_in_default ...
我正在尝试根据TRS进行推理，我遇到了以下证明义务：infinite_sequence：forall t'：期限，transitive_closure R t t'-> ...
我想知道什么样的策略来应对比赛。例如，我有以下形式的东西：F用|匹配m'。 true => Y m'| false => Z m'end = ...