Constructive logic

The logical aspects of Coq are based on constructive logic. In constructive logic, the proof of a sentence should always be constructed from the proofs of its constituents. More precisely:

• a proof of A /\ B is a proof of A combined with a proof of B
• a proof of A \/ B is either a proof of A or a proof of B
• a proof of A -> B is process by which, given a proof of A, we can construct a proof of B
• a proof of ~A is a process by which, if it were ever given a proof of A, we could construct a proof of an impossible proposition
• a proof of forall x. P(x) is a process by which, given some object a, we can construct a proof of P(a)
• a proof of exists x. P(x) is some object a combined with a proof of P(a)

This is different from classical logic. In classical logic:

• A \/ B is equivalent to ~(~A /\ ~B), and in particular A \/ ~A is a theorem
• A -> B is equivalent to ~(A /\ ~B)
• exists x. P(x) is equivalent to ~forall x. ~P(x)

In constructive logic, the implications hold from left to right, but not in the other direction.

Constructive proofs are more informative than classical ones. A constructive proof of A \/ B tells not only that one of A and B holds, but it also tells which one. A constructive proof of exists x. P(x) tells not only that there is some object for which P holds, but it also gives an example of such an object. Sometimes we can't give a constructive proof for a sentence we could prove classically.

The "processes" above should be "effective methods" of deriving one proof from another. In other words, computable functions. This immediately suggests that we can represent proofs as objects of a programming language, and processes as functions. This is the approach taken by Coq.

Once we have functions and other objects that are meant to represent proofs, we still have to answer what they are proofs of. We use types to represent propositions, and type checking makes sure that our objects are actually proofs of the propositions they are intended to prove.

Hence, in Coq proofs are just programs, no different from the "ordinary" programs we use for purely computational tasks. The difference is simply in how we interpret the programs and their types.

The Prop sort

We could in principle take the above at face value and e.g. prove the distributivity of conjunction and disjunction by writing a function with the type forall A B C : Type, A * (B + C) -> (A * B) + (A * C). However, this is not quite ideal, because then it's not obvious that this is intended to be a proof instead of a computational function.

To help make this distinction, Coq has Prop, which is a kind of an alternative to Type. There are some technical differences between them, but for us the most important one is in intent: if for some type P we have P : Prop, then we know that P is intended to be interpreted as a proposition. In particular, we are only interested in whether there is some term (proof) with type P or not, but we are not very interested in what the term is: one proof serves as well as another.

We can now define conjunction and disjunction. These inductive types are exactly similar to prod and sum, except that deal with Props, not Types.

We also often need the notion of equivalence between propositions, i.e. each implies the other. This is simply a conjunction of two implications.

Negation

Recall that the constructive notion of a proof of ~P is a process that shows that if we had a proof of P, we could construct a proof of a falsehood, an impossible proposition. What is this impossible proposition? We could choose arbitrarily some proposition that we believe to be false, but there is a more principled approach available.

A logic is consistent if not all propositions in it are provable. An inconsistent logic would be quite useless, so we have to assume that Coq is consistent (and in fact this has been proven). Hence, it is impossible that we could prove every proposition.

This suggests the following definition of falsehood:

This would in fact work just fine, but in Coq it is usually preferrable to use inductive types when possible. This is just a matter of style and convenience.

What should the inductive type be like? We want it to be one that is impossible to construct. Hence, it should have no constructors:

This is equivalent to the above definition of Absurd. From False, we can derive any proposition. Recall that when pattern matching a value of in inductive type A to produce a term of type B, we have to give a term of type B for every possible constructor of A. Since False has zero constructors, we don't need to give any such terms when matching it:

Now that we have a suitable definition of falsehood, we can define a neat syntax for negations.

As an example of propositions involving negation, let's consider one of De Morgan's laws: for any propositions P and Q, ~(P \/ Q) is equivalent with ~P /\ ~Q. Recall that equivalence means that each implies the other. Let's handle each direction separately.

To prove ~(P \/ Q) -> ~P /\ ~Q informally, the argument is simple. Suppose that P \/ Q is false. Then P can't be true, because if P were true, P \/ Q would be true, and that would lead to contradiction. By a similar argument, Q can't be true either. Hence ~P /\ ~Q.

Formally, we need to construct a term with type ~(P \/ Q) -> ~P /\ ~Q, as the first step, we need a process (function) for proving ~P /\ ~Q, when given ~(P \/ Q).

Let npvq be a proof of ~(P \/ Q), i.e. (P \/ Q) -> False. We need to prove the conjunction ~P /\ ~Q. We construct such a proof with conj. We now need proofs of ~P and ~Q as its arguments.

To prove ~P, we let p be a proof of P, and we need to give a proof of False. We can get one by applying npvq and giving it a proof of P \/ Q. We can get that by applying or_introl to the proof of P. Similarly for ~Q, except we use or_intror.

We end up with the following function:

The other direction is left as an exercise.

There is another De Morgan's law: the equivalence between ~P \/ ~Q and ~(P /\ Q). Here is a proof from left to right:

However, the other direction cannot be proven in constructive logic.

Truth

Every now and then we have need for "just some true proposition". While in principle we could pick some arbitrary proposition that we have proven, it's clearer to have a dedicated type for this purpose.

A proof of True is always of the form I. It does not tell us anything interesting, but it is trivial to prove.

Equality

What does it mean for two objects to be equal? A common definition is the so-called Leibniz equality: two objects are equal, if they have exactly the same properties. That is, a and b are equal, if for any property P, we have P a <-> P b. It turns out that it is in fact sufficient to have just one-way implication, and the other direction can be derived. (This is left as an exercise.)

Hence, we get the following definition for Leibniz equality:

There is something special about this definition. So far, we have had three different kinds of functions:

• functions from terms to terms, e.g. pred : nat -> nat
• functions from types to types, e.g. option : Type -> Type
• functions from types to terms, e.g. None : forall A : Type, option A

These correspond to the Haskell and ML concepts of ordinary functions, type constructors (polymorphic types), and polymorphic terms. However, leq takes terms (of type A), and returns a type (recall that propositions are just special kinds of types). In its definition, P does the same thing. This cannot be done (directly) in traditional programming languages.

This feature of the language, dependent types proper, allows us to have types (propositions) that talk about individual terms (objects), and gives Coq the power of predicate logic.

What can we do with Leibniz equality? For one thing, we can prove that it is reflexive, i.e. every object is equal to itself:

We can use reflexivity to prove computational equalities trivially.

This type-checks because the type checker evaluates 3 + 5, 2 * 4 and 8 to see that they are all the same. This is one reason why it's so crucial that the evaluation of terms always terminates: types can contain terms, and we need to evaluate them during type checking, and we definitely want type checking to terminate.

As long as we are discussing definite, concrete objects, like above, equality is quite boring. We don't need to prove a theorem to say that 2 + 2 = 4, since it is trivially true by computation. Equality becomes much more interesting when used in more general contexts, where the terms in the equality contain parameter variables. We can't just compute them away.

As an example, let's consider the sentence forall n m, leq n m -> leq (S n) (S m), i.e. successors of equals are equal. To prove this, we use the equality between n and m to show that a property that holds for n (its successor is equal to S n by reflexivity) also holds for m.

Another way of thinking about Leibniz equality is that it means substitutability: if a and b are equal, then whenever we have a proposition of the form ... a ..., then we also have a proposition of the form ... b ..., where a has just been substituted with b. We get it by invoking the equality by using a property of the form fun x => ... x .... We did this above.

However, the power of equality is not limited to plain substitutions. Recall that type checking in Coq involves computation. Hence, to show that Q implies R, given leq a b, we just need some property P such that P a evaluates to Q, and P b evaluates to R.

We use this technique in the proof of the injectivity of the successor function, below. S n has the property that its predecessor is equal to n. If S m is equal to S n, then it has the property as well. Since by computation pred (S m) evaluates to m, this means that m is equal to n.

Standard equality

The definition of leq above is a perfectly reasonable way define equality. However, like in the case of Absurd previously, it's not the "Coq way". Instead, an inductive type is used. Coq's infrastructure is heavily tied to the standard library definition of equality, so we will henceforth use that instead of defining our own. The standard definition looks approximately like this (in its own module, to avoid shadowing):

There is also a standard notation by which eq a b can be written as a = b.

The definition of eq gives us, for each a, the property of "being equal to a", and states that the only object that has this property is a. Note that here, too, we have a type that depends on terms, though now the type is inductive.

In fact eq is equivalent with our definition of leq earlier. Given eq a b, and some property P such that P a, we can get P b. However, the proof of this may be somewhat befuddling:

What happened here? We had pa : P a, pattern matched on something with just a single zero-argument constructor, and then the type checker accepted our pa as having the type P b. What happened was that Coq did some deep magic under the hood. Some of it can be seen by printing out the above definition in the form in which Coq ultimately sees it:

At this point we are on the verge of delving too deeply into the intricacies of Coq's type system. It becomes obvious that as we begin using standard equality, our proof terms become so hairy that writing them by hand becomes too difficult, and we need another way to develop proofs.