Coq是一种形式化的证明管理系统，半交互式定理证明器和函数式编程语言。 Coq用于软件验证，编程语言的形式化，数学定理的形式化，教学等。由于Coq的交互性，如果认为合适，我们建议将问题链接到https://x80.org/collacoq/上的可执行示例。
编辑：我包括了证明。我将一个证明（从软件基础获取的证明）从一个文件复制到另一个文件。在原始文件中，一切编译正常。在新文件中，错误：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 = ...
我试图证明Coq中的n <= 2 ^ n，并且我缺少一个必须存在于某处的简单引理：a <= b / \ c <= d-> a + c <= b + d更一般地说，如何搜索Coq库...
我正与这样的目标相等性绑定（我认为细节无关紧要）：tcast tc0 [take i（s_bs bs）的元组++ i。+ 1（s_bs bs）++的元组[:: [ffun⇒0]]] = ...我如何摆脱tcast ...
看来我无法正确安装Coq导入系统。我在Coq.Arith.PeanoNat中找到了pow_succ_r。所以我导入了它，并希望它可以使用Require Import Coq.Arith.PeanoNat。打印pow_succ_r。我得到了...
我有以下Coq程序试图通过自动证明n <= 2 ^ n：（***********）（*进口*）（********** *）需要输入Nat。 （****************************）（*指数函数*）（****** ...
我具有以下Haskell函数，该函数输出所有可能的方法来拆分列表：split :: [a]-> [（[a]，[a]）] split [] = [（[]，[]）] split（c：cs）=（[]，c：cs）：[（c：s1，s2）| （s1，s2）＆...
我不确定如何在coq中应用let表达式。这来自PF中的选择排序示例。一旦定义了选择函数，就证明了这一引理。引理select_perm：forall x l，让...