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. Another alternative is to define the concept of evenness directly. Instead of going via the evenb function ("a number is even if a certain computation yields true"), we can say what the concept of evenness means by giving two different ways of presenting evidence that a number is even.

Inductively Defined Propositions

This definition says that there are two ways to give evidence that a number m is even. First, 0 is even, and ev_0 is evidence for this. Second, if m = S (S n) for some n and we can give evidence e that n is even, then m is also even, and ev_SS n e is the evidence.

Exercise: 1 star (double_even)

☐

Discussion: Computational vs. Inductive Definitions

We have seen that the proposition "n is even" can be phrased in two different ways — indirectly, via a boolean testing function evenb, or directly, by inductively describing what constitutes evidence for evenness. These two ways of defining evenness are about equally easy to state and work with. Which we choose is basically a question of taste. However, for many other properties of interest, the direct inductive definition is preferable, since writing a testing function may be awkward or even impossible. One such property is beautiful. This is a perfectly sensible definition of a set of numbers, but we cannot translate its definition directly into a Coq Fixpoint (or into a recursive function in any other common programming language). We might be able to find a clever way of testing this property using a Fixpoint (indeed, it is not too hard to find one in this case), but in general this could require arbitrarily deep thinking. In fact, if the property we are interested in is uncomputable, then we cannot define it as a Fixpoint no matter how hard we try, because Coq requires that all Fixpoints correspond to terminating computations. On the other hand, writing an inductive definition of what it means to give evidence for the property beautiful is straightforward.

Exercise: 1 star (ev__even)

Here is a proof that the inductive definition of evenness implies the computational one.

Could this proof also be carried out by induction on n instead of E? If not, why not?

☐ The induction principle for inductively defined propositions does not follow quite the same form as that of inductively defined sets. For now, you can take the intuitive view that induction on evidence ev n is similar to induction on n, but restricts our attention to only those numbers for which evidence ev n could be generated. We'll look at the induction principle of ev in more depth below, to explain what's really going on.

Exercise: 1 star (l_fails)

The following proof attempt will not succeed. Intuitively, we expect the proof to fail because not every number is even. However, what exactly causes the proof to fail? (* FILL IN HERE *)
☐

Exercise: 2 stars (ev_sum)

Here's another exercise requiring induction.

☐

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.

Inference Rules

We will see many definitions like this one during the rest of the course, and 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:

	(b_0)
beautiful 0

	(b_3)
beautiful 3

	(b_5)
beautiful 5

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

Each of the textual rules above 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 b_sum says that, if n and m are both beautiful numbers, then it follows that n+m is beautiful too. If a rule has no premises above the line, then its conclusion hold unconditionally. These rules define the property beautiful. That is, if we want to convince someone that some particular number is beautiful, our argument must be based on these rules. For a simple example, suppose we claim that the number 5 is beautiful. To support this claim, we just need to point out that rule b_5 says so. Or, if we want to claim that 8 is beautiful, we can support our claim by first observing that 3 and 5 are both beautiful (by rules b_3 and b_5) and then pointing out that their sum, 8, is therefore beautiful by rule b_sum. This argument can be expressed graphically with the following proof tree:

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

Exercise: 1 star (varieties_of_beauty)

How many different ways are there to show that 8 is beautiful?

☐

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

☐

Exercise: 3 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:

Exercise: 1 star (gorgeous_tree)

Write out the definition of gorgeous numbers using inference rule notation. (* FILL IN HERE *)
☐

Exercise: 1 star (gorgeous_plus13)

☐

It seems intuitively obvious that, although gorgeous and beautiful are presented using slightly different rules, they are actually the same property in the sense that they are true of the same numbers. Indeed, we can prove this.

Notice that the argument proceeds by induction on the evidence H! Let's see what happens if we try to prove this by induction on n instead of induction on the evidence H.

The problem here is that doing induction on n doesn't yield a useful induction hypothesis. Knowing how the property we are interested in behaves on the predecessor of n doesn't help us prove that it holds for n. Instead, we would like to be able to have induction hypotheses that mention other numbers, such as n - 3 and n - 5. This is given precisely by the shape of the constructors for gorgeous.

Exercise: 2 stars (gorgeous_sum)

☐

Exercise: 3 stars, advanced (beautiful__gorgeous)

☐

Exercise: 3 stars, optional (g_times2)

Prove the g_times2 theorem below without using gorgeous__beautiful. You might find the following helper lemma useful.

☐

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.

Exercise: 1 star, optional (ev_minus2_n)

What happens if we try to use destruct on n instead of inversion on E?

☐

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

inversion revisited

These uses of inversion may seem a bit mysterious at first. Until now, we've only used inversion on equality propositions, to utilize injectivity of constructors or to discriminate between different constructors. But we see here that inversion can also be applied to analyzing evidence for inductively defined propositions. (You might also expect that destruct would be a more suitable tactic to use here. Indeed, it is possible to use destruct, but it often throws away useful information, and the eqn: qualifier doesn't help much in this case.) Here's how inversion works in general. Suppose the name I 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 I generates a subgoal in which I 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. In this particular case, the inversion analyzed the construction ev (S (S n)), determined that this could only have been constructed using ev_SS, and generated a new subgoal with the arguments of that constructor as new hypotheses. (It also produced an auxiliary equality, which happens to be useless here.) We'll begin exploring this more general behavior of inversion in what follows.

Exercise: 1 star (inversion_practice)

The inversion tactic can also be used to derive goals by showing the absurdity of a hypothesis.

☐

Exercise: 3 stars, advanced (ev_ev__ev)

Finding the appropriate thing to do induction on is a bit tricky here:

☐

Exercise: 3 stars, optional (ev_plus_plus)

Here's an exercise that just requires applying existing lemmas. No induction or even case analysis is needed, but some of the rewriting may be tedious.

☐

Additional Exercises

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

☐

Exercise: 5 stars, optional (palindrome_converse)

Using your definition of pal from the previous exercise, prove that

☐

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, is a subsequence of each of the lists but it is not a subsequence of any of the lists

• Define an inductive proposition subseq on list nat that captures what it means to be a subsequence. (Hint: You'll need three cases.)
• Prove that subsequence is reflexive, that is, any list is a subsequence of itself.
• Prove that for any lists l1, l2, and l3, if l1 is a subsequence of l2, then l1 is also a subsequence of l2 ++ l3.
• (Optional, harder) Prove that subsequence is transitive — that is, if l1 is a subsequence of l2 and l2 is a subsequence of l3, then l1 is a subsequence of l3. Hint: choose your induction carefully!

☐

Exercise: 2 stars, optional (R_provability)

Suppose we give Coq the following definition: Which of the following propositions are provable?

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

☐

Relations

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

One useful example is the "less than or equal to" relation on numbers. The following definition should be fairly intuitive. It says that there are two ways to give evidence that one number is less than or equal to another: either observe that they are the same number, or give evidence that the first is less than or equal to the predecessor of the second.

Proofs of facts about ≤ using the constructors le_n and le_S follow the same patterns as proofs about properties, like ev in chapter Prop. 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 (total_relation)

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

☐

Exercise: 2 stars (empty_relation)

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

☐

Exercise: 2 stars, 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.

Exercise: 2 stars, optional (ble_nat_false)

☐

Exercise: 3 stars (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 c5 from the definition of R, would the set of provable propositions change? Briefly (1 sentence) explain your answer.
• If we dropped constructor c4 from the definition of R, would the set of provable propositions change? Briefly (1 sentence) explain your answer.

(* FILL IN HERE *)
☐

Exercise: 3 stars, optional (R_fact)

Relation R actually encodes a familiar function. State and prove two theorems that formally connects the relation and the function. That is, if R m n o is true, what can we say about m, n, and o, and vice versa?

☐

Programming with Propositions Revisited

As we have seen, a proposition is a statement expressing a factual claim, like "two plus two equals four." In Coq, propositions are written as expressions of type Prop. .

Both provable and unprovable claims are perfectly good propositions. Simply being a proposition is one thing; being provable is something else!

Both 2 + 2 = 4 and 2 + 2 = 5 are legal expressions of type Prop.

We've mainly seen one place that propositions can appear in Coq: in Theorem (and Lemma and Example) declarations.

But they can be used in many other ways. For example, we have also seen that we can give a name to a proposition using a Definition, just as we have given names to expressions of other sorts.

We can later use this name in any situation where a proposition is expected — for example, as the claim in a Theorem declaration.

We've seen several ways of constructing propositions.

• We can define a new proposition primitively using Inductive.
• Given two expressions e1 and e2 of the same type, we can form the proposition e1 = e2, which states that their values are equal.
• We can combine propositions using implication and quantification.

We have also seen parameterized propositions, such as even and beautiful.

The type of even, i.e., nat→Prop, can be pronounced in three equivalent ways: (1) "even is a function from numbers to propositions," (2) "even is a family of propositions, indexed by a number n," or (3) "even is a property of numbers." Propositions — including parameterized propositions — are first-class citizens in Coq. For example, we can define functions from numbers to propositions...

... and then partially apply them:

We can even pass propositions — including parameterized propositions — as arguments to functions:

Here are two more examples of passing parameterized propositions as arguments to a function. The first function, true_for_all_numbers, takes a proposition P as argument and builds the proposition that P is true for all natural numbers.

The second, preserved_by_S, takes P and builds the proposition that, if P is true for some natural number n', then it is also true by the successor of n' — i.e. that P is preserved by successor:

Finally, we can put these ingredients together to define a proposition stating that induction is valid for natural numbers:

Exercise: 3 stars (combine_odd_even)

Complete the definition of the combine_odd_even function below. It takes as arguments two properties of numbers Podd and Peven. As its result, it should return a new property P such that P n is equivalent to Podd n when n is odd, and equivalent to Peven n otherwise.

To test your definition, see whether you can prove the following facts:

☐

One more quick digression, for adventurous souls: if we can define parameterized propositions using Definition, then can we also define them using Fixpoint? Of course we can! However, this kind of "recursive parameterization" doesn't correspond to anything very familiar from everyday mathematics. The following exercise gives a slightly contrived example.

Exercise: 4 stars, optional (true_upto_n__true_everywhere)

Define a recursive function true_upto_n__true_everywhere that makes true_upto_n_example work.

☐