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

Question

问题中的答案提到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.

[它们在 "opacity" 上有所不同，不用担心，但 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 并检查没有目标保持打开状态。

Answer 2

由于其理论基础，Coq 的逻辑并不依赖策略作为构建证明的原始方式。事实上，您可以使用 Coq 构建被认为是合法的证明，而无需使用惯用语的任何策略。

Lemma test3 A B : A \/ B -> B \/ A.
Proof 
 fun x => match x with
    or_introl p => or_intror p 
                  | or_introl p => or_introl p
 end.

所以“成套战术”的问题，意义不大。

另一方面，引入了策略来简化工作。因此，了解一套 相当完整的策略 是很有用的，这使得即使不完全了解 Coq 的理论基础也可以执行证明。我最喜欢的策略是：

intros,apply（处理全称量化和蕴涵）；
destruct（处理逻辑连接词and，也写成/\和or，也写成\/，以及存在量词，当在假设);
split在目标结束时处理and；
left,right处理or在目标结束时。
exists在结论中处理一个存在量化，
assert 建立中间事实（完整性不需要，但它确实可以帮助您编写更具可读性的证明），
exact 和 assumption 当你想要证明的内容从上下文中非常明显时。

在推理自然数时，您无疑会通过模式匹配和递归定义函数并推理它们的行为，因此了解策略也很重要 change、simpl、case、case_eq、injection 和 discriminate 最后，当您开始制作足够先进的证明时，您需要像 ring 和 [=34 这样的自动证明工具=].

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

Why would the tactic 'exact' be complete for Coq proofs?

coq

coq-tactic