The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

The problem with the nested recursive calls is that it makes the
productivity check non-local: if "cfp" goes in the argument "st" of
this function, you have to make sure that uses of argument "st" are
also protected by constructors in the whole function definition. While
this intuitively seems to be the case here, we can build a
counter-example that exhibits the problem:

CoFixpoint wrong b (st : Stream unit) :=
  match b with
    | true => tl (tl st)
    | false => Cons tt (wrong true (wrong false st))
  end.

If this was accepted, you would have the following bad reduction sequence

    tl (wrong false st)
-> tl (Cons tt (wrong true (wrong false st)))
-> wrong true (wrong false st)
-> tl (tl (wrong false st))

On Sun, Jan 5, 2014 at 1:01 PM, Jacques-Henri Jourdan
<jacques-henri.jourdan AT inria.fr>
 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?
>
> Thank you all,
> --
> JH Jourdan