coq 相关问题

Coq是一种形式化的证明管理系统，半交互式定理证明器和函数式编程语言。 Coq用于软件验证，编程语言的形式化，数学定理的形式化，教学等。由于Coq的交互性，如果认为合适，我们建议将问题链接到https://x80.org/collacoq/上的可执行示例。

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

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

coq

回答 1 投票 0

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

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

coq

回答 1 投票 0

关于 Coq 中的图的引理

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

coq

回答 1 投票 0

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

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

coq coq-tactic coqide

回答 1 投票 0

如何证明对于所有 n m, n <= m -> m <= n -> n = m

定理 le_trans: forall n m o, n <= m -> m <= o -> n <= o. Proof. intros n m o Lnm Lmo. generalize dependent Lnm. generalize dependent n. induction Lmo. -intros. apply Lnm. -intros....

coq

回答 1 投票 0

是否有`(A -> B \/ C) -> (A -> B) \/ (A -> C)`的直觉证明？

以下是经典命题逻辑中的一个有用的引理。 (A -> B \/ C) <-> (A -> B) \/ (A -> C)。向后的方向很容易证明。但我找不到直观的...

coq

回答 1 投票 0

消除 Coq 依赖模式匹配中不可能的分支

我在理解依赖类型的模式匹配方面遇到了麻烦。假设我们有以下代码：变体 Op := op1 |操作2。变体 Res : Op -> Set := | r1：Res op1 | r2：Res op2 |...

pattern-matching coq dependent-type

回答 1 投票 0

如何用coq来证明这第n题和第n题？

定理 fiset_ref_fact : forall (r r' n : nat) (f f' D g g' h h' : list nat) (bb' : bool), 长度 f = n /\ n > 0 /\ r < n /\ h = firstn r f /\ h' = (app h ((nth r f 0)::nil)) /\ r' = ...

list coq

回答 1 投票 0

InteractionTrees 库 - ASM 上的简单程序

我正在尝试在本教程中的 ASM（一种简单的控制流图语言）上编写简单的程序：交互树 -> ASM.v 我的最终目标是使用图书馆的

coq

回答 1 投票 0

Coq 中的引理和定理有什么区别

我不知道在什么情况下我应该使用定理而不是引理或相反。这之间有什么区别（语法除外）定理l：2 = 2。琐碎的。问。和这个引理 l : 2 ...

coq theorem-proving

回答 1 投票 0

在 GitHub Actions 上的 Windows 上安装 Coq 在一个存储库上成功，但在另一个存储库上失败

我尝试在 Windows 上的 GitHub Actions 上安装 Coq，但看到了奇怪的结果。我尝试了以下脚本，但由于缺少 gmp.h 错误而无法安装 Coq。名称：CI 在：推： ...