The Coq mailing list

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

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