Proof of commutativity of conaturals

conatural.v

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.

Lemma evalCoNat_eq : forall n : CoNat, n = evalCoNat n.
Proof.
  destruct n; simpl; reflexivity.
Qed. 

Lemma eq_implies_bisim: forall m n: CoNat, m = n -> bisimilar m n.
Proof.
  cofix eq_implies_bisim.  
  intros m n H.
  destruct n.
  - destruct m.
    +  apply bisimilar_CoZ.
    +  inversion H.
  - destruct m.
    + inversion H.
    + apply bisimilar_CoS.
      apply eq_implies_bisim.
      inversion H.
      reflexivity.
Qed.

Lemma bisim_reflexive: forall n: CoNat, bisimilar n n.
Proof.
  intros n.
  apply eq_implies_bisim.
  reflexivity.
  Show Proof.
Qed.

Lemma bisim_symmetric: forall m n : CoNat, bisimilar m n -> bisimilar n m.
Proof.
  cofix bisim_symmetric.  
  intros m n H.
  destruct m; destruct n.
  - apply bisimilar_CoZ.
  - inversion H.
  - inversion H.
  - apply bisimilar_CoS.
    apply bisim_symmetric.
    inversion H.
    apply H2.
Qed.

Lemma bisim_transitive: forall m n o : CoNat, bisimilar m n -> bisimilar n o -> bisimilar m o.
Proof.
  cofix bisim_transitive.
  intros m n o Hmn Hno.
  destruct m; destruct n; destruct o; try(inversion Hmn); try (inversion Hno).
  - apply bisimilar_CoZ.
  - apply bisimilar_CoS.
    apply bisim_transitive with (n := n).
    + apply H1.
    + apply H4.
Qed.
    
CoFixpoint coadd (m : CoNat) (n : CoNat) :=
  match m with
  | CoZ => n
  | CoS m' => CoS (coadd m' n)
  end.

(* For rewriting purposes 
- n = coadd CoZ n
- CoS (coadd m n) = coadd (CoS m) n
*)

Lemma coadd_eq_CoZ : forall n, n = coadd CoZ n.
Proof.
  destruct n.
  - rewrite evalCoNat_eq with (n:= coadd CoZ CoZ).
    reflexivity.
  -  rewrite evalCoNat_eq with (n:= coadd CoZ (CoS n)).
    reflexivity.
Qed. 

Lemma coadd_eq_CoS: forall m n, CoS (coadd m n) = coadd (CoS m) n.
Proof. 
  intros m n. 
  rewrite evalCoNat_eq with (n:= coadd (CoS _) _). 
  reflexivity.
Qed.

Lemma bisimilar_coadd_n_CoZ: forall n,  bisimilar (coadd n CoZ) n.
Proof.
  cofix CIH.
  destruct n.
  - rewrite evalCoNat_eq with (n := coadd CoZ CoZ).
    simpl.
    apply bisimilar_CoZ.
  - rewrite evalCoNat_eq with (n := coadd (CoS n) CoZ).
    simpl.
    apply bisimilar_CoS.
    apply CIH.
Qed.

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

(* For rewriting purposes

  n = succN O n
  CoS (succN N n) = succ (S N) n
*)
 
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.

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.
    apply bisim_symmetric. apply bisimilar_coadd_n_CoZ.
  - simpl.
    rewrite evalCoNat_eq with (n:= coadd CoZ (CoS m)).  simpl.
    apply bisimilar_coadd_n_CoZ.
  - 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))).
    simpl (evalCoNat (coadd CoZ _)).
    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 _).
    simpl (evalCoNat (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.

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.