# Illustrating the paco library

*parameterized coinduction*, as described in our draft paper entitled

*The Power of Parameterization in Coinductive Proof*.

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

*incremental*proofs, i.e., proofs in which the coinduction hypothesis is extended gradually as the proof progresses.

## Example: stream equality

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.

Definition sunf s :=

match s with cons n s' => cons n s' end.

Lemma sunf_eq : ∀ s, s = sunf s.

Proof.

destruct s; auto.

Qed.

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

CoFixpoint enumerate n : stream :=

cons n (enumerate (S n)).

CoFixpoint map f s : stream :=

match s with cons n s' => cons (f n) (map f s') end.

### A proof using cofix

| seq_fold : ∀ n s1 s2 (R : seq s1 s2), seq (cons n s1) (cons n s2).

Inductive seq_gen seq : stream → stream → Prop :=

| _seq_gen : ∀ n s1 s2 (R : seq s1 s2 : Prop), seq_gen seq (cons n s1) (cons n s2).

Hint Constructors seq_gen.

CoInductive seq : stream → stream → Prop :=

| seq_fold : ∀ s1 s2, seq_gen seq s1 s2 → seq s1 s2.

Second, we do the actual proof.

Theorem example : ∀ n, seq (enumerate n) (cons n (map S (enumerate n))).

Proof.

cofix CIH.

intros; apply seq_fold.

pattern (enumerate n) at 1; rewrite sunf_eq; simpl.

constructor.

rewrite (sunf_eq (enumerate n)); simpl.

rewrite (sunf_eq (map _ _)); simpl.

apply CIH.

Qed.

*Note*: One might want to eliminate the use of pattern in the proof script by replacing the corresponding line with the following:

### A proof using our pcofix

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

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

Definition seq' s1 s2 := paco2 seq_gen bot2 s1 s2.

Hint Unfold seq'.

Lemma seq_gen_mon: monotone2 seq_gen. Proof. pmonauto. Qed.

Hint Resolve seq_gen_mon : paco.

Theorem example' : ∀ n, seq' (enumerate n) (cons n (map S (enumerate n))).

Proof.

pcofix CIH.

intros; pfold.

rewrite sunf_eq at 1; simpl.

constructor.

rewrite (sunf_eq (enumerate n)); simpl.

rewrite (sunf_eq (map _ _)); simpl.

right; apply CIH.

Qed.

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.
To understand seq' and the proof of example', we have to
explain some background. Given a monotone function f, we call
paco2 f the
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
To fold and unfold parameterized fixed points, we provide two
tactics, where upaco2 f r := paco2 f r ∪ 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
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.

#### How it works:

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

- 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

============================

∀ n : nat, seq (enumerate n) (cons n (map S (enumerate n)))

*cannot*apply CIH immediately to "solve" the goal: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)))

n : nat

============================

seq_gen seq (cons n (enumerate (S n))) (cons n (map S (enumerate n)))

n : nat

============================

seq (enumerate (S n)) (cons (S n) (map S (enumerate (S n))))

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

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

### Another example

Here is a proof for seq.

Theorem seq_cons : ∀ n1 n2 s1 s2 (SEQ : seq (cons n1 s1) (cons n2 s2)),

n1 = n2 ∧ seq s1 s2.

Proof.

intros.

inversion_clear SEQ; rename H into SEQ.

inversion_clear SEQ; auto.

Qed.

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

Theorem seq'_cons : ∀ n1 n2 s1 s2 (SEQ : seq' (cons n1 s1) (cons n2 s2)),

n1 = n2 ∧ seq' s1 s2.

Proof.

intros.

punfold SEQ.

inversion_clear SEQ; pclearbot; auto.

Qed.

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

## Example: infinite tree equality

CoInductive inftree :=

| node : nat → inftree → inftree → inftree.

Definition tunf t : inftree :=

match t with node n tl tr => node n tl tr end.

Lemma tunf_eq : ∀ t, t = tunf t.

Proof.

destruct t; auto.

Qed.

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

CoFixpoint one : inftree := node 1 one two

with two : inftree := node 2 one two.

CoFixpoint eins : inftree := node 1 eins (node 2 eins zwei)

with zwei : inftree := node 2 eins zwei.

### Incremental proofs using cofix

Inductive teq_gen teq : inftree → inftree → Prop :=

| _teq_gen : ∀ n t1l t1r t2l t2r (Rl : teq t1l t2l : Prop) (Rr : teq t1r t2r),

teq_gen teq (node n t1l t1r) (node n t2l t2r).

Hint Constructors teq_gen.

CoInductive teq t1 t2 : Prop :=

| teq_fold (IN : teq_gen teq t1 t2).

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.Theorem teq_one : teq one eins.

Proof.

cofix CIH.

apply teq_fold.

rewrite (tunf_eq one), (tunf_eq eins); simpl.

constructor; auto.

apply teq_fold.

rewrite (tunf_eq two); simpl.

constructor; auto.

cofix CIH'.

apply teq_fold.

rewrite (tunf_eq two), (tunf_eq zwei); simpl.

constructor; auto.

Qed.

Theorem teq_two : teq two zwei.

Proof.

cofix CIH.

apply teq_fold.

rewrite (tunf_eq two), (tunf_eq zwei); simpl.

constructor; auto.

cofix CIH'.

apply teq_fold.

rewrite (tunf_eq one), (tunf_eq eins); simpl.

constructor; auto.

apply teq_fold.

rewrite (tunf_eq two); simpl.

constructor; auto.

Qed.

### Incremental proofs using our pcofix

Definition teq' t1 t2 := paco2 teq_gen bot2 t1 t2.

Hint Unfold teq'.

Lemma teq_gen_mon: monotone2 teq_gen. Proof. pmonauto. Qed.

Hint Resolve teq_gen_mon : paco.

Theorem teq'_one : teq' one eins.

Proof.

pcofix CIH.

pfold.

rewrite (tunf_eq one), (tunf_eq eins); simpl.

constructor; auto.

left; pfold.

rewrite (tunf_eq two); simpl.

constructor; auto.

left; pcofix CIH'.

pfold.

rewrite (tunf_eq two), (tunf_eq zwei); simpl.

constructor; auto.

Qed.

Theorem teq'_two : teq' two zwei.

Proof.

pcofix CIH.

pfold.

rewrite (tunf_eq two), (tunf_eq zwei); simpl.

constructor; auto.

left; pcofix CIH'.

pfold.

rewrite (tunf_eq one), (tunf_eq eins); simpl.

constructor; auto.

left; pfold.

rewrite (tunf_eq two); simpl.

constructor; auto.

Qed.

### Pseudo-compositional proofs using cofix

Lemma teq_two_one_bad : teq two zwei → teq one eins.

Proof.

intros; rewrite (tunf_eq two), (tunf_eq zwei) in H.

destruct H; inversion IN; auto.

Defined.

Lemma teq_two_one : teq two zwei → teq one eins.

Proof.

intros; cofix CIH.

apply teq_fold.

rewrite (tunf_eq one), (tunf_eq eins); simpl.

constructor; auto.

apply teq_fold.

rewrite (tunf_eq two); simpl.

constructor; auto.

Defined.

Lemma teq_one_two : teq one eins → teq two zwei.

Proof.

intros; cofix CIH.

apply teq_fold.

rewrite (tunf_eq two), (tunf_eq zwei); simpl.

constructor; auto.

Defined.

Theorem teq_eins : teq one eins.

Proof.

cofix CIH.

apply teq_two_one, teq_one_two, CIH.

Qed.

Theorem teq_zwei : teq two zwei.

Proof.

cofix CIH.

apply teq_one_two, teq_two_one, CIH.

Qed.

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

Theorem teq_eins_bad : teq one eins.

Proof.

cofix CIH.

apply teq_two_one_bad, teq_one_two, CIH.

Abort.

### Compositional proofs using our pcofix

*not*a proof of the corresponding lemma here, and (ii) we are not forced to make the lemmas transparent.

Lemma teq'_two_one : ∀ r,

(r two zwei : Prop) → paco2 teq_gen r one eins.

Proof.

intros; pcofix CIH.

pfold.

rewrite (tunf_eq one), (tunf_eq eins); simpl.

constructor; auto.

left; pfold.

rewrite (tunf_eq two); simpl.

constructor; auto.

Qed.

Lemma teq'_one_two : ∀ r,

(r one eins : Prop) → paco2 teq_gen r two zwei.

Proof.

intros; pcofix CIH.

pfold.

rewrite (tunf_eq two), (tunf_eq zwei); simpl.

constructor; auto.

Qed.

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

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

Theorem teq'_eins : teq' one eins.

Proof.

pcofix CIH.

pmult; apply teq'_two_one, teq'_one_two, CIH.

Qed.

Theorem teq'_zwei : teq' two zwei.

Proof.

pcofix CIH.

pmult; apply teq'_one_two, teq'_two_one, CIH.

Qed.

## Example: mutual coinduction

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

Inductive eqone_gen eqone eqtwo : inftree → Prop :=

| _eqone_gen : ∀ tl tr (EQL : eqone tl : Prop) (EQR : eqtwo tr : Prop),

eqone_gen eqone eqtwo (node 1 tl tr).

Inductive eqtwo_gen eqone eqtwo : inftree → Prop :=

| _eqtwo_gen : ∀ tl tr (EQL : eqone tl : Prop) (EQR : eqtwo tr : Prop),

eqtwo_gen eqone eqtwo (node 2 tl tr).

Hint Constructors eqone_gen eqtwo_gen.

### A proof via cofix

CoInductive eqone (t : inftree) : Prop :=

| eqone_fold (EQ : eqone_gen eqone eqtwo t)

with eqtwo (t : inftree) : Prop :=

| eqtwo_fold (EQ : eqtwo_gen eqone eqtwo t).

Lemma eqone_eins : eqone eins.

Proof.

cofix CIH0; apply eqone_fold.

rewrite tunf_eq; simpl; constructor.

apply CIH0.

cofix CIH1; apply eqtwo_fold.

constructor.

apply CIH0.

rewrite tunf_eq; apply CIH1.

Qed.

### A proof via pcofix

Definition eqone' t := paco1_2_0 eqone_gen eqtwo_gen bot1 bot1 t.

Definition eqtwo' t := paco1_2_1 eqone_gen eqtwo_gen bot1 bot1 t.

Hint Unfold eqone' eqtwo'.

Lemma eqone_gen_mon: monotone1_2 eqone_gen. Proof. pmonauto. Qed.

Lemma eqtwo_gen_mon: monotone1_2 eqtwo_gen. Proof. pmonauto. Qed.

Hint Resolve eqone_gen_mon eqtwo_gen_mon : paco.

Lemma eqone'_eins: eqone' eins.

Proof.

pcofix CIH0; pfold.

rewrite tunf_eq; simpl; constructor.

right; apply CIH0.

left; pcofix CIH1; pfold.

constructor.

right; apply CIH0.

right; rewrite tunf_eq; apply CIH1.

Qed.

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

This page has been generated by coqdoc