The Coq mailing list

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

Hi Thorsten, Nils, and others,

Thanks for your help so far. Although I now understand the problem a bit better I still keep getting stuck in my proof; it's frustrating :( With the help so far however I think I can explain my problem a bit better now (stand-alone example at http://www.cs.tcd.ie/Edsko.de.Vries/bisimulation.v). So let me try again, from scratch.

Consider adding all numbers in an infinite stream of (partial, co-natural) numbers, and applying some function h:

  h (x1 + (x2 + (x3 + ..)))

If h is a morphism from nat to nat (i.e., h 0 ~ 0 and h (i + j) ~ h i + h j), then this should be bisimilar to 

  h x1 + (h x2 + (h x3 + ..))

(To anticipate the problem, to prove that the right summands (x2 + (x3 + ..) and (h x2 + (h x3 + ..)) are bisimilar, we will want to use guarded corecursion.) To define the function that adds all numbers in a stream it is convenient to define a datatype conatP which includes addition as a constructor:

CoInductive conatP : Set :=
  | cozeroP : conatP
  | cosuccP : conatP -> conatP
  | tau_conatP : conatP -> conatP 
  | sum_conatP : colist conatP -> conatP.

As in the paper Nils cited, we can translate conatP to conat (which is like conatP but without sum_conatP) using an intermediate conatW datatype, defined as

Inductive conatW : Set :=
  | cozeroW : conatW
  | cosuccW : conatP -> conatW
  | tau_conatW : conatP -> conatW.

The translation from conatP to conatW and from conatW to conat is not too difficult, and follows the pattern in the paper (the generalization to a colist rather than just two summands in the sum_conatP is crucial, though). Note that the sum arguments are coinductive: an infinitely branching sum is possible:

Definition conatP_conatW (n : conatP) : conatW :=
  match n with
  | cozeroP => cozeroW
  | cosuccP n' => cosuccW n'
  | tau_conatP n' => tau_conatW n'
  | sum_conatP ns => 
      match ns with
      | conil => cozeroW
      | cocons n' ns' => 
          match n' with
          | cozeroP => tau_conatW (sum_conatP ns')
          | cosuccP n'' => cosuccW (sum_conatP (cocons n'' ns'))
          | tau_conatP n'' => tau_conatW (sum_conatP (cocons n'' ns'))
          | sum_conatP ns'' => tau_conatW (sum_conatP (coappend ns'' ns'))
          end
      end
  end.

CoFixpoint conatW_conat (n : conatW) : conat :=
  match n with
  | cozeroW => cozero
  | cosuccW n' => cosucc (conatW_conat (conatP_conatW n'))
  | tau_conatW n' => tau_conat (conatW_conat (conatP_conatW n'))
  end.

Note that for infinitely branching sums, we simply get (tau (tau (tau ..))) as the answer. 

So far, so good. However, now consider the proof mentioned at the start. The standard bisimulation on conat's is defined like Thorsten did, except that I index the maximum delay (number of taus) using a natural number, rather than mixing coinduction and induction:

CoInductive bisimilar_conat : nat -> conat -> conat -> Prop :=
  | bisim_cozero : forall d,
      bisimilar_conat d cozero cozero
  | bisim_cosucc : forall d' d m n,
      bisimilar_conat d' m n ->
      bisimilar_conat d (cosucc m) (cosucc n)
  | bisim_tau : forall d' d m n,
      bisimilar_conat d' m n ->
      bisimilar_conat d (tau_conat m) (tau_conat n)
  | bisim_tau_left : forall d m n,
      bisimilar_conat d m n ->
      bisimilar_conat (S d) (tau_conat m) n
  | bisim_tau_right : forall d m n,
      bisimilar_conat d m n ->
      bisimilar_conat (S d) m (tau_conat n).

(Note that the delay must be strictly decreasing in rules bisim_tau_left and bisim_tau_right and is left free otherwise.)

For the proof it is convenient to explicitly support sums in the bisimulation, so we define a relation which is very similar to the standard bisimulation, but has one extra constructor (actually, we will want to add transitivity as a rule, too, but one thing at the time..).

CoInductive bisimilarP_conat : nat -> conat -> conat -> Prop :=
  | bisimP_cozero : forall d,
      bisimilarP_conat d cozero cozero
  | bisimP_cosucc : forall d' d m n,
      bisimilarP_conat d' m n ->
      bisimilarP_conat d (cosucc m) (cosucc n)
  | bisimP_tau : forall d' d m n,
      bisimilarP_conat d' m n ->
      bisimilarP_conat d (tau_conat m) (tau_conat n)
  | bisimP_tau_left : forall d m n,
      bisimilarP_conat d m n ->
      bisimilarP_conat (S d) (tau_conat m) n
  | bisimP_tau_right : forall d m n,
      bisimilarP_conat d m n ->
      bisimilarP_conat (S d) m (tau_conat n)
  | bisimP_sum_conat : forall d ms ns,
      (bisimilar_colist (fun m n => exists d', bisimilarP_conat d m n) ms ns) ->
      bisimilarP_conat d (sum_conat ms) (sum_conat ns).

where (bisimilar_colist R) is the standard bisimulation on streams, parametrized by the relation R on the elements of the stream.

Note that again this datatype supports infinitely branching proofs of bisimulation of sums; this is necessary because the sums themselves may be infinitely branching. Nevertheless, I feel that it should be possible to give a translation from bisimP, probably through an intermediate data type

Inductive bisimilarW_conat : nat -> conat -> conat -> Prop :=
  | bisimW_cozero : forall d,
      bisimilarW_conat d cozero cozero
  | bisimW_cosucc : forall d' d m n,
      bisimilarP_conat d' m n ->
      bisimilarW_conat d (cosucc m) (cosucc n)
  | bisimW_tau : forall d' d m n,
      bisimilarP_conat d' m n ->
      bisimilarW_conat d (tau_conat m) (tau_conat n)
  | bisimW_tau_left : forall d m n,
      bisimilarP_conat d m n ->
      bisimilarW_conat (S d) (tau_conat m) n
  | bisimW_tau_right : forall d m n,
      bisimilarP_conat d m n ->
      bisimilarW_conat (S d) m (tau_conat n).

I did get quite far in the proof that bisimP implies bisimW, but got stuck in the following lemma:

Lemma bisimP_tau_inv : forall i m n,
  bisimilarP_conat i (tau_conat m) n ->
  exists j, bisimilarP_conat j m n.

and I get stuck exactly because the maximum delay for the elements of a sum need not be smaller than the maximum delay allowed for the sum itself - but I don't want to change that because that means that we can no longer have infinite proofs that consist of bisimP_add_conat constructors only. 

Am I trying to do the impossible, or am I missing something obvious? 

Edsko