The Coq mailing list

[Edsko de Vries <Edsko.de.Vries AT cs.tcd.ie>]

(*
Hi,

I have a question about guardedness checking in cofixpoint definitions.
I have simplified my problem as much as I could; hopefully, I have not
simplified it too much (you can copy and paste this email into Coq).

Given the definition of a stream, we can easily write a map function:
*)

  Set Implicit Arguments.
  
  CoInductive stream (A : Set) : Set :=
    | nil : stream A
    | cons : A -> stream A -> stream A.
  
  CoFixpoint map (A B : Set) (f : A -> B) (xs : stream A) : stream B :=
    match xs with
    | nil => nil B
    | cons x xs' => cons (f x) (map f xs')
    end.

(*
But now suppose that we want to write this map function in a different
way (the "why" is complicated, and I'd have to give a *lot* more
background): we will construct a type stream', which is basically the
top-level decomposition of a stream: 
*)

  Definition stream' (A : Set) : Set := (unit + A * stream A)%type.
  
  Definition fromStream (A : Set) (xs : stream A) : stream' A :=
    match xs with
    | nil => inl _ tt
    | cons x xs' => inr _ (x, xs')
    end.
  
  Definition toStream (A : Set) (xs : stream' A) : stream A :=
    match xs with
    | inl _ => nil A
    | inr (x, xs') => cons x xs'
    end.

(*
We now define a non-recursive function across stream', which leaves the
recursion to a different function, which it is passed as an argument:
*)

  Definition map' (A B : Set) (f : A -> B) 
      (rec : (A -> B) -> stream A -> stream B)
      (xs : stream' A) : stream' B :=
    match xs with
    | inl u => inl _ u
    | inr (x, xs') => inr _ (f x, rec f xs')
    end.

(*
Finally, we want to define the recursive map (say, map2) in terms of
map'; obviously, the function 'rec' that map' needs is map2 itself:
*)

  CoFixpoint map2 (A B : Set) (f : A -> B) (xs : stream A) : stream B :=
    toStream (map' f (@map2 A B) (fromStream xs)).

(*
Unfortunately, this definition is not accepted by Coq:

  Error:
  Recursive definition of map2 is ill-formed.
  In environment
  map2 : forall A B : Set, (A -> B) -> stream A -> stream B
  A : Set
  B : Set
  f : A -> B
  xs : stream A
  Recursive call in the argument of cases in
  "match
     match
       match xs with
       | nil => inl (A * stream A) tt
       | cons x xs' => inr unit (x, xs')
       end
     with
     | inl u => inl (B * stream B) u
     | inr (pair x xs') => inr unit (f x, map2 A B f xs')
     end
   with
   | inl _ => nil B
   | inr (pair x xs') => cons x xs'
   end".

This is very unfortunate: I presume that Coq rejects this definition
because the recursive call to 'map2' is not guarded by 'cons'. However,
when you look at this definition a little longer, it becomes obvious
that the recursive call *is* in fact guarded: the recursive call only
occurs as part of

  inr unit (f x, map2 A B f xs')

which will only match with the second part of the outermost match, and
therefore simplify to

  cons (f x) (map2 A B f xs')

which is exactly the recursive call that we made in the simple
definition of map, above. 

Is there a way that we can convince Coq that this definition is in fact
ok? (Without modifying map')? 

That would *really* be a big help :) No, *really* :)

Thanks,

Edsko
*)