## Coinduction in Coq and Isabelle

Published 2017-07-27 in sections English, Coq.

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

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.

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

``````module ENat where

data ENat' (ENat : Set) : Set where
N : ENat' ENat
S : ENat → ENat' ENat

record ENat : Set where
coinductive
field force-ENat : ENat' ENat

open ENat

min : ENat → ENat → ENat
min n m .force-ENat with force-ENat n | force-ENat m
... | (S n') | (S m') = S (min n' m')
... | _      | _      = N

data le' (_<_ : ENat → ENat → Set) : ENat' ENat → ENat' ENat → Set where
N : ∀ {m}           → le' _<_ N m
S : ∀ {n m} → n < m → le' _<_ (S n) (S m)

record _<_ (n m : ENat) : Set where
coinductive
field force-< : le' _<_ (force-ENat n) (force-ENat m)

open _<_

min-< : ∀ n m → min n m < n
min-< n m .force-< with force-ENat n | force-ENat m
... | N    | _    = N
... | S n' | N    = N
... | S n' | S m' = S (min-< n' m')``````
#1 am 2017-07-27

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.

#2 am 2017-07-28

The old coinductives presented in Coq are broken in the sense that using them breaks subject reduction because they are treated as positive types enjoying full dependent elimination which is wrong. To see, why, in your example you show:

``````Lemma evalN_eq : forall n, evalN n = n.
Proof. intros. destruct n; reflexivity. Qed.``````

Now if you take the infinite successor N and build `evalN_eq infS`, you have a closed term of type `evalN infS = infS` in the empty context, so by canonicity it should be convertible to `eq_refl`, however:

``````CoFixpoint infS : ENat := S infS.

Eval simpl in evalN_eq infS.
Fail Check eq_refl : evalN infS = infS.``````

This happens because one cannot “blindly” unfold cofixpoints during conversion, only a “match” on a cofixpoint value reduces, but there’s no match here in the (`evalN infS = infS`) type so Coq compares only the codes (not the behavior) of the two cofixpoints and fails. The solution adopted in Agda can also be formalized in Coq using CoInductive primitive records, which treat coinductive values as “negative” connectives not subject to full dependent elimination, as they can now only be accessed through their projections (`evalN` cannot be defined on this type).

``````Require Import Utf8.
Set Primitive Projections.
Inductive ENat' (ENat : Set) : Set :=
| N : ENat' ENat
| S : ENat -> ENat' ENat.
Arguments N [ENat].
Arguments S [ENat] x.

CoInductive ENat : Set :=
{ forceENat : ENat' ENat }.

Definition min_ENat' (min : ENat -> ENat -> ENat) (n m : ENat' ENat) : ENat' ENat :=
match n, m with
| S n', S m' => S (min n' m')
| _, _ => N
end.

CoFixpoint min (n : ENat) (m : ENat) : ENat :=
{| forceENat := min_ENat' min (forceENat n) (forceENat m) |}.

Inductive le' {le : ENat → ENat → Set} : ENat' ENat → ENat' ENat → Set :=
leN : ∀ {m}           , le' N m
| leS : ∀ {n m}, le n m → le' (S n) (S m).

CoInductive le (n m : ENat) : Set :=
{ forcele : @le' le (forceENat n) (forceENat m) }.

(** Use program mode for bidirectional typing hint *)
Set Program Mode.
Require Import Coq.Program.Tactics.

CoFixpoint minle (n m : ENat) : le (min n m) n :=
{| forcele := match forceENat n as n', forceENat m as m' return @le' le (min_ENat' min n' m') n' with
| N, _ => leN
| S n', N => leN
| S n', S m' => leS (minle n' m')
end |}.``````

Hope this helps understanding this rather subtle but essential difference.

#3 am 2017-11-25

Now if you take the infinite successor N and build `evalN_eq infS`, you have a closed term of type `evalN infS = infS` in the empty context, so by canonicity it should be convertible to `eq_refl`, however:

``````CoFixpoint infS : ENat := S infS.

Eval simpl in evalN_eq infS.
Fail Check eq_refl : evalN infS = infS.``````

naively, I wonder: so what? What are the (negative) consequences of this?

#4 am 2017-11-25

The negative consequence is that the system does not enjoy subject reduction anymore. Morally, equality of coonductive values should be bisimulation instead of the very intentional `@eq` type of Coq. OTT and HoTT are both leaning towards such a definition of equality. In that case the dependent elimination would be ok I think, as every construction of the language would respect bisimulation instead of the more restrictive intensional equality. The problem becomes that there’s not only eqrefl as an inhabitant of the equality type anymore so canonicity becomes more complicated (see canonicity for cubical TT for example).

#5 am 2017-11-25

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.