“ Qed”和“ Qed”之间有什么区别？和“已定义”？ [英] What is the difference between "Qed" and "Defined"?

问题描述

在交互式定理证明者Coq中，可以使用 Qed 或 Defined 终止任何交互式证明或定义。 Qed 强制执行某些不透明概念，而 Defined 强制执行。例如，亚当·克莱帕拉（Adam Chlipala）撰写的《 具有依赖类型的认证编程》 ，状态：

In the interactive theorem prover Coq, any interactive proof or definition can be terminated with either Qed or Defined. There is some concept of "opacity" which Qed enforces but Defined does not. For instance, the book Certified Programming with Dependent Types, by Adam Chlipala, states:

我们以 已定义而不是 Qed ，因此我们构造的定义仍然可见。这与以 Qed 结尾的证明相反，后者的证明细节随后被隐藏。 （更正式地说，已定义将标识符标记为透明，允许其展开；而 Qed 将标识符标记为不透明，以防止展开。）

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

但是，我不确定这在实践中意味着什么。在后面的示例中，有必要使用已定义，原因是需要修复来检查某个证明的结构，但我不完全了解这种检查 ，或者为什么使用 Qed 会失败。 （查看 Fix 的定义也不是完全有启发性的。）

However, I'm not quite sure what this means in practice. There is a later example in which it is necessary to use Defined due to the need for Fix to inspect the structure of a certain proof, but I don't understand exactly what this "inspection" entails, or why it would fail if Qed were used instead. (Looking at the definition of Fix wasn't exactly enlightening either).

从表面上讲，很难分辨出什么 Qed 实际上在做。例如，如果我写：

Superficially, it's hard to tell what Qed is actually doing. For instance, if I write:

Definition x : bool.
exact false.
Qed.

我仍然可以看到 x 的值通过执行命令 Print x。另外，稍后允许我对 x ：

I can still see the value of x by executing the command Print x. In addition, I'm allowed later to pattern-match on the "opaque" value of x:

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

因此，看来我可以使用 x 就好。 Chlipala教授在这里展开是什么意思？不透明和透明差异到底有什么区别？最重要的是，修复有什么特别之处呢？

Therefore it seems like I'm able to use the value of x just fine. What does Prof. Chlipala mean by "unfolding" here? What exactly is the difference between an opaque and a transparent difference? Most importantly, what is special about Fix that makes this matter?

推荐答案

您实际上不能使用 x 的值，而只能使用其类型。例如，由于 x 为 false ，请尝试证明 x = false 或 x = true ，您将无法执行此操作。您可以展开 not_x 的定义（其定义与 x 相同，但使用已定义），但您将无法检查 x 的值，只知道它是布尔值。

You are not really able to use the value of x, but only its type. For example, since x is false, try to prove that x = false or that x = true, and you won't be able to. You can unfold the definition of not_x (its definition is the same as that of x, but using Defined), but you won't be able to inspect the value of x, you only know that it is a boolean.

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 vs 已定义的背后是，在某些情况下，您不想查看证明项的内容（因为它不相关，或者只是一个非常大的名词，您不想展示它），并且您只需要知道该语句是正确的，而不是为什么它是正确的即可。最后，在使用 Qed 或 Defined 之前，您要问的问题是：我是否需要知道为什么一个定理是正确的，或者我只需要知道它是正确的？

The idea behind Qed vs Defined is that in some cases, you don't want to look at the content of proof term (because it is not relevant, or just a really huge term you don't want to unfold), and all you need to know is that the statement is true, not why it is true. In the end, the question you have to ask before using Qed or Defined is: Do I need to know why one theorem is true, or do I only need to know that it is true?

这篇关于“ Qed”和“ Qed”之间有什么区别？和“已定义”？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！