ProofObjectsWorking with Explicit Evidence in Coq

We have seen that Coq has mechanisms both for programming, using inductive data types (like nat or list) and functions over these types, and for proving properties of these programs, using inductive propositions (like ev or eq), implication, and universal quantification. So far, we have treated these mechanisms as if they were quite separate, and for many purposes this is a good way to think. But we have also seen hints that Coq's programming and proving facilities are closely related. For example, the keyword Inductive is used to declare both data types and propositions, and → is used both to describe the type of functions on data and logical implication. This is not just a syntactic accident! In fact, programs and proofs in Coq are almost the same thing. In this chapter we will study how this works. We have already seen the fundamental idea: provability in Coq is represented by concrete evidence. When we construct the proof of a basic proposition, we are actually building a tree of evidence, which can be thought of as a data structure. If the proposition is an implication like A → B, then its proof will be an evidence transformer: a recipe for converting evidence for A into evidence for B. So at a fundamental level, proofs are simply programs that manipulate evidence. Q. If evidence is data, what are propositions themselves? A. They are types! Look again at the formal definition of the beautiful property.

The trick is to introduce an alternative pronunciation of ":". Instead of "has type," we can also say "is a proof of." For example, the second line in the definition of beautiful declares that b_0 : beautiful 0. Instead of "b_0 has type beautiful 0," we can say that "b_0 is a proof of beautiful 0." Similarly for b_3 and b_5. 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        ~  data values

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

This can be read "b_sum is a constructor that takes four arguments — two numbers, n and m, and two values, of types beautiful n and beautiful m — and yields evidence for the proposition beautiful (n+m)." Now let's look again at a previous proof involving beautiful.

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

In view of this, we might wonder whether we can write such an expression ourselves. Indeed, we can:

The expression b_sum 3 5 b_3 b_5 can be thought of as instantiating the parameterized constructor b_sum with the specific arguments 3 5 and the corresponding proof objects for its premises beautiful 3 and beautiful 5 (Coq is smart enough to figure out that 3+5=8). Alternatively, we can think of b_sum as a primitive "evidence constructor" that, when applied to two particular numbers, wants to be further applied to evidence that those two numbers are beautiful; its type, [ ∀ n m, beautiful n → beautiful m → beautiful (n+m), ] expresses this functionality, in the same way that the polymorphic type ∀ X, list X in the previous chapter expressed the fact that the constructor nil can be thought of as a function from types to empty lists with elements of that type. This gives us an alternative way to write the proof that 8 is beautiful:

Notice that we're using apply here in a new way: instead of just supplying the name of a hypothesis or previously proved theorem whose type matches the current goal, we are supplying an expression that directly builds evidence with the required type.

Proof Scripts and Proof Objects

These proof objects lie at the core of how Coq operates. When Coq is following a proof script, what is happening internally is that it is gradually constructing a proof object — a term whose type is the proposition being proved. The tactics between the Proof command and the Qed instruct Coq how to build up a term of the required type. To see this process in action, let's use the Show Proof command to display the current state of the proof tree at various points in the following tactic proof.

At any given moment, Coq has constructed a term with some "holes" (indicated by ?1, ?2, and so on), and it knows what type of evidence is needed at each hole. Each of the holes corresponds to a subgoal, and the proof is finished when there are no more subgoals. At this point, the Theorem command gives a name to the evidence we've built and stores it in the global context. Tactic proofs are useful and convenient, but they are not essential: in principle, we can always construct the required evidence by hand, as shown above. Then we can use Definition (rather than Theorem) to give a global name directly to a piece of evidence.

All these different ways of building the proof lead to exactly the same evidence being saved in the global environment.

Exercise: 1 star (six_is_beautiful)

Give a tactic proof and a proof object showing that 6 is beautiful.

☐

Exercise: 1 star (nine_is_beautiful)

Give a tactic proof and a proof object showing that 9 is beautiful.

☐

Quantification, Implications and Functions

In Coq's computational universe (where we've mostly been living until this chapter), there are two sorts of values with arrows in their types: constructors introduced by Inductive-ly defined data types, and functions. Similarly, in Coq's logical universe, there are two ways of giving evidence for an implication: constructors introduced by Inductive-ly defined propositions, and... functions! For example, consider this statement:

What is the proof object corresponding to b_plus3? We're looking for an expression whose type is ∀ n, beautiful n → beautiful (3+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:

Recall that fun n => blah means "the function that, given n, yields blah." Another equivalent way to write this definition is:

When we view the proposition being proved by b_plus3 as a function type, one aspect of it may seem a little unusual. The second argument's type, beautiful n, mentions the value of the first argument, n. While such dependent types are not commonly found in programming languages, even functional ones like ML or Haskell, they can be useful there too. 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 LHS of the arrow. For example, consider this proposition:

A proof term inhabiting this proposition would be a function with two arguments: a number n and some evidence E that n is beautiful. But the name E for this evidence is not used in the rest of the statement of funny_prop1, so it's a bit silly to bother making up a name for it. We could write it like this instead, using the dummy identifier _ in place of a real name:

Or, equivalently, we can write it in more familiar notation:

In general, "P → Q" is just syntactic sugar for "∀ (_:P), Q".

Exercise: 3 stars (b_times2)

First prove this theorem using tactics.

☐ Now write a corresponding proof object directly.

☐

Exercise: 2 stars, optional (gorgeous_plus13_po)

Give a proof object corresponding to the theorem gorgeous_plus13 from Prop.v

☐ It is particularly revealing to look at proof objects involving the logical connectives that we defined with inductive propositions in Logic.v.

Let's take a look at the proof object for the above theorem.

Note that the proof is of the form as you'd expect, given the type of conj.

Exercise: 1 star, optional (case_proof_objects)

The Case tactics were commented out in the proof of and_example to avoid cluttering the proof object. What would you guess the proof object will look like if we uncomment them? Try it and see. ☐

Once again, we have commented out the Case tactics to make the proof object for this theorem easier to understand. It is still a little complicated, but after performing some simple reduction steps, we can see that all that is really happening is taking apart a record containing evidence for P and Q and rebuilding it in the opposite order:

After simplifying some direct application of fun expressions to arguments, we get:

Exercise: 2 stars, optional (conj_fact)

Construct a proof object demonstrating the following proposition.

☐

Exercise: 2 stars, advanced (beautiful_iff_gorgeous)

We have seen that the families of propositions beautiful and gorgeous actually characterize the same set of numbers. Prove that beautiful n ↔ gorgeous n for all n. Just for fun, write your proof as an explicit proof object, rather than using tactics. (Hint: if you make use of previously defined theorems, you should only need a single line!)

☐

Exercise: 2 stars, optional (or_commut'')

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

☐ Recall that we model an existential for a property as a pair consisting of a witness value and a proof that the witness obeys that property. We can choose to construct the proof explicitly. For example, consider this existentially quantified proposition:

To prove this proposition, we need to choose a particular number as witness — say, 4 — and give some evidence that that number is even.

Exercise: 2 stars (ex_beautiful_Sn)

Complete the definition of the following proof object:

☐

Giving Explicit Arguments to Lemmas and Hypotheses

Even when we are using tactic-based proof, it can be very useful to understand the underlying functional nature of implications and quantification. For example, it is often convenient to apply or rewrite using a lemma or hypothesis with one or more quantifiers or assumptions already instantiated in order to direct what happens. For example:

In this case, giving just one argument would be sufficient.

Arguments must be given in order, but wildcards (_) may be used to skip arguments that Coq can infer.

The author of a lemma can choose to declare easily inferable arguments to be implicit, just as with functions and constructors. The with clauses we've already seen is really just a way of specifying selected arguments by name rather than position:

Exercise: 2 stars (trans_eq_example_redux)

Redo the proof of the following theorem (from MoreCoq.v) using an apply of trans_eq but not using a with clause.

☐

Programming with Tactics

If we can build proofs with explicit terms rather than tactics, you may be wondering if we can build programs using tactics rather than explicit terms. Sure!

Notice that we terminate the Definition with a . rather than with := followed by a term. This tells Coq to enter proof scripting mode to build an object of type nat → nat. Also, we terminate the proof with Defined rather than Qed; this makes the definition transparent so that it can be used in computation like a normally-defined function. This feature is mainly useful for writing functions with dependent types, which we won't explore much further in this book. But it does illustrate the uniformity and orthogonality of the basic ideas in Coq.