The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

Le Wed, 20 Jan 2010 14:12:30 +0100, Jeff Terrell 
<jeff AT kc.com>
 a écrit:

> Hi,
>
> Is Coq being too conservative in rejecting the definition of f?
>
> Require Import List.
>
> CoInductive A : Set :=
>    Build_A : list B -> A
> with B : Set :=
>    Build_B : A -> B.
>
> Definition RB := fun a : A => let (RB) := a in RB.
> Definition RA := fun b : B => let (RA) := b in RA.
>
> CoInductive X : Set :=
>    Build_X : list Y -> X
> with Y : Set :=
>    Build_Y : X -> Y.
>
> CoFixpoint f(a : A) : X :=
>    Build_X (map g (RB a))
> with g (b : B) : Y :=
>     Build_Y (f (RA b)).
>
> Thanks.
>
> Regards,
> Jeff.

I think Coq should accept this definition as both f and g are clearly  
productive;
it is not the case and so it should be reported to the bug-tracking system.

I am not an expert in coinduction, maybe someone can explain us why coq  
doesn't accept it.

For an even less explicit message error replace f definition with:
CoFixpoint f(a : A) : X :=
   let (RB) := a in Build_X (match map g RB with nil => nil | p::q => p::q  
end)
with g (b : B) : Y :=
   let (RA) := b in Build_Y (f RA).
or
CoFixpoint f(a : A) : X :=
   match a with
   | Build_A nil => Build_X nil
   | Build_A ((Build_B p)::q) =>
             match f (Build_A q) with
             | Build_X l => Build_X ((Build_Y (f p))::l)
             end
   end.

I am not sure the last 2 defs should be accepted; but I don't see reasons  
why Jeff's one is not.
Problem is even simplier with:

Require Import List.

CoInductive A : Set :=
  Build_A : list A -> A.

Definition RA := fun b : A => let (RA) := b in RA.

CoInductive X : Set :=
  Build_X : list X -> X.

CoFixpoint f (a: A): X :=
  Build_X (map f (RA a)).

--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay