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