The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

I tend to find it helpful to think of Stream T as essentially covered by
Definition state_iterator {S T:Type} (f : S -> T * S) : S -> Stream T :=
cofix F (s:S) :=
let (x, s') := f s in Cons x (F s').

So basically, in order for a CoFixpoint definition to be accepted, it
has to be easy to translate it into an iterated stream of this type,
using a fairly simple state variable.  (Of course, the translation
becomes a bit more complex when it comes to things like stream_map2 :
forall T1 T2 T3:Type, (T1 -> T2 -> T3) -> Stream T1 -> Stream T2 ->
Stream T3, as you'd have to "take apart" the Stream T1 and Stream T2
inputs to get their state types, and then take the product.  So this
heuristic needs to be taken with a grain of salt.)
-- 
Daniel Schepler

On Wed, Aug 20, 2014 at 8:31 AM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:
> Hi,
> Why does Coq not notice that the following definition is manifestly
> productive?
>
> Require Import Coq.Lists.Streams.
>
> Fixpoint stream_prepend_list {T} (ls : list T) (rest : Stream T) : Stream T
> :=
>   match ls with
>     | nil => rest
>     | cons x xs => Cons x (stream_prepend_list xs rest)
>   end.
>
> CoFixpoint flatten_stream {T} (s : Stream (T * list T)) : Stream T :=
>   match s with
>     | Cons x xs => Cons (fst x) (stream_prepend_list (snd x) (flatten_stream
> xs))
>   end.
> (* Error:
> Recursive definition of flatten_stream is ill-formed.
> In environment
> flatten_stream : forall T : Type, Stream (T * list T) -> Stream T
> T : Type
> s : Stream (T * list T)
> x : T * list T
> xs : Stream (T * list T)
> Sub-expression "stream_prepend_list (snd x) (flatten_stream T xs)" not in
> guarded form (should be a constructor, an abstraction, a match, a cofix or a
> recursive call).
> Recursive definition is:
> "fun (T : Type) (s : Stream (T * list T)) =>
>  match s with
>  | Cons x xs =>
>      Cons (fst x) (stream_prepend_list (snd x) (flatten_stream T xs))
>  end". *)
>
>
> It seems that Coq doesn't want me to put anything between the recursive call
> and the constructor, but it's syntactically obvious that my definition is
> productive...
>
> -Jason