In previous chapters, we have seen many examples of factual claims (propositions) and ways of presenting evidence of their truth (proofs). In particular, we have worked extensively with equality propositions of the form e1 = e2, with implications (P → Q), and with quantified propositions (∀ x, P). In this chapter we take a deeper look at the way propositions are expressed in Coq and at the structure of the logical evidence that we construct when we carry out proofs. Some of the concepts in this chapter may seem a bit abstract on a first encounter. We've included a lot of exercises, most of which should be quite approachable even if you're still working on understanding the details of the text. Try to work as many of them as you can, especially the one-starred exercises.

Inductively Defined Propositions

As a running example for the first part of the chapter, let's consider a simple property of natural numbers, and let's say that the numbers possessing this property are "beautiful." Informally, a number is beautiful if it is 0, 3, 5, or the sum of two beautiful numbers. More pedantically, we can define beautiful numbers by giving four rules:

• Rule b_0: The number 0 is beautiful.
• Rule b_3: The number 3 is beautiful.
• Rule b_5: The number 5 is beautiful.
• Rule b_sum: If n and m are both beautiful, then so is their sum.

We will see many definitions like this one during the rest of the course, and for purposes of informal discussions, it is helpful to have a lightweight notation that makes them easy to read and write. Inference rules are one such notation:

	(b_0)
beautiful 0

	(b_3)
beautiful 3

	(b_5)
beautiful 5

beautiful n     beautiful m	(b_sum)
beautiful (n+m)

Each of the textual rules above is reformatted here as an inference rule; the intended reading is that, if the premises above the line all hold, then the conclusion below the line follows. For example, the rule b_sum says that, if n and m are both beautiful numbers, then it follows that n+m is beautiful too. The rules with no premises above the line are called axioms. These rules define the property beautiful. That is, if we want to convince someone that some particular number is beautiful, our argument must be based on these rules. For a simple example, suppose we claim that the number 5 is beautiful. To support this claim, we just need to point out that rule b_5 says it is. Or, if we want to claim that 8 is beautiful, we can support our claim by first observing that 3 and 5 are both beautiful (by rules b_3 and b_5) and then pointing out that their sum, 8, is therefore beautiful by rule b_sum. This argument can be expressed graphically with the following proof tree: Of course, there are other ways of using these rules to argue that 8 is beautiful — for instance:

Exercise: 1 star (varieties_of_beauty)

How many different ways are there to show that 8 is beautiful?

☐ In Coq, we can express the definition of beautiful as follows:

The first line declares that beautiful is a proposition — or, more formally, a family of propositions "indexed by" natural numbers. (For each number n, the claim that "n is beautiful" is a proposition.) Such a family of propositions is often called a property of numbers. Each of the remaining lines embodies one of the rules for beautiful numbers. We can use Coq's tactic scripting facility to assemble proofs that particular numbers are beautiful.

Proof Objects

Look again at the formal definition of the beautiful property. The opening keyword, Inductive, has been used up to this point to declare new types of data, such as numbers and lists. Does this interpretation also make sense for the Inductive definition of beautiful? That is, can we view evidence of beauty as some kind of data structure? Yes, we can! 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 ":" as "has type" and : as "is a proof of" is called the Curry-Howard correspondence (or sometimes Curry-Howard isomorphism). It proposes a deep connection between the world of logic and the world of computation.

                 propositions  ~  types
                 evidence      ~  data 

Many useful things follow from this connection. To begin with, it gives us a natural interpretation of the b_sum constructor: If we read : as "has type," this says that b_sum is a data constructor that takes four arguments: two numbers, n and m, and two values of type beautiful n and beautiful m. That is, b_sum can be viewed as a function that, given evidence for the propositions beautiful n and beautiful m, gives us evidence for the proposition that beautiful (n+m). In view of this, we might wonder whether we can write an expression of type beautiful 8 by applying b_sum to appropriate arguments. 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. In the Show Proof output, lines of the form ?1 → beautiful n record these requirements. (The → here has nothing to do with either implication or function types — it is just an unfortunate choice of concrete syntax for the output!) 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 because they avoid building proof trees by hand, but they are not essential: in principle, we can always construct the required evidence by hand. Indeed, we don't even need the Theorem command: we can use Definition instead, to directly give a global name 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.

☐

Implications and Functions

If we want to substantiate the claim that P → Q, what sort of proof object should count as evidence? We've seen one case above: the b_sum constructor, which is primitive evidence for an implication proposition — it is part of the very meaning of the word "beautiful" in this context. But what about other implications that we might want to prove? For example, consider this statement:

What is the proof object corresponding to b_plus3? We've made a notational pun between → as implication and → as the type of functions. If we take this pun seriously, then what we're looking for is 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:

Exercise: 2 stars (b_times2)

☐

Exercise: 3 stars, optional (b_times2')

Write a proof object corresponding to b_times2 above

Exercise: 2 stars (b_timesm)

☐

Induction Over Proof Objects

Since we use the keyword Induction to define primitive propositions together with their evidence, we might wonder whether there are some sort of induction principles associated with these definitions. Indeed there are, and in this section we'll take a look at how they can be used. Besides constructing evidence that numbers are beautiful, we can also reason about such evidence. The fact that we introduced beautiful with an Inductive declaration tells us not only that the constructors b_0, b_3, b_5 and b_sum are ways to build evidence, but also that these two constructors are the only ways to build evidence that numbers are beautiful. In other words, if someone gives us evidence E justifying the assertion beautiful n, then we know that E can only have one of four forms: either E is b_0 (and n is O) or E is b_3 (and n is 3), or E is b_5 (and n is 5), or E is b_sum n1 n2 E1 E2 (and n is (n1+n2), and E1 is evidence that n1 is beauiful and E2 is evidence that n2 is beautiful). Thus, it makes sense to use the tactics that we have already seen for inductively defined data to reason instead about inductively defined evidence. Let's introduce a new property of numbers to help illustrate the role of induction.

Exercise: 1 star (gorgeous_tree)

Write out the definition of gorgeous numbers using the inference rule notation. (* FILL IN HERE *)
☐ It seems intuitively obvious that, although gorgeous and beautiful are presented using slightly different rules, they are actually the same property in the sense that they are true of the same numbers. Indeed, we can prove this.

Let's see what happens if we try to prove this by induction on n instead of induction on the evidence H.

Exercise: 1 star (gorgeous_plus13)

☐

Exercise: 2 stars (gorgeous_plus13_po):

Give the proof object for theorem gorgeous_plus13 above.

☐

Exercise: 2 stars (gorgeous_sum)

☐

Exercise: 3 stars (beautiful__gorgeous)

☐

Exercise: 3 stars, optional (b_times2)

Prove the g_times2 theorem below without using gorgeous__beautiful. You might find the following helper lemma useful.

☐

Evenness

In chapter Basics we defined a function evenb that tests a number for evenness, yielding true if so. This gives us an obvious way of defining the concept of evenness:

That is, we can define "n is even" to mean "the function evenb returns true when applied to n." Another alternative is to define the concept of evenness directly. Instead of going via the evenb function ("a number is even if a certain computation yields true"), we can say what the concept of evenness means by giving two different ways of presenting evidence that a number is even.

This definition says that there are two ways to give evidence that a number m is even. First, 0 is even, and ev_0 is evidence for this. Second, if m = S (S n) for some n and we can give evidence e that n is even, then m is also even, and ev_SS n e is the evidence.

Exercise: 1 star (double_even)

Construct a tactic proof of the following proposition.

☐

Exercise: 4 stars, optional (double_even_pfobj)

Try to predict what proof object is constructed by the above tactic proof. (Before checking your answer, you'll want to strip out any uses of Case, as these will make the proof object look a bit cluttered.) ☐

Discussion: Computational vs. Inductive Definitions

We have seen that the proposition "some number is even" can be phrased in two different ways — indirectly, via a boolean testing function evenb, or directly, by inductively describing what constitutes evidence for evenness. These two ways of defining evenness are about equally easy to state and work with. Which we choose is basically a question of taste. However, for many other properties of interest, the direct inductive definition is preferable, since writing a testing function may be awkward or even impossible. One such property is beautiful. This is a perfectly sensible definition of a set of numbers, but we cannot translate its definition directly as a Coq Fixpoint (or translate it directly into a recursive function in any other programming language). We might be able to find a clever way of testing this property using a Fixpoint (indeed, it is not too hard to find one in this case), but in general this could require arbitrarily deep thinking. In fact, if the property we are interested in is uncomputable, then we cannot define it as a Fixpoint no matter how hard we try, because Coq requires that all Fixpoints correspond to terminating computations. On the other hand, writing an inductive definition of what it means to give evidence for the property beautiful is straightforward.

Inverting Evidence

Besides induction, we can use the other tactics in our toolkit with evidence. For example, this proof uses destruct on evidence.

Exercise: 1 star, optional (ev_minus2_n)

What happens if we try to destruct on n instead of E? ☐

Exercise: 1 star, recommended (ev__even)

Here is a proof that the inductive definition of evenness implies the computational one.

Could this proof also be carried out by induction on n instead of E? If not, why not?

☐ The induction principle for inductively defined propositions does not follow quite the same form as that of inductively defined sets. For now, you can take the intuitive view that induction on evidence ev n is similar to induction on n, but restricts our attention to only those numbers for which evidence ev n could be generated. We'll look at the induction principle of ev in more depth below, to explain what's really going on.

Exercise: 1 star (l_fails)

The following proof attempt will not succeed. Briefly explain why. (* FILL IN HERE *)
☐

Exercise: 2 stars (ev_sum)

Here's another exercise requiring induction.

☐ Here's another situation where we want to analyze evidence for evenness: proving that if n+2 is even, then n is. Our first idea might be to use destruct for this kind of case analysis:

In the first sub-goal, we've lost the information that n is 0. We could have used remember, but then we still need inversion on both cases.

There is a much simpler way to this: we can use inversion directly on the inductively defined proposition ev (S (S n)).

This use of inversion may seem a bit mysterious at first. Until now, we've only used inversion on equality propositions, to utilize injectivity of constructors or to discriminate between different constructors. But we see here that inversion can also be applied to analyzing evidence for inductively defined propositions. Here's how inversion works in general. Suppose the name I refers to an assumption P in the current context, where P has been defined by an Inductive declaration. Then, for each of the constructors of P, inversion I generates a subgoal in which I has been replaced by the exact, specific conditions under which this constructor could have been used to prove P. Some of these subgoals will be self-contradictory; inversion throws these away. The ones that are left represent the cases that must be proved to establish the original goal. In this particular case, the inversion analyzed the construction ev (S (S n)), determined that this could only have been constructed using ev_SS, and generated a new subgoal with the arguments of that constructor as new hypotheses. (It also produced an auxiliary equality, which happens to be useless here.) We'll begin exploring this more general behavior of inversion in what follows.

Exercise: 1 star (inversion_practice)

The inversion tactic can also be used to derive goals by showing the absurdity of a hypothesis.

☐ We can generally use inversion on inductive propositions. This illustrates that in general, we get one case for each possible constructor. Again, we also get some auxiliary equalities that are rewritten in the goal but not in the other hypotheses.

Exercise: 3 stars, recommended (ev_ev__ev)

Finding the appropriate thing to do induction on is a bit tricky here:

☐

Exercise: 3 stars, optional (ev_plus_plus)

Here's an exercise that just requires applying existing lemmas. No induction or even case analysis is needed, but some of the rewriting may be tedious. You'll want the replace tactic used for plus_swap' in Basics.v

☐

Programming with Propositions

A proposition is a statement expressing a factual claim, like "two plus two equals four." In Coq, propositions are written as expressions of type Prop. Although we haven't mentioned it explicitly, we have already seen numerous examples.

Both provable and unprovable claims are perfectly good propositions. Simply being a proposition is one thing; being provable is something else!

Both 2 + 2 = 4 and 2 + 2 = 5 are legal expressions of type Prop. We've seen one way that propositions can be used in Coq: in Theorem (and Lemma and Example) declarations.

But they can be used in many other ways. For example, we can give a name to a proposition using a Definition, just as we have given names to expressions of other sorts (numbers, functions, types, type functions, ...).

Now we can use this name in any situation where a proposition is expected — for example, as the claim in a Theorem declaration.

There are many ways of constructing propositions. We can define a new proposition primitively using Inductive, we can form an equality proposition from two computational expressions, and we can build up a new proposition from existing ones using implication and quantification.

Also, given a proposition P with a free variable n, we can form the proposition ∀ n, P.

We can also define parameterized propositions, such as the property of being even.

The type of even, nat→Prop, can be pronounced in three equivalent ways: (1) "even is a function from numbers to propositions," (2) "even is a family of propositions, indexed by a number n," or (3) "even is a property of numbers." Propositions — including parameterized propositions — are first-class citizens in Coq. For example, we can define them to take multiple arguments...

... and then partially apply them:

We can even pass propositions — including parameterized propositions — as arguments to functions:

Here are two more examples of passing parameterized propositions as arguments to a function. The first takes a proposition P as argument and builds the proposition that P is true for all natural numbers. The second takes P and builds the proposition that, if P is true for some natural number n', then it is also true by the successor of n' — i.e. that P is preserved by successor:

Induction Principles

This is a good point to pause and take a deeper look at induction principles in general.

Induction Principles for Inductively Defined Types

Every time we declare a new Inductive datatype, Coq automatically generates an axiom that embodies an induction principle for this type. The induction principle for a type t is called t_ind. Here is the one for natural numbers:

The induction tactic is a straightforward wrapper that, at its core, simply performs apply t_ind. To see this more clearly, let's experiment a little with using apply nat_ind directly, instead of the induction tactic, to carry out some proofs. Here, for example, is an alternate proof of a theorem that we saw in the Basics chapter.

This proof is basically the same as the earlier one, but a few minor differences are worth noting. First, in the induction step of the proof (the "S" case), we have to do a little bookkeeping manually (the intros) that induction does automatically. Second, we do not introduce n into the context before applying nat_ind — the conclusion of nat_ind is a quantified formula, and apply needs this conclusion to exactly match the shape of the goal state, including the quantifier. The induction tactic works either with a variable in the context or a quantified variable in the goal. Third, the apply tactic automatically chooses variable names for us (in the second subgoal, here), whereas induction lets us specify (with the as... clause) what names should be used. The automatic choice is actually a little unfortunate, since it re-uses the name n for a variable that is different from the n in the original theorem. This is why the Case annotation is just S — if we tried to write it out in the more explicit form that we've been using for most proofs, we'd have to write n = S n, which doesn't make a lot of sense! All of these conveniences make induction nicer to use in practice than applying induction principles like nat_ind directly. But it is important to realize that, modulo this little bit of bookkeeping, applying nat_ind is what we are really doing.

Exercise: 2 stars, optional (plus_one_r')

Complete this proof as we did mult_0_r' above, without using the induction tactic.

☐ The induction principles that Coq generates for other datatypes defined with Inductive follow a similar pattern. If we define a type t with constructors c1 ... cn, Coq generates a theorem with this shape: The specific shape of each case depends on the arguments to the corresponding constructor. Before trying to write down a general rule, let's look at some more examples. First, an example where the constructors take no arguments:

Exercise: 1 star (rgb)

Write out the induction principle that Coq will generate for the following datatype. Write down your answer on paper, and then compare it with what Coq prints.

☐ Here's another example, this time with one of the constructors taking some arguments.

Exercise: 1 star (natlist1)

Suppose we had written the above definition a little differently:

Now what will the induction principle look like? ☐ From these examples, we can extract this general rule:

• The type declaration gives several constructors; each corresponds to one clause of the induction principle.
• Each constructor c takes argument types a1...an.
• Each ai can be either t (the datatype we are defining) or some other type s.
• The corresponding case of the induction principle says (in English):
  • "for all values x1...xn of types a1...an, if P holds for each of the xs of type t, then P holds for c x1 ... xn".

Exercise: 1 star (ex_set)

Here is an induction principle for an inductively defined set. Give an Inductive definition of ExSet:

☐ What about polymorphic datatypes? The inductive definition of polymorphic lists is very similar to that of natlist. The main difference is that, here, the whole definition is parameterized on a set X: that is, we are defining a family of inductive types list X, one for each X. (Note that, wherever list appears in the body of the declaration, it is always applied to the parameter X.) The induction principle is likewise parameterized on X: Note the wording here (and, accordingly, the form of list_ind): The whole induction principle is parameterized on X. That is, list_ind can be thought of as a polymorphic function that, when applied to a type X, gives us back an induction principle specialized to the type list X.

Exercise: 1 star (tree)

Write out the induction principle that Coq will generate for the following datatype. Compare your answer with what Coq prints.

☐

Exercise: 1 star (mytype)

Find an inductive definition that gives rise to the following induction principle: ☐

Exercise: 1 star, optional (foo)

Find an inductive definition that gives rise to the following induction principle: ☐

Exercise: 1 star, optional (foo')

Consider the following inductive definition:

What induction principle will Coq generate for foo'? Fill in the blanks, then check your answer with Coq.) ☐

Induction Hypotheses

Where does the phrase "induction hypothesis" fit into this story? The induction principle for numbers is a generic statement that holds for all propositions P (strictly speaking, for all families of propositions P indexed by a number n). Each time we use this principle, we are choosing P to be a particular expression of type nat→Prop. We can make the proof more explicit by giving this expression a name. For example, instead of stating the theorem mult_0_r as "∀ n, n * 0 = 0," we can write it as "∀ n, P_m0r n", where P_m0r is defined as...

... or equivalently...

Now when we do the proof it is easier to see where P_m0r appears.

This extra naming step isn't something that we'll do in normal proofs, but it is useful to do it explicitly for an example or two, because it allows us to see exactly what the induction hypothesis is. If we prove ∀ n, P_m0r n by induction on n (using either induction or apply nat_ind), we see that the first subgoal requires us to prove P_m0r 0 ("P holds for zero"), while the second subgoal requires us to prove ∀ n', P_m0r n' → P_m0r n' (S n') (that is "P holds of S n' if it holds of n'" or, more elegantly, "P is preserved by S"). The induction hypothesis is the premise of this latter implication — the assumption that P holds of n', which we are allowed to use in proving that P holds for S n'.

Optional Material

This section offers some additional details on how induction works in Coq and the process of building proof trees. It can safely be skimmed on a first reading. (We recommend skimming rather than skipping over it outright: it answers some questions that occur to many Coq users at some point, so it is useful to have a rough idea of what's here.)

Induction Principles in Prop

Earlier, we looked in detail at the induction principles that Coq generates for inductively defined sets. The induction principles for inductively defined propositions like gorgeous are a tiny bit more complicated. As with all induction principles, we want to use the induction principle on gorgeous to prove things by inductively considering the possible shapes that something in gorgeous can have — either it is evidence that 0 is gorgeous, or it is evidence that, for some n, 3+n is gorgeous, or it is evidence that, for some n, 5+n is gorgeous and it includes evidence that n itself is. Intuitively speaking, however, what we want to prove are not statements about evidence but statements about numbers. So we want an induction principle that lets us prove properties of numbers by induction on evidence. For example, from what we've said so far, you might expect the inductive definition of gorgeous... ...to give rise to an induction principle that looks like this... ... because:

• Since gorgeous is indexed by a number n (every gorgeous object e is a piece of evidence that some particular number n is gorgeous), the proposition P is parameterized by both n and e — that is, the induction principle can be used to prove assertions involving both a gorgeous number and the evidence that it is gorgeous.
• Since there are three ways of giving evidence of gorgeousness (gorgeous has three constructors), applying the induction principle generates three subgoals:
  • We must prove that P holds for O and b_0.
  • We must prove that, whenever n is a gorgeous number and e is an evidence of its gorgeousness, if P holds of n and e, then it also holds of 3+m and g_plus3 n e.
  • We must prove that, whenever n is a gorgeous number and e is an evidence of its gorgeousness, if P holds of n and e, then it also holds of 5+m and g_plus5 n e.
• If these subgoals can be proved, then the induction principle tells us that P is true for all gorgeous numbers n and evidence e of their gorgeousness.

But this is a little more flexibility than we actually need or want: it is giving us a way to prove logical assertions where the assertion involves properties of some piece of evidence of gorgeousness, while all we really care about is proving properties of numbers that are gorgeous — we are interested in assertions about numbers, not about evidence. It would therefore be more convenient to have an induction principle for proving propositions P that are parameterized just by n and whose conclusion establishes P for all gorgeous numbers n: For this reason, Coq actually generates the following simplified induction principle for gorgeous:

In particular, Coq has dropped the evidence term e as a parameter of the the proposition P, and consequently has rewritten the assumption ∀ (n : nat) (e: gorgeous n), ... to be ∀ (n : nat), gorgeous n → ...; i.e., we no longer require explicit evidence of the provability of gorgeous n. In English, gorgeous_ind says:

• Suppose, P is a property of natural numbers (that is, P n is a Prop for every n). To show that P n holds whenever n is gorgeous, it suffices to show:
  • P holds for 0,
  • for any n, if n is gorgeous and P holds for n, then P holds for 3+n,
  • for any n, if n is gorgeous and P holds for n, then P holds for 5+n.

We can apply gorgeous_ind directly instead of using induction.

Exercise: 3 stars, optional (p_provability)

Consider the following inductively defined proposition:

Describe, in English, the conditions under which the proposition p t n is provable. (* FILL IN HERE *)
☐

More on the induction Tactic

The induction tactic actually does even more low-level bookkeeping for us than we discussed above. Recall the informal statement of the induction principle for natural numbers:

• If P n is some proposition involving a natural number n, and we want to show that P holds for all numbers n, we can reason like this:
  • show that P O holds
  • show that, if P n' holds, then so does P (S n')
  • conclude that P n holds for all n.

So, when we begin a proof with intros n and then induction n, we are first telling Coq to consider a particular n (by introducing it into the context) and then telling it to prove something about all numbers (by using induction). What Coq actually does in this situation, internally, is to "re-generalize" the variable we perform induction on. For example, in the proof above that plus is associative...

It also works to apply induction to a variable that is quantified in the goal.

Note that induction n leaves m still bound in the goal — i.e., what we are proving inductively is a statement beginning with ∀ m. If we do induction on a variable that is quantified in the goal after some other quantifiers, the induction tactic will automatically introduce the variables bound by these quantifiers into the context.

Exercise: 1 star, optional (plus_explicit_prop)

Rewrite both plus_assoc' and plus_comm' and their proofs in the same style as mult_0_r'' above — that is, for each theorem, give an explicit Definition of the proposition being proved by induction, and state the theorem and proof in terms of this defined proposition.

☐

One more quick digression, for adventurous souls: if we can define parameterized propositions using Definition, then can we also define them using Fixpoint? Of course we can! However, this kind of "recursive parameterization" doesn't correspond to anything very familiar from everyday mathematics. The following exercise gives a slightly contrived example.

Exercise: 4 stars, optional (true_upto_n__true_everywhere)

Define a recursive function true_upto_n__true_everywhere that makes true_upto_n_example work.

☐

Building Proof Objects Incrementally

As you probably noticed while solving the exercises earlier in the chapter, constructing proof objects is more involved than constructing the corresponding tactic proofs. Fortunately, there is a bit of syntactic sugar that we've already introduced to help in the construction: the admit term, which we've sometimes used to force Coq into accepting incomplete exercies. As an example, let's walk through the process of constructing a proof object demonstrating the beauty of 16.

Maybe we can use b_sum to construct a term of type beautiful 16? Recall that b_sum is of type If we can demonstrate the beauty of 5 and 11, we should be done.

In the attempt above, we've omitted the proofs of the propositions that 5 and 11 are beautiful. But the first of these is already axiomatized in b_5:

What remains is to show that 11 is beautiful. We repeat the procedure:

And finally, we can complete the proof object:

To recap, we've been guided by an informal proof that we have in our minds, and we check the high level details before completing the intricacies of the proof. The admit term allows us to do this.

Additional Exercises

Exercise: 4 stars, recommended (palindromes)

A palindrome is a sequence that reads the same backwards as forwards.

• Define an inductive proposition pal on list X that captures what it means to be a palindrome. (Hint: You'll need three cases. Your definition should be based on the structure of the list; just having a single constructor
  c : ∀ l, l = rev l → pal l
  may seem obvious, but will not work very well.)
• Prove that
   ∀ l, pal (l ++ rev l).
• Prove that
   ∀ l, pal l → l = rev l.

☐

Exercise: 5 stars, optional (palindrome_converse)

Using your definition of pal from the previous exercise, prove that

☐

Exercise: 4 stars (subsequence)

A list is a subsequence of another list if all of the elements in the first list occur in the same order in the second list, possibly with some extra elements in between. For example, is a subsequence of each of the lists but it is not a subsequence of any of the lists

• Define an inductive proposition subseq on list nat that captures what it means to be a subsequence. (Hint: You'll need three cases.)
• Prove that subsequence is reflexive, that is, any list is a subsequence of itself.
• Prove that for any lists l1, l2, and l3, if l1 is a subsequence of l2, then l1 is also a subsequence of l2 ++ l3.
• (Optional, harder) Prove that subsequence is transitive — that is, if l1 is a subsequence of l2 and l2 is a subsequence of l3, then l1 is a subsequence of l3. Hint: choose your induction carefully!

☐

Exercise: 2 stars, optional (foo_ind_principle)

Suppose we make the following inductive definition: Fill in the blanks to complete the induction principle that will be generated by Coq. ☐

Exercise: 2 stars, optional (bar_ind_principle)

Consider the following induction principle: Write out the corresponding inductive set definition. ☐

Exercise: 2 stars, optional (no_longer_than_ind)

Given the following inductively defined proposition: write the induction principle generated by Coq. ☐

Exercise: 2 stars, optional (R_provability)

Suppose we give Coq the following definition: Which of the following propositions are provable?

• R 2 [1,0]
• R 1 [1,2,1,0]
• R 6 [3,2,1,0]

☐