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. Note: For the sake of simplicity, most of this chapter uses an inductive definition of "evenness" as a running example. This is arguably a bit confusing, since we already have a perfectly good way of defining evenness as a proposition ("n is even if it is equal to the result of doubling some number"). Rest assured that we will see many more compelling examples of inductively defined propositions toward the end of this chapter and in future chapters. We've already seen two ways of stating a proposition that a number n is even: We can say (1) evenb n = true, or (2) ∃ k, n = double k. A third possibility that we'll explore here is to say that n is even if we can establish its evenness from the following rules:

• Rule eveni_0: The number 0 is even.
• Rule eveni_SS: If n is even, then S (S n) is even.

To illustrate how this new definition of evenness works, let's imagine using it to show that 4 is even. By rule eveni_SS, it suffices to show that 2 is even. This, in turn, is again guaranteed by rule eveni_SS, as long as we can show that 0 is even. But this last fact follows directly from the eveni_0 rule. We will see many definitions like this one during the rest of the course. 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. (We'll use eveni for the name of this property, since even is already used.)

	(eveni_0)
eveni 0

eveni n	(eveni_SS)
eveni (S (S n))

Each of the textual rules that we started with 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 eveni_SS says that, if n satisfies eveni, then S (S n) also does. If a rule has no premises above the line, then its conclusion holds unconditionally. We can represent a proof using these rules by combining rule applications into a proof tree. Here's how we might transcribe the above proof that 4 is even:
                             -------- (eveni_0)
                              eveni 0
                             -------- (eveni_SS)
                              eveni 2
                             -------- (eveni_SS)
                              eveni 4

(Why call this a "tree", rather than a "stack", for example? Because, in general, inference rules can have multiple premises. We will see examples of this shortly.)

Inductive Definition of Evenness

Putting all of this together, we can translate the definition of evenness into a formal Coq definition using an Inductive declaration, where each constructor corresponds to an inference rule:

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 eveni 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 eveni_0 and S (S n) in the type of eveni_SS. Accordingly, the type of each constructor must be specified explicitly (after a colon), and each constructor's type must have the form eveni 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).

This definition introduces the X parameter globally, to the left of the colon, forcing the result of nil and cons to be the same (i.e., list X). Had we tried to bring nat to the left of the colon in defining eveni, 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; in Inductive eveni : nat → Prop := ..., the unnamed nat argument is an index. We can think of this as defining a Coq property eveni : nat → Prop, together with "evidence constructors" eveni_0 : eveni 0 and eveni_SS : ∀ n, eveni n → eveni (S (S n)). 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 eveni 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 eveni.

Exercise: 1 star, standard (eveni_double)

Using Evidence in Proofs

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

• E is eveni_0 (and n is O), or
• E is eveni_SS n' E' (and n is S (S n'), where E' is evidence for eveni n').

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

Inversion on Evidence

Suppose we are proving some fact involving a number n, and we are given eveni 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 that eveni n directly. As a tool, we can prove our characterization of evidence for eveni 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 that a number is eveni, and the inversion lemma makes this explicit. The following theorem can easily be proved using destruct on evidence.

However, this variation cannot easily be handled with just destruct.

Intuitively, we know that evidence for the hypothesis cannot consist just of the eveni_0 constructor, since O and S are different constructors of the type nat; hence, eveni_SS is the only case that applies. Unfortunately, destruct is not smart enough to realize this, and it still generates two subgoals. Even worse, in doing so, it keeps the final goal unchanged, failing to provide any useful information for completing the proof.

What happened, exactly? Calling destruct has the effect of replacing all occurrences of the property argument by the values that correspond to each constructor. This is enough in the case of eveni_minus2 because that argument n is mentioned directly in the final goal. However, it doesn't help in the case of evSS_eveni since the term that gets replaced (S (S n)) is not mentioned anywhere. If we remember that term S (S n), the proof goes through. (We'll discuss remember in more detail below.)

Alternatively, the proof is straightforward using the inversion lemma that we proved above.

Note how both proofs produce two subgoals, which correspond to the two ways of proving eveni. 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 that common pattern. The inversion tactic can detect (1) that the first case (n = 0) does not apply and (2) that the n' that appears in the eveni_SS case must be the same as n. It has an "as" variant 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. For example:

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, more generally, to analyze evidence for inductively defined propositions. 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 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. For those, inversion adds all equations into the proof context that must hold of the arguments given to P (e.g., S (S n') = n in the proof of evSS_eveni). The eveni_double exercise above shows 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 eveni is mentioned in a premise, this strategy would probably lead to a dead end, 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 eveni. 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 ∃ k, S (S n') = double k, but the only available assumption is E', which states that eveni 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 eveni: namely E'. More formally, we can finish our proof by showing 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 suffices. Unforunately, now we are stuck. To make that apparent, let's move E' back into the goal from the hypotheses.

Now it is clear we are trying to prove another instance of the same theorem we set out to prove. This instance is with n', instead of n, where n' is a smaller natural number than n.

Induction on Evidence

If this looks 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 a property of n holds for all numbers for which eveni n holds, we can use induction on eveni n. This requires us to prove two things, corresponding to the two ways in which eveni n could have been constructed. If it was constructed by eveni_0, then n=0, and the property must hold of 0. If it was constructed by eveni_SS, then the evidence of eveni n is of the form eveni_SS n' E', where n = S (S n') and E' is evidence for eveni n'. In this case, the inductive hypothesis says that the property we are trying to prove holds for n'. Let's try our current lemma again:

Here, we can see that Coq produced an IH that corresponds to E', the single recursive occurrence of eveni 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, and in particular when formalizing the semantics of programming languages, where many properties of interest are defined inductively. The following exercises provide simple examples of this technique, to help you familiarize yourself with it.

Exercise: 2 stars, standard (eveni_sum)

Exercise: 4 stars, advanced, optional (eveni'_eveni)

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

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

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

There are two pieces of evidence you could attempt to induct upon here. If one doesn't work, try the other.

Exercise: 3 stars, standard, optional (eveni_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?

Inductive Relations

A proposition parameterized by a number (such as eveni) 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.

... And, just like properties, relations can be defined inductively. One useful example is the "less than or equal to" relation on numbers. The following definition says 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.

Proofs of facts about ≤ using the constructors le_n and le_S follow the same patterns as proofs about properties, like eveni 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.

Here are a few more simple relations on numbers:

Exercise: 2 stars, standard, optional (total_relation)

Define an inductive binary relation total_relation that holds between every pair of natural numbers.

Exercise: 2 stars, standard, optional (empty_relation)

Define an inductive binary relation empty_relation (on numbers) that never holds.

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'.

Exercise: 3 stars, standard, optional (le_exercises)

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.

Hint: the next one may be easiest to prove by induction on n.

Hint: The next one may be easiest to prove by induction on m.

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

Exercise: 2 stars, standard, optional (leb_iff)

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: 2 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₃.
• (Optional, 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₃. Hint: choose your induction carefully!

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]

Case Study: Regular Expressions

The eveni property provides a simple example for illustrating inductive definitions and the basic techniques for reasoning about them, but it is not terribly exciting -- after all, it is equivalent to the two non-inductive definitions of evenness that we had already seen, and does not seem to offer any concrete benefit over them. To give a better sense of the power of inductive definitions, we now show how to use them to model a classic concept in computer science: regular expressions. Regular expressions are a simple language for describing sets of strings. Their syntax is defined as follows:

Note that this definition is polymorphic: Regular expressions in reg_exp T describe strings with characters drawn from T -- that is, lists of elements of T. (We depart slightly from standard practice in that we do not require the type T to be finite. This results in a somewhat different theory of regular expressions, but the difference is not significant for our purposes.) We connect regular expressions and strings via the following rules, which define when a regular expression matches some string:

• The expression EmptySet does not match any string.
• The expression EmptyStr matches the empty string [].
• The expression Char x matches the one-character string [x].
• If re₁ matches s₁, and re₂ matches s₂, then App re₁ re₂ matches s₁ ++ s₂.
• If at least one of re₁ and re₂ matches s, then Union re₁ re₂ matches s.
• Finally, if we can write some string s as the concatenation of a sequence of strings s = s_1 ++ ... ++ s_k, and the expression re matches each one of the strings s_i, then Star re matches s.
  In particular, the sequence of strings may be empty, so Star re always matches the empty string [] no matter what re is.

We can easily translate this informal definition into an Inductive one as follows. We use the notation s =~ re in place of exp_match s re. (By "reserving" the notation before defining the Inductive, we can use it in the definition.)

Again, for readability, we can also display this definition using inference-rule notation.

	(MEmpty)
[] =~ EmptyStr

	(MChar)
[x] =~ Char x

s1 =~ re1    s2 =~ re2	(MApp)
s1 ++ s2 =~ App re1 re2

s1 =~ re1	(MUnionL)
s1 =~ Union re1 re2

s2 =~ re2	(MUnionR)
s2 =~ Union re1 re2

	(MStar0)
[] =~ Star re

s1 =~ re    s2 =~ Star re	(MStarApp)
s1 ++ s2 =~ Star re

Notice that these rules are not quite the same as the informal ones that we gave at the beginning of the section. First, we don't need to include a rule explicitly stating that no string matches EmptySet; we just don't happen to include any rule that would have the effect of some string matching EmptySet. (Indeed, the syntax of inductive definitions doesn't even allow us to give such a "negative rule.") Second, the informal rules for Union and Star correspond to two constructors each: MUnionL / MUnionR, and MStar0 / MStarApp. The result is logically equivalent to the original rules but more convenient to use in Coq, since the recursive occurrences of exp_match are given as direct arguments to the constructors, making it easier to perform induction on evidence. (The exp_match_ex₁ and exp_match_ex₂ exercises below ask you to prove that the constructors given in the inductive declaration and the ones that would arise from a more literal transcription of the informal rules are indeed equivalent.) Let's illustrate these rules with a few examples.

(Notice how the last example applies MApp to the string [1] directly. Since the goal mentions [1; 2] instead of [1] ++ [2], Coq wouldn't be able to figure out how to split the string on its own.) Using inversion, we can also show that certain strings do not match a regular expression:

We can define helper functions for writing down regular expressions. The reg_exp_of_list function constructs a regular expression that matches exactly the list that it receives as an argument:

We can also prove general facts about exp_match. For instance, the following lemma shows that every string s that matches re also matches Star re.

(Note the use of app_nil_r to change the goal of the theorem to exactly the same shape expected by MStarApp.)

Exercise: 3 stars, standard (exp_match_ex₁)

The following lemmas show that the informal matching rules given at the beginning of the chapter can be obtained from the formal inductive definition.

The next lemma is stated in terms of the fold function from the Poly chapter: If ss : list (list T) represents a sequence of strings s₁, ..., sn, then fold app ss [] is the result of concatenating them all together.

Exercise: 4 stars, standard, optional (reg_exp_of_list_spec)

Prove that reg_exp_of_list satisfies the following specification:

Since the definition of exp_match has a recursive structure, we might expect that proofs involving regular expressions will often require induction on evidence. For example, suppose that we wanted to prove the following intuitive result: If a regular expression re matches some string s, then all elements of s must occur as character literals somewhere in re. To state this theorem, we first define a function re_chars that lists all characters that occur in a regular expression:

We can then phrase our theorem as follows:

Something interesting happens in the MApp case. We obtain two induction hypotheses: One that applies when x occurs in s₁ (which matches re₁), and a second one that applies when x occurs in s₂ (which matches re₂).

Here again we get two induction hypotheses, and they illustrate why we need induction on evidence for exp_match, rather than induction on the regular expression re: The latter would only provide an induction hypothesis for strings that match re, which would not allow us to reason about the case In x s₂.

Exercise: 4 stars, standard (re_not_empty)

Write a recursive function re_not_empty that tests whether a regular expression matches some string. Prove that your function is correct.

The remember Tactic

One potentially confusing feature of the induction tactic is that it will let you try to perform an induction over a term that isn't sufficiently general. The effect of this is to lose information (much as destruct without an eqn: clause can do), and leave you unable to complete the proof. Here's an example:

Now, just doing an inversion on H₁ won't get us very far in the recursive cases. (Try it!). So we need induction (on evidence!). Here is a naive first attempt. (We can begin by generalizing s₂, since it's pretty clear that we are going to have to walk over both s₁ and s₂ in parallel.)

But now, although we get seven cases (as we would expect from the definition of exp_match), we have lost a very important bit of information from H₁: the fact that s₁ matched something of the form Star re. This means that we have to give proofs for all seven constructors of this definition, even though all but two of them (MStar0 and MStarApp) are contradictory. We can still get the proof to go through for a few constructors, such as MEmpty...

... but most cases get stuck. For MChar, for instance, we must show that
    s₂ =~ Char x' → x' :: s₂ =~ Char x',

which is clearly impossible.

The problem is that induction over a Prop hypothesis only works properly with hypotheses that are completely general, i.e., ones in which all the arguments are variables, as opposed to more complex expressions, such as Star re. (In this respect, induction on evidence behaves more like destruct-without-eqn: than like inversion.) An awkward way to solve this problem is "manually generalizing" over the problematic expressions by adding explicit equality hypotheses to the lemma:

We can now proceed by performing induction over evidence directly, because the argument to the first hypothesis is sufficiently general, which means that we can discharge most cases by inverting the re' = Star re equality in the context. This idiom is so common that Coq provides a tactic to automatically generate such equations for us, avoiding thus the need for changing the statements of our theorems.

As we saw above, The tactic remember e as x causes Coq to (1) replace all occurrences of the expression e by the variable x, and (2) add an equation x = e to the context. Here's how we can use it to show the above result:

We now have Heqre' : re' = Star re.

The Heqre' is contradictory in most cases, allowing us to conclude immediately.

The interesting cases are those that correspond to Star. Note that the induction hypothesis IH₂ on the MStarApp case mentions an additional premise Star re'' = Star re, which results from the equality generated by remember.

Exercise: 4 stars, standard, optional (exp_match_ex₂)

The MStar'' lemma below (combined with its converse, the MStar' exercise above), shows that our definition of exp_match for Star is equivalent to the informal one given previously.

Exercise: 5 stars, advanced (weak_pumping)

One of the first really interesting theorems in the theory of regular expressions is the so-called pumping lemma, which states, informally, that any sufficiently long string s matching a regular expression re can be "pumped" by repeating some middle section of s an arbitrary number of times to produce a new string also matching re. (For the sake of simplicity in this exercise, we consider a slightly weaker theorem than is usually stated in courses on automata theory.) To get started, we need to define "sufficiently long." Since we are working in a constructive logic, we actually need to be able to calculate, for each regular expression re, the minimum length for strings s to guarantee "pumpability."

You may find these lemmas about the pumping constant useful when proving the pumping lemma below.

Next, it is useful to define an auxiliary function that repeats a string (appends it to itself) some number of times.

This auxiliary lemma might also be useful in your proof of the pumping lemma.

The (weak) pumping lemma itself says that, if s =~ re and if the length of s is at least the pumping constant of re, then s can be split into three substrings s₁ ++ s₂ ++ s₃ in such a way that s₂ can be repeated any number of times and the result, when combined with s₁ and s₃ will still match re. Since s₂ is also guaranteed not to be the empty string, this gives us a (constructive!) way to generate strings matching re that are as long as we like.

You are to fill in the proof. Several of the lemmas about le that were in an optional exercise earlier in this chapter may be useful.

Exercise: 5 stars, advanced, optional (pumping)

Now here is the usual version of the pumping lemma. In addition to requiring that s₂ ≠ [], it also requires that length s₁ + length s₂ ≤ pumping_constant re.

You may want to copy your proof of weak_pumping below.

Case Study: Improving Reflection

We've seen in the Logic chapter that we often need to relate boolean computations to statements in Prop. But performing this conversion as we did it there can result in tedious proof scripts. Consider the proof of the following theorem:

In the first branch after destruct, we explicitly apply the eqb_eq lemma to the equation generated by destructing n =? m, to convert the assumption n =? m = true into the assumption n = m; then we had to rewrite using this assumption to complete the case. We can streamline this by defining an inductive proposition that yields a better case-analysis principle for n =? m. Instead of generating an equation such as (n =? m) = true, which is generally not directly useful, this principle gives us right away the assumption we really need: n = m. Following the terminology introduced in IndProp, we call this the "reflection principle for equality (between numbers)," and we say that the boolean n =? m is reflected in the proposition n = m.

The reflect property takes two arguments: a proposition P and a boolean b. Intuitively, it states that the property P is reflected in (i.e., equivalent to) the boolean b: that is, P holds if and only if b = true. To see this, notice that, by definition, the only way we can produce evidence for reflect P true is by showing P and then using the ReflectT constructor. If we invert this statement, this means that it should be possible to extract evidence for P from a proof of reflect P true. Similarly, the only way to show reflect P false is by combining evidence for ¬ P with the ReflectF constructor. To put this observation to work, we first prove that the statements P ↔ b = true and reflect P b are indeed equivalent. First, the left-to-right implication:

Now you prove the right-to-left implication:

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

The advantage of reflect over the normal "if and only if" connective is that, by destructing a hypothesis or lemma of the form reflect P b, we can perform case analysis on b while at the same time generating appropriate hypothesis in the two branches (P in the first subgoal and ¬ P in the second).

A smoother proof of filter_not_empty_In now goes as follows. Notice how the calls to destruct and rewrite are combined into a single call to destruct. (To see this clearly, look at the two proofs of filter_not_empty_In with Coq and observe the differences in proof state at the beginning of the first case of the destruct.)

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

Use eqbP as above to prove the following:

This small example shows reflection giving us a small gain in convenience; in larger developments, using reflect consistently can often lead to noticeably shorter and clearer proof scripts. We'll see many more examples in later chapters and in Programming Language Foundations. The use of the reflect property has been popularized by SSReflect, a Coq library that has been used to formalize important results in mathematics, including as the 4-color theorem and the Feit-Thompson theorem. The name SSReflect stands for small-scale reflection, i.e., the pervasive use of reflection to simplify small proof steps with boolean computations.

Additional Exercises

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

Formulating inductive definitions of properties is an important skill you'll need in this course. Try to solve this exercise without any help at all. We say that a list "stutters" if it repeats the same element consecutively. (This is different from not containing duplicates: the sequence [1;4;1] repeats the element 1 but does not stutter.) The property "nostutter mylist" means that mylist does not stutter. Formulate an inductive definition for nostutter.

Make sure each of these tests succeeds, but feel free to change the suggested proof (in comments) if the given one doesn't work for you. Your definition might be different from ours and still be correct, in which case the examples might need a different proof. (You'll notice that the suggested proofs use a number of tactics we haven't talked about, to make them more robust to different possible ways of defining nostutter. You can probably just uncomment and use them as-is, but you can also prove each example with more basic tactics.)

Exercise: 4 stars, advanced (filter_challenge)

Let's prove that our definition of filter from the Poly chapter matches an abstract specification. Here is the specification, written out informally in English: A list l is an "in-order merge" of l₁ and l₂ if it contains all the same elements as l₁ and l₂, in the same order as l₁ and l₂, but possibly interleaved. For example,
    [1;4;6;2;3]

is an in-order merge of
    [1;6;2]

and
    [4;3].

Now, suppose we have a set X, a function test: X→bool, and a list l of type list X. Suppose further that l is an in-order merge of two lists, l₁ and l₂, such that every item in l₁ satisfies test and no item in l₂ satisfies test. Then filter test l = l₁. Translate this specification into a Coq theorem and prove it. (You'll need to begin by defining what it means for one list to be a merge of two others. Do this with an inductive relation, not a Fixpoint.)

Exercise: 5 stars, advanced, optional (filter_challenge_2)

A different way to characterize the behavior of filter goes like this: Among all subsequences of l with the property that test evaluates to true on all their members, filter test l is the longest. Formalize this claim and prove it.

Exercise: 4 stars, standard, optional (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 like
          c : ∀ l, l = rev l → pal l
  may seem obvious, but will not work very well.)
• Prove (pal_app_rev) that
         ∀ l, pal (l ++ rev l).
• Prove (pal_rev that)
         ∀ l, pal l → l = rev l.

Exercise: 5 stars, standard, optional (palindrome_converse)

Again, the converse direction is significantly more difficult, due to the lack of evidence. Using your definition of pal from the previous exercise, prove that
     ∀ l, l = rev l → pal l.

Exercise: 4 stars, advanced, optional (NoDup)

Recall the definition of the In property from the Logic chapter, which asserts that a value x appears at least once in a list l:

Your first task is to use In to define a proposition disjoint X l₁ l₂, which should be provable exactly when l₁ and l₂ are lists (with elements of type X) that have no elements in common.

Next, use In to define an inductive proposition NoDup X l, which should be provable exactly when l is a list (with elements of type X) where every member is different from every other. For example, NoDup nat [1;2;3;4] and NoDup bool [] should be provable, while NoDup nat [1;2;1] and NoDup bool [true;true] should not be.

Finally, state and prove one or more interesting theorems relating disjoint, NoDup and ++ (list append).

Exercise: 4 stars, advanced, optional (pigeonhole_principle)

The pigeonhole principle states a basic fact about counting: if we distribute more than n items into n pigeonholes, some pigeonhole must contain at least two items. As often happens, this apparently trivial fact about numbers requires non-trivial machinery to prove, but we now have enough... First prove an easy useful lemma.