Programming and proving in Coq are two sides of the same coin. Proofs manipulate evidence, much as programs manipulate data. Question: If evidence is data, what are propositions themselves? Answer: They are types!

Look again at the formal definition of the ev property.

Suppose we introduce an alternative pronunciation of ":". Instead of "has type," we can say "is a proof of." For example, the second line in the definition of ev declares that ev_0 : ev 0. Instead of "ev_0 has type ev 0," we can say that "ev_0 is a proof of ev 0."

This pun between types and propositions -- between : as "has type" and : as "is a proof of" or "is evidence for" -- is called the Curry-Howard correspondence. It proposes a deep connection between the world of logic and the world of computation:

                 propositions  ~  types
                 proofs        ~  programs

See [Wadler 2015] for a brief history and up-to-date exposition.

Many useful insights follow from this connection. To begin with, it gives us a natural interpretation of the type of the ev_SS constructor:

This can be read "ev_SS is a constructor that takes two arguments -- a number n and evidence for the proposition ev n -- and yields evidence for the proposition ev (S (S n))."

Now let's look again at a previous proof involving ev.

As with ordinary data values and functions, we can use the Print command to see the proof object that results from this proof script.

Indeed, we can also write down this proof object directly, without the need for a separate proof script:

Similarly, as we've seen, we can directly apply theorems to arguments in proof scripts:

Proof Scripts

When we write a proof using tactics, what we are doing is instructing Coq to build a proof object under the hood. We can see this using Show Proof:

Tactic proofs are convenient, but they are not essential in Coq: in principle, we can always just construct the required evidence by hand. Then we can use Definition (rather than Theorem) to introduce a global name for this evidence.

Quantifiers, Implications, Functions

In Coq's computational universe (where data structures and programs live), there are two sorts of values that have arrows in their types: constructors introduced by Inductively defined data types, and functions. Similarly, in Coq's logical universe (where we carry out proofs), there are two ways of giving evidence for an implication: constructors introduced by Inductively defined propositions, and... functions!

For example, consider this statement:

What is the proof object corresponding to ev_plus4?

We're looking for an expression whose type is ∀ n, ev n → ev (4 + n) -- that is, a function that takes two arguments (one number and a piece of evidence) and returns a piece of evidence! Here it is:

Or equivalently:

When we view the proposition being proved by ev_plus4 as a function type, one interesting point becomes apparent: The second argument's type, ev n, mentions the value of the first argument, n. While such dependent types are not found in most mainstream programming languages, they can be quite useful in programming too, as the flurry of activity in the functional programming community over the past couple of decades demonstrates.

Notice that both implication (→) and quantification (∀) correspond to functions on evidence. In fact, they are really the same thing: → is just a shorthand for a degenerate use of ∀ where there is no dependency, i.e., no need to give a name to the type on the left-hand side of the arrow:
           ∀ (x:nat), nat
        = ∀ (_:nat), nat
        = nat → nat

Programming with Tactics

If we can build proofs by giving explicit terms rather than executing tactic scripts, you may be wondering whether we can build programs using tactics rather than by writing down explicit terms. Naturally, the answer is yes!

Logical Connectives as Inductive Types

Inductive definitions are powerful enough to express most of the logical connectives we have seen so far. Indeed, only universal quantification (with implication as a special case) is built into Coq; all the others are defined inductively. Let's see how.

Conjunction

To prove that P ∧ Q holds, we must present evidence for both P and Q. Thus, it makes sense to define a proof object for P ∧ Q to consist of a pair of two proofs: one for P and another one for Q. This leads to the following definition.

Notice the similarity with the definition of the prod type, given in chapter Poly; the only difference is that prod takes Type arguments, whereas and takes Prop arguments.

This similarity should clarify why destruct and intros patterns can be used on a conjunctive hypothesis. Case analysis allows us to consider all possible ways in which P ∧ Q was proved -- here just one (the conj constructor).

Similarly, the split tactic actually works for any inductively defined proposition with exactly one constructor. In particular, it works for and:

This shows why the inductive definition of and can be manipulated by tactics as we've been doing. We can also use it to build proofs directly, using pattern-matching. For instance:

Disjunction

The inductive definition of disjunction uses two constructors, one for each side of the disjunct:

This declaration explains the behavior of the destruct tactic on a disjunctive hypothesis, since the generated subgoals match the shape of the or_introl and or_intror constructors.

Once again, we can also directly write proof objects for theorems involving or, without resorting to tactics.

Existential Quantification

To give evidence for an existential quantifier, we package a witness x together with a proof that x satisfies the property P:

The more familiar form ∃ x, ev x desugars to an expression involving ex:

Here's how to define an explicit proof object involving ex:

To destruct existentials in a proof term we simply use match:

True and False

The inductive definition of the True proposition is simple:

It has one constructor (so every proof of True is the same, so being given a proof of True is not informative.)

False is equally simple -- indeed, so simple it may look syntactically wrong at first glance!

That is, False is an inductive type with no constructors -- i.e., no way to build evidence for it. For example, there is no way to complete the following definition such that it succeeds.

But it is possible to destruct False by pattern matching. There can be no patterns that match it, since it has no constructors. So the pattern match also is so simple it may look syntactically wrong at first glance.

Since there are no branches to evaluate, the match expression can be considered to have any type we want, including 0 = 1. Fortunately, it's impossible to ever cause the match to be evaluated, because we can never construct a value of type False to pass to the function.

Equality

Even Coq's equality relation is not built in. We can define it ourselves:

Coq terms are "the same" if they are convertible according to a simple set of computation rules: evaluation of function applications, inlining of definitions, and simplification of matches.

reflexivity is essentially just apply eq_refl.

We can also pattern-match on an equality proof:

A tactic-based proof runs into some difficulties if we try to use our usual repertoire of tactics, such as rewrite and reflexivity. Those work with *setoid* relations that Coq knows about, such as =, but not our ==. We could prove to Coq that == is a setoid, but a simpler way is to use destruct and apply instead.

Coq's Trusted Computing Base

The Coq typechecker is what actually checks our proofs. We have to trust it, but it's relatively small and straightforward. For example, it rejects this broken proof:

And these:

Complex tactics can (in principle and occasionally in practice) produce invalid proof objects. Qed runs the type checker to detect such situations.