Coq是一种形式化的证明管理系统，半交互式定理证明器和函数式编程语言。 Coq用于软件验证，编程语言的形式化，数学定理的形式化，教学等。由于Coq的交互性，如果认为合适，我们建议将问题链接到https://x80.org/collacoq/上的可执行示例。
如何证明对于所有 n m, n <= m -> m <= n -> n = m
定理 le_trans: forall n m o, n <= m -> m <= o -> n <= o. Proof. intros n m o Lnm Lmo. generalize dependent Lnm. generalize dependent n. induction Lmo. -intros. apply Lnm. -intros....
是否有`(A -> B \/ C) -> (A -> B) \/ (A -> C)`的直觉证明？
以下是经典命题逻辑中的一个有用的引理。 (A -> B \/ C) <-> (A -> B) \/ (A -> C)。 向后的方向很容易证明。但我找不到直观的...
我在理解依赖类型的模式匹配方面遇到了麻烦。假设我们有以下代码： 变体 Op := op1 |操作2。 变体 Res : Op -> Set := | r1：Res op1 | r2：Res op2 |...
定理 fiset_ref_fact : forall (r r' n : nat) (f f' D g g' h h' : list nat) (bb' : bool), 长度 f = n /\ n > 0 /\ r < n /\ h = firstn r f /\ h' = (app h ((nth r f 0)::nil)) /\ r' = ...
InteractionTrees 库 - ASM 上的简单程序
我正在尝试在本教程中的 ASM（一种简单的控制流图语言）上编写简单的程序： 交互树 -> ASM.v 我的最终目标是使用图书馆的
我不知道在什么情况下我应该使用定理而不是引理或相反。这之间有什么区别（语法除外） 定理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 我好像找不到任何信息...