The Coq mailing list

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

Actually, never mind that mutually recursive bisim datatype. It still has the same problem as the definition with a coinductive/inductive data type. Consider trying to prove that bisimulation is symmetric. This now becomes a mutually-recursive proof:

Lemma bisim_sym : forall m n,
  bisim m n -> bisim n m
with bisim'_sym : forall d m n,
  bisim' d m n -> bisim' d n m.

in the second part of this proof (bisim') we want to use induction on d; but in the case for strong-tau, we have that bisim n m; we now want to apply strong_tau, then corecursive using bisim_sym to get bisim m n, but again the definition is no longer guarded: we have used bisim_sym as an argument to the induction principle for nat, and the definition is rejected.

This is very frustrating :( Is it really necessary to use something like complete ordered families of equivalences? Why does this seem to much easier in Agda?

Edsko