Inductively Defined Propositions

In the Logic chapter, we looked at several ways of writing propositions, including conjunction, disjunction, and existential quantification. In this chapter, we bring yet another new tool into the mix: inductively defined propositions. To begin, some examples...

The Collatz Conjecture

The Collatz Conjecture is a famous open problem in number theory. Its statement is surprisingly simple. First, we define a function f on numbers, as follows:

Next, we look at what happens when we repeatedly apply f to some given starting number. For example, f 12 is 6, and f 6 is 3, so by repeatedly applying f we get the sequence 12, 6, 3, 10, 5, 16, 8, 4, 2, 1. Similarly, if we start with 19, we get the longer sequence 19, 58, 29, 88, 44, 22, 11, 34, 17, 52, 26, 13, 40, 20, 10, 5, 16, 8, 4, 2, 1. Both of these sequences eventually reach 1. The question posed by Collatz was: Does the sequence starting from any natural number eventually reach 1? To formalize this question in Coq, we might try to define a recursive function that computes the total number of steps that it takes for such a sequence to reach 1.

This definition is rejected by Coq's termination checker, since the argument to the recursive call, f n, is not "obviously smaller" than n. Indeed, this isn't just a silly limitation of the termination checker. Functions in Coq are required to be total, and checking that this particular function is total would be equivalent to settling the Collatz conjecture! Fortunately, there is another way to do it: We can express the concept "reaches 1 eventually" as an inductively defined property of numbers reaches1 : nat → Prop. Intuitively, this property is defined by a set of rules:

	(reach_one)
reaches1 1

Even n      reaches1 (div2 n)	(reach_even)
reaches1 n

~Even n     reaches1 ((3 * n) + 1)	(reach_odd)
reaches1 n

So there are three ways to prove that a number n reaches 1 in the Collatz sequence:

• n is 1;
• n is even and div2 n reaches 1;
• n is odd and (3 × n) + 1 reaches 1.

We can prove that a number reaches 1 by constructing a (finite) derivation using these rules. For instance, here is the derivation proving that 12 reaches 1 (where we left out the evenness/oddness premises):
                        ——————————— (reach_one)
                        reaches1 1
                        ——————————— (reach_even)
                        reaches1 2
                        ——————————— (reach_even)
                        reaches1 4
                        ——————————— (reach_even)
                        reaches1 8
                        ——————————— (reach_even)
                        reaches1 16
                        ——————————— (reach_odd)
                        reaches1 5
                        ——————————— (reach_even)
                        reaches1 10
                        ——————————— (reach_odd)
                        reaches1 3
                        ——————————— (reach_even)
                        reaches1 6
                        ——————————— (reach_even)
                        reaches1 12 Formally in Coq, reaches1 is an inductively defined property of numbers:

The details of how such inductive definitions are written are not important and will be explained later. For the moment, note that the 3 constructors correspond exactly to the 3 rules above. The Collatz conjecture then states that the sequence beginning from any number reaches 1:

If you succeed in proving this conjecture, you've got a bright future as a number theorist. But don't spend too long on it -- it's been open since 1937!

Binary relations

A binary relation on a set X has Coq type X → X → Prop. This is a family of propositions parameterized by two elements of X -- i.e., a proposition about pairs of elements of X. For example, a familiar binary relation on nat is le : nat → nat → Prop, the less-than-or-equal-to relation, which can be inductively defined by the following two rules:

	(le_n)
le n n

le n m	(le_S)
le n (S m)

These rules say that there are two ways to show that one number is less than or equal to another: either observe that they are the same number, or, if the second has the form S m, give evidence that the first is less than or equal to m. This corresponds to the following inductive definition in Coq:

This is a bit simpler and more elegant than the Boolean function leb we defined in Basics. As usual, le and leb are equivalent, and there is an exercise about that.

The Collatz step function f also allows us to define a corresponding binary relation:

This Collatz step relation is useful in conjunction with the reflexive and transitive closure operation below.

Reflexive and Transitive Closure

The reflexive and transitive closure of a relation R is the smallest relation that contains R and that is reflexive and transitive. This can be defined by the following three rules:

R x y	(rt_step)
clos_refl_trans R x y

	(rt_refl)
clos_refl_trans R x x

clos_refl_trans R x y    clos_refl_trans R y z	(rt_trans)
clos_refl_trans R x z

Computing the reflexive and transitive closure can be undecidable even for a relation R that is decidable (e.g. collatz_step_rel), so in general we can't expect to define reflexive and transitive closure as a boolean function. Fortunately, Coq allows us to define reflexive and transitive closure as an inductive relation directly encoding the three rules above:

The reflexive and transitive closure of a binary relation cannot, in general, be expressed in first-order logic. The logic of Coq is, however, much more powerful, and can easily define such inductive relations. This enables an equivalent definition of the Collatz conjecture:

This cms (Collatz multi-step) relation defined in terms of clos_refl_trans allows for more interesting derivations than the linear ones of the directly defined reaches1 relation:

f 16 = 8 f 8 = 4 f 4 = 2 f 2 = 1
————————(rt_step) ———————(rt_step) ———————(rt_step) ———————(rt_step)
cms 16 8 cms 8 4 cms 4 2 cms 2 1
—————————————————————————(rt_trans) ————————————————————————(rt_trans)
        cms 16 4 cms 4 1
        —————————————————————————————————————————————(rt_trans)
                           cms 16 1

Exercise: 1 star, standard, optional (close_refl)

How would you modify this definition so that it defines transitive closure (i.e. not reflexive)? How about reflexive, symmetric, and transitive closure?

Permutations

The familiar mathematical concept of permutation also has an elegant formulation as an inductive relation. For simplicity, let's focus on permutations of lists with exactly three elements. We can define them by the following rules:

	(perm3_swap12)
Perm3 [a;b;c] [b;a;c]

	(perm3_swap23)
Perm3 [a;b;c] [a;c;b]

Perm3 l1 l2       Perm3 l2 l3	(perm3_trans)
Perm3 l1 l3

For instance we can derive Perm3 [1;2;3] [3;2;1] as follows:

————————(perm_swap12) —————————————————————(perm_swap23)
Perm3 [1;2;3] [2;1;3] Perm3 [2;1;3] [2;3;1]
——————————————————————————————(perm_trans) ————————————(perm_swap12)
    Perm3 [1;2;3] [2;3;1] Perm [2;3;1] [3;2;1]
    —————————————————————————————————————————————————————(perm_trans)
                      Perm3 [1;2;3] [3;2;1] In Coq Perm3 is given the following inductive definition:

This definition says:

• If l₂ can be obtained from l₁ by swapping the first and second elements, then l₂ is a permutation of l₁.
• If l₂ can be obtained from l₁ by swapping the second and third elements, then l₂ is a permutation of l₁.
• If l₂ is a permutation of l₁ and l₃ is a permutation of l₂, then l₃ is a permutation of l₁.

Exercise: 1 star, standard, optional (perm)

According to this definition, is [1;2;3] a permutation of itself?

Evenness (yet again)

We've already seen two ways of stating a proposition that a number n is even: We can say (1) even n = true, or (2) ∃ k, n = double k. A third possibility, which we'll use as a running example for some of this chapter, is to say that n is even if we can establish its evenness from the following two rules:

• The number 0 is even.
• If n is even, then S (S n) is even.

(Defining evenness in this way may seem a bit confusing, since we have already seen another perfectly good way of doing it -- "n is even if it is equal to the result of doubling some number". But it makes a convenient running example because it is simple and compact.) To illustrate how this new definition of evenness works, let's imagine using it to show that 4 is even. First, we give the rules names for easy reference:

	(ev_0)
ev 0

ev n	(ev_SS)
ev (S (S n))

Now we can use the following derivation to show ev 4:
                           ———— (ev_0)
                           ev 0
                       ———————————— (ev_SS)
                       ev (S (S 0))
                   ———————————————————— (ev_SS)
                   ev (S (S (S (S 0)))) In words, to show that 4 is even, by rule ev_SS, it suffices to show that 2 is even. This, in turn, is again guaranteed by rule ev_SS, as long as we can show that 0 is even. But this last fact follows directly from the ev_0 rule. We can translate the informal definition of evenness from above into a formal Inductive declaration, where each "way that a number can be even" corresponds to a separate constructor:

This definition is interestingly different from previous uses of Inductive. For one thing, we are defining not a Type (like nat) or a function yielding a Type (like list), but rather a function from nat to Prop -- that is, a property of numbers. But what is really new is that, because the nat argument of ev appears to the right of the colon on the first line, it is allowed to take different values in the types of different constructors: 0 in the type of ev_0 and S (S n) in the type of ev_SS. Accordingly, the type of each constructor must be specified explicitly (after a colon), and each constructor's type must have the form ev n for some natural number n. In contrast, recall the definition of list:
    Inductive list (X:Type) : Type :=
      | nil
      | cons (x : X) (l : list X). or equivalently:
    Inductive list (X:Type) : Type :=
      | nil : list X
      | cons (x : X) (l : list X) : list X. This definition introduces the X parameter globally, to the left of the colon, forcing the result of nil and cons to be the same type (i.e., list X). But if we had tried to bring nat to the left of the colon in defining ev, we would have seen an error:

In an Inductive definition, an argument to the type constructor on the left of the colon is called a "parameter", whereas an argument on the right is called an "index" or "annotation." For example, in Inductive list (X : Type) := ..., the X is a parameter, while in Inductive ev : nat → Prop := ..., the unnamed nat argument is an index. We can think of the inductive definition of ev this as defining a Coq property ev : nat → Prop, together with "evidence constructors" ev_0 : ev 0 and ev_SS : ∀ n, ev n → ev (S (S n)). In fact, Coq also accepts the following equivalent definition of ev:

These evidence constructors can be thought of as "primitive evidence of evenness", and they can be used just like proven theorems. In particular, we can use Coq's apply tactic with the constructor names to obtain evidence for ev of particular numbers...

... or we can use function application syntax to combine several constructors:

In this way, we can also prove theorems that have hypotheses involving ev.

Exercise: 1 star, standard (ev_double)

Constructing Evidence for Permutations

Similarly we can apply the evidence constructors to obtain evidence of Perm3 [1;2;3] [3;2;1]:

And again we can equivalently use function application syntax to combine several constructors. Note that the Coq type checker can infer not only types, but also nats and lists.

So the informal derivation trees we drew above are not too far from what's happening formally. Formally we're using the evidence constructors to build evidence trees, similar to the trees we built using the constructors of data types such as nat, list, binary trees storing numbers, etc.

Exercise: 1 star, standard (Perm3)

Using Evidence in Proofs

Besides constructing evidence that numbers are even, we can also destruct such evidence, reasoning about how it could have been built. Introducing ev with an Inductive declaration tells Coq not only that the constructors ev_0 and ev_SS are valid ways to build evidence that some number is ev, but also that these two constructors are the only ways to build evidence that numbers are ev. In other words, if someone gives us evidence E for the proposition ev n, then we know that E must be one of two things:

• E = ev_0 and n = O, or
• E = ev_SS n' E', where n = S (S n') and E' is evidence for ev n'.

This suggests that it should be possible to analyze a hypothesis of the form ev n much as we do inductively defined data structures; in particular, it should be possible to argue by case analysis or by induction on such evidence. Let's look at a few examples to see what this means in practice.

Destructing and Inverting Evidence

Suppose we are proving some fact involving a number n, and we are given ev n as a hypothesis. We already know how to perform case analysis on n using destruct or induction, generating separate subgoals for the case where n = O and the case where n = S n' for some n'. But for some proofs we may instead want to analyze the evidence for ev n directly. As a tool for such proofs, we can formalize the intuitive characterization that we gave above for evidence of ev n, using destruct.

Facts like this are often called "inversion lemmas" because they allow us to "invert" some given information to reason about all the different ways it could have been derived. Here, there are two ways to prove ev n, and the inversion lemma makes this explicit.

Exercise: 1 star, standard (le_inversion)

Let's prove a similar inversion lemma for le.

We can use the inversion lemma that we proved above to help structure proofs:

Note how the inversion lemma produces two subgoals, which correspond to the two ways of proving ev. The first subgoal is a contradiction that is discharged with discriminate. The second subgoal makes use of injection and rewrite. Coq provides a handy tactic called inversion that factors out this common pattern, saving us the trouble of explicitly stating and proving an inversion lemma for every Inductive definition we make. Here, the inversion tactic can detect (1) that the first case, where n = 0, does not apply and (2) that the n' that appears in the ev_SS case must be the same as n. It includes an "as" annotation similar to destruct, allowing us to assign names rather than have Coq choose them.

The inversion tactic can apply the principle of explosion to "obviously contradictory" hypotheses involving inductively defined properties, something that takes a bit more work using our inversion lemma. Compare:

Exercise: 1 star, standard (inversion_practice)

Prove the following result using inversion. (For extra practice, you can also prove it using the inversion lemma.)

Exercise: 1 star, standard (ev5_nonsense)

Prove the following result using inversion.

The inversion tactic does quite a bit of work. For example, when applied to an equality assumption, it does the work of both discriminate and injection. In addition, it carries out the intros and rewrites that are typically necessary in the case of injection. It can also be applied to analyze evidence for arbitrary inductively defined propositions, not just equality. As examples, we'll use it to re-prove some theorems from chapter Tactics. (Here we are being a bit lazy by omitting the as clause from inversion, thereby asking Coq to choose names for the variables and hypotheses that it introduces.)

Here's how inversion works in general.

• Suppose the name H 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 H generates a subgoal in which H has been replaced by the 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. For those, inversion adds to the proof context all equations that must hold of the arguments given to P -- e.g., S (S n') = n in the proof of evSS_ev).

The ev_double exercise above allows us to easily show that our new notion of evenness is implied by the two earlier ones (since, by even_bool_prop in chapter Logic, we already know that those are equivalent to each other). To show that all three coincide, we just need the following lemma.

We could try to proceed by case analysis or induction on n. But since ev is mentioned in a premise, this strategy seems unpromising, because (as we've noted before) the induction hypothesis will talk about n-1 (which is not even!). Thus, it seems better to first try inversion on the evidence for ev. Indeed, the first case can be solved trivially. And we can seemingly make progress on the second case with a helper lemma.

Unfortunately, the second case is harder. We need to show ∃ n₀, S (S n') = double n₀, but the only available assumption is E', which states that ev n' holds. Since this isn't directly useful, it seems that we are stuck and that performing case analysis on E was a waste of time. If we look more closely at our second goal, however, we can see that something interesting happened: By performing case analysis on E, we were able to reduce the original result to a similar one that involves a different piece of evidence for ev: namely E'. More formally, we could finish our proof if we could show that
        ∃ k', n' = double k', which is the same as the original statement, but with n' instead of n. Indeed, it is not difficult to convince Coq that this intermediate result would suffice.

Unfortunately, now we are stuck. To see this clearly, let's move E' back into the goal from the hypotheses.

Now it is obvious that we are trying to prove another instance of the same theorem we set out to prove -- only here we are talking about n' instead of n.

Induction on Evidence

If this story feels familiar, it is no coincidence: We've encountered similar problems in the Induction chapter, when trying to use case analysis to prove results that required induction. And once again the solution is... induction! The behavior of induction on evidence is the same as its behavior on data: It causes Coq to generate one subgoal for each constructor that could have used to build that evidence, while providing an induction hypothesis for each recursive occurrence of the property in question. To prove that a property of n holds for all even numbers (i.e., those for which ev n holds), we can use induction on ev n. This requires us to prove two things, corresponding to the two ways in which ev n could have been constructed. If it was constructed by ev_0, then n=0 and the property must hold of 0. If it was constructed by ev_SS, then the evidence of ev n is of the form ev_SS n' E', where n = S (S n') and E' is evidence for ev n'. In this case, the inductive hypothesis says that the property we are trying to prove holds for n'. Let's try proving that lemma again:

Here, we can see that Coq produced an IH that corresponds to E', the single recursive occurrence of ev in its own definition. Since E' mentions n', the induction hypothesis talks about n', as opposed to n or some other number. The equivalence between the second and third definitions of evenness now follows.

As we will see in later chapters, induction on evidence is a recurring technique across many areas -- in particular for formalizing the semantics of programming languages. The following exercises provide simpler examples of this technique, to help you familiarize yourself with it.

Exercise: 2 stars, standard (ev_sum)

Exercise: 3 stars, advanced, especially useful (ev_ev__ev)

Exercise: 3 stars, standard, optional (ev_plus_plus)

This exercise can be completed without induction or case analysis. But, you will need a clever assertion and some tedious rewriting. Hint: Is (n+m) + (n+p) even?

Exercise: 4 stars, advanced, optional (ev'_ev)

In general, there may be multiple ways of defining a property inductively. For example, here's a (slightly contrived) alternative definition for ev:

Prove that this definition is logically equivalent to the old one. To streamline the proof, use the technique (from the Logic chapter) of applying theorems to arguments, and note that the same technique works with constructors of inductively defined propositions.

We can do similar inductive proofs on the Perm3 relation:

Exercise: 2 stars, standard (Perm3_In)

Exercise: 1 star, standard, optional (Perm3_NotIn)

Exercise: 2 stars, standard, optional (NotPerm3)

Proving that something is NOT a permutation is quite tricky. Some of the lemmas above, like Perm3_In can be useful for this.

Inductive Relations

A proposition parameterized by a number (such as ev) can be thought of as a property -- i.e., it defines a subset of nat, namely those numbers for which the proposition is provable. In the same way, a two-argument proposition can be thought of as a relation -- i.e., it defines a set of pairs for which the proposition is provable.

Just like properties, relations can be defined inductively. One useful example is the "less than or equal to" relation on numbers that we briefly saw above.

(We've written the definition a bit differently this time, giving explicit names to the arguments to the constructors and moving them to the left of the colons.) Proofs of facts about ≤ using the constructors le_n and le_S follow the same patterns as proofs about properties, like ev above. We can apply the constructors to prove ≤ goals (e.g., to show that 3<=3 or 3<=6), and we can use tactics like inversion to extract information from ≤ hypotheses in the context (e.g., to prove that (2 ≤ 1) → 2+2=5.) Here are some sanity checks on the definition. (Notice that, although these are the same kind of simple "unit tests" as we gave for the testing functions we wrote in the first few lectures, we must construct their proofs explicitly -- simpl and reflexivity don't do the job, because the proofs aren't just a matter of simplifying computations.)

The "strictly less than" relation n < m can now be defined in terms of le.

The ≥ is defined in terms of ≤.

From the definition of le, we can sketch the behaviors of destruct, inversion, and induction on a hypothesis H providing evidence of the form le e₁ e₂. Doing destruct H will generate two cases. In the first case, e₁ = e₂, and it will replace instances of e₂ with e₁ in the goal and context. In the second case, e₂ = S n' for some n' for which le e₁ n' holds, and it will replace instances of e₂ with S n'. Doing inversion H will remove impossible cases and add generated equalities to the context for further use. Doing induction H will, in the second case, add the induction hypothesis that the goal holds when e₂ is replaced with n'. Here are a number of facts about the ≤ and < relations that we are going to need later in the course. The proofs make good practice exercises.

Exercise: 3 stars, standard, especially useful (le_facts)

Exercise: 2 stars, standard, especially useful (plus_le_facts1)

Hint: May be easiest to prove by induction on n.

Exercise: 2 stars, standard, especially useful (plus_le_facts2)

Exercise: 3 stars, standard, optional (lt_facts)

Exercise: 4 stars, standard, optional (leb_le)

Hint:

Hint: The next two can easily be proved without using induction.

Exercise: 3 stars, standard, especially useful (R_provability)

We can define three-place relations, four-place relations, etc., in just the same way as binary relations. For example, consider the following three-place relation on numbers:

• Which of the following propositions are provable?
  • R 1 1 2
  • R 2 2 6
• If we dropped constructor c₅ from the definition of R, would the set of provable propositions change? Briefly (1 sentence) explain your answer.
• If we dropped constructor c₄ from the definition of R, would the set of provable propositions change? Briefly (1 sentence) explain your answer.

Exercise: 3 stars, standard, optional (R_fact)

The relation R above actually encodes a familiar function. Figure out which function; then state and prove this equivalence in Coq.

Exercise: 4 stars, advanced (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,
      [1;2;3] is a subsequence of each of the lists
      [1;2;3]
      [1;1;1;2;2;3]
      [1;2;7;3]
      [5;6;1;9;9;2;7;3;8] but it is not a subsequence of any of the lists
      [1;2]
      [1;3]
      [5;6;2;1;7;3;8].

• Define an inductive proposition subseq on list nat that captures what it means to be a subsequence. (Hint: You'll need three cases.)
• Prove subseq_refl that subsequence is reflexive, that is, any list is a subsequence of itself.
• Prove subseq_app that for any lists l₁, l₂, and l₃, if l₁ is a subsequence of l₂, then l₁ is also a subsequence of l₂ ++ l₃.
• (Harder) Prove subseq_trans that subsequence is transitive -- that is, if l₁ is a subsequence of l₂ and l₂ is a subsequence of l₃, then l₁ is a subsequence of l₃.

Exercise: 2 stars, standard, optional (R_provability2)

Suppose we give Coq the following definition:
    Inductive R : nat → list nat → Prop :=
      | c₁ : R 0 []
      | c₂ n l (H: R n l) : R (S n) (n :: l)
      | c₃ n l (H: R (S n) l) : R n l. Which of the following propositions are provable?

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