[Agda] Re: [Coq-Club] Adding (inductive) transitivity to weak bisimilarity not sound? (was: Need help with coinductive proof)

[Edsko de Vries]

>
> So, what's left to be able to complete the proof is adding transitivity
> rules to the extended relation, and then presumably a translation from the
> extended extended relation to the extended relation, and then finally to the
> original bisimulation relation. Hopefully, that's not too difficult..


I thought I was almost there, when I realized that adding (inductive)
transitivity to my weak bisimularity relation is not sound, as any number is
now bisimilar to bottom:

      ------ reflexivity                -------- coinduction
      n ~ n                             n ~ _|_
    ---------- weak-tau-right       ---------------- strong_tau
    n ~ tau n                       tau n ~ tau _|_
    ------------------------------------------------- transitivity
                        n ~ _|_

note that this mixes coinduction and induction; the coinductive argument (n
~ _|_) in the leaf is guarded by an application of strong_tau; and the rest
of the proof is finite. At least, I think that's right (would Agda accept
it?); concretely, using my Coq encoding of mixed induction/coinduction with
nats to limit the application of the 'inductive' rules, I had

CoInductive bisim'P : nat -> coN' -> coN' -> Prop :=
  | strong_coZ'P : forall d,
      bisim'P d coZ' coZ'
  | strong_coS'P : forall d' d m n,
      bisim'P d' m n ->
      bisim'P d (coS' m) (coS' n)
  | strong_tau'P : forall d' d m n,
      bisim'P d' m n ->
      bisim'P d (tau' m) (tau' n)
  | strong_add'P : forall dm dn d m m' n n',
      bisim'P dm m m' ->
      bisim'P dn n n' ->
      bisim'P d (add' m n) (add' m' n')
  | weak_tau_left'P : forall d m n,
      bisim'P d m n ->
      bisim'P (S d) (tau' m) n
  | weak_tau_right'P : forall d m n,
      bisim'P d m n ->
      bisim'P (S d) m (tau' n)
  | bisim'P_trans : forall dm dn d m n p, (dm < d) -> (dn < d) ->
      bisim'P dm m n ->
      bisim'P dn n p ->
      bisim'P d m p.

which certainly has the above problem. I find this to be an extremely subtle
issue, and the solution is not clear to me. In particular, when I restrict
the rule for strong_tau so that it uses the same index above and below the
line

  | strong_tau'P : forall d m n,
      bisim'P d m n ->
      bisim'P d (tau' m) (tau' n)

I can no longer prove the flattening lemma for bisimulation so I again have
nothing :-(

We must somehow limit the rules that are applied as arguments to
transitivity to be strong steps, not weak steps (it reminds me a bit of the
problem of weak bisimulation up to weak bisimularity) -- I *think* that
might be enough, but at this point I'm not really sure about anything
anymore ;)

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