http://www.amazon.co.jp/Introduction-Bisimulation-Coinduction-Davide-Sangiorgi/dp/1107003636 の Example 1.4.4

gistfile1.coq

Require Import String List.
Import ListNotations.

Inductive Action : Type := action : string -> Action.

CoInductive Process : Type :=
| process : list (Action * Process) -> Process.

Inductive mu_derivative : Action -> Process -> Process -> Prop :=
| derivative_here : forall a q l, mu_derivative a (process ((a, q) :: l)) q
| derivative_later : forall a a' l q q', 
    mu_derivative a (process l) q ->
    mu_derivative a (process ((a', q') :: l)) q.

CoInductive Bisimilar : Process -> Process -> Prop :=
| bisimilar : forall p q,
    (forall p' mu, mu_derivative mu p p' -> exists q', mu_derivative mu q q' /\ Bisimilar p' q') ->
    (forall q' mu, mu_derivative mu q q' -> exists p', mu_derivative mu p p' /\ Bisimilar p' q') ->
    Bisimilar p q.

CoFixpoint p1 := process [(action "a", p2)]
with p2 := process [(action "b", p1)].

CoFixpoint q1 := process [(action "a", q2)]
with q2 := process [(action "b", q3)]
with q3 := process [(action "a", q2)].

Definition destruct (p : Process) : Process :=
  match p with
    | process l => process l
  end.

Lemma destruct_eq : forall p, p = destruct p.
Proof.
  destruct p; auto.
Qed.

Goal Bisimilar p1 q1.
Proof.
  cofix.
  rewrite (destruct_eq p1).
  rewrite (destruct_eq q1).
  simpl.
  assert (Bisimilar p2 q2).
    cofix.
    rewrite (destruct_eq p2).
    rewrite (destruct_eq q2).
    simpl.
    assert (Bisimilar p1 q3).
      cofix.
      rewrite (destruct_eq p1).
      rewrite (destruct_eq q3).
      simpl.
      constructor; intros.
        inversion H; subst.
          exists q2.
          split; auto; constructor.

          inversion H5.
        inversion H; subst.
          exists p2.
          split; auto; constructor.

          inversion H5.
    constructor; intros.
      inversion H0; subst.
        exists q3.
        split; auto; constructor.

        inversion H6.
      inversion H0; subst.
        exists p1.
        split; auto; constructor.

        inversion H6.
  constructor; intros.
    inversion H0; subst.
      exists q2.
      split; auto; constructor.

      inversion H6.
    inversion H0; subst.
      exists p2.
      split; auto; constructor.

      inversion H6.
Qed.