Let's start off with the most basic philosophical question: What is True?

Straightforward enough. What is False?

We're not missing anything. False is simply an inductive type with no constructors. Like booleans and natural numbers, True and False have no special status. Let's define our own versions.

We can think of Coq Propositions as simply Types where we only care whether there is a term of of that type, not what that term is. Hence, we can equally well define as True as follows:

Traditionally, if we want to show that True'' is true, we state it as a lemma:

But we could also 'prove' it directly by exhibiting a term of type True''

This is actually what apply naturally produces!

We will return to the Coq proof engine at the end of this chapter.

Arrows, Functions and Implication

So far, we've portrayed Coq's arrow notation → as having two distinct meanings:

declares f as a function from nat to bool while

states the axiom P that False implies True. In fact, both f and P say "for every A, I can construct a B". Since we only care whether Props are inhabited by terms, we might summarize this as "if there is an A then there is a B" or "A implies B". But the proof demands constructing an element of Prop B, hence we call Coq a "constructive" logic. Here are the direct proofs of two basic theorems about True and False

That last one may seem funny, but we have indeed constructed an A for every element of F - vacuously! This corresponds exactly to our proof of ex_falso_quodlibet in Logic.v

You will have noticed that in the proofs above we wrote fun with two placeholders in constructing our proofs. This is because both ∀ and → correspond to function types. → 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: forall (x:nat), nat = forall (_:nat), nat = nat -> nat Hence, ∀ A, A → True is really ∀ (A : Prop) (_ : A), True

Exercise: 1 star, standard (A_then_A)

As a definition, show that A implies A

What does this correspond to computationally? ☐ You're probably familiar with these basic rules of logic, but we can easily express them as definitions:

Exercise: 1 star, standard (modus_tollens)

Prove modus tollens definitionally

Logical Connectives as Inductive Types

Inductive definitions are powerful enough to express most of the 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. We'll see these definitions in this section.

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 as consisting 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:

Exercise: 1 star, standard (and_assoc')

Construct a proof object (i.e. write a program) for and associativity.

Exercise: 2 stars, standard, optional (conj_fact)

Construct a proof object demonstrating the following proposition.

Disjunction

The inductive definition of disjunction uses two constructors, one for each side of the disjunct. This corresponds to a sum type in functional programming.

A quick example of a sum type in functional programming:

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.

Exercise: 1 star, standard (or_comm)

Write down an explicit proof object for or_comm (without using Print to peek at the ones we already defined!).

Exercise: 2 stars, standard, recommended (or_assoc)

Write down an explicit proof object for or_assoc.

Predicate Calculus and Dependent Types

So far, the logic we've expressed has been the simplest form of logic: Propositional Logic. In fact, we could write the proofs above in a simple polymorphic language like OCaml. To state more complicated propositions we will need dependent types. Consider the following inductive relations:

beautiful itself is not a proposition (or type), beautiful 2 and beautiful 3 are. That is, Coq allows our Props (and our types) to depend on terms. This allows us to state, and attempt to prove, the following:

In the second case we can state that three is beautiful, but we can't prove it. We can also try something more complex:

Note that the typechecker recognizes that in the only case of the match, n is 8.

Note the in and return in the match statement. in assigns a name to the arguments in type of w: specifically, it calls the argument to wonderous n₀. return then specifies the return type which may depend on the names assigned by in. Hence, Coq knows that it's trying to provide a beautiful n₀ for every wonderful n₀ and when n₀ is 8, the constructor b₈ suffices. Above Coq inferred the relevant parts of the match statement, but that tends to occur only in trivial cases. Most of the propositions we have looked at in this course use dependent types. Let's try to directly prove something about ev:

Exercise: 1 star, standard (ev_two)

Write a program proving that two is even

Existential Quantification

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

In English, for any predicate P, given an x and a term/proof of P x, we can construct a term/proof of ex P. Let's show that there is an x satisfying ev:

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

Equality

Even Coq's equality relation is not built in. It has the following inductive definition.

Of course, there are other, arguably more useful ways to define equality. Here's Leibniz's definition (and, as far as we know, not Newton's):

That is, 'a' is equal to 'b' if everything true of 'a' is true of 'b'. Let's show that eqL is at least as strong as eq.

This is actually easier to express definitionally, if harder to come up with.

Let's try going in the opposite direction.

For convenience, we can package these up into a single claim.

What does this tell us? It says that it's okay to replace a with b throughout a proposition if we know that eq a b. Let's try it out.

Exercise: 1 star, standard (eq_trans')

Exercise: Prove transitivity using our version of eq, which doesn't have rewrite.

Interlude: Dependent Types and Programming in the Proof Environment

You might be wondering: Given that we can write types in Coq that depend on terms, are there any interesting (non-proof) datatypes we can write? The answer is yes! We can write a variety of interesting datatypes in Coq that prevent common programming errors! For instance, here's a length-indexed list:

Exercise: 2 stars, standard (ilastn)

Use the proof environment to get the last n elements of an m + n ilist.

Exercise: 4 stars, standard, optional (bst)

Implement a dependently typed binary search tree and the efficient element_in procedure from the midterm. Prove that if an element is in the tree, the procedure finds it. ☐

Refine: Mixing the Program and Proof Environments