From 264743a60fd9fe01c432509a9206ff11fd07521d Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 11 Jul 2023 13:51:31 +0200 Subject: [PATCH] Add morphism instances for N.to_nat and N.of_nat --- theories/ssrZ.v | 32 ++++++++++++++++++++++++++++++-- 1 file changed, 30 insertions(+), 2 deletions(-) diff --git a/theories/ssrZ.v b/theories/ssrZ.v index 4456155..83c9f83 100644 --- a/theories/ssrZ.v +++ b/theories/ssrZ.v @@ -95,19 +95,47 @@ 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. +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. +Proof. by split=> // m n; rewrite /GRing.mul /=; lia. Qed. #[export] HB.instance Definition _ := GRing.isMultiplicative.Build N nat nat_of_bin nat_of_bin_is_multiplicative. +Fact N_of_nat_is_semi_additive : semi_additive N.of_nat. +Proof. by split=> //= m n; rewrite /GRing.add /=; lia. Qed. + +#[export] +HB.instance Definition _ := GRing.isSemiAdditive.Build nat N N.of_nat + N_of_nat_is_semi_additive. + +Fact N_to_nat_is_semi_additive : semi_additive N.to_nat. +Proof. by split=> //= m n; rewrite /GRing.add /=; lia. Qed. + +#[export] +HB.instance Definition _ := GRing.isSemiAdditive.Build N nat N.to_nat + N_to_nat_is_semi_additive. + +Fact N_of_nat_is_multiplicative : multiplicative N.of_nat. +Proof. by split=> // m n; rewrite /GRing.mul /=; lia. Qed. + +#[export] +HB.instance Definition _ := GRing.isMultiplicative.Build nat N N.of_nat + N_of_nat_is_multiplicative. + +Fact N_to_nat_is_multiplicative : multiplicative N.to_nat. +Proof. by split=> // m n; rewrite /GRing.mul /=; lia. Qed. + +#[export] +HB.instance Definition _ := GRing.isMultiplicative.Build N nat N.to_nat + N_to_nat_is_multiplicative. + Implicit Types (m n : Z). Fact eqZP : Equality.axiom Z.eqb.