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

[Edsko de Vries]

I don't understand; why doesn't there have to be a maximum delay? Isn't that
the point of using an inductive definition -- so that tau-left and tau-right
can be applied finitely many times? (Note that rules bisim_cozero,
bisim_cosucc and bisim_tau allow to "reset" the maximum delay.)

Note that my data type above, however, is probably not good enough because a
proof of (exists i, bisim i m n) cannot use coinduction, as (exists, ..) is
not a coinductive type. I'm now trying to use

CoInductive bisim : coN -> coN -> Prop :=
  | bisim_delay : forall d m n,
      bisim' d m n ->
      bisim m n
with bisim' : nat -> coN -> coN -> Prop :=
  | weak_tau_left : forall d m n,
      bisim' d m n ->
      bisim' (S d) (tau m) n
  | weak_tau_right : forall d m n,
      bisim' d m n ->
      bisim' (S d) m (tau n)
  | strong_coZ : forall d,
      bisim' d coZ coZ
  | strong_tau : forall d m n,
      bisim m n ->
      bisim' d (tau m) (tau n)
  | strong_coS : forall d m n,
      bisim m n ->
      bisim' d (coS m) (coS n).

which hides the existential inside the coinductive datatype so that we can
use coinduction (in a sense, this is a mixed inductive/coinductive
definition, even though bisim' is coinductive: we can do induction over the
maximum delay d.)

As regards your other question -- by using a nested coinductive/inductive
definition Coq, do you mean something like

Inductive weak (R : coN -> coN -> Prop) : coN -> coN -> Prop :=
  | weak_base : forall m n,
      R m n ->
      weak R m n
  | weak_tau_left : forall m n,
      weak R m n ->
      weak R (tau m) n
  | weak_tau_right : forall m n,
      weak R m n ->
      weak R m (tau n).

CoInductive weak_coN : coN -> coN -> Prop :=
  | strong_coZ :
      weak_coN coZ coZ
  | strong_coS : forall m n,
      weak_coN m n ->
      weak_coN (coS m) (coS n)
  | strong_tau : forall m n,
      weak_coN m n ->
      weak_coN (tau m) (tau n)
  | weak_tau : forall m n,
      weak weak_coN m n ->
      weak_coN m n.

This is a valid definition, but proofs are now painful; a proof L over
weak_coN by coinduction cannot recurse over the proof of (weak weak_coN m n)
passing L itself as an argument, because the occurrence of L is now not
guarded as it occurs as an argument to the induction hypothesis (the
recursor) for [weak] (this was the essence of my separate email asking about
mixing induction and coinduction in Coq). There are some papers on how to do
this ("Using Structural Recursion for Corecursion" is one, but limited in
scope and I'm not sure it applies here; "A Unifying Approach to Recursive
and Co-recursive Definitions" is much more general, using complete ordered
families of equivalances, but is difficult and I haven't yet been brave
enough to try it.

OTOH, it seems we get this for free in Agda -- so a simpler solution should
be possible?

-E
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090827/e714f636/attachment.html