Stream of all finite prefixes of a stream

Question

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?

Answer 1

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.

Answer 2

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.