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