The Coq mailing list

[Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>]

Hello, 

If I may intervene again with Tarmo Uustalu we are experimenting with a weak
trace-equivalence in Coq, which might be of some help to bridge 
Nils and Thorsten's solution in Agda and the problem in question in Coq. 

CoInductive trace: Set := 
| Zero | AddOne (_: trace) | AddZero (_: trace).

(* strong bisimilarity of two traces *)
CoInductive bisim: trace -> trace -> Prop :=
| bisim_zero: bisim Zero Zero 
| bisim_one: forall tr tr',
  bisim tr tr' ->
  bisim (AddOne tr) (AddOne tr')
| bisim_tau: forall tr tr',
  bisim tr tr' ->
  bisim (AddZero tr) (AddZero tr').


(* finite reductions to visible actions *)
Inductive red: trace -> trace -> Prop :=
| red_zero: red Zero Zero 
| red_one: forall tr tr',
  bisim tr tr' -> red (AddOne tr) (AddOne tr')
| red_tau: forall tr tr',
  red tr tr' -> red (AddZero tr) tr'.

(* a weak bisimulation *)
CoInductive wbisim: trace -> trace -> Prop :=
| wbisim_zero_1: forall tr, 
  red tr Zero -> 
  wbisim Zero tr
| wbisim_zero_2: forall tr, 
  red tr Zero -> 
  wbisim tr Zero
| wbisim_one_1: forall tr0 tr1 tr2,
  wbisim tr0 tr2 ->
  red tr1 (AddOne tr2) ->
  wbisim (AddOne tr0) tr1 
| wbisim_one_2: forall tr0 tr1 tr2,
  wbisim tr2 tr1 ->
  red tr0 (AddOne tr2) ->
  wbisim tr0 (AddOne tr1) 
| wbisim_tau: forall tr0 tr1,
  wbisim tr0 tr1 ->
  wbisim (AddZero tr0) (AddZero tr1).

At least I can prove in Coq wbisim is transitive.  If I understand, our
definition appears equivalent to Nils and Thorsten's.  But my proofs of
the transitivity as well as the definition of the weak bisimulation
are much more verbose than Nils and Thorsten's.  Indeed Nils' concise
proof in Agda is striking for me.

I agree that having induction/coinduction mixed will simplify my life :)

Best, 
Keiko