Set Implicit Arguments.
Unset Strict Implicit.
Set Printing Implicit Defensive.
Require Import List.

Section colistDef.

Variable t : Type.

(* A small custom stream datatype for infinite *and* finite streams *) 
CoInductive colist := 
  | cnil : colist
  | ccons: t -> colist -> colist.

Definition decomp_colist lst := 
  match lst with 
  | cnil => cnil | ccons x lst => ccons x lst
  end.

Theorem decomp_colist_thm : forall (l : colist), l = decomp_colist l.
Proof. intros. case l; auto. Qed.

Inductive FinCoList : colist -> list t -> Prop := 
  | FinCoListNil  : FinCoList cnil nil
  | FinCoListCons : forall (x : t) (clst : colist) (lst : list t), 
                    FinCoList clst lst -> FinCoList (ccons x clst) (x :: lst).

Inductive FinPrefix : colist -> colist -> Prop :=
  | FinPrefixNil : forall xs, FinPrefix cnil xs
  | FinPrefixCons : forall x xs ys, FinPrefix xs ys -> FinPrefix (ccons x xs) (ccons x ys).

CoInductive Prefix : colist -> colist -> Prop :=
  | PrefixNil : forall xs, Prefix cnil xs
  | PrefixCons : forall x xs ys, Prefix xs ys -> Prefix (ccons x xs) (ccons x ys).

Fixpoint ctake n (x:colist) :=
  match n with 0 => nil | S n => 
  match x with ccons h tl => h :: ctake n tl | cnil => nil end end. 

End colistDef.