为什么Coq证明的"准确"策略是完整的？

Question

在问题中Coq中有一套最小的完整策略吗？,提到的答案exact足以证明所有目标.有人可以解释一下吗？例如,A \/ B -> B \/ AA,B作为Prop 的目标如何仅通过一堆来证明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并检查没有目标保持打开状态.