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

[Edsko de Vries]

I'm very sorry to keep replying to myself. I was reading through the proof
that Keiko sent when I realized that I could complete my symmetry proof
without doing induction on d, but using some sort of double coinduction?

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.
Proof.
(* first *)
  intros.
  inversion H ; clear H ; subst.
  apply (@bisim_delay d).
  apply bisim'_sym.
  assumption.
(* second *)
  intros.
  inversion H ; clear H ; subst.
(* weak_tau_left *)
  apply weak_tau_right.
  apply bisim'_sym.
  assumption.
(* weak_tau_right *)
  apply weak_tau_left.
  apply bisim'_sym.
  assumption.
(* strong_coZ *)
  apply strong_coZ.
(* strong_tau *)
  apply strong_tau.
  apply bisim_sym.
  assumption.
(* strong_coS *)
  apply strong_coS.
  apply bisim_sym.
  assumption.
Qed.

Not sure this is going to solve the rest of my difficulties, but we'll see
;)

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