The Coq mailing list

[Edsko de Vries <edskodevries AT gmail.com>]

Hi Keiko,

How do you do your proofs? In particular, if you need to prove some property over wbisim, how do you recursive over the red relation? You'll need to combine recursion and corecursion in some way, no? What approach do you take? I've been looking at the paper cited by Ekaterina, but I'm not sure it applies in my case; in particular, the translation from a stream to a function on nats only works if the streams are all infinite; for "colists" it may not work? I'm now reading  "A Unifying Approach to Recursive and Co-recursive Definitions" by Gianantonio and Miculan but it's complicated..

Edsko