(* G54DTP Dependently Typed Programming.
    Introduction to coinductive types.
    Venanzio Capretta, March 2011.
*)

Require Import ZArith.
Open Scope Z_scope.
Set Implicit Arguments.

(* CoInductive types are similar to the inductive ones,
   but constructors can be repeated infinitely many times.
*)

CoInductive lList (A:Set): Set :=
  lnil: lList A
| lcons: A -> lList A -> lList A.

Print lList.

Definition l0: lList Z := lcons (-1) (lcons 3 (lcons 0 (lnil Z))).
Print l0.

CoFixpoint l1: lList Z := lcons 2 (lcons (-3) l1).  (* infinite list *)
Print l1.

(* Coq doesn't print the all infinite list, even if we tell it to compute it. *)

Eval compute in l1.

(* We must define an explicit unfold operation. *)

Definition lunfold (A:Set)(l:lList A): lList A :=
match l with
  lnil => lnil A
| lcons a l' => lcons a l'
end.

(* It looks like lunfold doesn't do anything, but it forces Coq to compute it. *)

Eval compute in (lunfold l1).

(* The next function unfolds a lazy list several times:
   the natural number n says how many.
*)

Fixpoint lunf (A:Set)(l:lList A)(n:nat): lList A :=
match n with
  O => l
| S n' => match l with
            lnil => lnil A
          | lcons a l' => lcons a (lunf l' n')
          end
end.

Eval compute in (lunf l1 10).

(* We can prove that the unfolding is equal to the original list. *)

Lemma lunf_eq: forall (A:Set)(n:nat)(l:lList A), l = lunf l n.
Proof.
induction n.
trivial.
intro l; case l.
trivial.
intros a l'.
simpl.
rewrite <- IHn.
trivial.
Qed.


(* Every finite list can be transformed into a lazy list. *)

Require Import List.

Fixpoint list_lazy (A:Set)(l:list A): lList A :=
match l with
  nil => lnil A
| cons a l' => lcons a (list_lazy l')
end.

Eval compute in (list_lazy (1::-3::0::-2::7::nil)).

(* The other way around doesn't work; try this:

Fixpoint lazy_list (A:Set)(l:lList A): list A :=
match l with
  lnil => nil
| lcons a l' => cons a (lazy_list l')
end.
*)

(* Instead we must characterize the finite lazy lists
   by an inductive predicate.
*)

Inductive lFinite (A:Set): lList A -> Set :=
  fin_lnil: lFinite (lnil A)
| fin_lcons: forall a l, lFinite l -> lFinite (lcons a l).

Fixpoint lazy_list (A:Set)(l:lList A)(h:lFinite l): list A :=
match h with
  fin_lnil => nil
| fin_lcons a l' h' => a :: lazy_list h'
end.

(* Constant infinite lists. *)

CoFixpoint lconst (A:Set)(a:A): lList A :=
  lcons a (lconst a).

Eval simpl in (lunf (lconst 13) 10).

(* Definition of the list of numbers starting from a given one. *)

CoFixpoint lfrom (x:Z): lList Z :=
  lcons x (lfrom (x+1)).

Definition lnum := lfrom 0.

Eval simpl in (lunf lnum 10).