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