The Coq mailing list

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

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