The Coq mailing list

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

Hi,

(I tried to keep this as short as I could, which means this cannot be  
copied&pasted into Coq as there are definitions missing; if anybody  
wants to experiment, the full file can be found at http://www.cs.tcd.ie/Edsko.de.Vries/conat.v)

I am stuck in a lemma, and would appreciate some suggestions. It is  
possible that the lemma is not true; if that is the case, I would like  
to know, too :) (I've tried hard to come up with a counter-example and  
failed, but that doesn't mean very much).

I have a definition of co-natural numbers, which include an 'add zero'  
constructor (as suggested by Adam a while back) and a sum constructor:

CoInductive conat : Set :=
 | cozero : conat
 | cosucc : conat -> conat
 | coadd : conat -> conat -> conat
 | coaddzero : conat -> conat.

I defined a function [flatten : conat -> conat] which removes [coadd]s  
(but not [coaddzero]s): basically, addition. We now define weak  
bisimularity (~) over conat's, so that 5 ~ 2 + 3 for instance and  
infinitely many [coaddzero (coaddzero (...))] ~ 0 but not to any  
number larger than 0. I define it in a process-calculus style, really  
just because I don't know how else; we set up an LTS, define the  
standard weak step (=>) relation, and set up the standard weak  
bisimilarity relation:

Inductive red_label := tau | succ.

Inductive red : red_label -> conat -> conat -> Prop :=
  | red_cosucc : forall m,
      red succ (cosucc m) m
  | red_coadd : forall m n,
      red tau (coadd m n) (flatten_conat (coadd m n))
  | red_coaddzero : forall m,
      red tau (coaddzero m) m.

Definition tau_steps := clos_refl_trans _ (red tau).

Inductive weak_hat : red_label -> conat -> conat -> Prop :=
  | weak_hat_succ : forall m m' n' n,
      tau_steps m m' ->
      red succ m' n' ->
      tau_steps n' n ->
      weak_hat succ m n
  | weak_hat_tau : forall m n,
      tau_steps m n ->
      weak_hat tau m n.

CoInductive bisimilar_conat : conat -> conat -> Prop :=
  | bisim_conat : forall m n,
     (forall l m', red l m m' ->
       exists n', weak_hat l n n' /\ bisimilar_conat m' n') ->
     (forall l n', red l n n' ->
       exists m', weak_hat l m m' /\ bisimilar_conat m' n') ->
     bisimilar_conat m n

I've proven various standard properties of this bisimilarity relation  
(equivalence relation, Park principle, some up-to techniques, etc.) so  
everything seems ok so far.

But now for my question: in a particular proof that two conats are  
bisimilar, it was quite difficult to satisfy the guardedness condition  
(for various reasons Park principle could not really be used, so that  
I had to prove bisimilarity directly). I therefore defined an  
auxiliary relation bisim_CF (defined below), and proved that the two  
conats are related in bisim_CF instead. The idea was that guardedness  
for the auxiliary relation was easily satisfied in the original proof  
(a bit like Ana Bove's technique for induction, perhaps);  of course,  
there is now a separate proof obligation that bisim_CF is included in  
bisimularity - and that's the proof that I cannot do. Here is the  
definition of bisim_CF and the statement of the lemma:

CoInductive bisim_CF : conat -> conat -> Prop :=
  | bisim_CF_bisim : forall m n,
      bisimilar_conat m n ->
      bisim_CF m n
  | bisim_CF_prod : forall h m m' n n',
      bisimilar_conat (h cozero) cozero ->
      (forall i j, bisimilar_conat (h (coadd i j)) (coadd (h i) (h  
j))) ->
      bisim_CF (h m) m' ->
      bisim_CF (h n) n' ->
      bisim_CF (h (coadd m n)) (coadd m' n').

Lemma bisim_CF_bisimilar : forall m n,
  bisim_CF m n -> bisimilar_conat m n.

Graphically:

    m ~ n                      h m CF m'   h n CF n'
  ------------                  ----------------------------
   m CF n                     h (m + n) CF m' + n'

for any morphism h from conat -> conat (h 0 ~ 0 and h (i + j) ~ h i +  
h j).

Now, waving my hands, in the proof that this implies bisimularity, we  
proceed by coinduction, inversion on [bisim_CF], and then for the case  
of [bisim_CF_prod] we simply reason

  h (m + n) ~ h m + h n ~ m' + n'

which uses an auxiliary lemma "add_bisim" that m + n ~ m' + n' if m ~  
m' and n ~ n'; we need to reason that h m ~ m' and h n ~ n' "by  
coinduction". Unfortunately, this is not guarded, because the  
recursive calls will be used as arguments to "add_bisim" and to  
transitivity.

It is quite possible that bisim_CF was a very bad idea and that this  
way of trying to do the original proof is not possible, because  
bisim_CF is too large; but if that is the case, I cannot see it.  
However, I also keep getting stuck in [bisim_CF_bisimilar] -- the  
guardedness checker is never happy.

Any suggestions on how to proceed would be appreciated,

Edsko