The Coq mailing list

[roconnor AT theorem.ca]

Maybe not what you want, but I can define map2 after a CPS transform:

Definition stream' (A : Set) : Type :=
 forall C:Type,C -> (A -> stream A -> C) -> C.

Definition fromStream (A : Set) (xs : stream A) : stream' A :=
fun C c f =>
 match xs with
 | nil => c
 | cons x xs' => f x xs'
 end.

Definition toStream (A : Set) (xs : stream' A) : stream A :=
xs _ (nil A) (@cons _).

Definition map' (A B : Set) (f : A -> B)
(rec : (A -> B) -> stream A -> stream B)
(xs : stream' A) : stream' B :=
fun C c g => (xs C c (fun x xs' => g (f x) (rec f xs'))).

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


On Sun, 26 Apr 2009, Edsko de Vries wrote:

> (*
> 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
> *)
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''