What is the difference between "Qed" and "Defined"?

Question

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:

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

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

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

Definition x : bool.
exact false.
Qed.

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.

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?

Answer 1

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

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?