Joachim Breitner's Homepage

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.