Coq是一种形式化的证明管理系统，半交互式定理证明器和函数式编程语言。 Coq用于软件验证，编程语言的形式化，数学定理的形式化，教学等。由于Coq的交互性，如果认为合适，我们建议将问题链接到https://x80.org/collacoq/上的可执行示例。
我不知道在什么情况下我应该使用定理而不是引理或相反。这之间有什么区别（语法除外） 定理l：2 = 2。 琐碎的。 问。 和这个 引理 l : 2 ...
在 GitHub Actions 上的 Windows 上安装 Coq 在一个存储库上成功，但在另一个存储库上失败
我尝试在 Windows 上的 GitHub Actions 上安装 Coq，但看到了奇怪的结果。 我尝试了以下脚本，但由于缺少 gmp.h 错误而无法安装 Coq。 名称：CI 在： 推： ...
我的问题的一个最小示例如下所示： 目标让 x := x 中的 True。 这个问题可以通过 simpl 立即解决。自动，但是自动。不起作用。 在我的实际情况中，搜索树比...
抱歉，我不确定标题是否是适当的问题。 我一直在学习逻辑基础。在引理“double_plus”中，我用这个解决方案解决了它： 引理 double_plus : fo...
Coq：与 InteractionTrees 库中的 [mrec] 相互递归定义
我正在研究这个很棒的库，用于在 Coq 中表示递归和不纯程序 我在相互递归方面遇到问题（文档中的第一个示例给了我一个错误） https://深...
在 Haskell 中，将 listify 与 Data 结合使用可以从深度嵌套结构中提取特定类型的值，而无需使用大量 getter。例如，使用以下代码： {-# LANGUAGE DeriveDataTypeab...
电影中有这样的逻辑，我无法完全形式化（例如在 Coq 中）。 有人想在他的农场发射一枚火箭，监视该地点的联邦调查局人员正在互相讨论为什么......
如何证明 (X !-> 3) =[ <{ X := X + 2 }> ]=> (X !-> 5)？
我知道如何使用软件基础第 1 卷中定义的 Imp 证明 3 + 2 = 5。 定义 plus2_3_is_5: Prop := forall (st: state), (X !-> 3) =[ <{ X := X + 2 }> ]=> st -> st ...
Kami（Bluespec 的 Coq 框架）能够在 WSL Ubuntu 上运行的正确设置是什么？
我目前正在使用最新的 Kami 存储库文件，但在尝试运行 Makefile 时无法解决问题。我在此链接中找到了另一个具有类似请求的帖子，但有...
我试图通过 coq 中的显式计算来证明多项式的相等性。这是一个显示我陷入困境的示例： 从 mathcomp 需要导入 all_ssreflect all_algebra。 设置隐式参数...
我正在构建一个在列表 l 上进行匹配的递归函数。在 cons 分支中，我需要使用 l = cons a l' 的信息来证明递归函数终止。然而...
有人可以向我解释一下下面的 coq 策略在做什么吗？ case x : fun H => [|[]] // _. 我将如何使用 destruct 重写它？ 更好的是，有人能指点我到 coq 的某个地方吗
作为 nat 的替代归纳原理，nat_ind2 的定义如下： 定义 nat_ind2 ： forall (P : nat -> Prop), P 0 - > P 1 -> (对于所有 n : nat, P n -> P (S(S n))) ->...
您能否向我提供有关依赖归纳/依赖析构策略的用例以及它们如何工作的高级解释（我将不胜感激高级解释...
是否有一种策略可以将目标中的多个连接拆分为子目标？ 如果我有目标 P /\ Q /\ R，我想将其拆分以一次产生三个子目标： P、Q 和 R 我好像找不到任何信息...
我有一个定义如下的图表。 定义 ldd_state ：类型 := gmap loc (nat * (loc * loc))。 这是从 loc（正数）到值 nat 和两个子项的映射。每个节点都“活着”...
我得到了 com 的以下定义，它可以在单个命令中将新值分配给多个变量： 感应式 com : 类型 := |跳过 | CAsgn (xs : 列表字符串) (es : 列表 aexp) (* ...
我对 coq 比较陌生，我不知道如何继续。 我想为列表库的 In Fixpoint 编写一个可判定性函数，如下所示： 程序定点 InDec (s : K) (l : 列表...
如何证明nat_to_bin结合了bin_to_nat b = Coq中标准化b
我是新手，用参考书软件基础入门学习Coq 在这句话的最后部分，有一个练习证明 将二进制更改为自然数并且
在 Coq 中，作为一个简化的例子（使用 False 忽略结论）， 定理例子 (f : nat -> 布尔) (g : 布尔 -> 布尔 -> 布尔) (cmplx:= 让 a := f 0 进入 让...