Coq是一种形式化的证明管理系统，半交互式定理证明器和函数式编程语言。 Coq用于软件验证，编程语言的形式化，数学定理的形式化，教学等。由于Coq的交互性，如果认为合适，我们建议将问题链接到https://x80.org/collacoq/上的可执行示例。
如何证明所有x y, x<=y -> div2 x <= div2 y in coq?
我想证明这个引理“forall x y, x<=y -> div2 x <= div2 y” in coq by induction, however I got stucked. How can I prove this by induction? Thanks! I tried to prove by induction...
我正在尝试在 Coq 中实现二元决策图。我想使用 2CNF 公式创建 BDD。 一、进口； 需要导入 Coq.Lists.List。 需要导入 Coq.Init.Nat。 需要导入 Coq。
我被使用 coq 的证明所困扰。我有以下定义： 需要进口清单。 需要导入 Nat。 定点 Inb(x: nat) (A: 列表 nat) := 将 A 与 |零=>假 | h :: t =>...
我有定义： 定义 f (b1 b2 : bool) :bool := 将 b1 与 |真=>真 |假=> b2 结尾。 还有引理... 引理 l1：forall p : bool, f p false = true。 我尝试过的是这样的：
我一直在使用 https://coq.inria.fr/ 的下载链接为 Windows 和 Mac 安装 Coq。但是，当我在终端或命令提示符下尝试 coqc 或 coqtop 时，我收到错误消息...
软件基础基础 - 定理 lower_grade_lowers 需要证明蕴涵 Eq = Lt -> Eq = Lt
我正在自己研究软件基础，并陷入了 lower_grade_lowers 的最后一个项目。我的定理很好地遵循了提示，直到最终的情况，这显然是症结所在......
我开始使用 Coq 并尝试将自动摊销分析形式化。我在引理 4.13： 引理保存：forall (Sigma : prog_sig) (Gamma : context) (p : program) （s：堆栈）（h h'：...
给定 Coq 中二叉树和任意分支树（K 树）的两个标准定义（为简单起见，nat 硬编码）： 归纳二叉树：类型：= |叶子：bintree |节点：bintree -&g...
我有以下文件夹结构： - BaseDefs.v - 使用BaseDefs.v 在这里，BaseDefs.v 包含我想在 UsingBaseDefs.v 中使用的定义。我尝试使用
我正在尝试编写一个——我的第一个——Coq 策略。 它应该将 forall x y z ..., A <-> B 分成两部分：forall x y z ..., A -> B 和 forall xy z ..., B -> A。 这是我的第一次尝试： 乳酸菌
我正在学习 Coq 并且需要知道为什么以下代码在 Coq 中不起作用？我来自 Haskell 背景，那里没问题。 需要进口清单。 需要导入布尔。 需要输入...
语法错误：“。”当对整数使用归纳时，在 Coq 中预期在 [vernac:gallina]（在 [vernac_aux] 中）之后
所以我试图在 coq 中定义一个从 0 到 10 的整数的归纳集： 感应OD：设置：= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10. 我收到这条消息： 语法错误：'.'预计在 [
我试图将带有双换行符的字符串解析为 Coq 中的 int 列表列表，但我无法使其按预期工作。 示例字符串： 1个 2个 3个 4个 上面的字符串需要解析...
我目前的假设和目标是： 1个子目标 x：实体 H : ~ P x x -> 存在 z : Entity, P z x /\ ~ O z x ______________________________________(1/1) × 我想申请对立面...
我正在使用 Cotnoir 和 Varzi（2021 年）的“Mereology”一书来锻炼我的证明技能。在接受原始二元关系 P 之后，书中给出的第一个定义是： (D1) PPxy := ...
在 Coq 中，A+B 是类型 A 和 B 的不相交和。 有没有办法引入两种类型的（可能）不相交的总和？ 例如，如果可能 A = B 怎么办？ 我找不到关于 ...
我试图在 Coq 中证明一个叫做 alignof_correct 的引理，它验证我为一个类型定义的 alignof 函数返回一个正值。我已经定义了类型和函数，我...
我试图在 Coq 中证明一个叫做 alignof_correct 的引理，它验证我为一个类型定义的 alignof 函数返回一个正值。我已经定义了类型和函数，我...
对于我即将开始的项目，我正在探索编译器的形式验证。我遇到了 CompCert C 编译器，它是 ACM 授予的、经过正式验证的 C 编译器。 当我进一步阅读...