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: inductive definitions.

In past chapters, we have seen two ways of stating that a number n is even: We can say (1) evenb n = true, or (2) ∃ k, n = double k. Yet another possibility is to say that n is even if we can establish its evenness from the following rules:

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

Such definitions are often presented using inference rules, they consist of a line separating the premises above from the conclusion below:

	(ev_0)
even 0

even n	(ev_SS)
even (S (S n))

We can use a proof tree to display the reasoning steps demonstrating that 4 is even:

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:

We can think of the definition of even as defining a Coq property even : nat → Prop, together with primitive theorems ev_0 : even 0 and ev_SS : ∀ n, even n → even (S (S n)). That definition can also be written as follows...

Such "constructor theorems" have the same status as proven theorems. In particular, we can use Coq's apply tactic with the rule names to prove even for particular numbers...

... or we can use function application syntax:

We can also prove theorems that have hypotheses involving even.

Using Evidence in Proofs

Besides constructing evidence that numbers are even, we can also reason about such evidence. Introducing even 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 even, but also that these two constructors are the only ways to build evidence that numbers are even (in the sense of even).

In other words, if someone gives us evidence E for the assertion even n, then we know that E must have one of two shapes:

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

This suggests that it should be possible to do induction and case analysis on evidence of evenness...

Inversion on Evidence

We can prove our characterization of evidence for even n, using destruct.

The following theorem can easily be proved using destruct on evidence.

However, this variation cannot easily be handled with destruct.

The proof is straightforward using our inversion lemma.

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

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

We can use inversion to reprove some theorems from Tactics.v.

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

• For each constructor of P, make a subgoal and replace H by how exactly this constructor could have been used to prove P.
• Discard contradictory subgoals (such as ev_0 above).
• Generate auxiliary equalities (as with ev_SS above).

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

Induction on Evidence

Let's try our current lemma again:

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.

Inductive Relations

Just as a single-argument proposition defines a property, a two-argument proposition defines a relation.

One useful example is the "less than or equal to" relation on numbers.

Some sanity checks...

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

Here are a few more simple relations on numbers:

Case Study: Regular Expressions

Regular expressions are a simple language for describing sets of strings. Their syntax is defined as follows:

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.
  As a special case, 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:

Again, for readability, we can also display this definition using inference-rule notation. At the same time, let's introduce a more readable infix 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

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:

Something more interesting:

Naturally, proofs about exp_match often require induction. 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:

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:

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 that 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. An 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 requires making the statement of the lemma a bit ugly, which is a shame. Fortunately, there is a better way:

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.

Case Study: Improving Reflection

We've seen that we often need to relate boolean computations to statements in Prop. Unfortunately, this can sometimes result in tedious proof scripts. Consider:

The first subcase (where n =? m = true) is a bit awkward. It would be annoying to have to do this kind of thing all the time.

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.

The only way to produce evidence for reflect P true is by showing P and using the ReflectT constructor. If we invert this reasoning, it says we can extract evidence for P from evidence for reflect P true.

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

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

To use reflect to produce a better proof of filter_not_empty_In, we begin by recasting the eqb_iff_true lemma in terms of reflect:

A smoother proof of filter_not_empty_In now goes as follows. Notice how the calls to destruct and apply are combined into a single call to destruct.

This small example shows how reflection gives 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.