Consider these algorithms and data structures:

• sort a sequence of numbers
• finite maps from numbers to (arbitrary-type) data
• finite maps from any ordered type to (arbitrary-type) data
• priority queues: finding/deleting the highest number in a set

To prove the correctness of such programs, we need to reason about comparisons, and about whether two collections have the same contents. In this chapter, we introduce some techniques for reasoning about:

• less-than comparisons on natural numbers, and
• permutations (rearrangements of lists).

In later chapters, we'll apply these proof techniques to reasoning about algorithms and data structures.

The Coq Standard Library

In this volume, we're going to import the definitions and theorems we need directly from Coq's standard library, rather than from chapters in Volume 1. You should not notice much difference, though, because we've been careful to name our own definitions and theorems the same as their counterparts in the standard library.

The Less-Than Order on the Natural Numbers

In our proofs about searching and sorting algorithms, we often have to reason about the less-than order on natural numbers. Recall that the Coq standard library contains both propositional and Boolean less-than operators on natural numbers. We write x < y for the proposition that x is less than y:

And we write x <? y for the computation that returns true or false depending on whether x is less than y:

Operation < is a reflection of <?, as discussed in Logic and IndProp. The Nat module has a theorem showing how they relate:

The Nat module contains a synonym for lt.

For unknown reasons, Nat does not define >=? or >?. So we define them here:

The Lia Tactic

Reasoning about inequalities by hand can be a little painful. Luckily, Coq provides a tactic called lia that is quite helpful.

The hard way to prove this is by hand.

Since subtraction is truncated, does lia_example1 actually hold? It does. Let's try again, the hard way, to find the proof.

That was tedious. Here's a much easier way:

Lia is a decision procedure for integer linear arithemetic. The lia tactic was made available by importing Lia at the beginning of the file. The tactic works with Coq types Z and nat, and these operators: < = > ≤ ≥ + - ¬, as well as multiplication by small integer literals (such as 0,1,2,3...), and some uses of ∨, ∧, and ↔. Lia does not "understand" other operators. It treats expressions such as f x y as variables. That is, it can prove f x y > a × b → f x y + 3 ≥ a × b, in the same way it would prove u > v → u + 3 ≥ v.

Swapping

Consider trying to sort a list of natural numbers. As a small piece of a sorting algorithm, we might need to swap the first two elements of a list if they are out of order.

Applying maybe_swap twice should give the same result as applying it once. That is, maybe_swap is idempotent.

Now what? We have a contradiction in the hypotheses: it cannot hold that a is less than b and b is less than a. Unfortunately, lia cannot immediately show that for us, because it reasons about comparisons in Prop not bool.

Of course we could finish the proof by reasoning directly about inequalities in bool. But this situation is going to occur repeatedly in our study of sorting. Let's set up some machinery to enable using lia on boolean tests.

Reflection

The reflect type, defined in the standard library (and presented in IndProp), relates a proposition to a Boolean. That is, a value of type reflect P b contains a proof of P if b is true, or a proof of ¬ P if b is false.

The standard library proves a theorem that says if P is provable whenever b = true is provable, then P reflects b.

Using that theorem, we can quickly prove that the propositional (in)equality operators are reflections of the Boolean operators.

Here's an example of how you could use these lemmas. Suppose you have this simple program, (if a <? 5 then a else 2), and you want to prove that it evaluates to a number smaller than 6. You can use ltb_reflect "by hand":

For the ReflectT constructor, the guard a <? 5 must be equal to true. The if expression in the goal has already been simplified to take advantage of that fact. Also, for ReflectT to have been used, there must be evidence H that a < 5 holds. From there, all that remains is to show a < 5 entails a < 6. The lia tactic, which is capable of automatically proving some theorems about inequalities, succeeds. For the ReflectF constructor, the guard a <? 5 must be equal to false. So the if expression simplifies to 2 < 6, which is immediately provable by lia. A less didactic version of the above proof wouldn't do the assert and remember: we can directly skip to destruct.

But even that proof is a little unsatisfactory. The original expression, a <? 5, is not perfectly apparent from the expression ltb_reflect a 5 that we pass to destruct. It would be nice to be able to just say something like destruct (a <? 5) and get the reflection "for free." That's what we'll engineer, next.

A Tactic for Boolean Destruction

We're now going to build a tactic that you'll want to use, but you won't need to understand the details of how to build it yourself. Let's put several of these reflect lemmas into a Hint database. We call it bdestruct, because we'll use it in our boolean-destruction tactic:

Here is the tactic, the body of which you do not need to understand. Invoking bdestruct on Boolean expression b does the same kind of reasoning we did above: reflection and destruction. It also attempts to simplify negations involving inequalities in hypotheses.

This tactic makes quick, easy-to-read work of our running example.

Finishing the maybe_swap Proof

Now that we have bdestruct, we can finish the proof of maybe_swap's idempotence.

Note how a > b is a hypothesis, rather than a >? b = true.

lia can take care of the contradictory propositional inequalities.

When proving theorems about a program that uses Boolean comparisons, use bdestruct followed by lia, rather than destruct followed by application of various theorems about Boolean operators.

Permutations

Another useful fact about maybe_swap is that it doesn't add or remove elements from the list: it only reorders them. That is, the output list is a permutation of the input. List al is a permutation of list bl if the elements of al can be reordered to get the list bl. Note that reordering does not permit adding or removing duplicate elements. Coq's Permutation library has an inductive definition of permutations.

You might wonder, "is that really the right definition?" And indeed, it's important that we get a right definition, because Permutation is going to be used in our specifications of searching and sorting algorithms. If we have the wrong specification, then all our proofs of "correctness" will be useless. It's not obvious that this is indeed the right specification of permutations. (It happens to be, but that's not obvious.) To gain confidence that we have the right specification, let's use it prove some properties that permutations ought to have. Let's use the permutation theorems in the library to prove the following theorem.

Let's group [u;t;t;e;r] together on both sides. Tactic change t with u replaces t with u. Terms t and u must be convertible, here meaning that they evaluate to the same term.

We don't actually need to know the list elements in [u;t;t;e;r]. Let's forget about them and just remember them as a variable named utter.

Likewise, let's group [f;l] and remember it as a variable.

Next, let's cancel fl from both sides. In order to do that, we need to bring it to the beginning of each list. For the right list, that follows easily from the associativity of ++.

But for the left list, we can't just use associativity. Instead, we need to reason about permutations and use some library theorems.

A library theorem will now help us cancel fl.

Next let's cancel utter.

Finally we're left with just y and b.

That example illustrates a general method for proving permutations involving cons :: and append ++:

• Identify some portion appearing in both sides.
• Bring that portion to the front on each side using lemmas such as Permutation_app_comm and perm_swap, with generous use of perm_trans.
• Use Permutation_app_head to cancel an appended head. You can also use perm_skip to cancel a single element.

Exercise: 3 stars, standard (permut_example)

Use the permutation rules in the library to prove the following theorem. The following Check commands are a hint about useful lemmas. You don't need all of them, and depending on your approach you will find some lemmas to be more useful than others. Use Search to find others, if you like.

Exercise: 2 stars, standard (not_a_permutation)

Prove that [1;1] is not a permutation of [1;2]. Hints are given as Check commands.

Correctness of maybe_swap

Now we can prove that maybe_swap is a permutation: it reorders elements but does not add or remove any.

And, we can prove that maybe_swap permutes elements such that the first is less than or equal to the second.

An Inversion Tactic

Coq's inversion H tactic is so good at extracting information from the hypothesis H that H sometimes becomes completely redundant, and one might as well clear it from the goal. Then, since the inversion typically creates some equality facts, why not subst? Tactic inv does just that.

Exercise: 3 stars, standard (Forall_perm)

Forall is Coq library's version of the All proposition defined in Logic, but defined as an inductive proposition rather than a fixpoint. Prove this lemma by induction. You will need to decide what to induct on: al, bl, Permutation al bl, and Forall f al are possibilities.

Summary: Comparisons and Permutations

To prove correctness of algorithms for sorting and searching, we'll reason about comparisons and permutations using the tools developed in this chapter. The maybe_swap program is a tiny little example of a sorting program. The proof style in maybe_swap_correct will be applied (at a larger scale) in the next few chapters.