-2
$\begingroup$

While examining the package Library ZFC.Sets, I found the following definition:

Definition Paire : forall E E' : Ens, Ens.
intros.
apply (sup bool).
simple induction 1.
exact E.
exact E'.
Defined.

I don't care, for the moment what is actually defined. What I do care about is that I don't understand this syntax for definitions. Up to now, I've seen definitions follow the syntax of Definition name : statement . This definition, however, is paired with a Defined. at the end, and includes various tactics. My question is: What kind of a definition is this, and where can I read about such definitions?

$\endgroup$
  • 1
    $\begingroup$ I don't think this question is suitable here, as it is not a research-level question in computer science. I've flagged it for migration to Stack Overflow, where questions about Coq are acceptable. Do not repost unless the question is closed here without being migrated. I recommend that you create an account on Stack Overflow so as to retain control of your question after the migration. $\endgroup$ – Gilles Apr 13 '12 at 23:13
  • $\begingroup$ Welcome to cstheory, a Q&A site for research-level questions in theoretical computer science (TCS). Your question does not appear to be a research-level question in TCS. Please see the FAQ for more information on what is meant by this and suggestions for sites that might welcome your question. Finally, if your question is closed for being out of scope, and you believe you can edit the question to make it a research-level question, please feel free to do so. Closing is not permanent and questions can be reopened, check the FAQ for more information. $\endgroup$ – Kaveh Apr 14 '12 at 4:55
  • 3
    $\begingroup$ @Gilles: It's not very consistent to suggest that this is off-topic and also to answer the question before the moderators could do anything about it. $\endgroup$ – Dave Clarke Apr 14 '12 at 17:12
  • $\begingroup$ And now that it has an accepted answer, I suggest we leave it here. Migrating doesn't really help at this point. $\endgroup$ – Suresh Venkat Apr 14 '12 at 17:46
  • 1
    $\begingroup$ @Gilles: Except that you give the question credibility here, which makes it more difficult to migrate. As Suresh says, it has an accepted answer, so it won't be migrated. $\endgroup$ – Dave Clarke Apr 14 '12 at 19:15
3
$\begingroup$

An important theoretical observation behind Coq is the Curry-Howard correspondence, which states that types and logical formulas are fundamentally the same thing, and so are programs and proofs. The intuition is that a proof is a program that constructs an object of the desired type; a formula is true if there is a way to construct a proof of it, i.e. the corresponding type is not empty. In this correspondence, applying a function is the modus ponens rule.

When you prove a theorem in Coq, Coq constructs a proof term behind the scenes. However, you state the proof in Coq's proof language, by stating a sequence of tactics to apply. Executing these tactics builds a term, which Coq typechecks when you write Qed; if the term has the desired type, i.e. proves the desired formula, then Coq accepts the proof. (The tactic language is constructed so that most tactic sequences form a valid proof when all subgoals are fulfilled, but this can be bypassed.)

You can terminate a proof with Defined instead of Qed. If you do that, the proof term is transparent, which means that you can make use of how the theorem has been proved. With Qed, the proof is opaque, so you know that the theorem holds, but you can't rely on its having any particular proof.

Knowing the way a theorem is proved is rarely useful. But theorems are the same as types; knowing a way to build a value of a type is often useful — the difference between + and * (both of type nat -> nat -> nat) is very often relevant. So ending a theorem with Defined is a way to define a term; if you do that, you might as well use the keyword Definition rather than Theorem or Lemma (and in fact the syntax treats these keywords as equivalent).

The reason one would use tactics rather than write out a proof term is that terms with heavily dependent types can be hard to write manually. Often, these terms are what you'd think of as data structures or functions building data structures with bits of proofs embedded in them. Since all Coq guarantees that you're building a term of the right type, you'd better carefully review the tactics when you do this, as it's easy to accidentally build a term which is not what you intended. The Program facility (which is more recent than the ZFC library) makes it easier to write such programs with embedded bits of proofs: you write the program bits as terms, and then complete the proof bits with tactics.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.