0
$\begingroup$

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?

$\endgroup$

2 Answers 2

2
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$ Feb 11, 2023 at 16:27
  • $\begingroup$ 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) $\endgroup$
    – oisdk
    Feb 12, 2023 at 11:27
0
$\begingroup$

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.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.