<p>An important theoretical observation behind Coq is the <a href="http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence" rel="nofollow">Curry-Howard correspondence</a>, 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 <a href="http://en.wikipedia.org/wiki/Implication_elimination" rel="nofollow"><em>modus ponens</em></a> rule.</p>

<p>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 <code>Qed</code>; 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.)</p>

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

<p>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 <code>+</code> and <code>*</code> (both of type <code>nat -&gt; nat -&gt; nat</code>) is very often relevant. So ending a theorem with <code>Defined</code> is a way to define a term; if you do that, you might as well use the keyword <code>Definition</code> rather than <code>Theorem</code> or <code>Lemma</code> (and in fact the <a href="http://coq.inria.fr/refman/Reference-Manual003.html#toc13" rel="nofollow">syntax</a> treats these keywords as equivalent).</p>

<p>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 <a href="http://coq.inria.fr/refman/Reference-Manual028.html" rel="nofollow"><code>Program</code></a> facility (which is more recent than the <code>ZFC</code> 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.</p>

CC BY-SA 3.0
2012-04-13T23:10:07.747Z
2012-04-13T23:10:07.747Z
Gilles 'SO- stop being evil'
<p>While examining the package Library <code>ZFC.Sets</code>, I found the following definition:</p>

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

<p>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?</p>

CC BY-SA 3.0
2012-04-13T23:13:25.543Z
I don't think this question is suitable here, as it is not a [research-level question in computer science](http://cstheory.stackexchange.com/). I've flagged it for migration to [so], 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 [so] so as to retain control of your question after the migration.
Gilles 'SO- stop being evil'
CC BY-SA 3.0
2012-04-14T04:55:31.877Z
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.
Kaveh
CC BY-SA 3.0
2012-04-14T17:12:47.483Z
@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.
Dave Clarke
CC BY-SA 3.0
2012-04-14T17:46:22.217Z
And now that it has an accepted answer, I suggest we leave it here. Migrating doesn't really help at this point.
Suresh Venkat
CC BY-SA 3.0
2012-04-14T18:23:23.903Z
@DaveClarke Uh? I expected it to be migrated to a site where it would be on-topic. No sense in holding off answering until the migration happens.
Gilles 'SO- stop being evil'
CC BY-SA 3.0
2012-04-14T19:15:14.023Z
@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.
Dave Clarke
CC BY-SA 3.0
2012-04-15T01:52:51.867Z
@Gilles, on csthoery we don't answer clearly off-topic questions. You should wait till the question is migrated (if migrated) to answer an off-topic question.
Kaveh
<lo.logic><coq><proof-assistants>
Coq definition with unusual syntax (Definition ... Defined.)
Mayer Goldberg
# Coq definition with unusual syntax (Definition ... Defined.)

(Asked by: username_0 on 2012-04-13)

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?

**Tags:** lo.logic, coq, proof-assistants
> **Comments:**
> **username_1**: I don't think this question is suitable here, as it is not a [research-level question in computer science](http://cstheory.stackexchange.com/). I've flagged it for migration to [so], 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 [so] so as to retain control of your question after the migration.  
> **username_2**: 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.  
> **username_3**: @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.  
> **username_4**: And now that it has an accepted answer, I suggest we leave it here. Migrating doesn't really help at this point.  
> **username_1**: @DaveClarke Uh? I expected it to be migrated to a site where it would be on-topic. No sense in holding off answering until the migration happens.  
> **username_3**: @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.  
> **username_2**: @Gilles, on csthoery we don't answer clearly off-topic questions. You should wait till the question is migrated (if migrated) to answer an off-topic question.  

---

## 1 answers

### Answer by username_1 on 2012-04-13. Score: 3 | Accepted answer

An important theoretical observation behind Coq is the [Curry-Howard correspondence](http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_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*](http://en.wikipedia.org/wiki/Implication_elimination) 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](http://coq.inria.fr/refman/Reference-Manual003.html#toc13) 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`](http://coq.inria.fr/refman/Reference-Manual028.html) 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.


---

