[Agda] Re: [Coq-Club] Need help with coinductive proof

[Edsko de Vries]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090827/837731fd/attachment.html