# How to prove that addition is commutative for conatural numbers in Coq

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_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.
- rewrite evalCoNat_eq with (n := coadd Z n). simpl.
destruct n.
+ rewrite evalCoNat_eq with (n := coadd Z Z). simpl.
apply bisimilar_Z.
- 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
(bisimilar_m_Sn n 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

You just have to be a bit smarter about the definition of coadd so that it consumes both arguments.

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, n with
|   Z,   Z => Z
|   Z, S n => S n
| S m,   Z => S m
| S m, S n => S (S (coadd m n))
end.

Definition evalCoNat (n : CoNat) :=
match n with
| Z => Z
| S n => S n
end.

Lemma bisim_reflexive: forall n: CoNat, bisimilar n n.
Proof.
cofix CIH.
intros [|n] ; now constructor.
Qed.

Lemma evalCoNat_eq : forall n : CoNat,  n = evalCoNat n.
Proof.
intros [|n] ; reflexivity.
Qed.

forall m n : CoNat, bisimilar (coadd m n) (coadd n m).
Proof.
cofix CIH.
intros m n.
destruct m ; destruct n.
- rewrite (evalCoNat_eq (coadd Z Z)).
constructor.
- rewrite (evalCoNat_eq (coadd Z (S n))).
rewrite (evalCoNat_eq (coadd (S n) Z)).
constructor.
apply bisim_reflexive.
- rewrite (evalCoNat_eq (coadd (S m) Z)).
rewrite (evalCoNat_eq (coadd Z (S m))).
constructor.
apply bisim_reflexive.
- rewrite (evalCoNat_eq (coadd (S m) (S n))).
rewrite (evalCoNat_eq (coadd (S n) (S m))).
simpl.
apply bisimilar_S.
now apply bisimilar_S.
Qed.

• Thanks! So I guess this definition of coadd is what is standard? Jun 25, 2022 at 7:44
• I wouldn't say that. Yours is more like concatenation and mine is more like interweaving. Mine happens to be better suited for proving commutativity. Jun 25, 2022 at 7:45

You could try to use the techniques described in Nils Anders Danielsson's Beating the Productivity Checker Using Embedded Languages.

I've used them in the Agda standard library and successfully deployed the resulting DSL to prove lemmas involving transitivity (e.g. this one) in a guarded manner.

• Thanks! I'll try looking into this technique. Jun 24, 2022 at 13:04

Andrej Bauer has introduced a smarter definition of coadd and has proven that it is commutative.

However, I would like to show that we can prove commutativity without updating the definition of coadd.

The full proof can be found here

The proof involves natural numbers so I will update my notation to hopefully avoid confusion.

For example, S is replaced with CoS to avoid confusion with the successor constructor S for natural numbers.

Futhermore, I will be using n and m for CoNat and N for nat

The definitions from my question are updated as follows (note that only the notation has changed)

CoInductive CoNat :=
| CoZ : CoNat
| CoS : CoNat -> CoNat.

CoInductive bisimilar : CoNat -> CoNat -> Prop :=
| bisimilar_CoZ: bisimilar CoZ CoZ
| bisimilar_CoS: forall n m, bisimilar m n ->  bisimilar (CoS m) (CoS n).

Definition evalCoNat (n : CoNat) :=
match n with
| CoZ => CoZ
| CoS n => CoS n
end.

CoFixpoint coadd (m : CoNat) (n : CoNat) :=
match m with
| CoZ => n
| CoS m' => CoS (coadd m' n)
end.


from these definitions you are able to prove the following

bisim_reflexive: forall n: CoNat, bisimilar n n
bisim_symmetric: forall m n : CoNat, bisimilar m n -> bisimilar n m

(* These helped when rewriting *)



Now the trick I found was to introduce

Fixpoint succN (N: nat) (n : CoNat) :=
match N with
| O => n
| S N' =>  CoS (succN N' n)
end.


If we are able to prove a more general lemma

Lemma bisimilar_m_succN_n_eq_n_succN_m:
forall (m n : CoNat) (N : nat), bisimilar (coadd m (succN N n)) (coadd n (succN N m)).


then we can prove commutativity as it is a specific case of the lemma above, namely when N = 0. That proof is as follows,

Lemma bisimilar_coadd_comm: forall m n : CoNat, bisimilar (coadd m n) (coadd n m).
Proof.
intros m n.
specialize bisimilar_m_succN_n_eq_n_succN_m with (n:= n) (m:=m) (N:= O).
auto.
Qed.


Before proving bisimilar_m_succN_n_eq_n_succN_m we need some auxilliary lemmas


(*  succN_eq_O and succN_eq_S helped when rewriting *)
Lemma succN_eq_O: forall n, n = succN O n.
Proof. intros n. reflexivity. Qed.

Lemma succN_eq_S: forall N n, CoS (succN N n) = succN (S N) n.
Proof. intros N n. reflexivity. Qed.

Lemma succ_N_Cos_n_eq_succN_SN_n: forall N n,  succN N (CoS n) = succN (S N) n.
Proof.
simpl.
intros N n.
induction N.
- simpl. reflexivity.
- simpl. rewrite IHN. reflexivity.
Qed.


Now we have everything we need to prove bisimilar_m_succN_n_eq_n_succN_m

Lemma bisimilar_m_succN_n_eq_n_succN_m:
forall (m n : CoNat) (N : nat), bisimilar (coadd m (succN N n)) (coadd n (succN N m)).
Proof.
cofix CIH.
intros m n N.
destruct N; destruct m; destruct n.
- simpl. apply bisim_reflexive.
- simpl.
rewrite evalCoNat_eq with (n:= coadd CoZ (CoS n)).  simpl.
- simpl.
rewrite evalCoNat_eq with (n:= coadd CoZ (CoS m)).  simpl.
- simpl.
rewrite evalCoNat_eq with (n:= coadd (CoS m) (CoS n)). simpl.
rewrite evalCoNat_eq with (n:= coadd (CoS n) (CoS m)). simpl.
apply bisimilar_CoS.
specialize CIH with (n:= n) (m:=m) (N:= S O).
simpl in CIH.
apply CIH.
- simpl. apply bisim_reflexive.
- rewrite evalCoNat_eq with (n:= coadd CoZ (succN (S N) (CoS n))).
rewrite succ_N_Cos_n_eq_succN_SN_n.
rewrite evalCoNat_eq with (n:= coadd (CoS n) (succN (S N) CoZ)).
simpl (evalCoNat (coadd (CoS n) _)).
apply bisimilar_CoS.
rewrite succN_eq_S.
rewrite coadd_eq_CoZ with (n:= succN (S N) n).
apply CIH.
- rewrite evalCoNat_eq with (n:= coadd CoZ _).
rewrite succ_N_Cos_n_eq_succN_SN_n.
rewrite evalCoNat_eq with (n:= coadd _ _).
simpl (evalCoNat (coadd (CoS m) (succN (S N) CoZ))).
apply bisimilar_CoS.
rewrite succN_eq_S.
rewrite coadd_eq_CoZ with (n:= succN (S N) m).
apply CIH.
- rewrite evalCoNat_eq with (n:= coadd (CoS m) (succN (S N) (CoS n))). simpl.
rewrite evalCoNat_eq with (n:= coadd (CoS n) (CoS (succN N (CoS m)))). simpl.
apply bisimilar_CoS.
rewrite succ_N_Cos_n_eq_succN_SN_n.
rewrite succ_N_Cos_n_eq_succN_SN_n.
rewrite succN_eq_S.
rewrite succN_eq_S.
apply CIH.
Qed


I understand the names for lemmas and proofs are far from elegant. Any improvements will be appreciated!

• I wonder how hard it is to prove that the two definitions of coadd coincide, as that may be a useful technique to have at hand: use whichever seesm most appropriate in a given situation. Jun 25, 2022 at 7:44
• I believe that they do coincide. It'll probably give rise to a simpler proof than what I have. Jun 25, 2022 at 7:47
• By the way, the crucial lemma you proved, that's a typical situation one often faces, namely to find a slightly more general statement that does go through in a (co)inductive proof. In this case, one needs to know what is going on when some amount of the second arguments has been consumed, and the answer is "you get a bunch of successors inserted in" – so you need to account for that. Jun 25, 2022 at 7:47
• I would actually expect that showing the two definitions to coincide will be exactly as hard as your proof. That's because mine is very easy, and by The Law of Preservation of Trouble, we won't make trouble go away magically. Jun 25, 2022 at 7:48
• Hmm. Well I guess the only way to be know for certain is by trying. Jun 25, 2022 at 7:55