Illustrating the paco library

This tutorial shows how to use our paco library to reason about coinductive predicates in Coq. By coinductive predicates we mean objects that one can define using CoInductive and whose type ends in Prop. The library implements parameterized coinduction, as described in our draft paper entitled The Power of Parameterization in Coinductive Proof . How does parameterized coinduction compare to Coq's existing support for coinductive proofs? For proofs by induction, Coq provides a tactic called fix, but proofs done directly with fix are required to satisfy a syntactic guardedness criterion. Fortunately, Coq also generates induction lemmas for every inductive definition, which eliminate the need to ever use the low-level fix tactic and worry about guardedness. For proofs by coinduction, Coq provides a tactic cofix analogous to fix, i.e., also based on a syntactic guardedness criterion. However, Coq does not generate any lemmas for coinductive definitions. Consequently, to reason about such definitions, the user must use the low-level cofix tactic. Due to its syntactic nature, cofix is problematic in several ways (please see the paper linked above for detailed discussion of these points):

• It is non-compositional.
• It is inefficient.
• It is not user-friendly.
• It interacts poorly with builtin automation tactics.

The paco library provides a tactic, pcofix, which can be seen as a replacement for Coq's builtin cofix tactic (in the case of predicates) that does not involve any syntactic guardedness criterion and thus avoids all of these problems. In addition, like Coq's cofix, pcofix provides built-in support for incremental proofs, i.e., proofs in which the coinduction hypothesis is extended gradually as the proof progresses. We believe this combination of compositionality, incrementality, robustness, and ease of use makes pcofix a superior alternative to cofix for proofs about coinductive predicates. The rest of this tutorial illustrates the use of the paco library with the help of three examples.

Example: stream equality

The first example involves streams of natural numbers and an equality thereon. We prove a particular equality via cofix, and then explain how that proof can be turned into one via pcofix. We start by defining a type of streams of natural numbers.

The following, seemingly useless, lemma is a common trick for working with corecursive terms such as our streams. (It will be used in the example proofs.) For details, see for instance Adam Chlipala's book on Certified Programming with Dependent Types.

In order to state our example equality, we define an enumeration stream and a map operation for streams.

A proof using cofix

We will now prove, using cofix, that for any n the stream enumerate n is equal to the stream cons n (map S (enumerate n)). First, we define an equality seq on streams. Usually, one would do this as follows. CoInductive seq : stream → stream → Prop :=
| seq_fold : ∀ n s1 s2 (R : seq s1 s2), seq (cons n s1) (cons n s2). Instead, we define the generating function, seq_gen, beforehand, and then define seq as its greatest fixed point using CoInductive. The reason is simply that we need seq_gen later when using paco. If applying parameterized coinduction to an existing development where the generating function is not explicit, it can always easily be made explicit. Note that, albeit the use of Inductive, the definition of seq_gen is not recursive.

Second, we do the actual proof.

Note: One might want to eliminate the use of pattern in the proof script by replacing the corresponding line with the following: rewrite sunf_eq at 1; simpl. However, doing so will result in an invalid proof (rejected at Qed-time). The reason is that the proof term created by rewrite ... at 1 involves some lemmas from the Setoid library. Like most lemmas, these are opaque, so guardedness checking cannot inspect their proofs and thus fails. This is a great example of two of the previously mentioned problems with the cofix approach, namely lack of compositionality and poor interaction with standard tactics.

A proof using our pcofix

We will now do the same proof, but using the paco library. We first simply show the new (but equivalent) definition of stream equality and the new proof of the example, and then explain what is going on behind the scenes. In both, we use paco constructs with suffix "2" because we are dealing with predicates of arity 2 here. Note: Paco supports predicates of arity up to 8. Also, it supports up to three mutually coinductive predicates (see the last example of this tutorial). In either case, extending this is just a matter of copy and paste. We also have to prove monotonicity of the generating function seq_gen, which can be discharged by the tactic pmonauto, and register it in the Hint databse paco. Remark: Unlike CoInductive, paco does not care whether the generating function is given in a strictly positive syntactic form; all that matters is that the function is monotone. More specifically, paco2 f is well defined for an arbitrary generating function f regardless of whether it is monotone or not. However, in order to ensure that paco2 f bot2 is the greatest fixed point of f, we need monotonicity of f.

Observe that the proof script is essentially the same as before (this is no accident). The main change is the use of pcofix instead of cofix, which allows us to avoid any syntactic guardedness checking at Qed-time. As a minor benefit of that, we are able to use rewrite ... at 1, which we could not do before.

How it works:

To understand seq' and the proof of example', we have to explain some background. Given a monotone function f, we call paco2 f the parameterized greatest fixed point of f. For a relation r, paco2 f r is defined as the greatest fixed point of the function fun x => f (x ∪ r). Clearly, paco2 f bot2 (where bot2 is the empty relation) is just the ordinary greatest fixed point of f. Let us look at our example domain to understand better. A proof of paco2 seq_gen r s1 s2 can be seen as a proof of r ⊆ seq → seq s1 s2, where the use of the premise is guarded semantically, rather than syntactically. More precisely, paco2 seq_gen r relates two streams iff their heads are equal and their tails are either related by r or again related by paco2 seq_gen r. Compare this to seq, the ordinary greatest fixed point of seq_gen, which relates two streams iff their heads are equal and their tails are again related by seq. This should also make it clear why our definition of seq' is equivalent to seq. To fold and unfold parameterized fixed points, we provide two tactics, where upaco2 f r := paco2 f r ∪ r:

• pfold : when the conclusion is paco2 f r for some f and r, pfold converts it to f (upaco2 f r)
• punfold H : when the hypothesis H is paco2 f r for some f and r, punfold H converts it to f (upaco2 f r)

Other useful lemmas are:

• paco2_mon f : monotone2 (paco2 f)
• paco2_mult f : ∀ r, paco2 f (paco2 f r) ⊆ paco2 f r
• paco2_mult_strong f : ∀ r, paco2 f (upaco2 f r) ⊆ paco2 f r

We will see an example involving paco2_mult in a moment. But first let us have another look at the proof scripts of example and example'. In the former, after calling cofix, the proof state is as follows: CIH : ∀ n : nat, seq (enumerate n) (cons n (map S (enumerate n)))
============================
∀ n : nat, seq (enumerate n) (cons n (map S (enumerate n)))
In this state, the hypothesis precisely matches the conclusion, and there is nothing preventing one from simply concluding the goal directly. Of course, if one were to do that, one's "proof" would be subsequently rejected by Qed for failing to obey syntactic guardedness. Calling pcofix results in a similar state, except that the added hypothesis CIH now governs a fresh relation variable r, which represents the current coinduction hypothesis relating enumerate n and cons n (map S (enumerate n)) for all n. The new goal then says that, in proving the two streams equal, we can use r coinductively, but only in a semantically guarded position, i.e. after unfolding paco2 seq_gen r. In particular, one cannot apply CIH immediately to "solve" the goal: r : stream → stream → Prop
CIH : ∀ n : nat, r (enumerate n) (cons n (map S (enumerate n)))
============================
∀ n : nat, paco2 seq_gen r (enumerate n) (cons n (map S (enumerate n)))
The remaining differences between the proof scripts of example and example' are as follows. First, let us examine example. After applying seq_fold and unfolding enumerate n in the proof of example, we have the following goal: CIH : ∀ n : nat, seq (enumerate n) (cons n (map S (enumerate n)))
n : nat
============================
seq_gen seq (cons n (enumerate (S n))) (cons n (map S (enumerate n)))
By the definition of seq_gen and unfolding map S (enumerate n), this reduces to showing CIH : ∀ n : nat, seq (enumerate n) (cons n (map S (enumerate n)))
n : nat
============================
seq (enumerate (S n)) (cons (S n) (map S (enumerate (S n))))
which follows directly by applying the coinduction hypothesis CIH. In the case of example', the proof is slightly different. First, we use the tactic pfold rather than apply seq_fold, simply because we now reason about seq' rather than seq. After applying pfold and unfolding enumerate n, we have: r : stream → stream → Prop
CIH : ∀ n : nat, r (enumerate n) (cons n (map S (enumerate n)))
n : nat
============================
seq_gen (paco2 seq_gen r ∪ r) (cons n (enumerate (S n))) (cons n (map S (enumerate n)))
As you see, the relation r appears in the argument of seq_gen. Thus by definition of seq_gen and unfolding map S (enumerate n), we need to show enumerate (S n) and cons (S n) (map S (enumerate (S n))) are related by either paco2 seq_gen r or r: r : stream → stream → Prop
CIH : ∀ n : nat, r (enumerate n) (cons n (map S (enumerate n)))
n : nat
============================
paco2 seq_gen r (enumerate (S n)) (cons (S n) (map S (enumerate (S n))))
\/ r (enumerate (S n)) (cons (S n) (map S (enumerate (S n))))
As the coinduction hypothesis gives us that they are related by r, we first have to select the right disjunct, before we apply CIH. Summing up, the two proofs are very similar, but in the one using paco, the guardedness of the coinduction is guaranteed at every step by the way the proof is constructed, rather than by a syntactic check of the whole proof term after the fact.

Another example

Before moving on to the second part, we briefly demonstrate the use of the tactics punfold and pclearbot.

Here is a proof for seq.

And here is the corresponding proof for seq'. Note that the tactic pclearbot simplifies all hypotheses of the form upaco{n} gf bot{n} to paco{n} gf bot{n}.

We also provide two tactics pdestruct and pinversion. They are simply defined as follows:

• pdestruct H := punfold H; destruct H; pclearbot
• pinversion H := punfold H; inversion H; pclearbot

Using this the proof of the above theorem seq'_cons can be simplified as intros; pinversion SEQ; auto.

Example: infinite tree equality

The second example involves infinite binary trees of natural numbers and an equality thereon. We prove two particular equalities via cofix in an incremental fashion, and then show how these proofs can be done just as easily via pcofix. We then show how, using pcofix, the proofs can additionally be modularly decomposed. As before, we first define the coinductive type and the unfolding trick.

In order to state our example equalities, we define the following four trees.

Incremental proofs using cofix

As before, we define the tree equality as the greatest fixed point of its generating function.

We now prove, using cofix, that one equals eins and, separately, that two equals zwei. Note the nested use of cofix in either proof script, which lets us strengthen the coinductive hypothesis in the middle of the proof. For instance, in the proof teq_one, we start out with the coinductive hypothesis that one and eins are equal (CIH). Later on, we use cofix again to additionally assume that two and zwei are equal (CIH'). This is a prime example of incremental proof: we start with no coinductive assumptions, and we progressively add more coinductive assumptions as the proof progresses.

Incremental proofs using our pcofix

As before, we can easily turn the above cofix-proofs into pcofix-proofs.

Pseudo-compositional proofs using cofix

It is easy to see that the proofs of teq_one and teq_two are essentially the same. We can avoid duplicating some work by decomposing the proofs as follows. First we prove that teq two zwei holds under the coinductive assumption teq one eins. This is basically the second part of the proof of teq_one (and the first part of the proof of teq_two). Then we prove the converse, i.e., that teq one eins holds under the coinductive assumption teq two zwei. This is basically the first part of the proof of teq_one (and the second part of the proof of teq_two). The issue is that there seems to be no way to express these two properties. The best we can do is prove teq two zwei → teq one eins and teq one eins → teq two zwei, and make sure that in these proofs any use of the assumption is syntactically guarded. For instance, we are not allowed to prove teq two zwei → teq one eins by inspecting teq two zwei and extracting teq one eins from that (see the proof of teq_two_one_bad below). Although a valid proof of that goal by itself, it could not be composed later to yield a proof of teq one eins or teq two zwei (see the aborted theorem teq_eins_bad below). Moreover, both lemmas must then be made transparent by using Defined instead of Qed at the end, such that, when composing them to prove teq one eins or teq two zwei, guardedness checking can inspect their proof terms. In other words, cofix is not properly compositional.

The following proof would fail guardedness checking at Qed-time, because in the proof of the lemma teq_two_one_bad the assumption is used "too early".

Compositional proofs using our pcofix

Using parameterized coinduction, we can state the actual desired lemmas as follows and prove them using pcofix (again, only minimal changes to the previous proof scripts are required). Observe that (i) the earlier "wrong" proof of teq two zwei → teq one eins (teq_two_one_bad) is not a proof of the corresponding lemma here, and (ii) we are not forced to make the lemmas transparent.

We now compose them with the help of the lemma paco2_mult:

• paco2_mult f : paco2 f (paco2 f r) ⊆ paco2 f r

The tactic pmult applies paco{n}_mult to the conclusion for an appropriate n.

Example: mutual coinduction

The third and last example shows that paco also works for mutual coinduction. Here, the mutuality involves two predicates.

We define two generating functions (using the inftree type from before).

A proof via cofix

Using these, we now define two mutually coinductive predicates eqone and eqtwo. It is easy to see intuitively that they contain all trees that are equal to one and two from above, respectively. We then prove that eqone contains eins.

A proof via pcofix

To define the paco versions of eqone and eqtwo, we apply the two constructors paco1_2_0 and paco1_2_1, respectively ("1" because we are dealing with unary predicates). Again, the translation of the lemma and of its proof is almost trivial.

Remark: For three mutually coinductive predicates, the constructors are paco{n}_3_0, paco{n}_3_1, and paco{n}_3_2.