代码之家 › 专栏 › 技术社区 › Jian Wang

为什么Coq证明的策略“精确”是完整的?

coq-tactic coq

2

Jian Wang · 技术社区 · 8 年前

在问题中 Is there a minimal complete set of tactics in Coq? ,答案提到 exact 足以证明所有的进球。有人能解释一下并举个例子吗?例如,目标是什么 A \/ B -> B \/ A 准确的

2 回复 | 直到 8 年前

1

8

ejgallego 8 年前

回想一下,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.

事实上 精炼 exact T 基本上执行 refine T

2

3

Yves 4 年前

由于其理论基础,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 处理 和 在目标结束时;
left right 处理在进球结束时。
exists 为了在结论中处理存在量化,
assert
exact 和 assumption 当你想证明的东西从上下文来看是显而易见的时候。

在对自然数进行推理时,您无疑会通过模式匹配和递归定义函数,并对其行为进行推理,因此了解策略也很重要 change simpl case , case_eq , injection discriminate 最后,当你开始做足够先进的证明时,你需要自动化证明的工具,如 ring lia