coinduction.v

Set Implicit Arguments.

Require Import List.

Import ListNotations.

(** definition of streams *)

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

(** example of cofixpoint *)

CoFixpoint zeroes : stream nat := Cons 0 zeroes.

(** taking a finite prefix of a stream *)

Fixpoint approx {A : Type}(s : stream A)(n : nat) : list A :=
  match n with
  | O => []
  | S n' =>
    match s with
    | Cons x xs => x :: approx xs n'
    end
  end.

Lemma approx_zero : forall n xs, xs = approx zeroes n ->
                            forallb (fun x => Nat.eqb x 0) xs = true.
Proof.
  induction n ; intros xs Hxs ; simpl in * ; subst ; simpl ; auto.
Qed.

CoFixpoint truefalse : stream bool := Cons true falsetrue
with falsetrue : stream bool := Cons false truefalse.

(** Evaluating a cofixpoint *)

Eval simpl in approx truefalse 5.

(** coinductive proofs *)

CoFixpoint comap {A B : Type}(f : A -> B)(s : stream A) : stream B :=
  match s with
  | Cons x s' => Cons (f x ) (comap f s')
  end.

CoFixpoint ones : stream nat := Cons 1 ones.

Definition ones' := comap S zeroes.

(** coinductive equality *)

CoInductive stream_eq {A : Type} : stream A -> stream A -> Prop :=
| Stream_eq : forall x xs xs',
    stream_eq xs xs' ->
    stream_eq (Cons x xs) (Cons x xs').

(** auxiliar definitions *)

Definition frob {A : Type} (s : stream A) : stream A :=
  match s with
  | Cons x xs => Cons x xs
  end.

Lemma frob_eq {A : Type} : forall (s : stream A), s = frob s.
Proof.
  destruct s ; reflexivity.
Qed.

Theorem ones_eq : stream_eq ones ones'.
Proof.
  cofix CHones_eq.
  rewrite (frob_eq ones) ; rewrite (frob_eq ones').
  simpl.
  constructor.
  assumption.
Qed.


(** "Lazy" lists *)

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

Arguments LNil [A].


Infix "<:>" := LCons (at level 60, right associativity).
Notation "[*]" := LNil.


Definition test : LList nat :=  0 <:> 1 <:> [*].

CoFixpoint lrepeat {A : Type}(x : A) : LList A :=
  x <:> lrepeat x.

CoFixpoint lapp {A : Type}(xs ys : LList A) : LList A :=
  match xs with
  | [*] => ys
  | x <:> xs => x <:> (lapp xs ys)
  end.

Definition LList_decompose {A : Type}(xs : LList A) : LList A :=
  match xs with
  | [*] => [*]
  | x <:> xs => x <:> xs 
  end.

Lemma LList_decompose_lemma {A : Type}
  : forall (xs : LList A), xs = LList_decompose xs.
Proof.
  intros xs ; case xs ; trivial.
Qed.

Theorem lapp_nil 
  : forall {A : Type}(xs : LList A), lapp [*] xs = xs.
Proof.
  intros A xs ;
    rewrite (LList_decompose_lemma (lapp [*] xs)) ;
    case xs ; simpl ; auto.
Qed.

Theorem lapp_cons
  : forall {A : Type}(x : A)(xs ys : LList A),
    lapp (x <:> xs) ys = x <:> (lapp xs ys).
Proof.
  intros A x xs ys ; rewrite (LList_decompose_lemma (lapp (x <:> xs) ys)) ;
    case ys ; simpl ; auto.
Qed. 

(** predicates over coinductive types *)

Inductive finite {A : Type} : LList A -> Prop :=
| NilFinite : finite [*]
| ConsFinite : forall x xs, finite xs -> finite (x <:> xs).

Hint Resolve NilFinite ConsFinite.

Theorem finite_app {A : Type}
  : forall (xs ys : LList A), finite xs -> finite ys -> finite (lapp xs ys).
Proof.
  induction 1 ; intros.
  +
    rewrite lapp_nil ; auto.
  +
    rewrite lapp_cons ; auto.
Qed.


CoFixpoint from (n : nat) : LList nat :=
  n <:> from (S n).

Lemma from_unfold : forall n:nat, from n = n <:> (from (S n)).
Proof.
 intro n.
 rewrite (LList_decompose_lemma (from n)).
 simpl ; trivial.
Qed.


CoInductive infinite {A : Type} : LList A -> Prop :=
| ConsInfinite
  : forall x xs, infinite xs -> infinite (x <:> xs).

Theorem from_infinite : forall n, infinite (from n).
Proof.
  cofix CH.
  intro n ; rewrite (from_unfold n) ; split ; auto.
Qed.