coq - 为什么策略 'exact' 对于 Coq 证明是完整的？

Question

在问题Is there a minimal complete set of tactics in Coq? ，答案提到 exact 足以证明所有目标。有人可以解释并举个例子吗？例如，A、B 为 Prop 的目标 A\/B -> B\/A 如何仅通过一堆 exact 来证明？如果您有其他更好的示例，请不要犹豫，也请回答。重点是对这个问题给出一些解释，并给出一个重要的例子。

Answer 1

回想一下，Coq 中的证明只是归纳构造的 (lambda) 微积分中的项。因此，您的引理被证明为:

Lemma test A B : A \/ B -> B \/ A.
Proof.
exact (fun x => match x with
  | or_introl p => or_intror p
  | or_intror p => or_introl p
  end).
Qed.

这几乎是一样的:

Definition test' A B : A \/ B -> B \/ A :=
fun x => match x with
  | or_introl p => or_intror p
  | or_intror p => or_introl p
  end.

[它们在“不透明度”方面有所不同，不用担心，但 Coq 8.8 可能会支持 Lemma foo := term 语法，更接近 exact term .]

构建证明的更方便的策略是refine，它允许您指定部分项:

Lemma test'' A B : A \/ B -> B \/ A.
Proof.
refine (fun x => _).
refine (match x with | or_introl _ => _ | or_intror _ => _ end).
+ refine (or_intror a).
+ refine (or_introl b).
Qed.

事实上，refine 是 Coq 证明引擎的基本策略； exact T 基本上执行 refine T 并检查是否没有目标保持开放。