Merge pull request #47 from math-comp/N-semiring

`N` forms a semiring

examples/test_algebra.v

@@ -7,6 +7,42 @@ Unset Printing Implicit Defensive.
 
 Local Delimit Scope Z_scope with Z.
 
+Fact test_zero_nat : Z.of_nat 0%R = 0%Z.
+Proof. zify_op; reflexivity. Qed.
+
+Fact test_add_nat n m : Z.of_nat (n + m)%R = (Z.of_nat n + Z.of_nat m)%Z.
+Proof. zify_op; reflexivity. Qed.
+
+Fact test_one_nat : Z.of_nat 1%R = 1%Z.
+Proof. zify_op; reflexivity. Qed.
+
+Fact test_mul_nat n m : Z.of_nat (n * m)%R = (Z.of_nat n * Z.of_nat m)%Z.
+Proof. zify_op; reflexivity. Qed.
+
+Fact test_natmul_nat n m : Z.of_nat (n *+ m)%R = (Z.of_nat n * Z.of_nat m)%Z.
+Proof. zify_op; reflexivity. Qed.
+
+Fact test_exp_nat n m : Z.of_nat (n ^+ m)%R = (Z.of_nat n ^ Z.of_nat m)%Z.
+Proof. zify_op; reflexivity. Qed.
+
+Fact test_zero_N : Z.of_N 0%R = 0%Z.
+Proof. zify_op; reflexivity. Qed.
+
+Fact test_add_N n m : Z.of_N (n + m)%R = (Z.of_N n + Z.of_N m)%Z.
+Proof. zify_op; reflexivity. Qed.
+
+Fact test_one_N : Z.of_N 1%R = 1%Z.
+Proof. zify_op; reflexivity. Qed.
+
+Fact test_mul_N n m : Z.of_N (n * m)%R = (Z.of_N n * Z.of_N m)%Z.
+Proof. zify_op; reflexivity. Qed.
+
+Fact test_natmul_N n m : Z.of_N (n *+ m)%R = (Z.of_N n * Z.of_nat m)%Z.
+Proof. zify_op; reflexivity. Qed.
+
+Fact test_exp_N n m : Z.of_N (n ^+ m)%R = (Z.of_N n ^ Z.of_nat m)%Z.
+Proof. zify_op; reflexivity. Qed.
+
 Fact test_unit_int m :
   m \is a GRing.unit = (Z_of_int m =? 1)%Z || (Z_of_int m =? - 1)%Z.
 Proof. zify_pre_hook; zify_op; reflexivity. Qed.

examples/test_ssreflect.v

@@ -63,6 +63,8 @@ Proof. zify_op; reflexivity. Qed.
 Fact test_dual_max_bool (b1 b2 : bool^d) : Order.dual_max b1 b2 = b1 && b2.
 Proof. zify_op; reflexivity. Qed.
 
+(* FIXME: meet and join below are broken but the tests pass because they are  *)
+(* convertible anyway.                                                        *)
 Fact test_meet_bool b1 b2 : (b1 `&` b2)%O = b1 && b2.
 Proof. zify_op; reflexivity. Qed.
 
@@ -75,17 +77,17 @@ Proof. zify_op; reflexivity. Qed.
 Fact test_dual_join_bool (b1 b2 : bool^d) : (b1 `|^d` b2)%O = b1 && b2.
 Proof. zify_op; reflexivity. Qed.
 
-Fact test_bottom_bool : 0%O = false :> bool.
+Fact test_bottom_bool : \bot%O = false :> bool.
 Proof. zify_op; reflexivity. Qed.
 
-Fact test_top_bool : 1%O = true :> bool.
+Fact test_top_bool : \top%O = true :> bool.
 Proof. zify_op; reflexivity. Qed.
 
 (* FIXME: Notations 0^d and 1^d are broken. *)
-Fact test_dual_bottom_bool : 0%O = true :> bool^d.
+Fact test_dual_bottom_bool : \bot%O = true :> bool^d.
 Proof. zify_op; reflexivity. Qed.
 
-Fact test_dual_top_bool : 1%O = false :> bool^d.
+Fact test_dual_top_bool : \top%O = false :> bool^d.
 Proof. zify_op; reflexivity. Qed.
 
 Fact test_sub_bool b1 b2 : (b1 `\` b2)%O = b1 && ~~ b2.
@@ -235,7 +237,7 @@ Fact test_dual_join_nat (n m : nat^d) :
   Z.of_nat (n `|^d` m)%O = Z.min (Z.of_nat n) (Z.of_nat m).
 Proof. zify_op; reflexivity. Qed.
 
-Fact test_bottom_nat : Z.of_nat 0%O = 0%Z.
+Fact test_bottom_nat : Z.of_nat \bot%O = 0%Z.
 Proof. zify_op; reflexivity. Qed.
 
 (******************************************************************************)
@@ -315,15 +317,14 @@ Fact test_dual_join_natdvd (n m : natdvd^d) :
   Z.of_nat (n `|` m)%O = Z.gcd (Z.of_nat n) (Z.of_nat m).
 Proof. zify_op; reflexivity. Qed.
 
-Fact test_bottom_natdvd : Z.of_nat (0%O : natdvd) = 1%Z.
+Fact test_bottom_natdvd : Z.of_nat (\bot%O : natdvd) = 1%Z.
 Proof. zify_op; reflexivity. Qed.
 
-Fact test_top_natdvd : Z.of_nat (1%O : natdvd) = 0%Z.
+Fact test_top_natdvd : Z.of_nat (\top%O : natdvd) = 0%Z.
 Proof. zify_op; reflexivity. Qed.
 
-(* FIXME: Notations 0^d and 1^d are broken. *)
-Fact test_dual_bottom_natdvd : Z.of_nat (0%O : natdvd^d) = 0%Z.
+Fact test_dual_bottom_natdvd : Z.of_nat (\bot^d%O : natdvd^d) = 0%Z.
 Proof. zify_op; reflexivity. Qed.
 
-Fact test_dual_top_natdvd : Z.of_nat (1%O : natdvd^d) = 1%Z.
+Fact test_dual_top_natdvd : Z.of_nat (\top^d%O : natdvd^d) = 1%Z.
 Proof. zify_op; reflexivity. Qed.

theories/ssrZ.v

@@ -35,7 +35,78 @@ case=> [[|n]|n] //=.
 rewrite addnC /=; congr Negz; lia.
 Qed.
 
-Module ZInstances.
+Module Instances.
+
+(* Instances taken from math-comp/math-comp#1031, authored by Pierre Roux *)
+(* TODO: remove them when we drop support for MathComp 2.0 *)
+#[export]
+HB.instance Definition _ := GRing.isNmodule.Build nat addnA addnC add0n.
+
+#[export]
+HB.instance Definition _ := GRing.Nmodule_isComSemiRing.Build nat
+  mulnA mulnC mul1n mulnDl mul0n erefl.
+
+#[export]
+HB.instance Definition _ (V : nmodType) (x : V) :=
+  GRing.isSemiAdditive.Build nat V (GRing.natmul x) (mulr0n x, mulrnDr x).
+
+#[export]
+HB.instance Definition _ (R : semiRingType) :=
+  GRing.isMultiplicative.Build nat R (GRing.natmul 1) (natrM R, mulr1n 1).
+
+Fact Posz_is_semi_additive : semi_additive Posz.
+Proof. by []. Qed.
+
+#[export]
+HB.instance Definition _ := GRing.isSemiAdditive.Build nat int Posz
+  Posz_is_semi_additive.
+
+Fact Posz_is_multiplicative : multiplicative Posz.
+Proof. by []. Qed.
+
+#[export]
+HB.instance Definition _ := GRing.isMultiplicative.Build nat int Posz
+  Posz_is_multiplicative.
+(* end *)
+
+#[export]
+HB.instance Definition _ := Countable.copy N (can_type nat_of_binK).
+
+#[export]
+HB.instance Definition _ := GRing.isNmodule.Build N
+  Nplus_assoc Nplus_comm Nplus_0_l.
+
+#[export]
+HB.instance Definition _ := GRing.Nmodule_isComSemiRing.Build N
+  Nmult_assoc Nmult_comm Nmult_1_l Nmult_plus_distr_r N.mul_0_l isT.
+
+Fact bin_of_nat_is_semi_additive : semi_additive bin_of_nat.
+Proof. by split=> //= m n; rewrite /GRing.add /=; lia. Qed.
+
+#[export]
+HB.instance Definition _ := GRing.isSemiAdditive.Build nat N bin_of_nat
+  bin_of_nat_is_semi_additive.
+
+Fact nat_of_bin_is_semi_additive : semi_additive nat_of_bin.
+Proof. by split=> //= m n; rewrite /GRing.add /=; lia. Qed.
+
+#[export]
+HB.instance Definition _ := GRing.isSemiAdditive.Build N nat nat_of_bin
+  nat_of_bin_is_semi_additive.
+
+Fact bin_of_nat_is_multiplicative : multiplicative bin_of_nat.
+Proof. by split => // m n; rewrite /GRing.mul /=; lia. Qed.
+
+#[export]
+HB.instance Definition _ := GRing.isMultiplicative.Build nat N bin_of_nat
+  bin_of_nat_is_multiplicative.
+
+Fact nat_of_bin_is_multiplicative : multiplicative nat_of_bin.
+Proof. exact: can2_rmorphism bin_of_natK nat_of_binK. Qed.
+
+#[export]
+HB.instance Definition _ := GRing.isMultiplicative.Build N nat nat_of_bin
+  nat_of_bin_is_multiplicative.
 
 Implicit Types (m n : Z).
 
@@ -121,7 +192,7 @@ HB.instance Definition _ := GRing.isAdditive.Build Z int int_of_Z
   int_of_Z_is_additive.
 
 Fact Z_of_int_is_multiplicative : multiplicative Z_of_int.
-Proof. by split => // n m; rewrite !Z_of_intE rmorphM. Qed.
+Proof. by split => // m n; rewrite !Z_of_intE rmorphM. Qed.
 
 #[export]
 HB.instance Definition _ := GRing.isMultiplicative.Build int Z Z_of_int
@@ -134,8 +205,36 @@ Proof. exact: can2_rmorphism Z_of_intK int_of_ZK. Qed.
 HB.instance Definition _ := GRing.isMultiplicative.Build Z int int_of_Z
   int_of_Z_is_multiplicative.
 
+Fact Z_of_nat_is_semi_additive : semi_additive Z.of_nat.
+Proof. by split=> //= m n; rewrite /GRing.add /=; lia. Qed.
+
+#[export]
+HB.instance Definition _ := GRing.isSemiAdditive.Build nat Z Z.of_nat
+  Z_of_nat_is_semi_additive.
+
+Fact Z_of_nat_is_multiplicative : multiplicative Z.of_nat.
+Proof. by split => // m n; rewrite /GRing.mul /=; lia. Qed.
+
+#[export]
+HB.instance Definition _ := GRing.isMultiplicative.Build nat Z Z.of_nat
+  Z_of_nat_is_multiplicative.
+
+Fact Z_of_N_is_semi_additive : semi_additive Z.of_N.
+Proof. by split=> //= m n; rewrite /GRing.add /=; lia. Qed.
+
+#[export]
+HB.instance Definition _ := GRing.isSemiAdditive.Build N Z Z.of_N
+  Z_of_N_is_semi_additive.
+
+Fact Z_of_N_is_multiplicative : multiplicative Z.of_N.
+Proof. by split => // m n; rewrite /GRing.mul /=; lia. Qed.
+
+#[export]
+HB.instance Definition _ := GRing.isMultiplicative.Build N Z Z.of_N
+  Z_of_N_is_multiplicative.
+
 Module Exports. HB.reexport. End Exports.
 
-End ZInstances.
+End Instances.
 
-Export ZInstances.Exports.
+Export Instances.Exports.

theories/zify_algebra.v

@@ -17,6 +17,86 @@ Local Delimit Scope Z_scope with Z.
 
 Import Order.Theory GRing.Theory Num.Theory SsreflectZifyInstances.
 
+(* TODO: remove natn below when we drop support for MathComp 2.0 *)
+Local Lemma natn n : n%:R%R = n :> nat.
+Proof. by elim: n => // n; rewrite mulrS => ->. Qed.
+
+(******************************************************************************)
+(* nat                                                                        *)
+(******************************************************************************)
+
+#[global]
+Instance Op_nat_0 : CstOp (0%R : nat) := ZifyInst.Op_O.
+Add Zify CstOp Op_nat_0.
+
+#[global]
+Instance Op_nat_add : BinOp (+%R : nat -> nat -> nat) := Op_addn.
+Add Zify BinOp Op_nat_add.
+
+#[global]
+Instance Op_nat_1 : CstOp (1%R : nat) := { TCst := 1%Z; TCstInj := erefl }.
+Add Zify CstOp Op_nat_1.
+
+#[global]
+Instance Op_nat_mul : BinOp ( *%R : nat -> nat -> nat) := Op_muln.
+Add Zify BinOp Op_nat_mul.
+
+Fact Op_nat_natmul_subproof (n m : nat) :
+  Z.of_nat (n *+ m)%R = (Z.of_nat n * Z.of_nat m)%Z.
+Proof. by rewrite raddfMn -mulr_natr -[m in RHS]natn rmorph_nat. Qed.
+
+#[global]
+Instance Op_nat_natmul : BinOp (@GRing.natmul _ : nat -> nat -> nat) :=
+  { TBOp := Z.mul; TBOpInj := Op_nat_natmul_subproof }.
+Add Zify BinOp Op_nat_natmul.
+
+Fact Op_nat_exp_subproof (n : nat) (m : nat) :
+  Z_of_nat (n ^+ m)%R = (Z_of_int n ^ Z.of_nat m)%Z.
+Proof. rewrite -Zpower_nat_Z; elim: m => //= m <-; rewrite exprS; lia. Qed.
+
+#[global]
+Instance Op_nat_exp : BinOp (@GRing.exp _ : nat -> nat -> nat) :=
+  { TBOp := Z.pow; TBOpInj := Op_nat_exp_subproof }.
+Add Zify BinOp Op_nat_exp.
+
+(******************************************************************************)
+(* N                                                                          *)
+(******************************************************************************)
+
+#[global]
+Instance Op_N_0 : CstOp (0%R : N) := ZifyInst.Op_N_N0.
+Add Zify CstOp Op_N_0.
+
+#[global]
+Instance Op_N_add : BinOp (+%R : N -> N -> N) := ZifyInst.Op_N_add.
+Add Zify BinOp Op_N_add.
+
+#[global]
+Instance Op_N_1 : CstOp (1%R : N) := { TCst := 1%Z; TCstInj := erefl }.
+Add Zify CstOp Op_N_1.
+
+#[global]
+Instance Op_N_mul : BinOp ( *%R : N -> N -> N) := ZifyInst.Op_N_mul.
+Add Zify BinOp Op_N_mul.
+
+Fact Op_N_natmul_subproof (n : N) (m : nat) :
+  Z.of_N (n *+ m)%R = (Z.of_N n * Z.of_nat m)%Z.
+Proof. by rewrite raddfMn -mulr_natr -[m in RHS]natn rmorph_nat. Qed.
+
+#[global]
+Instance Op_N_natmul : BinOp (@GRing.natmul _ : N -> nat -> N) :=
+  { TBOp := Z.mul; TBOpInj := Op_N_natmul_subproof }.
+Add Zify BinOp Op_N_natmul.
+
+Fact Op_N_exp_subproof (n : N) (m : nat) :
+  Z_of_N (n ^+ m)%R = (Z_of_N n ^ Z.of_nat m)%Z.
+Proof. rewrite -Zpower_nat_Z; elim: m => //= m <-; rewrite exprS; lia. Qed.
+
+#[global]
+Instance Op_N_exp : BinOp (@GRing.exp _ : N -> nat -> N) :=
+  { TBOp := Z.pow; TBOpInj := Op_N_exp_subproof }.
+Add Zify BinOp Op_N_exp.
+
 (******************************************************************************)
 (* ssrint                                                                     *)
 (******************************************************************************)
@@ -287,7 +367,7 @@ Instance Op_Z_exp : BinOp (@GRing.exp _ : Z -> nat -> Z) :=
 Add Zify BinOp Op_Z_exp.
 
 #[global]
-Instance Op_unitZ : UnOp (has_quality 1 ZInstances.unitZ : Z -> bool) :=
+Instance Op_unitZ : UnOp (has_quality 1 Instances.unitZ : Z -> bool) :=
   { TUOp x := (x =? 1)%Z || (x =? - 1)%Z; TUOpInj _ := erefl }.
 Add Zify UnOp Op_unitZ.
 
@@ -296,7 +376,7 @@ Instance Op_Z_unit : UnOp (has_quality 1 GRing.unit : Z -> bool) := Op_unitZ.
 Add Zify UnOp Op_Z_unit.
 
 #[global]
-Instance Op_invZ : UnOp ZInstances.invZ := { TUOp := id; TUOpInj _ := erefl }.
+Instance Op_invZ : UnOp Instances.invZ := { TUOp := id; TUOpInj _ := erefl }.
 Add Zify UnOp Op_invZ.
 
 #[global]
@@ -427,6 +507,18 @@ Instance Op_coprimez : BinOp coprimez :=
 Add Zify BinOp Op_coprimez.
 
 Module Exports.
+Add Zify CstOp Op_nat_0.
+Add Zify BinOp Op_nat_add.
+Add Zify CstOp Op_nat_1.
+Add Zify BinOp Op_nat_mul.
+Add Zify BinOp Op_nat_natmul.
+Add Zify BinOp Op_nat_exp.
+Add Zify CstOp Op_N_0.
+Add Zify BinOp Op_N_add.
+Add Zify CstOp Op_N_1.
+Add Zify BinOp Op_N_mul.
+Add Zify BinOp Op_N_natmul.
+Add Zify BinOp Op_N_exp.
 Add Zify InjTyp Inj_int_Z.
 Add Zify UnOp Op_Z_of_int.
 Add Zify UnOp Op_Posz.