The Coq mailing list

[Nils Anders Danielsson <nad AT Cs.Nott.AC.UK>]

On 2009-08-24 16:28, Edsko de Vries wrote:
> Now, waving my hands, in the proof that this implies bisimularity, we 
> proceed by coinduction, inversion on [bisim_CF], and then for the case 
> of [bisim_CF_prod] we simply reason
>
>   h (m + n) ~ h m + h n ~ m' + n'
>
> which uses an auxiliary lemma "add_bisim" that m + n ~ m' + n' if m ~ m' 
> and n ~ n'; we need to reason that h m ~ m' and h n ~ n' "by 
> coinduction". Unfortunately, this is not guarded, because the recursive 
> calls will be used as arguments to "add_bisim" and to transitivity.

This is a common problem with guarded corecursion. There are several
possible workarounds. Currently I like to use a technique which I posted
about on this mailing list last year; you can read about it in the
following paper draft (written with Thorsten Altenkirch):

 Mixing Induction and Coinduction
 http://www.cs.nott.ac.uk/~nad/publications/danielsson-altenkirch-mixing.html

I have not checked whether the technique would work in this particular
case, though.

--
/NAD

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.