The Coq mailing list

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

On 2009-09-01 17:16, Edsko de Vries wrote:
> Right. So, we have a relation R (weak bisimularity), which is provably
> transitive. Then, we can give a definition of a similar relation R'
> which is like R except that it has an extra, inductive, transitivity
> rule. This is "useful" in the sense that a proof which was previously
>
>   transitivity_lemma (...) (coinductive_constructor (...)
> coinductive_recursive_call))
>
> and was rejected because the coinductive_recursive_call was not
> guarded can now be replaced by
>
>   transitivity_constructor (...) (coinductive_constructor (...)
> coinductive_recursive_call))
>
> which *is* guarded. It is not "sound" in the sense that R' is larger than R.

Yes, and the reason why it is not sound is that transitivity_lemma is
not (in some sense) contractive: the lemma consumes coinductive
constructors "faster" than it produces them.

--
/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.