如何在Coq中导入模块？
我在Coq中导入模块定义时遇到了问题。我对Coq不太熟悉，但无法通过语言参考手册或在线教程解决这个问题。我有一个模块，定义了有限集的签名和公理，我打算在另一个模块中实现它。还有更多细节，但大致看起来是这样的（供参考，我正在紧密跟随Filliatre关于有限自动机的论文）：Module FinS...
如何在Coq中仅展开一次递归函数
这里是一个递归函数all_zero，用于检查自然数列表中的所有成员是否都为零：Require Import Lists.List. Require Import Basics. Fixpoint all_zero ( l : list nat ) : bool := match l wi...
我能否告诉Coq从n归纳到n+2？
我试图从https://softwarefoundations.cis.upenn.edu/lf-current/Logic.html中证明evenb n = true <-> exists k, n = double k，而不涉及奇数。我尝试了以下内容： Theorem eve...
Coq QArith除以零的结果为零，为什么？
我注意到在Coq中有理数的定义中，0的倒数被定义为0。(通常情况下，除以零是没有被明确定义/合法/允许的。) 我注意到在Coq中有理数的定义中，0的倒数被定义为0。(通常情况下，除以零是没有被明确定义/合法/允许的。)Require Import QArith. Lemma inv_zer...
Coq: 在 Type(n) 中 Prop 和 Set 的区别
我希望考虑以下三个（相关的？）Coq定义。Inductive nat1: Prop := | z1 : nat1 | s1 : nat1 -> nat1. Inductive nat2 : Set := | z2 : nat2 | s2 : nat2 -> na...
在Coq中，无法使用let-destruct来处理元组。
我是Coq的新用户。我定义了一些函数: Definition p (a : nat) := (a + 1, a + 2, a + 3). Definition q := let (s, r, t) := p 1 in s + r + t. Definition q' := match p...
Coq中的逐步简化是什么？
有没有一种逐步简化的方法？假设你有f1(f2 x)，它们都可以通过单个simpl逐步简化，是否可以首先简化f2 x，然后检查中间结果，然后再简化f1？以定理为例：Theorem pred_length : forall n : nat, forall l : list nat, pred ...
如何将Coq中的Set或Type作为命题？
我正在阅读有关Coq的教程。它使用以下方式构造了一个bool类型：Coq < Inductive bool : Set := true | false. bool is defined bool_rect is defined bool_ind is defined bool_rec ...
Coq: 类型类 vs 依赖记录
我不太理解 Coq 中类型类和依赖记录之间的区别。参考手册提供了类型类的语法，但没有说明它们到底是什么以及应该如何使用它们。经过一番思考和搜索后，发现类型类本质上 是 带有一点语法糖的依赖记录，这使得 Coq 能够自动推断一些隐式实例和参数。当任意给定上下文中只有一个可能的类型类实例时，类型类...