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

Example: The Collatz Conjecture

The Collatz Conjecture is a famous open problem in number theory. Its statement is quite simple. First, we define a function csf on numbers, as follows (where csf stands for "Collatz step function"):

Next, we look at what happens when we repeatedly apply csf to some given starting number. For example, csf 12 is 6, and csf 6 is 3, so by repeatedly applying csf 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: Is the sequence starting from any positive natural number guaranteed to reach 1 eventually?

To formalize this question in Coq, we might try to define a recursive function that calculates the total number of steps that it takes for such a sequence to reach 1.

You can write this definition in a standard programming language. This definition is, however, rejected by Coq's termination checker, since the argument to the recursive call, csf n, is not "obviously smaller" than n. Indeed, this isn't just a pointless limitation: functions in Coq are required to be total, to ensure logical consistency. Moreover, we can't fix it by devising a more clever termination checker: deciding whether this particular function is total would be equivalent to settling the Collatz conjecture!

Another idea could be to express the concept of "eventually reaches 1 in the Collatz sequence" as an recursively defined property of numbers Collatz_holds_for : nat → Prop.

This recursive function is also rejected by the termination checker, since while we can in principle convince Coq that div2 n is smaller than n, we can't convince it that (3 × n) + 1 is smaller than n. Since it's definitely not!

Fortunately, there is another way to do it: We can express the concept "reaches 1 eventually in the Collatz sequence" as an inductively defined property of numbers. Intuitively, this property is defined by a set of rules:

	(Chf_one)
Collatz_holds_for 1

even n = true      Collatz_holds_for (div2 n)	(Chf_even)
Collatz_holds_for n

even n = false    Collatz_holds_for ((3 * n) + 1)	(Chf_odd)
Collatz_holds_for n

So there are three ways to prove that a number n eventually 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):

                    ———————————————————— (Chf_one)
                    Collatz_holds_for 1
                    ———————————————————— (Chf_even)
                    Collatz_holds_for 2
                    ———————————————————— (Chf_even)
                    Collatz_holds_for 4
                    ———————————————————— (Chf_even)
                    Collatz_holds_for 8
                    ———————————————————— (Chf_even)
                    Collatz_holds_for 16
                    ———————————————————— (Chf_odd)
                    Collatz_holds_for 5
                    ———————————————————— (Chf_even)
                    Collatz_holds_for 10
                    ———————————————————— (Chf_odd)
                    Collatz_holds_for 3
                    ———————————————————— (Chf_even)
                    Collatz_holds_for 6
                    ———————————————————— (Chf_even)
                    Collatz_holds_for 12

Formally in Coq, the Collatz_holds_for property is inductively defined:

For particular numbers, we can now prove that the Collatz sequence reaches 1 (we'll go through the details of how it works a bit later in the chapter):

The Collatz conjecture then states that the sequence beginning from any positive 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.

Example: Binary relation for comparing numbers

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, one 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)

This corresponds to the following inductive definition in Coq:

Example: Transitive Closure

As another example, the transitive closure of a relation R is the smallest relation that contains R and that is transitive. This can be defined by the following two rules:

R x y	(t_step)
clos_trans R x y

clos_trans R x y    clos_trans R y z	(t_trans)
clos_trans R x z

In Coq this looks as follows:

For example, suppose we define a "parent of" relation on a group of people...

The parent_of relation is not transitive, but we can define an "ancestor of" relation as its transitive closure:

Here is a derivation showing that Sage is an ancestor of Moss:

 ———————————————————(po_SC) ———————————————————(po_CM)
 parent_of Sage Cleo parent_of Cleo Moss
—————————————————————(t_step) —————————————————————(t_step)
ancestor_of Sage Cleo ancestor_of Cleo Moss
————————————————————————————————————————————————————(t_trans)
                ancestor_of Sage Moss

Example: Reflexive and Transitive Closure

As another example, 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 (where we added a reflexivity rule to clos_trans):

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

For instance, this enables an equivalent definition of the Collatz conjecture. First we define the binary relation corresponding to the Collatz step function csf:

This Collatz step relation can be used in conjunction with the reflexive and transitive closure operation to define a Collatz multi-step (cms) relation, expressing that a number n reaches another number m in zero or more Collatz steps:

Example: 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:

Example: 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 (using the recursive boolean function even), or (2) ∃ k, n = double k (using an existential quantifier).

A third possibility, which we'll use as a simple running example here, is to say that a number is even if we can establish its evenness from the following two rules:

	(ev_0)
ev 0

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

To illustrate how this new definition of evenness works, let's imagine using it to show that 4 is even:
                           ———— (ev_0)
                           ev 0
                       ———————————— (ev_SS)
                       ev (S (S 0))
                   ———————————————————— (ev_SS)
                   ev (S (S (S (S 0))))

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:

We put off discussing syntax so far, but there are both similarities and a few differences between inductive properties like ev and inductive types like nat or list:
    Inductive list (X:Type) : Type :=
      | nil : list X
      | cons (x : X) (l : list X) : list X.

Beyond this syntactic distinction, we can think of the inductive definition of ev as defining a Coq property ev : nat → Prop, together with two "evidence constructors":

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.

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 finite trees we built using the constructors of data types such as nat, list, binary trees, etc.

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. Defining 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 do case analysis and even induction on evidence of evenness...

Destructing and Inverting Evidence

We can prove our characterization of evidence for 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.

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

Coq provides a handy tactic called inversion that does the work of our inversion lemma and more besides.

We can use inversion to re-prove some theorems from Tactics.v. Note that inversion also works on equality propositions.

The tactic inversion actually works on any H : P where P is defined Inductively:

• For each constructor of P, make a subgoal where H is constrained by the form of this constructor.
• Discard contradictory subgoals (such as ev_0 above).
• Generate auxiliary equalities (as with ev_SS above).

Let's try to show that our new notion of evenness implies our earlier notion (the one based on double).

Induction on Evidence

If this story feels familiar, it is no coincidence: We 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! Let's try proving that lemma again:

Case Study: Regular Expressions

Regular expressions are a natural 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 -- which in this exercise we represent as lists with elements from T.

We connect regular expressions and strings by defining when a regular expression matches some string. Informally this looks as follows:

• 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 intuition into a set of rules, where we write s =~ re to say that s matches re:

	(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)

This directly corresponds to the following Inductive definition. 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.)

Something more interesting:

Naturally, proofs about exp_match often require induction (on evidence!). For example, suppose we want to prove the following intuitive result: If a string s matches a regular expression re, then all elements of s must occur as character literals somewhere in re. To state this as a theorem, we first define a function re_chars that lists all characters that occur in a regular expression:

The remember Tactic

Since the definition of exp_match has a recursive structure, we might expect that proofs involving regular expressions will often require induction on evidence. 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:

Here is a naive first attempt at setting up the induction. (Note that we are performing induction on evidence!)

We can get through the first case...

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

The problem here 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 like Star re. A possible, but awkward, way to solve this problem is "manually generalizing" over the problematic expressions by adding explicit equality hypotheses to the lemma:

This works, but it makes the statement of the lemma a bit ugly. Fortunately, there is a better way...

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

We now have Eq : re' = Star re.

The Eq 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.

The remainder of this section in the full version of the chapter develops an extended exercise on regular expressions, leading up to a proof of the well-known "pumping lemma." Informally, this lemma states 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.

Case Study: Improving Reflection

We've seen that we often need to relate boolean computations to statements in Prop:

However, this can result in some tedium in proof scripts. Consider:

The first subcase (where n =? m = true) is awkward because we have to explicitly "switch worlds." It would be annoying to have to do this kind of thing all the time.

We can streamline this sort of reasoning by defining an inductive proposition that yields a better case-analysis principle for n =? m. Instead of generating the assumption (n =? m) = true, which usually requires some massaging before we can use it, this principle gives us right away the assumption we really need: n = m. Following the terminology introduced in Logic, we call this the "reflection principle for equality on numbers," and we say that the boolean n =? m is reflected in the proposition n = m.

Notice that the only way to produce evidence for reflect P true is by showing P and then using the ReflectT constructor. If we play this reasoning backwards, it says we can extract evidence for P from evidence for reflect P true. 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:

(The right-to-left implication is left as an exercise.)

We can think of reflect as a variant of the usual "if and only if" connective; the advantage of reflect 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).

Let's use reflect to produce a smoother proof of filter_not_empty_In. We begin by recasting the eqb_eq lemma in terms of reflect:

The proof of filter_not_empty_In now goes as follows. Notice how the calls to destruct and rewrite in the earlier proof of this theorem are combined here into a single call to destruct.

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. This way of using reflect was popularized by SSReflect, a Coq library that has been used to formalize important results in mathematics, including 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 streamline small proof steps by turning them into boolean computations.