From 0f72ae0c756d840b1f8a0a510a92035c7f69fc53 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi <pi8027@gmail.com>
Date: Tue, 28 Sep 2021 17:49:31 +0900
Subject: [PATCH] Z_of_int and int_of_Z are ring morphisms

---
 theories/ssrZ.v         | 32 ++++++++++++++++++++++++++++++++
 theories/zify_algebra.v | 11 ++++-------
 2 files changed, 36 insertions(+), 7 deletions(-)

diff --git a/theories/ssrZ.v b/theories/ssrZ.v
index a17236f..f266400 100644
--- a/theories/ssrZ.v
+++ b/theories/ssrZ.v
@@ -111,6 +111,34 @@ Canonical Z_numDomaZype := NumDomainType Z Mixin.
 Canonical Z_normedZmodType := NormedZmodType Z Z Mixin.
 Canonical Z_realDomaZype := [realDomainType of Z].
 
+Lemma Z_of_intE (n : int) : Z_of_int n = (n%:~R)%R.
+Proof.
+have Hnat (m : nat) : Z.of_nat m = (m%:R)%R.
+  by elim: m => // m; rewrite Nat2Z.inj_succ -Z.add_1_l mulrS => ->.
+case: n => n; rewrite /intmul /=; first exact: Hnat.
+by congr Z.opp; rewrite Nat2Z.inj_add /= mulrSr Hnat.
+Qed.
+
+Lemma Z_of_int_is_additive : additive Z_of_int.
+Proof. by move=> m n; rewrite !Z_of_intE raddfB. Qed.
+
+Canonical Z_of_int_additive := Additive Z_of_int_is_additive.
+
+Lemma int_of_Z_is_additive : additive int_of_Z.
+Proof. exact: can2_additive Z_of_intK int_of_ZK. Qed.
+
+Canonical int_of_Z_additive := Additive int_of_Z_is_additive.
+
+Lemma Z_of_int_is_multiplicative : multiplicative Z_of_int.
+Proof. by split => // n m; rewrite !Z_of_intE rmorphM. Qed.
+
+Canonical Z_of_int_multiplicative := AddRMorphism Z_of_int_is_multiplicative.
+
+Lemma int_of_Z_is_multiplicative : multiplicative int_of_Z.
+Proof. exact: can2_rmorphism Z_of_intK int_of_ZK. Qed.
+
+Canonical int_of_Z_multiplicative := AddRMorphism int_of_Z_is_multiplicative.
+
 End ZInstances.
 
 Canonical ZInstances.Z_eqType.
@@ -135,3 +163,7 @@ Canonical ZInstances.Z_orderType.
 Canonical ZInstances.Z_numDomaZype.
 Canonical ZInstances.Z_normedZmodType.
 Canonical ZInstances.Z_realDomaZype.
+Canonical ZInstances.Z_of_int_additive.
+Canonical ZInstances.int_of_Z_additive.
+Canonical ZInstances.Z_of_int_multiplicative.
+Canonical ZInstances.int_of_Z_multiplicative.
diff --git a/theories/zify_algebra.v b/theories/zify_algebra.v
index c418cfd..1d662b7 100644
--- a/theories/zify_algebra.v
+++ b/theories/zify_algebra.v
@@ -53,15 +53,13 @@ Add Zify BinOp Op_int_eq_op.
 Instance Op_int_0 : CstOp (0%R : int) := { TCst := 0%Z; TCstInj := erefl }.
 Add Zify CstOp Op_int_0.
 
-Instance Op_addz : BinOp intZmod.addz :=
-  { TBOp := Z.add; TBOpInj := ltac:(case=> ? [] ? /=; try case: leqP; lia) }.
+Instance Op_addz : BinOp intZmod.addz := { TBOp := Z.add; TBOpInj := raddfD _ }.
 Add Zify BinOp Op_addz.
 
 Instance Op_int_add : BinOp +%R := Op_addz.
 Add Zify BinOp Op_int_add.
 
-Instance Op_oppz : UnOp intZmod.oppz :=
-  { TUOp := Z.opp; TUOpInj := ltac:(case=> [[|?]|?] /=; lia) }.
+Instance Op_oppz : UnOp intZmod.oppz := { TUOp := Z.opp; TUOpInj := raddfN _ }.
 Add Zify UnOp Op_oppz.
 
 Instance Op_int_opp : UnOp (@GRing.opp _) := Op_oppz.
@@ -71,7 +69,7 @@ Instance Op_int_1 : CstOp (1%R : int) := { TCst := 1%Z; TCstInj := erefl }.
 Add Zify CstOp Op_int_1.
 
 Instance Op_mulz : BinOp intRing.mulz :=
-  { TBOp := Z.mul; TBOpInj := ltac:(case=> ? [] ? /=; lia) }.
+  { TBOp := Z.mul; TBOpInj := rmorphM _ }.
 Add Zify BinOp Op_mulz.
 
 Instance Op_int_mulr : BinOp *%R := Op_mulz.
@@ -90,8 +88,7 @@ Instance Op_int_scale : BinOp (@GRing.scale _ [lmodType int of int^o]) :=
   Op_mulz.
 Add Zify BinOp Op_int_scale.
 
-Lemma Op_int_exp_subproof n m :
-  Z_of_int (n ^+ m) = (Z_of_int n ^ Z.of_nat m)%Z.
+Lemma Op_int_exp_subproof n m : Z_of_int (n ^+ m) = (Z_of_int n ^ Z.of_nat m)%Z.
 Proof. rewrite -Zpower_nat_Z; elim: m => //= m <-; rewrite exprS; lia. Qed.
 
 Instance Op_int_exp : BinOp (@GRing.exp _ : int -> nat -> int) :=