So far, all of our theorems have concluded with an equality proposition of the form e1 = e2. But Coq supports a much broader range of primitive propositions.

Inductively Defined Propositions

As a running example, let's define a simple property of natural numbers — we'll call it "beautiful." Informally, a number is beautiful if it is 0, 3, 5, or the sum of two beautiful numbers. More pedantically, we can define beautiful numbers by giving four rules:

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

Such definitions are often presented using inference rules:

	(b_0)
beautiful 0

	(b_3)
beautiful 3

	(b_5)
beautiful 5

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

The following proof tree demonstrates that 8 is beautiful: Of course, there are other ways of using these rules to argue that 8 is beautiful, for instance:

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

The first line declares that beautiful is a proposition — or, more formally, a family of propositions "indexed by" natural numbers. (That is, for each number n, the claim that "n is beautiful" is a proposition.) Such a family of propositions is often called a property of numbers. Each of the remaining lines embodies one of the rules for beautiful numbers. The rules introduced this way have the same status as proven theorems; that is, they are true axiomatically. So we can use Coq's apply tactic with the rule names to prove that particular numbers are beautiful.

As you would expect, we can also prove theorems that have hypotheses about beautiful.

Exercise: 2 stars (b_timesm)

☐

Induction Over Evidence

Besides constructing evidence that numbers are beautiful, we can also reason about such evidence. The fact that we introduced beautiful with an Inductive declaration tells Coq not only that the constructors b_0, b_3, b_5 and b_sum are ways to build evidence, but also that these two constructors are the only ways to build evidence that numbers are beautiful. In other words, if someone gives us evidence E for the assertion beautiful n, then we know that E must have one of four shapes:

• E is b_0 (and n is O),
• E is b_3 (and n is 3),
• E is b_5 (and n is 5), or
• E is b_sum n1 n2 E1 E2 (and n is n1+n2, where E1 is evidence that n1 is beautiful and E2 is evidence that n2 is beautiful).

This permits us to analyze any hypothesis of the form beautiful n to see how it was constructed, using the tactics we already know. In particular, we can use the induction tactic that we have already seen for reasoning about inductively defined data to reason about inductively defined evidence. To illustrate this, let's define another property of numbers:

Now let's prove that every gorgeous number is also beautiful.

Notice that the argument proceeds by induction on the evidence H!

From Boolean Functions to Propositions

In chapter Basics we defined a function evenb that tests a number for evenness, yielding true if so. We can use this function to define the proposition that some number n is even:

That is, we can define "n is even" to mean "the function evenb returns true when applied to n." Note that here we have given a name to a proposition using a Definition, just as we have given names to expressions of other sorts. This isn't a fundamentally new kind of proposition; it is still just an equality. A different way to talk about evenness is to define an inductively defined proposition ev n.

Discussion: Computational vs. Inductive Definitions

Many concepts (like evenness) can be defined in Coq in two different ways:

• as a recursive function returning a boolean
• as an inductively defined predicate

Both methods have advantages:

• Functions can be easier to work with because they are subject to Coq's machinery for simplifying expressions
  • evenb 1000 = true definitionally
  • ev 1000 must be justified by a largeish proof
• Inductively defined predicates are more flexible
  • not subject to the requirement that Fixpoints always terminate
  • suitable for properties that are awkward, unnatural, or impossible to define as recursive functions (e.g. beautiful)

Sometimes it is helpful to define a given concept both ways, prove that they are equivalent (∀ n. evenb n = true ↔ ev n), and then switch back and forth as convenient.

Inversion on Evidence

Another situation where we want to analyze evidence for evenness is when proving that, if n is even, then pred (pred n)) is too. In this case, we don't need to do an inductive proof. The right tactic turns out to be inversion.

Another example, in which inversion helps narrow down to the relevant cases.

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

• For each constructor of P, make a subgoal and replace I 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).