The Coq mailing list

[Ekaterina Komendantskaya <komendantskaya AT gmail.com>]

Hi,

Yves Bertot and myself had a paper about it in the proceedings of
TYPES'08, and we also gave references to other approaches (there are
quite a few).
The paper is available here:
http://hal.inria.fr/inria-00322331/en/
The paper dealt in particular with non-guarded corecursive definitions
containing "map", like in your example.

A related discussion in this mailing list was under the topic
[Coq-Club] Codata: problem with guardedness condition?
And in particular, there was given a nice link to a similar discussion
at Nottingham FP lunch:
http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=109
Perhaps some of this has already been published...

Best,
Ekaterina

2009/8/26 Edsko de Vries 
<edskodevries AT gmail.com>:
> Hi,
>
> This is related to my previous question, but a lot simpler (hopefully I
> didn't simplify the problem too much). I don't understand how to
> mix induction and coinduction in Coq. Here is a *very* simple example:
>
> Require Import List.
>
> CoInductive T : Set :=
>   | A : T -> T
>   | B : list T -> T.
>
> CoFixpoint f (t : T) : T :=
>   match t with
>   | A t1' => A (f t1')
>   | B t1s => B (map f t1s)
>   end.
>
> This definition of [f] seems ok to me, but is rejected as not guarded
> because the recursive argument appears as argument to a function (in this
> case, map). How should one define functions and data types like this? (I
> don't care if I have to redefine list; I'm only using list as an example --
> the loss of the use of library functions is not an issue.)
>
> Thanks,
>
> Edsko
>
> PS. I seem to recall that a question like this came up before, but I can't
> find it.
>



-- 
Ekaterina Komendantskaya
School of Computer Science
University of St Andrews
St Andrews,
KY16 9SX, UK
Tel. 01334 463238