# Joachim Breitner's Homepage

## Coinduction in Coq and Isabelle

The DeepSpec Summer School is almost over, and I have had a few good discussions. One revolved around coinduction: What is it, how does it differ from induction, and how do you actually prove something. In the course of the discussion, I came up with a very simple coinductive exercise, and solved it both in Coq and Isabelle

### The task

Define the extended natural numbers coinductively. Define the min function and the ≤ relation. Show that min(*n*, *m*) ≤ *n* holds.

### Coq

The definitions are straight forward. Note that in Coq, we use the same command to define a coinductive data type and a coinductively defined relation:

```
CoInductive ENat :=
| N : ENat
| S : ENat -> ENat.
CoFixpoint min (n : ENat) (m : ENat)
:=match n, m with | S n', S m' => S (min n' m')
| _, _ => N end.
CoInductive le : ENat -> ENat -> Prop :=
| leN : forall m, le N m
| leS : forall n m, le n m -> le (S n) (S m).
```

The lemma is specified as

`Lemma min_le: forall n m, le (min n m) n.`

and the proof method of choice to show that some coinductive relation holds, is `cofix`

. One would wish that the following proof would work:

```
Lemma min_le: forall n m, le (min n m) n.
Proof.
cofix.
destruct n, m.
* apply leN.
* apply leN.
* apply leN.
* apply leS.
apply min_le.
Qed.
```

but we get the error message

```
Error:
In environment
min_le : forall n m : ENat, le (min n m) n
Unable to unify "le N ?M170" with "le (min N N) N
```

Effectively, as Coq is trying to figure out whether our proof is correct, i.e. type-checks, it stumbled on the equation `min N N = N`

, and like a kid scared of coinduction, it did not dare to “run” the `min`

function. The reason it does not just “run” a `CoFixpoint`

is that doing so too daringly might simply not terminate. So, as Adam explains in a chapter of his book, Coq reduces a cofixpoint *only* when it is the scrutinee of a `match`

statement.

So we need to get a `match`

statement in place. We can do so with a helper function:

```
Definition evalN (n : ENat) :=
match n with | N => N
| S n => S n end.
Lemma evalN_eq : forall n, evalN n = n.
Proof. intros. destruct n; reflexivity. Qed.
```

This function does not really do anything besides nudging Coq to actually evaluate its argument to a constructor (`N`

or `S _`

). We can use it in the proof to guide Coq, and the following goes through:

```
Lemma min_le: forall n m, le (min n m) n.
Proof.
cofix.
destruct n, m; rewrite <- evalN_eq with (n := min _ _).
* apply leN.
* apply leN.
* apply leN.
* apply leS.
apply min_le.
Qed.
```

### Isabelle

In Isabelle, definitions and types are very different things, so we use different commands to define `ENat`

and `le`

:

```
theory ENat imports Main begin
codatatype ENat = N | S ENat
primcorec min where
"min n m = (case n of
N ⇒ N
| S n' ⇒ (case m of
N ⇒ N
| S m' ⇒ S (min n' m')))"
coinductive le where
leN: "le N m"
| leS: "le n m ⟹ le (S n) (S m)"
```

There are actually many ways of defining `min`

; I chose the one most similar to the one above. For more details, see the `corec`

tutorial.

Now to the proof:

```
lemma min_le: "le (min n m) n"
proof (coinduction arbitrary: n m)
case le
show ?case
proof(cases n)
case N then show ?thesis by simp
next
case (S n') then show ?thesis
proof(cases m)
case N then show ?thesis by simp
next
case (S m') with ‹n = _› show ?thesis
unfolding min.code[where n = n and m = m]
by auto
qed
qed
qed
```

The `coinduction`

proof methods produces this goal:

```
proof (state)
goal (1 subgoal):
1. ⋀n m. (∃m'. min n m = N ∧ n = m') ∨
(∃n' m'.
min n m = S n' ∧
n = S m' ∧
((∃n m. n' = min n m ∧ m' = n) ∨ le n' m'))
```

I chose to spell the proof out in the Isar proof language, where the outermost proof structure is done relatively explicity, and I proceed by case analysis mimiking the `min`

function definition.

In the cases where one argument of `min`

is `N`

, Isabelle’s *simplifier* (a term rewriting tactic, so to say), can solve the goal automatically. This is because the `primcorec`

command produces a bunch of lemmas, one of which states `n = N ∨ m = N ⟹ min n m = N`

.

In the other case, we need to help Isabelle a bit to reduce the call to `min (S n) (S m)`

using the `unfolding`

methods, where `min.code`

contains exactly the equation that we used to specify `min`

. Using just `unfolding min.code`

would send this method into a loop, so we restrict it to the concrete arguments `n`

and `m`

. Then `auto`

can solve the remaining goal (despite all the existential quantifiers).

### Summary

Both theorem provers are able to prove the desired result. To me it seems that it is slightly more convenient in Isabelle because a lot of Coq infrastructure relies on the type checker being able to effectively evaluate expressions, which is tricky with cofixpoints, wheras *evaluation* plays a much less central role in Isabelle, where *rewriting* is the crucial technique, and while one still cannot simply throw `min.code`

into the simpset, so working with objects that do not evaluate easily or completely is less strange.

### Agda

I was challenged to do it in Agda. Here it is:

```
module ENat where
open import Coinduction
data ENat : Set where
N : ENat
S : ∞ ENat → ENat
min : ENat → ENat → ENat
min (S n') (S m') = S (♯ (min (♭ n') (♭ m')))
min _ _ = N
data le : ENat → ENat → Set where
leN : ∀ {m} → le N m
leS : ∀ {n m} → ∞ (le (♭ n) (♭ m)) → le (S n) (S m)
min_le : ∀ {n m} → le (min n m) n
min_le {S n'} {S m'} = leS (♯ min_le)
min_le {N} {S m'} = leN
min_le {S n'} {N} = leN
min_le {N} {N} = leN
```

I will refrain from commenting it, because I do not really know what I have been doing here, but it typechecks, and refer you to the official documentation on coinduction in Agda. But let me note that I wrote this using plain inductive types and recursion, and added `∞`

, `♯`

and `♭`

until it worked.

## Comments

You may also be interested in Johannes Hölzl's implementation of coinductive predicates in pure Lean, which compile down to inductive predicates. Doing the same for coinductive types is an open issue.

Have something to say? You can post a comment by sending an e-Mail to me at <mail@joachim-breitner.de>, and I will include it here.

FYI, "musical" coinduction is deprecated in Agda. Agda's new coinduction framework differs significantly from Coq's and solves a lot of issues, among them the one where you have to manually unfold cofixpoints everywhere. I can rewrite the example in the new style