The Coq mailing list

[Jeff Terrell <jeff AT kc.com>]

Dear Andreas & Cedric,

Many thanks for your comments. Unfortunately, this problem is a show 
stopper for my project. Does anyone know if there's a prototypical 
implementation of Coq that would allow f to pass the guardedness checker?

Regards,
Jeff.

Andreas Abel wrote:
> Hi Jeff,
>
> your counterexample can be simplified to
>
> Require Import List.
>
> CoInductive A : Set :=
> | Build_A : list A -> A.
>
> CoInductive X : Set :=
> | Build_X : list X -> X.
>
> CoFixpoint f (a : A) : X :=
>   match a with
>   | Build_A l => Build_X (map f l)
>   end.
>
> The Coq guardedness checker does not see that the call to "f" in "map 
> f l" is guarded by constructor Build_X, because it does not take the 
> behavior of map into account.  A theoretical solution to this problem 
> has been found and it is called "size types" or "type based 
> termination".  So far, only prototypical implementations exist, for 
> instance MiniAgda (see http://www2.tcs.ifi.lmu.de/~abel/miniagda ).  
> In MiniAgda this code passes guardedness checking:
>
> data List (+ A : Set) : Set
> { -- ...
> }
>
> fun map : (A : Set) -> (B : Set) -> (f : A -> B) -> List A -> List B
> { -- ...
> }
>
> sized codata A : Size -> Set
> { Build_A : (i : Size) -> List (A i) -> A ($ i)
> }
>
> sized codata X : Size -> Set
> { Build_X : (i : Size) -> List (X i) -> X ($ i)
> }
>
> cofun f : (i : Size) -> A i -> X i
> { f .($ i) (Build_A i l) = Build_X _ (map (A _) (X _) (f i) l)
> }
>
> Using sized types, one can see that the r.h.s.
>
>   Build_X _ (map (A _) (X _) (f i) l)
>
> has one guard more ($ i) than the recursive call f i  (which has i 
> guards).
>
> Cheers,
> Andreas
>
> Jeff Terrell 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.