The Coq mailing list

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

On Tue, Sep 1, 2009 at 5:05 PM, Nils Anders Danielsson <nad AT cs.nott.ac.uk> wrote:

On 2009-09-01 15:45, Edsko de Vries wrote:

On Tue, Sep 1, 2009 at 2:59 PM, Thorsten Altenkirch <txa AT cs.nott.ac.uk>wrote:

It is sound but useless.

Then I clearly don't understand the rules for mixed inductive/coinductive
definitions. Is

  inductive_constructor (..) (coinductive_constructor (coinductive
recursive call))

a valid call or not?

It is (currently, in Agda). I think you and Thorsten interpret the word
"sound" differently here.

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.

I find this counter-intuitive because I would have thought that adding an inductive transitivity rule to a provably transitive relation would not change anything. Again, it strongly reminds me of the problem of weak bisimulation up to weak bisimilarity (see "Techniques of weak bisimulation up-to", R.Milner and D. Sangiorgi).

Edsko