The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Sunday, January 05, 2014 01:01:48 PM Jacques-Henri Jourdan wrote:
> Hi Coq-Club !
> 
> I face a case where the cofixpoint guard condition seems too strong to me.
> Here is a simplified version:
> 
> Require Import Streams.
> 
> CoInductive Tr :=
> 
> | L : nat -> Tr
> | N : nat -> Tr -> Tr -> Tr.
> 
> CoFixpoint cfp (tr:Tr) (st:Stream nat) :=
> match tr with
> 
> | L n => Cons n st
> | N n l r =>
> 
> Cons n (cfp l (cfp r st))
> end.
> 
> How can I make this definition accepted by Coq?

How about:

CoFixpoint cfps (trs:list Tr) (st:Stream nat) :=
  match trs with
  | nil => st
  | cons (L n) trs' => Cons n (cfps trs' st)
  | cons (N n l r) trs' => Cons n (cfps (cons l (cons r trs')) st)
  end.

Definition cfp (tr:Tr) (st:Stream nat) :=
  cfps (cons tr nil) st.
-- 
Daniel Schepler