Coq是一种形式化的证明管理系统，半交互式定理证明器和函数式编程语言。 Coq用于软件验证，编程语言的形式化，数学定理的形式化，教学等。由于Coq的交互性，如果认为合适，我们建议将问题链接到https://x80.org/collacoq/上的可执行示例。
这就是我要证明的内容：定理add_n_injective：对于所有n m p，n + m = n + p -> m = p。 我已经尝试过 Coq 的内置策略，但它们不起作用。有没有简单的方法可以证明这一点？ 这里是
我正在解决下面的 Coq 问题，我很好奇如何再次重用引理本身（作为假设）来进行证明。 归纳 lparen : T -> Prop := | leps : lparen eps | lseq : forall (lp: T) (...
如何证明顺序命令C1；如果我们知道 C1 总是终止，那么 C2 总是可以执行到 C2？
我正在使用定理证明器来演示程序的进度。 程序的语义是使用小步关系定义的，表示为 ctran，程序配置之间。一个程序
为什么 Coqsolve_in_Union 策略直接失败，但通过断言相同目标起作用？
我在 Coq 中遇到了一个令人困惑的情况，我正在与关系和合奏团合作。我定义了他们之间的强制以及解决会员目标的策略： 需要导入 Lia Reals Lra
我对 Coq 还很陌生，我正在尝试证明以下引理（使用 Reals 库）： forall (An : nat -> R) (a : R), Un_cv An a -> Un_cv (fun i : nat => An i - a) 0。 现在，我明白了...
如何用给定的假设证明排除中间（对于所有 P Q : Prop, (P -> Q) -> (~P \/ Q)）？
我目前对如何证明以下定理感到困惑： 定理exclusion_middle2： (forall P Q : Prop, (P -> Q) -> (~P \/ Q)) -> (forall P, P \/ ~P)。 我被困在这里： 定理
研究依赖类型的应用，我发现了以下依赖向量的定义。 归纳向量(A: 类型): nat -> 类型 := 空向量：向量 A 0 | nonempty_vector：foral...
我想证明一个简单的数学定理，但我未能实现以下子目标： IHn : 可整除3 (n * n * n + n + n) --------------------------------------(1/1) 可整除 3 (S n * S...
为什么 Coq 不接受这个引理作为提示？ 引理控制：forall p1：Prop，False -> p1。 证明。塔图。问。 提示解决控制：提示。 或者其他以 Prop 变量结尾的引理？
我目前正在解决软件基础问题，并在 IndProp 章节中进行练习“filter_challenge”。我在 merge_filter 定理中遇到了以下问题。公鸡呃...
我目前正在解决软件基础问题，并在 IndProp 章节中进行练习“filter_challenge”。我在 merge_filter 定理中遇到了以下问题。公鸡呃...
我正在尝试使用 Coq 交互式定理证明器来形式化稳定币协议。我的证明涉及大量涉及有理数的线性和非线性方程的操作......
我想创建 Coq 策略来解决各种等式子目标，这些子目标可以通过使用混合重写规则（例如运算符的结合性和交换性）来解决。 虽然...
就像其他问题一样，我正在 -nois 下重新开发 Coq.Init.Prelude 进行练习。 我想使用战术，但它们不起作用。 我尝试声明 ML 模块“ltac_plugin”。但我...
几个例子表明，目标中的矛盾（例如当尝试对列表的长度使用归纳法时“0 > 0 意味着某些东西”）可以通过以下方式处理 也同样。欧米茄。 作为 O...
我是 Coq 新手。我对定义递归函数 c(k) 感兴趣。基本情况 c(0) 是常数 0。给定 c(k)，有 a(k+1, i) = g(i, c(k))，其中 g 是函数，c(k+1 ) = a(k+1, j),
作为 Coq 新手，我被这个问题困扰了。希望有人可以提供帮助！ 给定 Coq 中有限类型的编码如下 - 定点 fin (n : nat) : 类型 := 匹配 n 与 | 0 => 假 ...
我们如何在 ssreflect 中使用熟悉的整数算术表示法？
我想在 ssreflect (ssrint) 中使用熟悉的整数算术运算表示法。我已经成功地（我不知道如何做得更好）通过打开
我不明白为什么 Visual Studio Code 将计算命令用蓝色下划线。错误消息没有说明这一点。 感应日：类型：= |周一 |周二 |周三 |周四 |
我想用自然数证明不等式的反转： forall i j : nat, i <= j -> forall w : nat, i <= w -> j <= w -> w - i >= w - j。 我试图证明...