# Stream of all finite prefixes of a stream

If I want to construct of list of all (obviously finite) prefixes of a list, I can define this function:

Fixpoint list_prefixes {A : Type} (l : list A) : list (list A) :=
match l with
| [] => [[]]
| a :: l' => [] :: map (cons a) (list_prefixes l')
end.


I tried to do the same for streams, and the most natural way for me is:

CoFixpoint stream_prefixes {A : Type} (s : Stream A) : Stream (list A) :=
match s with
| Streams.Cons a s' => Streams.Cons [] (Streams.map (cons a) (stream_prefixes s'))
end.


Which naturally fails, since I'm applying stream s' to a function which is not a constructor (Streams.map).

How can I construct a stream of all finite prefixes?

If you do not care about algorithmic efficiency, the simplest way to do this is to thread an accumulator in your cofixpoint:

Require Import List Streams.

CoFixpoint stream_prefixes_rec {A : Type} (s : Stream A) (accu : list A) : Stream (list A) :=
match s with
| Cons a s' => Cons (List.rev accu) (stream_prefixes_rec s' (cons a accu))
end.

Definition stream_prefixes {A} s := @stream_prefixes_rec A s nil.


You have to reverse the accumulator at every step, which leads to a quadratic blowup, but if you only care about proofs then this should not matter.

• So what would a more efficient solution do? I can think of the solution that spews a stream take 0 s, take 1 s, take 2 s, ... where take n s takes the first n elements of a stream s. But is that really more efficient? We're still taking n steps to construct the n-th list. Feb 11 at 16:27
• I think this solution is the best you can do, algorithmically. The resulting data will be quadratic in size, anyway, and you can't possibly get any sharing since prefixes of cons-lists don't share spines. (other approaches like using a difference list amount to doing the same thing) Feb 12 at 11:27

A more involved solution that I found:

CoFixpoint all_nats_helper (n : nat) : Stream nat := Streams.Cons n (all_nats_helper (S n)).

Definition all_nats : Stream nat := all_nats_helper 0.

Fixpoint Str_take {A : Type} (n : nat) (s : Stream A) : list A :=
match n with
| 0 => []
| S n' => let (a, s') := s in a :: Str_take n' s'
end.

Definition stream_prefixes {A : Type} (s : Stream A) := Streams.map (fun n => Str_take n s) all_nats.