Coq是一种形式化的证明管理系统，半交互式定理证明器和函数式编程语言。 Coq用于软件验证，编程语言的形式化，数学定理的形式化，教学等。由于Coq的交互性，如果认为合适，我们建议将问题链接到https://x80.org/collacoq/上的可执行示例。
将 `P(?x)` 转换为 `exists x,P(x)`，为 Coq 中的不同子目标提供不同的实例化
我有一个存在变量 ?x 的目标。为了证明这一点，我需要解构一个项 t，并且在解构 t 生成的不同情况下，实例化 ?x 的项应该是
这是我的 Coq 代码。 我期望检查 x ∪ y。显示 x ∪ y 但 ∪ {x, y}。 为什么？或者还有另一种定义符号的想法吗？ 我的 Coq 版本是 8.16.1。 部分测试。 变量集：类型。 变量输入：...
定义用于提取列表前半部分的修复点时出现“无法猜测修复的递减参数”错误
我正在尝试为列表 X 定义一个 Fixpoint 函数来获取其子列表的前半部分，如果它是奇数个元素，则中间元素不计入。 这是我尝试过的： 修复点...
为什么列表的“half”的 Fixpoint 定义不起作用？
我正在尝试为列表 X 定义一个 Fixpoint 函数来获取其子列表的前半部分，如果它的元素数量为奇数，则中间元素不计入。 这是我尝试过的： 固定点一半...
“递归必须作用于单个判别参数。”在这个减法的递归定义中，递归不是同时作用于两者吗？
这是 Gert Smolka 关于计算类型理论的书的摘录。 难道不是在第三种模式中，我们对通过区分两个参数获得的变量应用否定...
我正在尝试基于 CoqExtLib 中定义的有限映射来执行以下证明。但是，我遇到了一个问题，证明中显示的 RelDec 实例与实例不同......
我一直在尝试解决 Coq 中的 Pumping 引理。 我正在实现第三个子目标，Mapp。 引理泵送：forall T (re : reg_exp T) s， s =~ 重新 -> 泵送常数 <= length s -> 存在...
我想编写一种策略，将一种策略应用于每个假设，该假设至少是构造函数的一层深度应用。例如，将该策略应用于 0 = m 和 S n = m，但不适用于 n = m。 是
在下面的 Coq 脚本中：为什么在 Foo2 中搜索“foo”没有找到任何东西？我希望它能找到 foo，因为脚本中此时的 foo 是当前上下文的一部分。有没有一些...
我试图理解我在不同证明中看到的方形刹车图案。所以我按照 SSReflect 示例，尝试了几种模式： 引理测试：正确。 证明。 有：存在 v：nat，v &g...
证明汇编语言在 Coq 中执行可变数量的指令后从某种状态进入另一种状态的轻量级方法
我想证明我为玩具语言编写的编译器是正确的。我定义了一个谓词 P，它将源玩具语言和目标玩具程序集的运行时配置相关联。
在 macOS Sonoma 14.5 下的 M1 Mac 上，我尝试从源 coq 版本 2023.11.0 安装。在“创建 opam switch”步骤中，我收到以下错误： [CP.2023.11.0.patch_ocaml] 启动...
感应 Foo : 类型 := |富：富 |酒吧：Foo -> Foo。 引理 Foo_contr f: 条 f = f -> 假。 证明。 简介 H. 归纳 f 为 [|f IH]。 - 歧视。 - 注射H. 申请...
如何使用vellvm框架从llvmir代码制作OCaml（或Coq）代码
我正在研究vellvm框架。 如何使用 vellvm 验证 C 上的简单函数？ 我知道我可以在 .ll 代码中使用断言 ; ASSERT EQ： i32 0 = 调用 i32 @foo(i32 0) 但我想要更多 这是...
在 macOS 上安装 Frama-C (23)、Why3 和 Coq 后，我运行了命令 rm -f ~/.why3.conf ; Why3 配置检测 显示以下消息 找到了 Prover Coq 版本 8.10.2，但没有 Why3 库
我需要证明一个涉及2个变量a和b的定理，一个指定a的可能值的假设H（a = v1 \/ a = v2 \/ ... \/ a = vn），以及一个假设H0指定 b 的值 (b = v1'...
我的目标看起来像 (A <-> B) -> ~A，具有复杂的表达式 A 和 B，我希望我的目标成为 ~B。 我尝试创建一个简单的引理 (A <-> B) -> ~A -> ~B 教派...
我试图理解为什么 Coq 中的特定证明有效。这是归纳类型定义和我试图证明的定理： 归纳 my_s ：类型 := |循环（s：my_s）。 定理 p_of_...