coq - 如何在 Coq 中留下未完成的目标

Question

在 Isabelle 中，您可以通过两种方式留下未完成的目标：

• 对不起：会留下你的证明，这个事实可以在以后的证明中使用。
• 哎呀：将留下证明，但事实不能在以后的证明中使用。

Coq 中是否有类似的功能可以让我留下未完成的目标以便稍后返回？这对于在不填写所有细节的情况下勾勒出证明的结构很有用。请注意如何在 Coq 中切换当前目标中的方法？修改证明结构。这不是我要找的。

标签： coq

Answer 1

在 Coq 中有几种方法可以终止证明。您可能知道Qed哪个断言证明已完成。Defined当您希望证明具有计算内容时，也可以使用。

您正在寻找的东西是：

• Admitted它承认证明，因此以后可以使用；
• Abort它放弃了证明引理。

它们可以这样使用：

Lemma foo : forall n, n = 0.
Proof.
  intro n. destruct n.
  - reflexivity.
  -
Abort.

Lemma bar : forall n, n = n.
Admitted.

Admitted在这两种情况下，您都可以在/之前有一个部分证明脚本，Abort或者根本没有。

正如@HTNW 指出的那样，您还可以使用等效的策略admit和give_up证明的内部子目标。然而，使用这些，证明必须使用Admitted或来结束Abort。

Lemma lem : forall A, A + A -> A.
Proof.
  intros A h.
  destruct h.
  - admit.
  - give_up.
Admitted.

无论如何，这个解决方案都抛弃了部分证明。如果出于某种原因您想继续使用部分证明（例如，如果您想用它进行计算），一个常见的技巧是使用公理来关闭您想要稍后留下的目标。

Axiom cheating : forall A, A.

Tactic Notation "cheat" := apply cheating.

Lemma lem : forall A, A + A -> A.
Proof.
  intros A h.
  destruct h.
  - cheat.
  - cheat.
Defined. (* This is now ok *)

但是，您必须小心使用该技巧。您可以使用Print Assumptions lem. 如果它说“在上下文中关闭”你很好，否则它会列出它所依赖的公理，如果cheating出现你知道它没有被完全证明。