scope - "Qed"和 "Defined"有什么区别？

Question

在交互式定理证明器 Coq 中，任何交互式证明或定义都可以用 Qed 终止。或 Defined .有一些“不透明度”的概念 Qed强制执行但 Defined才不是。例如，Adam Chlipala 所著的《Certified Programming with Dependent Types》一书，states :

We end the "proof" with Defined instead of Qed, so that the definition we constructed remains visible. This contrasts to the case of ending a proof with Qed, where the details of the proof are hidden afterward. (More formally, Defined marks an identifier as transparent, allowing it to be unfolded; while Qed marks an identifier as opaque, preventing unfolding.)

但是，我不太确定这在实践中意味着什么。后面还有 example其中需要使用 Defined由于需要 Fix检查某个证明的结构，但我不明白这种“检查”到底意味着什么，或者如果 Qed 会失败，为什么会失败。改为使用。 (查看 Fix 的定义也不完全有启发性)。

从表面上看，很难说是什么 Qed实际上是在做。例如，如果我写:

Definition x : bool.
exact false.
Qed.

我仍然可以看到 x 的值通过执行命令 Print x.此外，我可以稍后对 x 的“不透明”值进行模式匹配。 :

Definition not_x : bool :=
  match x with
    | true => false
    | false => true
  end.

因此，我似乎可以使用 x 的值正好。 Chlipala 教授在这里所说的“展开”是什么意思？不透明和透明的区别到底是什么？最重要的是 Fix的特别之处这有什么关系？

Answer 1

您不能真正使用 x 的值。 ，但仅限于它的类型。例如，由于 x是 false ，尝试证明x = false或者那个x = true ，而你将无法做到。您可以展开not_x的定义(其定义与 x 相同，但使用 Defined )，但您将无法检查 x 的值，你只知道它是一个 bool 值。

Lemma not_x_is_true : not_x = true.
Proof.
unfold not_x. (* this one is fine *)
unfold x. (* This one is not. Error: Cannot coerce x to an evaluable reference. *)

背后的理念 Qed对比 Defined是在某些情况下，您不想查看证明项的内容(因为它不相关，或者只是一个您不想展开的非常大的项)，您只需要知道陈述是真的，而不是为什么它是真的。最后，你在使用前要问的问题 Qed或 Defined是:我需要知道为什么一个定理是真的，还是我只需要知道它是真的？