The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

As a follow-up to this, here's an example of how you could write an
equivalent definition that's accepted (where if s is generated using
state type S, prepend_list_and_flatten_stream ls s is generated using
state type list T * S):

Require Import Streams.

CoFixpoint prepend_list_and_flatten_stream {T}
  (ls : list T) (s : Stream (T * list T)) : Stream T :=
match ls with
| nil => match s with
         | Cons (x, xs) s' => Cons x (prepend_list_and_flatten_stream xs s')
         end
| cons x xs => Cons x (prepend_list_and_flatten_stream xs s)
end.

Definition flatten_stream {T} (s : Stream (T * list T)) : Stream T :=
match s with
| Cons (x, xs) s' => Cons x (prepend_list_and_flatten_stream xs s')
end.

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.

Lemma stream_decomp : forall {T} (s : Stream T),
  s = Cons (hd s) (tl s).
Proof.
destruct s; reflexivity.
Qed.

Lemma prepend_list_and_flatten_stream_eqn :
  forall {T} (ls : list T) (s : Stream (T * list T)),
  prepend_list_and_flatten_stream ls s =
  stream_prepend_list ls (flatten_stream s).
Proof.
induction ls; simpl.
+ destruct s as [[x xs] s']; simpl.
  match goal with |- ?LHS = _ => rewrite (stream_decomp LHS) end.
  simpl. reflexivity.
+ intros.
  match goal with |- ?LHS = _ => rewrite (stream_decomp LHS) end.
  simpl. f_equal; auto.
Qed.

Lemma flatten_stream_step : forall T (x : T) (xs : list T)
  (s' : Stream (T * list T)),
  flatten_stream (Cons (x, xs) s') =
  Cons x (stream_prepend_list xs (flatten_stream s')).
Proof.
intros; simpl.
f_equal.
apply prepend_list_and_flatten_stream_eqn.
Qed.
-- 
Daniel Schepler

On Wed, Aug 20, 2014 at 10:00 AM, Daniel Schepler 
<dschepler AT gmail.com>
 wrote:
> 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