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

Question

在交互式定理证明器Coq的,任何交互证明或定义可与被终止Qed或Defined.有一些"不透明"的概念Qed强制执行但Defined不强制执行.例如,Adam Chlipala 撰写的" 依赖类型认证编程 "一书指出:

我们用" Defined而不是"结束"证据" Qed,以便我们构建的定义仍然可见.这与结束证明的情况形成对比Qed,其中证据的细节随后被隐藏.(更正式地,Defined将标识符标记为透明,允许它展开;同时Qed将标识符标记为不透明,防止展开.)

但是,我不太确定这在实践中意味着什么.有一个后来的例子,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,你只知道它是一个布尔值.

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. *)

Qedvs 背后的想法Defined是,在某些情况下,你不想看看证明术语的内容(因为它不相关,或者只是一个你不想展开的非常大的术语),以及你需要的所有内容知道这个陈述是真的,不是为什么它是真的.最后,你有问题要在使用前询问Qed或Defined为:我需要知道,为什么一个定理是真实的,还是我只需要知道这是真的吗？