Coq是一种形式化的证明管理系统，半交互式定理证明器和函数式编程语言。 Coq用于软件验证，编程语言的形式化，数学定理的形式化，教学等。由于Coq的交互性，如果认为合适，我们建议将问题链接到https://x80.org/collacoq/上的可执行示例。
我非常熟悉在声明归纳类型时区分参数和索引的处理。我不确定的是把事情放在...之前是否有什么区别
同伦类型论中存在一个函数： || P + ~P || -> P + ~P, 对于任何单纯的命题 P（||_|| 表示命题截断）。这个函数是通过证明 P + ~P...
我试图证明软件基础>归纳法中的以下定理 我正在使用 Coq 8.19.2 我的解决方案的开头如下： 定理 mult_plus_distr_r : forall n m p : nat, ...
在下面的证明脚本中： 定理 foo ：存在 p，p = (1, 1)。 证明。存在吗？[p]。破坏？p。 我们最终的目标是： n, n0 : 自然 =========================== (n, n0) = (1, 1) 难道是……
这是ProofObjects章节“逻辑基础”中的一道题。 我想证明命题外延性， forall (P Q : Prop), (P <-> Q) -> P = Q 暗示证明
我想通过使用修复策略来证明列表的两步归纳 在下面的尝试中，我在调用 self 之前在结构上缩小了目标（通过将 pxy 应用于目标），所以我期望
我想证明 Peano 公理与 coq 一致并将它们定义为 公理：类型。 公理 znt ：nt。 公理 snt ： nt -> nt。 定义 nt_neq := forall n: nt, znt <> snt n。 定义...
我必须解决这个练习： 制定并证明 lambda 演算的汇合定理（即，证明如果 λ 表达式 e 约简为 e1 和 e2，则存在 e' 使得 e1 和 e2 ...
我正在尝试编写以下程序，将算术公式 e 与变量 x 微分，称为 diff 与 Coq ，如下所示： 归纳 aexp : 类型 := |常量：Z -> aexp |变量：字符串...
Coq 错误 语法错误：'.'预计在 [gallina] 之后（在 [vernac_aux] 中）
所以我有这个代码： 需要导入 Unicode.Utf8。 需要导入字符串。 感应 AExp := | avar : 字符串 → AExp | anum : nat → AExp | aplus : AExp → AExp → AExp | amul : AExp → AExp → AExp。
Coq 和 Emacs：无法编译 Coq - 没有这样的文件或目录
当我尝试在 Emacs 中使用 C-c 编译 Coq 文件时，出现以下错误： Coq 编译错误：((coqdep -Q /home/****/cs54 DMFP /tmp/ProofGeneral-coqUMWPyn.v) 没有这样的文件或目录 我在...
在软件基础、Coq 中的逻辑中，我们引入了参数化命题： 定义 is_two (n : nat) : Prop := n = 3。 检查 is_two。 (* ===> nat -> 道具 *) 这让我想起了
我在 coq 中使用方程包，目前我的目标中有这个表达式： evalMS (if_then_else (if_then_else t1_1 t1_2 t1_3) t4 t5) 在我的背景下 H：无 = evalS (if_then_els...
我已经在 Coq 中实现了一篇论文的证明系统，如下所示。 期限证明系统 归纳术语：类型 := | VarTerm (v: Var) | PrivKeyTerm（k：名称） |公共密钥术语（k：名称） | PairTerm (t1 t2: T...
Coq 正在重复使用归纳假设中的一个术语，而不是创建一个新术语
我有这个目标我想证明。 1 个进球 t1, t2 : FCPLang H : evalS t1 = 一些 t2 ______________________________________(1/1) 评估BS t1 = 评估BS t2 为了证明这一点，我使用归纳法 t1.，但这些是
考虑以下互归纳命题 感应式 A 型 : 道具 := |构造函数A：类型B -> 类型A 与 TypeB : Prop := |构造函数B：类型A -> 类型B。 这是
coq 中关键字/命令“Some”是什么意思？ 此外，我如何查找它的定义？考虑到 some 这个词的流行，使用 coq some 并没有多大帮助。
Coq/Proof General 中类似 Agda 的编程？
与 Agda 不同，Coq 倾向于将证明与函数分开。 Coq 提供的策略非常适合编写证明，但我想知道是否有办法复制一些 Agda 模式功能。 具体...
这就是我要证明的内容：定理add_n_injective：对于所有n m p，n + m = n + p -> m = p。 我已经尝试过 Coq 的内置策略，但它们不起作用。有没有简单的方法可以证明这一点？ 这里是
我正在解决下面的 Coq 问题，我很好奇如何再次重用引理本身（作为假设）来进行证明。 归纳 lparen : T -> Prop := | leps : lparen eps | lseq : forall (lp: T) (...