# Library CoindStart

# An Introduction to Coinduction

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

Require Import Bool.

Require Import List.

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

Set Implicit Arguments.

## Computing with Infinite Data

*streams*.

If we want

*both*finite and infinite lists, then we can also keep the nil constructor (llist stands for ``lazy list'').
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.
Pattern matching on coinductive values works as usual

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)

Definition head (A : Type) (s : stream A) :=

match s with

| Cons a s' => a

end.

Definition tail (A : Type) (s : stream A) :=

match s with

| Cons a s' => s'

end.

#### 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.
Note: whereas recursive definitions (fixpoints) were necessary to
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:

*use*values of recursive inductive types effectively, we need co-recursive definitions (co-fixpoints) to*build*(infinite) values of co-inductive typesCoFixpoint to_bool (x : stream nat) : bool := false.

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

end

end.

Definition ones := same 1.

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

end.

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

end.

Using iterate we can define the stream of natural numbers:

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).CoFixpoint trues_falses : stream bool := Cons true falses_trues

with falses_trues : stream bool := Cons false trues_falses.

#### Exercise (easy)

Find two more ways for constructing the stream that infinitely alternates the values true and false.*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.

CoFixpoint looper : stream nat := looper.

Error: Recursive definition of looper is ill-formed. In environment looper : stream nat unguarded recursive call in "looper"

Fixpoint length (A : Type) (s : stream A) : nat :=

match s with

| Cons _ s' => S (length s')

end.

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

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

#### 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.Theorem ones_eq : stream_eq ones ones'.

cofix. Show Proof.

assumption. (* "proof completed" *)

(* Qed. *)

Unguarded recursive call in "ones_eq"

Show Proof.

cofix ones_eq : stream_eq ones ones' := ones_eq

*before*we think we are ready to run Qed.

Restart.

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.

cofix.

simpl. (* does nothing *)

Abort.

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.

We can use the theorem to rewrite the two streams.

Now simpl is able to reduce the streams.

simpl.

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
Since we have exposed the Cons structure of each stream, we
can apply the constructor of stream_eq to conclude the proof.

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

assumption.

Qed.

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.

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

Abort.

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
It turns out that we can usually do the same with

*induction principles*, and then simply applies those principles.*co-induction principles*. Coq will not generate co-induction principles for us though, so we need to define them by hand using co-fixpoints.
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).

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.

Qed.

End stream_eq_coind1.

We can now return to the proof of ones_eq

Theorem ones_eq' : stream_eq ones ones'.

Proof.

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.

Qed.

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.

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

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.

Qed.

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.

Qed.

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

Proof.

apply stream_eq_coind with

(R := fun s1 s2 => s1 = ones /\ s2 = ones'); crush.

Qed.

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

Proof.

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

crush.

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!

Abort.

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

Proof.

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.

Qed.

Theorem nats_eq : stream_eq nats nats'.

Proof. apply nats_eq_helper. Qed.

### Recipe for constructing the "bisimulation" relation

forall x1, ..., xn,

H1 -> ... -> Hm ->

P t1 ... tl

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

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

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

Proof.

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.

Qed.

### Automating the whole thing

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)

end.

Ltac step1_arity1 :=

match goal with

| [|- ?P ?s] =>

if_is_not_var s then remember s

end.

Ltac step2conj1 :=

match goal with

| [|- _] => generalize I

end.

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

end

end.

Ltac step2exn_arity2 :=

match goal with

| [s1 : _, s2 : _, x : ?T |- ?Q -> ?P ?s1 ?s2] =>

generalize dependent x; apply exists_forall_impl

end.

Ltac step2exn_arity1 :=

match goal with

| [s : _, x : ?T |- ?Q -> ?P ?s] =>

generalize dependent x; apply exists_forall_impl

end.

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

end.

Ltac step3_arity1 X :=

match goal with

| [|- ?Q -> ?P ?s] => generalize dependent s; apply X

end.

Ltac destrs :=

match goal with

| [H : exists x, _ |- _] => destruct H

| [H : _ /\ _ |- _] => destruct H

| [H : True |- _] => destruct H

end.

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

end.

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

fun s1 s2 =>

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

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

Proof.

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.

Qed.

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

Proof.

(* write proof here *)

Abort.

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

Proof.

(* write proof here *)

Abort.

#### 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.Fixpoint add A (l : list A) (s : stream A) : stream A :=

match l with

| nil => s

| h :: t => Cons h (add t s)

end.

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)

end.

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

end.

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

Proof.

(* write proof here *)

Abort.

Lemma cycles_collatz_100 : cycles (collatz 100).

Proof.

(* write proof here *)

Abort.