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.