Coq是一种形式化的证明管理系统，半交互式定理证明器和函数式编程语言。 Coq用于软件验证，编程语言的形式化，数学定理的形式化，教学等。由于Coq的交互性，如果认为合适，我们建议将问题链接到https://x80.org/collacoq/上的可执行示例。
我开始使用 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 编译器。 当我进一步阅读...
在 CoqId 中，我输入了 Variables s p e t f: Type。 我现在想要解释类型 e 的元素集具有完整原子布尔代数的结构。当然，为此...
说我有以下内容： 引理 my_lemma ： 对于所有 a b c， a -> (b -> c) -> d。 证明。 介绍。 然后，在线上方，我得到： ×：一个 X0 : b -> c 假设在我的证明中，我知道我是......
如何告诉 vscode Coq 在哪里？ （修复无法启动 coqtop（coqtop））
我试图在 vscode 中使用 coq，但我似乎无法让它工作。 错误： 无法启动 coqtop (coqtop) 我得到这个选项： 这很令人费解，因为我的终端机似乎知道在哪里...
我想定义一个归纳类型Foo，构造函数接受一些属性作为参数。我想让这些属性依赖于我当前定义的类型的归纳参数。我想...
我有两个定理tst4和tst3，为什么 "omega "能解tst4而不能解tst3？这对我来说是没有意义的。定理tst4 : forall (a b c : nat), (a = b + 1 \ b = 0) -> (False / a & ...
如何在Coq中证明以下内容？Require Import Coq.Reals.Reals. 定义 f (x:R) :R := pow x 2.Lemma f_2: f 2 = 4%R. 证明：f 2 = 4%R. 承认。
这可能看起来是个愚蠢的问题，但我想知道为什么规范类型(例如 nat)会 "继承 "Set类型(和Type类型)，而程序类型不会？这种包容性是用来做什么的？...