Coq中的“Error: Universe inconsistency”是什么意思？
我正在学习《软件基础》，目前在做关于“Church数”的练习。这里是自然数的类型签名：Definition nat := forall X : Type, (X -> X) -> X -> X. 我已经定义了一个类型为 nat -> nat 的函数 succ。现在我想这...
如何在Coq中切换当前的目标？
在 Coq 中是否可以切换当前目标或子目标以进行证明？ 例如，我有一个类似这样的目标（来自 eexists）：______________________________________(1/1) ?s > 0 /\ r1 * (r1 + s1) + ?s = r3 * (r3 + s...
在使用感应技术时如何保留信息？
我正在使用Coq证明助手实现一个（小型）编程语言的模型（扩展了Bruno De Fraine、Erik Ernst和Mario Südholt实现的Featherweight Java）。在使用归纳策略(induction tactic)时，经常遇到如何保留类型构造中包含的信息的问题。 我已...
Coq中的“Verbose”自动模式
我正在学习Coq，并且使用的教材是 (CPDT)，在证明中广泛使用了 auto。 由于我正在学习，因此我认为看到 auto 在幕后执行的确切步骤可能会对我有所帮助（起初尽量减少神秘感）。是否有任何方法可以强制它显示计算证明时使用的确切策略或技术？ 如果没有，请问是否有地方详细介绍了 aut...
在目标类型中局部抽象化子项的Ltac策略
作为一个粗糙而未受教育的背景，在HoTT中，人们通过推导归纳定义类型。 Inductive paths {X : Type } : X -> X -> Type := | idpath : forall x: X, paths x x. 这允许非常通用的构造 Lemma ...
要求，导入，要求导入
在 Coq 中，三个语句 Require X、Import X 和 Require Import X 有何不同？通常使用 Require Import X，但是也可以使用 Import ListNotation 或者 Require X。它们之间的区别是什么？请给出一些实际的例子。
为什么 Coq 中逻辑连接词和布尔值是分开的？
我来自JavaScript/Ruby编程背景，习惯于这是如何处理true/false（在JS中）：!true // false !false // true 然后您可以像这样使用这些 true/false 值与 && 一起使用var a = true, b = false; a...
在 Coq 中定义 Ackermann 函数时出现错误
我正在尝试在Coq中定义Ackermann-Peters函数，但是我收到了一个我不理解的错误消息。正如您所见，我正在将Ackermann的参数a、b打包成一对ab；我提供了一个用于定义参数排序的排序函数。然后，我使用Function表单来定义Ackermann本身，并为ab参数提供了排序函数。...
在Coq中规范计算理论
我尝试通过形式化推理来证明我熟悉的数学定理：停机问题的不可判定性，以及其他计算理论中的各种定理。由于我对计算模型（如图灵机、寄存器机、λ演算等）的细节不感兴趣，因此我试图通过假设 "Axiom" 来表述Coq认为可计算的函数（即类型为“nat -> nat”的可定义函数）的性质。 例如...