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

[Edsko de Vries]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090826/f07d5a3c/attachment-0001.html