coq 相关问题

在 Coq 中，证明解决数独或 Takuzu 等难题的函数的正确性的步骤是什么？

证明解决谜题的函数（例如数独或卓祖）的正确性的一般步骤是什么？

Coq 中的高效记录构建：直接证明包含可能吗？

我想在 Coq 中定义一个小记录，其中也包含某些条件。此外，我想要一个定义来以简单的方式创建记录。这是我的方法： 需要导入算术。 (* 德菲...

如何在 coq 中证明 b = c if (andb b c = orb b c) ？

我是coq新手，我正在努力证明这一点...... 定理 andb_eq_orb ： forall (b c : bool), (andb b c = orb b c) -> (b = c)。 这是我的证明，但当我达到目标时我陷入困境（错误=...

归纳法和递归法的等价

我对自然数的阶乘有两个定义。一种是归纳定义，另一种是固定点。我想证明这两个定义的等价性，但还没有...

如何证明 (X × Y = ∅) <-> (X = ∅) ∨ (Y = ∅)

我希望使用 Coq 和 mathcomp.classical_sets 证明下面的引理。 设 A × B - 某些集合的乘积，即 {(z1, z2) | z1 Î A /\ z2 Î B} 那么 (A × B = ∅) <-> (A = ∅) ∨ (B = ∅) 我的证明是

Iris/Coq 替换文字

我正在使用 Iris for Coq，但我遇到了一些问题。 在这里，我想从 hd' 获取 snd 值 l'。然后我可以使用 IH 与 Hl 和 Hphi 来完成目标。有谁知道如何替换 hd' in...

需要帮助证明 (X × Y = ∅) <-> (X = ∅) ∨ (Y = ∅)

请帮助我使用 Coq 和 mathcomp.classical_sets 证明下面的引理。 设 A × B - 某些集合的乘积，即 {(z1, z2) | z1 Î A /\ z2 Î B} 那么 (A × B = ∅) <-> (A = ∅) ∨ (B = ∅) 我的证明

如何在 coq 中安装库？ （苹果系统）

我正在尝试使用 VSCoq 中的 mathcomp 库。我按照图书馆网站上的安装说明进行操作。 opam 存储库添加 coq-released https://coq.inria.fr/opam/released opam 安装 coq-

有没有关于模式的三值案例分析（a < b) (a = b) (a > b）？

我希望我的学生通过二叉搜索树证明一些东西。 大多数证明需要对三种情况下的算术不等式进行案例分析： 一个< b (recursive call in ...

如何证明不等式

我如何在 Coq 中证明这一点？战术“欧米茄”不起作用。 “利亚”也没有。 需要导入 ZArith。 需要导入 Psatz。 打开范围 Z。 引理 ge1： 对于所有 b k: Z, b>=1 -> ...

如何为 coq 中的类型指定别名

假设我想在 coq 中创建一个自然数矩阵。 我有内置的 coq 列表，要创建自然数列表，我只需编写 list nat。 为了创建一个二维列表（我...

如何使用ssreflect以更优雅的方式证明目标？

看来我的 coq 证明比预期更长、更难看，尽管我尝试了，但我无法在其中实现 ssreflect 优势。我想我错过了一些关键点。或者也许我只是需要了解更多

如何在coq中继续进行嵌套匹配的案例分析？

我最近从coq得到了一个目标（其实我这个目标是通过案例分析得到的）： 1 个进球（ID 110） 地址： NAT x：状态 l : 列出 nat Heqo : write_list_index (重复 0 (addr + 1)) addr 0 = Som...

为什么“专门化”在证明中不是无效策略？

在软件基础书籍（已存档）中，引入了专门策略作为简化假设的一种方法。 我不明白，为什么这是证明中的有效步骤。 提供的示例添加...

如何在 Coq 中推理集合？ - 定义完整格子

我在 Coq 中定义了一个 Lattice 类型类： 类 PartialOrder A : 类型 := { le : A -> A -> 道具； }。 符号“x <= y" := (le x y). Class Lattice A `{PartialOrder A} : Type := {...

证明身份类型中的对象

我正在阅读软件基础，他们将平等定义为 归纳式 {X:Type} : X -> X -> Prop := | eq_refl ：对于所有 x，eq x x。 符号 "x == y" := (eq x y) ...

图书馆提供的自定义策略

有没有办法从 Coq 内部查看库提供的所有自定义策略？ 使用搜索来搜索它们不起作用。

在 stdpp 库中找不到集合相等的引理

我正在使用 stdpp 库，我想展示这两个集合的相等性： {[x0]} ∪ dom X = {[x0]} ∪ dom Y 但是，我无法在 stdpp 中找到引理来将问题减少为： dom X = dom Y 哪...

如何通过 apply 创建新的假设？

当我运行下面的 Coq 脚本时（原始脚本的简化版）： 归纳w(g: nat): nat -> Prop:= | z：wg 0。 引理x： forall (i j: nat), w i j -> (forall k: nat, k <= k). P...

目标状态 Coq 为真

在尝试证明软件基础第 1 卷 Logic.v 中的 All 时，我遇到了一个简单的 True 证明状态。 IE。我的证明状态如下： T：类型 P : T -> 道具 H：forall x：T，Fal...