Library CoindStart

An Introduction to Coinduction

This material builds on:
  • section 7.1 from the tutorial by Giménez and Castéran {1}
  • sections 5.1 and 5.2 from the CPDT book by Adam Chlipala {2}
{1} A Tutorial on Co-Inductive Types in Coq. Eduardo Giménez, Pierre Castéran.
{2} Certified Programming with Dependent Types. Adam Chlipala. Chapter 5: Coinduction: Infinite Data and Proofs.
Last updated on 2012-12-05 by Catalin Hritcu.

Require Import Bool.
Require Import List.

Require Import CpdtTactics. (* we only use crush *)

Set Implicit Arguments.

Computing with Infinite Data

The most basic type of infinite data is infinite lists, usually known as streams.

CoInductive stream (A : Type) : Type :=
  | Cons : A -> stream A -> stream A.

If we want both finite and infinite lists, then we can also keep the nil constructor (llist stands for ``lazy list'').

CoInductive llist (A: Type) : Type :=
| LNil : llist A
| LCons : A -> llist A -> llist A.

Side-note: The positivity restriction is still there, so we can still not do HOAS:

  CoInductive term : Set :=
  | Var : nat -> term
  | Lam : (term -> term) -> term.
  Error: Non strictly positive occurrence of "term" in
   "(term -> term) -> term".

Exercise (easy)

Define the coinductive types representing the following 3 infinite data structures:
  • infinite binary trees
  • infinitely branching infinite trees (i.e. infinitely wide and infinitely deep)
  • finitely and infinitely branching infinite trees (i.e. finitely or infinitely wide and infinitely deep)
Pattern matching on coinductive values works as usual

Definition head (A : Type) (s : stream A) :=
  match s with
  | Cons a s' => a

Definition tail (A : Type) (s : stream A) :=
  match s with
  | Cons a s' => s'

Exercise (easy)

Using the functions head and tail, define a recursive function that takes the n-th element of an infinite stream. As computer scientists we start counting at 0, so the head of the list is the 0-th element.
Infinite objects are defined using the CoFixpoint command.

CoFixpoint same (A : Type) (a : A) : stream A := Cons a (same a).

Note: whereas recursive definitions (fixpoints) were necessary to use values of recursive inductive types effectively, we need co-recursive definitions (co-fixpoints) to build (infinite) values of co-inductive types
Every CoFixpoint has to return a coinductive type (in the same way every Fixpoint has to take and break up an inductive argument). For instance, this bad co-fixpoint is rejected (it works if we replace CoFixpoint by Definition, though):

  CoFixpoint to_bool (x : stream nat) : bool := false.
Co-inductive values can be arguments to recursive functions. However, there also needs to be an inductive argument in order to convince Coq that the function is terminating. We can use this to write a function that computes the finite approximation of a stream:

Fixpoint approx A (n : nat) (s : stream A) {struct n} : list A :=
  match n with
    | O => nil
    | S n' =>
      match s with
        | Cons h t => h :: approx n' t

Definition ones := same 1.

Eval simpl in approx 10 ones.

We can of course also define ones directly, without using same.

CoFixpoint ones' : stream nat := Cons 1 ones'.

Eval simpl in approx 10 ones'.

In order to prevent non-termination, co-fixpoints are evaluated lazily. They are unfolded only when they appear as the argument of a match expression. We can check this using Eval.

Eval compute in (same 4).

Eval compute in (head (same 4)).

Here are three useful co-recursive functions on streams:

CoFixpoint iterate (A : Type) (f : A -> A) (a : A) : stream A :=
  Cons a (iterate f (f a)).

CoFixpoint map (A B : Type) (f : A -> B) (s : stream A) : stream B :=
  match s with
  | Cons h t => Cons (f h) (map f t)

CoFixpoint interleave (A : Type) (s1 s2 : stream A) : stream A :=
  match s1, s2 with
  | Cons n1 s1', Cons n2 s2' => Cons n1 (Cons n2 (interleave s1' s2'))

Using iterate we can define the stream of natural numbers:

Definition nats : stream nat := iterate S 0.
Eval simpl in approx 10 nats.

We can of course also define nats more directly:

CoFixpoint nats_from_n (n : nat) : stream nat :=
  Cons n (nats_from_n (S n)).
Definition nats' := nats_from_n 0.

Eval simpl in approx 10 nats.

We can define a stream that alternates between true and false using a mutual co-fixpoint (there are simpler ways, though).

Exercise (easy)

Find two more ways for constructing the stream that infinitely alternates the values true and false.
Not every co-fixpoint is accepted by Coq, though: there are important restrictions that are dual to the restrictions on the use of inductive types. Fixpoints consume values of inductive types, with restrictions on which arguments may be passed in recursive calls. Dually, co-fixpoints produce values of co-inductive types, with restrictions on what may be done with the results of co-recursive calls.
Coq enforces that every co-recursive call must be guarded by a constructor; that is, every co-recursive call must be a direct argument to a constructor of the co-inductive type we are generating. For instance, the following co-fixpoint does not pass Coq's guardedness condition:

CoFixpoint looper : stream nat := looper.
Recursive definition of looper is ill-formed.
In environment
looper : stream nat

unguarded recursive call in "looper"
It is a good thing that this guardedness condition is enforced. If the definition of looper were accepted, our head and tail functions would run forever when passed looper, and we would have fallen into inconsistency.
Many other standard functions on lazy data structures (like map, iterate and interleave above) can be implemented easily in Coq. Some, others like filter, cannot be implemented. (Why not?)
We can also not define the length of a stream as an (inductive) natural number, because the fix wouldn't be guarded:

Fixpoint length (A : Type) (s : stream A) : nat :=
  match s with
  | Cons _ s' => S (length s')

Exercise (easy, optional)

Prove that if one interprets bool co-inductively one gets a set that is isomorphic to bool. What's the intuitive reason for this?

Infinite Proofs

Suppose that we wanted to prove formally that the streams nats and nats' from above are equivalent. The naive way to do this is to state it as the following equality:

Theorem nats_eq : nats = nats'.
   unfold nats, nats', nats_from_n, iterate.
   Print eq.

However, faced with the initial subgoal, it is not at all clear how this theorem can be proved. In fact, it is unprovable. The inductive(!) eq predicate that we use is fundamentally limited to equalities that can be demonstrated by finite arguments. All we can prove this way is that any finite approximation of nats and nats' are equal.
First try:

Lemma approx_nats_eq : forall k,
  approx k nats = approx k nats'.
Proof. induction k. intros. reflexivity. simpl. Abort.

For this we need to work we need to first generalize the induction hypothesis and consider increasing streams of naturals starting at any natural number.

Lemma approx_nats_eq_helper : forall k n,
  approx k (iterate S n) = approx k (nats_from_n n).
Proof. induction k; crush. Qed.

Lemma approx_nats_eq : forall k,
  approx k nats = approx k nats'.
Proof. intros. eapply approx_nats_eq_helper. Qed.

In order to deal with interesting properties of infinite objects, it is necessary to construct infinite proofs. What we need for that is a co-inductive proposition. That is, we want to define a proposition whose proofs may be infinite (subject to the guardedness condition, of course).

CoInductive stream_eq (A : Type) : stream A -> stream A -> Prop :=
| Stream_eq : forall (h : A) t1 t2,
        stream_eq t1 t2
     -> stream_eq (Cons h t1) (Cons h t2).

We say that two streams are equal if and only if they have the same heads and their tails are equal. We use normal finite/syntactic equality for the heads, and we refer to our new equality (co-)recursively for the tails.

Exercise (easy, optional)

One might wonder what would happen if we took the definition of eq and interpreted it coinductively. Show that in fact, nothing would change. Define a ceq, a coinductive variant of eq, and prove that it is equivalent to eq.
In order to construct infinite proof terms we need to use a co-fixpoint, the same way we did for constructing infinite program terms. While in programming mode we used CoFixpoint; in tactic mode we can use the related cofix tactic for building co-fixpoints.
Before attacking the slightly harder problem of proving nats and nats' in the stream_eq relation, we first try to prove that ones and ones' are in stream_eq. We start by doing this directly using the cofix tactic.

Theorem ones_eq : stream_eq ones ones'.
  cofix. Show Proof.
  assumption. (* "proof completed" *)
(* Qed. *)
  Unguarded recursive call in "ones_eq"
The same guardedness condition applies to our co-inductive proofs as to our co-inductive data structures. We should be grateful that this proof is rejected, because, if it were not, the same proof structure could be used to prove any co-inductive theorem vacuously, by direct appeal to itself!
Looking at the proof term Coq generates from the proof script above, we see that the problem is that we are violating the guardedness condition.

Show Proof.
  cofix ones_eq  : stream_eq ones ones' := ones_eq
During our proofs, Coq can help us check whether we have yet gone wrong in this way. We can run the command Guarded in any context to see if it is possible to finish the proof in a way that will yield a properly guarded proof term. Guarded works for both fixpoints and co-fixpoints.
Running Guarded here gives us the same error message that we got when we tried to run Qed. In larger proofs, Guarded can be helpful in detecting problems before we think we are ready to run Qed.


We need to start the co-induction by applying stream_eq's constructor. To do that, we need to know that both arguments to the predicate are Conses. Informally, this is trivial, but simpl is not able to help us, because co-fixpoints are evaluated only if there are in a match position.

  simpl. (* does nothing *)


The simplest way to get off the ground with this proof is a commonly used hack:

Theorem stream_eta : forall A (s : stream A),
  s = Cons (head s) (tail s).
Proof. destruct s; reflexivity. Qed.

This theorem turns out to be just what we needed.

Theorem ones_eq : stream_eq ones ones'.

We can use the theorem to rewrite the two streams.

  rewrite (stream_eta ones).
  rewrite (stream_eta ones').

Now simpl is able to reduce the streams.


Why did this silly-looking trick help? The answer has to do with the constraints placed on Coq's evaluation rules by the need for termination. The cofix-related restriction that foiled our first attempt at using simpl is dual to a restriction for fix. In particular, an application of an anonymous fix only reduces when the top-level structure of the recursive argument is known. Otherwise, we would be unfolding the recursive definition ad infinitum.
So fixpoints only reduce when enough is known about the definitions of their arguments. Dually, co-fixpoints only reduce when enough is known about how their results will be used. In particular, a cofix is only expanded when it is the discriminee of a match. If cofixes reduced haphazardly, it would be easy to run into infinite loops in evaluation, since we are, after all, building infinite objects.
Since we have exposed the Cons structure of each stream, we can apply the constructor of stream_eq to conclude the proof.


The example above shows that one can construct infinite proofs by directly using cofix, but there are two important problems with this. First, it's hard to keep guardedness in mind when building large proofs. Second, using cofix directly interacts very badly with Coq's standard automation machinery. If we try to prove ones_eq with automation we get an invalid proof.

Theorem ones_eq' : stream_eq ones ones'.
  cofix; auto. Show Proof.
(* Guarded. *)
Recursive definition of ones_eq'0 is ill-formed.
In environment
ones_eq' : stream_eq ones ones'
ones_eq'0 : stream_eq ones ones'
Unguarded recursive call in "ones_eq'0".
Recursive definition is: "ones_eq'0".

The standard auto machinery sees that our goal matches an assumption and so applies that assumption, even though this violates guardedness. There are hacks that can help us get around this in specific cases. However, we can devise a more principled solution to this problem by looking at how the dual version of the problem is generally solved for induction. It's equally hard to build inductive proofs directly using fix, but one almost never does that. Instead one uses fix to proving general induction principles, and then simply applies those principles.
It turns out that we can usually do the same with co-induction principles. Coq will not generate co-induction principles for us though, so we need to define them by hand using co-fixpoints.

Section stream_eq_coind1.
  Variable A : Type.

The induction principle is parameterized over a (bisimulation) relation of the same type as the relation we're trying to show (stream_eq in this case).

  Variable R : stream A -> stream A -> Prop.

This hypothesis can be easily extracted from the structure of the definition of stream_eq:

  Hypothesis H : forall s1 s2, R s1 s2 ->
    exists h, exists t1, exists t2,
      s1 = Cons h t1 /\ s2 = Cons h t2 /\ R t1 t2.

  Theorem stream_eq_coind1 : forall s1 s2 : stream A,
    R s1 s2 -> stream_eq s1 s2.
  Proof. cofix. intros s1 s2 H0.
    destruct (H H0) as [? [? [? [? [? ?]]]]]. subst.
    apply Stream_eq. apply stream_eq_coind1. assumption.
End stream_eq_coind1.

We can now return to the proof of ones_eq

Theorem ones_eq' : stream_eq ones ones'.
  apply stream_eq_coind1 with
    (R := fun s1 s2 => s1 = ones /\ s2 = ones'); [clear | tauto].

We'll return later on how to mechanically construct the R from the statement of the theorem we're trying to prove. In this case what we do here corresponds to the remember we do before inducting on compound terms.

  intros s1 s2 [? ?]. subst. repeat esplit.
  rewrite (stream_eta ones) at 1. simpl. reflexivity.
  rewrite (stream_eta ones') at 1. simpl. reflexivity.

The previous coinduction principle for stream_eq works, but it can be further simplified to reach a more computational formulation (commonly called Park's principle) that's easier to use in automated proofs.

Section stream_eq_coind.
  Variable A : Type.
  Variable R : stream A -> stream A -> Prop.

We use head and tail instead of existential quantification

  Hypothesis H1 : forall s1 s2,
    R s1 s2 -> head s1 = head s2.
  Hypothesis H2 : forall s1 s2,
    R s1 s2 -> R (tail s1) (tail s2).

We can actually show that H1 /\ H2 is equivalent to the previous H using existential quantification

  Lemma equiv : forall s1 s2, R s1 s2 ->
    ((exists h, exists t1, exists t2,
      s1 = Cons h t1 /\ s2 = Cons h t2 /\ R t1 t2)
    (head s1 = head s2 /\ R (tail s1) (tail s2))).
  Proof. clear; split; intros.
    destruct H0 as [h [t1 [t2 [H1 [H2 H3]]]]].
      subst. simpl. eauto.
    destruct H0 as [H1 H2].
      exists (head s1). exists (tail s1). exists (tail s2).
      destruct s1; destruct s2; simpl in *; subst; intuition.

  Theorem stream_eq_coind : forall s1 s2 : stream A,
    R s1 s2 -> stream_eq s1 s2.
  Proof. cofix. intros s1 s2 H0. destruct s1. destruct s2.
    pose proof (H1 H0). simpl in *. subst.
    pose proof (H2 H0). simpl in *.
    apply Stream_eq. apply stream_eq_coind. assumption.
End stream_eq_coind.

We return again to the proof of ones_eq
The proof is more automated; e.g. we don't need to use the stream_eta trick because head and tail are already defined using match. So crush just does the trick.

Theorem ones_eq'' : stream_eq ones ones'.
  apply stream_eq_coind with
    (R := fun s1 s2 => s1 = ones /\ s2 = ones'); crush.

This principle is better in terms of automation. Let's try to use it to prove that nats and nats' are in stream_eq.

Lemma nats_eq : stream_eq nats nats'.
  apply stream_eq_coind with (R := fun s1 s2 => s1 = nats /\ s2 = nats');

At this point we get two goals that are wrong: iterate S 1 = nats and nats_from_n 1 = nats'. The co-induction hypothesis is not general enough!


In the same way we had to strengthen the inductive hypothesis in approx_nats_eq_helper, here we have to strengthen the co-inductive hypothesis

Lemma nats_eq_helper : forall n,
  stream_eq (iterate S n) (nats_from_n n).
  intro n. apply stream_eq_coind with
    (R := fun s1 s2 => exists n, s1 = iterate S n /\ s2 = nats_from_n n);
      [crush | clear | eauto].
    intros ? ? [n [? ?]]. exists (S n); crush.

Theorem nats_eq : stream_eq nats nats'.
Proof. apply nats_eq_helper. Qed.

Recipe for constructing the "bisimulation" relation

We can choose the instance of R needed for applying stream_eq_coind (or any other induction principle) in a mechanical fashion. We have a goal of the form:
forall x1, ..., xn,
  H1 -> ... -> Hm ->
  P t1 ... tl
Where P is a coinductively defined predicate for which you've already defined a coinduction principle P_coind. In order to call P_coind we need to provide a predicate R. Here is a receipe to build R.

Step 1 (remember and linearize)

Replace any argument tj that's not a variable from xs with a fresh variable yj, universally quantify over yj at the top and add an additional hypothesis Hj : yj = tk. Repeat this until the goal looks like this:
forall x1, ..., xn,
  H1' -> ... -> Hm' ->
  P y1 ... yl
This step corresponds to "remember"-ing compound terms before applying induction. Additionally, if a certain y appears twice in the proposition replace one of the occurrences with a fresh variable y' and add an equality of the form y = y' as a hypothesis.

Step 2 (conjunction + existentials)

Construct the conjunction of all premises H1' /\ ... /\ Hm', and existentially quantify over all xs that are not ys:

  exists x1', exists x2', ... exists xn', H1' /\ ... /\ Hm'

Step 3 (add a lambda on top)

Chose R to be:

   (fun y1 ... yl =>
       exists x1', exists x2', ... exists xn',
         H1' /\ ... /\ Hm')
If we wanted to take these steps manually we can do so (below we build tactics that do all these steps automatically)

Lemma exists_forall_impl : forall A (P : A -> Prop) (Q : Prop),
  ((exists x, P x) -> Q) -> forall x : A, P x -> Q.
Proof. firstorder. Qed.

Lemma nats_eq_helper_with_step_by_step_R : forall n,
  stream_eq (iterate S n) (nats_from_n n).
  intro n.

  (* step 1 (remember) *)
  remember (iterate S n). remember (nats_from_n n).

  (* step 2 *)

    (* conjunction *)
    cut (s = iterate S n /\ s0 = nats_from_n n);
      [clear Heqs Heqs0 | tauto].

    (* existential *)
    generalize dependent n. apply exists_forall_impl.

  (* step 3 (apply stream_eq_coind) *)
  generalize dependent s0. generalize dependent s.
  apply stream_eq_coind.

  (* now the real proof *)
  intros s1 s2 [n [H1 H2]]; subst. reflexivity.
  intros s1 s2 [n [H1 H2]]; subst. simpl. eauto.

Automating the whole thing

A slightly improved but slightly less readable version of this is given in CoindTactic.v.

Tactic Notation "if" tactic(t) "then" tactic(t1) "else" tactic(t2) :=
  first [ t; first [ t1 | fail 2 ] | t2 ].

Tactic Notation "if_is_not_var" tactic(t) "then" tactic(t1) :=
  if (is_var t) then idtac else t1.

Ltac step1_arity2 :=
  match goal with
  | [|- ?P ?s ?s] => remember s in * |- * at 1
  | [|- ?P ?s1 ?s2] =>
    (if_is_not_var s1 then remember s1);
    (if_is_not_var s2 then remember s2)

Ltac step1_arity1 :=
  match goal with
  | [|- ?P ?s] =>
    if_is_not_var s then remember s

Ltac step2conj1 :=
  match goal with
  | [|- _] => generalize I

Ltac step2conjn :=
  match goal with
  | [H : ?P |- ?Q -> ?R] =>
    match type of P with
    | Prop => let J := fresh "J" in
              intro J; cut (P /\ Q); [clear H J | tauto]
    | _ => fail

Ltac step2exn_arity2 :=
  match goal with
  | [s1 : _, s2 : _, x : ?T |- ?Q -> ?P ?s1 ?s2] =>
     generalize dependent x; apply exists_forall_impl

Ltac step2exn_arity1 :=
  match goal with
  | [s : _, x : ?T |- ?Q -> ?P ?s] =>
     generalize dependent x; apply exists_forall_impl

Ltac step2_arity2 :=
  step2conj1; repeat step2conjn; repeat step2exn_arity2.

Ltac step2_arity1 :=
  step2conj1; repeat step2conjn; repeat step2exn_arity1.

Ltac step3_arity2 X :=
  match goal with
  | [|- ?Q -> ?P ?s1 ?s2] =>
    generalize dependent s2; generalize dependent s1;
    apply X

Ltac step3_arity1 X :=
  match goal with
  | [|- ?Q -> ?P ?s] => generalize dependent s; apply X

Ltac destrs :=
  match goal with
  | [H : exists x, _ |- _] => destruct H
  | [H : _ /\ _ |- _] => destruct H
  | [H : True |- _] => destruct H

Ltac post := intros; repeat destrs; subst; simpl in *.

Tactic Notation "coind2" "using" constr(X) :=
  intros; step1_arity2; step2_arity2; step3_arity2 X; post.

Tactic Notation "coind1" "using" constr(X) :=
  intros; step1_arity1; step2_arity1; step3_arity1 X; post.

guess the arity of the co-inductive predicate

Tactic Notation "coind" "using" constr(X) :=
  intros; match goal with
          | [|- ?P ?x ?y] => coind2 using X
          | [|- ?P ?x] => coind1 using X

Using coind the proof of nats_eq_helper can be fully automated.

Lemma nats_eq_helper_auto : forall n,
  stream_eq (iterate S n) (nats_from_n n).
Proof. coind using stream_eq_coind; eauto. Qed.

Print nats_eq_helper_auto.

The R chosen by coind is exactly the same as in the manual proof above:

  fun s1 s2 =>
    exists n, s1 = iterate S n /\ s2 = nats_from_n n

Theorem nats_eq_auto : stream_eq nats nats'.
Proof. apply nats_eq_helper_auto. Qed.

Note: We can also prove nats_eq directly, without changing the statement, by choosing the more general R by hand when manually instantiating the coinduction principle. This doesn't seem as good in terms of automation, though.

Theorem nats_eq_direct : stream_eq nats nats'.
  apply stream_eq_coind with
    (R := fun s1 s2 => exists n, s1 = iterate S n /\ s2 = nats_from_n n);
      [crush | clear | eauto].
    intros ? ? [? [? ?]]. subst. simpl. eauto.
    exists 0. eauto.

Exercise (medium)

Prove map_iterate once using the coind tactic and once manually using stream_eq_coind directly. (Hint: if getting stuck in the manual proof try manually unfolding coind and have a look at what it's doing. You don't actually need all baby-steps in coind in this example though.)

Theorem map_iterate : forall (A : Type) (f : A -> A) (x : A),
  stream_eq (iterate f (f x)) (map f (iterate f x)).
  (* write proof here *)

Exercise (medium)

Prove that the equality of streams is an equivalence relation once using the coind tactic. Try to automate your proofs as much as you can.
Hint: try reflexivity first, then symmetry, then transitivity.

Exercise (medium)

Provide a suitable definition of "being an increasing stream of naturals" and define a co-induction principle (similar to the Park principle) for proving that a stream is increasing. Apply this method to prove the stream nats is increasing.
Hint: There are different ways of formulating the definition. If you find yourself having trouble proving things, back up and see if you can state the definition a different way.

Exercise (optional)

Below we define a co-inductive type Nat containing the non-standard natural numbers. Give a co-inductive definition of the ``less than'' (<) relation on Nats and prove that there exists m so that forall n we have that n < m.

CoInductive Nat : Set :=
| NO : Nat
| NS : Nat -> Nat.

CoInductive lt : Nat -> Nat -> Prop :=
  (* write definition here *)

Notation "x < y" := (lt x y).

Theorem non_standard :
  exists m, forall n, lt n m.
  (* write proof here *)

Exercise (hard, optional)

In this exercise we give a coinductive definition characterizing the streams that eventually cycle. Then we represent the Collatz sequence as a stream. It is conjectured that all Collatz sequences eventually cycle (and in particular reach 1 if they weren't 0 to begin with). Prove that the Collatz sequences starting at 5 and 100 eventually cycle.
(Hint: You might need to prove a co-inductive principle for loop, and getting that right will help you have a simple proof. For proving that collatz 100 cycles you might find more aggressive automation via Ltac useful)
We define what it means for a stream to cycle (coinductively)

Fixpoint add A (l : list A) (s : stream A) : stream A :=
  match l with
  | nil => s
  | h :: t => Cons h (add t s)

CoInductive loops A (l : list A) : stream A -> Prop :=
| ladd : forall s, loops l s -> loops l (add l s).

Fixpoint drop A (n : nat) (s : stream A) : stream A :=
  match n with
  | 0 => s
  | S n' => drop n' (tail s)

Definition cycles A (s : stream A) :=
  exists n, exists l, loops l (drop n s).

Then we represent that the Collatz sequence as a stream by iterating the step function cstep below.

Fixpoint evenb (n : nat) : bool :=
  match n with
  | S (S n) => evenb n
  | S n => false
  | O => true

Require Import Arith.Div2.

Definition cstep (n : nat) : nat :=
  if evenb n then div2 n else 3*n+1.

Definition collatz := iterate cstep.

Prove the following two statements:

Lemma cycles_collatz_5 : cycles (collatz 5).
  (* write proof here *)

Lemma cycles_collatz_100 : cycles (collatz 100).
  (* write proof here *)