Proof. 是什么意思？简单。反身性。 Qed。在 Coq 中是什么意思？

【问题标题】：What does Proof. simpl. reflexivity. Qed. mean in Coq?Proof. 是什么意思？简单。反身性。 Qed。在 Coq 中是什么意思？
【发布时间】：2020-10-07 14:47:02
【问题描述】：

我正在阅读《软件基础》这本书，但一开始就卡住了。

作者定义了一个布尔类型和常用操作：

Inductive bool: Type :=
  | true 
  | false.

Definition orb (b1: bool) (b2: bool) : bool :=
  match b1 with
  | true => true
  | false => b2
  end.

假设我们要证明 or 函数的正确性。作者写了一个测试，然后是一个证明：

Example test_orb1: (orb true false) = true.
Proof. simpl. reflexivity. Qed.

谁能向我解释一下简单。反身性 是什么意思？还有其他方法可以证明这个简单的测试吗？

【问题讨论】：

标签： coq

【解决方案1】：

simpl 是一种评估目标的策略。在您的情况下，执行后，目标将留给true = true。 reflexivity 是一种实现x = x 形式的目标的策略（最简单的化身）。它的底层功能是提供证明术语 eq_refl : x = x 作为当前证明义务的解决方案。

现在，有很多方法可以实现这件事，最终会产生相同的（相当简单的）证明eq_refl（尝试做Print test_orb1.）。首先，不需要simpl 操作，因为 Coq 在应用一个术语时会进行一些计算（特别是在调用reflexivity 时）。其次，调用constructor、apply eq_refl或refine eq_refl可以获得与reflexivity相同的效果。这些是具有不同目标的策略，但恰好在这里重合。

【讨论】：