Skip to content

Commit

Permalink
N forms a semiring
Browse files Browse the repository at this point in the history
  • Loading branch information
pi8027 committed Jun 8, 2023
1 parent 40637d5 commit 0baebd9
Showing 1 changed file with 64 additions and 0 deletions.
64 changes: 64 additions & 0 deletions theories/ssrZ.v
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,69 @@ case=> [[|n]|n] //=.
rewrite addnC /=; congr Negz; lia.
Qed.

Module NInstances.

(* 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).
(* 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=> //= n m; 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=> //= n m; 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 => // n m; 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.

Module Exports. HB.reexport. End Exports.

End NInstances.

Module ZInstances.

Implicit Types (m n : Z).
Expand Down Expand Up @@ -138,4 +201,5 @@ Module Exports. HB.reexport. End Exports.

End ZInstances.

Export NInstances.Exports.
Export ZInstances.Exports.

0 comments on commit 0baebd9

Please sign in to comment.