Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

N forms a semiring #47

Merged
merged 4 commits into from
Jul 3, 2023
Merged

N forms a semiring #47

Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
f8f3070
`N` forms a semiring
pi8027 Jun 8, 2023
1cecf59
More zify instances for nat and N
pi8027 Jun 8, 2023
1778402
Test cases
pi8027 Jul 3, 2023
2131f25
Move some declarations
pi8027 Jul 3, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
110 changes: 106 additions & 4 deletions theories/ssrZ.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,64 @@ 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).
(* 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.
Copy link
Member Author

@pi8027 pi8027 Jun 8, 2023 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just a remark: The commutative ring instance for Z below uses Zmult_plus_distr_*l* but here I use Nmult_plus_distr_*r*. Naming inconsistency in the Coq standard library :/


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).

Expand Down Expand Up @@ -121,7 +178,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
Expand All @@ -134,8 +191,53 @@ 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.

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.

Module Exports. HB.reexport. End Exports.

End ZInstances.
End Instances.

Export Instances.Exports.

Export ZInstances.Exports.
Lemma natn n : n%:R%R = n :> nat.
Proof. by elim: n => // n; rewrite mulrS => ->. Qed.
pi8027 marked this conversation as resolved.
Show resolved Hide resolved