I have defined the conatural numbers, bisimulation (extensional equality?) and addition as follows,
CoInductive CoNat :=
| Z : CoNat
| S : CoNat -> CoNat.
CoInductive bisimilar : CoNat -> CoNat -> Prop :=
| bisimilar_Z: bisimilar Z Z
| bisimilar_S: forall n m, bisimilar m n -> bisimilar (S m) (S n).
CoFixpoint coadd (m : CoNat) (n : CoNat) :=
match m with
| Z => n
| S m' => S (coadd m' n)
end.
and the following to help with reducing expressions
Definition evalCoNat (n : CoNat) :=
match n with
| Z => Z
| S n => S n
end.
Lemma evalCoNat_eq : forall n : CoNat, n = evalCoNat n.
To get myself acquainted with coinduction I was trying to prove the following
Lemma bisimilar_coadd_comm: forall m n : CoNat, bisimilar (coadd m n) (coadd n m).
I assumed that proving commutativity was analogous to proving commutativity of addition for natural numbers, so I proved the following,
Lemma bisim_reflexive: forall n: CoNat, bisimilar n n.
Lemma bisim_symmetric: forall m n : CoNat, bisimilar m n -> bisimilar n m.
Lemma bisim_transitive: forall m n o : CoNat, bisimilar m n -> bisimilar n o -> bisimilar m o.
Lemma bisimilar_coadd_n_Z: forall n, bisimilar (coadd n Z) n.
Lemma bisimilar_coadd_Z_n: forall n, bisimilar (coadd Z n) n.
Lemma bisimilar_m_Sn: forall m n : CoNat, bisimilar (S (coadd m n)) (coadd m (S n)).
Now I've attempted to prove bisimilar_coadd_comm but I'm getting an error saying I'm not in guarded form.
Lemma bisimilar_coadd_comm: forall m n : CoNat, bisimilar (coadd m n) (coadd n m).
Proof.
cofix CIH.
intros m n.
destruct m.
(* bisimilar (coadd Z n) (coadd n Z) *)
- rewrite evalCoNat_eq with (n := coadd Z n). simpl.
destruct n.
+ rewrite evalCoNat_eq with (n := coadd Z Z). simpl.
apply bisimilar_Z.
+ apply bisim_symmetric. apply bisimilar_coadd_n_Z.
(* bisimilar (coadd (S m) n) (coadd n (S m)) *)
- rewrite evalCoNat_eq with (n := coadd (S m) n).
simpl.
apply bisim_transitive with (n := S (coadd n m)).
+ apply bisimilar_S. apply CIH.
+ apply bisimilar_m_Sn.
Qed.
After reading Chapter 5 of Adam's Chipala's "Certified Programming with Dependent Types", I (kind of) understood how coinductive proofs correspond to corecursive functions and that "a corecursive call must be a direct argument to a constructor, only inside of other constructor calls or fun or match expressions".
After looking at my error again I find the proof object breaking this condition is
bisim_transitive
(S (coadd c n)) m
(S (coadd n c)) n
(coadd n (S c)) o
(bisimilar_S (coadd n c) (coadd c n) (bisimilar_coadd_comm c n))
(bisimilar_m_Sn n c)
:
bisimilar (evalCoNat (coadd (S c) n)) (coadd n (S c))
So my guess is that the guardedness condition is not met as bisimilar_S is under bisim_transitive? But I don't know how I could prove this without using the transitive property. Would I need an extra lemma? Is there a simple trick? Is there a some rule of thumb?
My current understanding of coinduction after reading a bit of Davide Sangiorgi's "An introduction to bisimulation and coinduction" is that I would need to prove is that properties are maintained backwards. That is if a property $P$ for a conclusion is true then the property $P$ is also true for the premises.
But maybe my understanding isn't right...
If possible I would like an informal proof, and then a proof in Coq. Moreover, a correction if I'm misunderstanding coinduction.
Edit: Renamed the coinduction hypothesis from bisimilar_coadd_comm to CIH in bisimilar_coadd_comm
