如何在Coq中切换当前的目标？
在 Coq 中是否可以切换当前目标或子目标以进行证明？ 例如，我有一个类似这样的目标（来自 eexists）：______________________________________(1/1) ?s > 0 /\ r1 * (r1 + s1) + ?s = r3 * (r3 + s...
如何在Coq中证明排中律不可驳斥？
我正在尝试证明在线课程中的以下简单定理：排中律是不可反驳的，但在第一步就卡住了。 Theorem excluded_middle_irrefutable: forall (P:Prop), ~~(P \/ ~ P). Proof. intros P. unfold not. intros...
Coq中的非空列表追加定理
我正在尝试在Coq中证明以下引理：Require Import Lists.List. Import ListNotations. Lemma not_empty : forall (A : Type) (a b : list A), (a <> [] \/ b <&...
Coq中分号“;”和句点“.”之间的执行区别
给定一个使用“;”策略的有效Coq证明，是否存在一般公式可以将其转换为使用“.”替代“;”的有效等价证明？ 许多Coq证明使用“;”或策略序列策略。作为初学者，我想观察每个步骤的执行情况，因此我想用“.”替换“;”，但令我惊讶的是，这可能会破坏证明。 关于“;”的文档很少，我没有在任何地方...
我该如何在Coq中将“+1”（加一）重写为“S”（后继）？
我有一个引理，但证明不完整： Lemma s_is_plus_one : forall n:nat, S n = n + 1. Proof. intros. reflexivity. Qed. 这个证明失败了： Unable to unify "n + 1" with "S n...
Coq中revert和generalize策略有什么区别？
根据 Coq 参考手册(8.5p1)的说法，我认为 revert 是 intro 的反义词，但在一定程度上 generalize 也是。例如，下面的 revert 和 generalize dependent 看起来是相同的。 Goal forall x y: nat, 1 + x = 2 ...
Coq中是否有一组最小完整的策略？
我见过很多Coq策略在功能上有重叠。 例如，当你在假设中确切地有结论时，你可以使用assumption、apply、exact、trivial，也许还有其他的。其他例子包括非归纳类型的destruct和induction。 我的问题是： 是否存在一组最小的基本策略（不包括auto及其类似...
如何在Coq中使用自定义归纳原理？
我读到类型归纳原理只是一个关于命题P的定理。因此，我基于右（或反向）列表构造器构建了一个List的归纳原理。 Definition rcons {X:Type} (l:list X) (x:X) : list X := l ++ x::nil. 归纳原理本身是： Definiti...
Coq：尽管已经设置了“Hint Unfold”，为什么我需要手动展开一个值？
我想出了以下的玩具证明脚本： Inductive myType : Type := | c : unit -> myType. Inductive myProp : myType -> Type := | d : forall t, myProp (c t). Hint Con...
能否在Coq中将统一错误转化为目标？
我一直在使用Coq对过程演算进行形式化（代码库在这里），常常发现自己尝试应用一个函数时会失败，因为等价但语法不同的子项。这往往是由于操作de Bruijn变量引起的。当统一失败时，通常我会事先明确地替换掉行为不良的子项，然后再应用所需的函数。下面是一个简单的代码示例，以说明我的意思： Req...