coq 相关问题

Frama-C 23 和 Coq

在 macOS 上安装 Frama-C (23)、Why3 和 Coq 后，我运行了命令 rm -f ~/.why3.conf ; Why3 配置检测 显示以下消息 找到了 Prover Coq 版本 8.10.2，但没有 Why3 库

Coq 对析取假设重复“破坏”，最终导致不必要的破坏

我需要证明一个涉及2个变量a和b的定理，一个指定a的可能值的假设H（a = v1 \/ a = v2 \/ ... \/ a = vn），以及一个假设H0指定 b 的值 (b = v1'...

如何在 Coq 中应用简单的引理和复杂的实例化？

我的目标看起来像 (A <-> B) -> ~A，具有复杂的表达式 A 和 B，我希望我的目标成为 ~B。 我尝试创建一个简单的引理 (A <-> B) -> ~A -> ~B 教派...

Coq 中没有 Base Case 的归纳类型

我试图理解为什么 Coq 中的特定证明有效。这是归纳类型定义和我试图证明的定理： 归纳 my_s ：类型 := |循环（s：my_s）。 定理 p_of_...

命题函数的函数外延性

我创建了以下简单定义，用于将类型 X 的对象集表示为函数 X -> Prop，并定义了各种操作，例如 cup（联合）。不过，在我开始之前

如何在 COQ 中使用 lambda 函数

我正在努力学习基本语法，我需要看一些示例。我的印象是我需要声明一个多态类型参数。 符号 "'λ' x .. y , t" := (fun x ...

有没有一种轻量级的方法来定义一个可变字典，可以在 Coq 中返回它的所有键？

我想定义一个可变字典，它可以返回其域中的所有键。钥匙不必订购。我在互联网上搜索了 coq 库文档，似乎没有找到任何东西

在递归函数中构造证明项

刚从 Coq 开始，尝试编写一个列表插入函数，该函数将返回新列表，或者如果提供的索引不合法，则使用 sumor 进行证明。我对递归没问题......

在模块内部定义的 Coq 表示法需要没有模块前缀的类型

我正在编写一个玩具语言的编译器及其证明，并且我有文件 L1、L2、C 和 P，其中 L1 和 L2 包含语言 l1 和 l2、C 包含的抽象语法和操作语义。 ..

如何证明 coq 中的定理：(x | a) -> (x | b) -> x <= (gcd a b)?

我对最大公约数有这样的认识： 定点 gcd_ (m n d : nat) : nat := 将 d 与 | 0 => if (m =? 0) then n else m | S k => if (m mod S k =? 0) && (n mod S k =? 0)...

依赖类型语言可以是图灵完备的吗？ [已关闭]

看起来依赖类型语言并不是图灵完备的。为什么我们不能允许每个函数都具有通用递归（这将使语言图灵完整）？ 有什么东西

DTT是否意味着图灵完备？ [已关闭]

例如： Agda：https://en.wikipedia.org/wiki/Agda_(programming_language)#:~:text=Agda%20is%20a%20total%20语言，可能%20to%20证明%20任意%20语句 Coq：有什么实用的

展开策略中 Delta 减少后的 Beta 减少

根据 coq 手册，unfold 策略对定义执行 delta 缩减，然后进行其他几个缩减，包括 beta 缩减。 似乎有时，要触发β-红...

为什么依赖类型语言通常不是图灵完备的？

例如Agda和Coq。 与 Idris2 和 Fstar 相比。 另外，诸如 Agda 之类的依赖类型编程语言不是图灵完备的，是否存在实际缺点，或者它是……

在 coq 中将列表转换为向量

我对使用 coq 还很陌生，而且对向量有点困惑。我想将列表转换为具有相同内容的向量。我正在尝试模式匹配，但它不断抛出有关 e 的错误...

Coq 中 sig 类型的元素相等

sig 类型定义如下： 归纳 A：集合 := mkA : nat-> A。 函数 getId (a: A) : nat := 将 a 与 mkA n => n 匹配。 函数过滤器 (a: A) : bool := if (beq_nat (getId a) 0) then ...

在 Coq 中定义相互递归类型？

假设我有 A、B、C、D、E、F 类型。 A 的构造函数之一采用 F 类型的参数； B 的构造函数需要 A，D 的构造函数需要 C 和 A 类型的参数，E 需要 D 和 F

如何在 Coq 中将部分与提示混合在一起？

我正在写一些大量涉及类型类的内容，我想利用提示来轻松证明局部引理以及导出定理。 例如，考虑 MyClass 类（A：类型）:=

关于 Coq 中的图的引理

我需要在 Coq 中证明一个关于具有某些属性的连通图的引理： 图的顶点是 V:Type 类型，并且有一个函数 f: V -> nat 关联一个自然麻木...

错误：找不到绑定到逻辑路径 Strand 的物理路径。在coq

我有 coq 文件，并且已经处理了好几天，但现在该文件给了我以下错误： 错误：找不到绑定到逻辑路径 Strand 的物理路径。 所需的包如下：