From 3fc281be495ba00aae6b8f380fb734c43e94426a Mon Sep 17 00:00:00 2001 From: Ali Caglayan Date: Thu, 19 Sep 2024 11:33:35 +0200 Subject: [PATCH] add smart constructors for AbGroup and CRing, drop laws for Loc Signed-off-by: Ali Caglayan --- theories/Algebra/AbGroups/AbelianGroup.v | 22 +++++++ theories/Algebra/AbGroups/Z.v | 16 +++-- theories/Algebra/Rings/CRing.v | 20 +++--- theories/Algebra/Rings/Localization.v | 83 ++++-------------------- theories/Algebra/Rings/Z.v | 5 +- 5 files changed, 58 insertions(+), 88 deletions(-) diff --git a/theories/Algebra/AbGroups/AbelianGroup.v b/theories/Algebra/AbGroups/AbelianGroup.v index 5cd6a5d22ec..89b27f2e93e 100644 --- a/theories/Algebra/AbGroups/AbelianGroup.v +++ b/theories/Algebra/AbGroups/AbelianGroup.v @@ -29,6 +29,28 @@ Proof. split; exact _. Defined. +(** Easier way to build abelian groups without redundant information. *) +Definition Build_AbGroup' (G : Type) + `{Zero G, Negate G, Plus G, IsHSet G} + (comm : Commutative (A:=G) (+)) + (assoc : Associative (A:=G) (+)) + (unit_l : LeftIdentity (A:=G) (+) 0) + (inv_l : LeftInverse (A:=G) (+) (-) 0) + : AbGroup. +Proof. + snrapply Build_AbGroup. + - (* TODO: introduce smart constructor for [Build_Group] *) + rapply (Build_Group G). + repeat split; only 1-3, 5: exact _. + + intros x. + lhs nrapply comm. + exact (unit_l x). + + intros x. + lhs nrapply comm. + exact (inv_l x). + - exact comm. +Defined. + Definition issig_abgroup : _ <~> AbGroup := ltac:(issig). Global Instance zero_abgroup (A : AbGroup) : Zero A := group_unit. diff --git a/theories/Algebra/AbGroups/Z.v b/theories/Algebra/AbGroups/Z.v index c8a31d9eec2..2c9b32a525f 100644 --- a/theories/Algebra/AbGroups/Z.v +++ b/theories/Algebra/AbGroups/Z.v @@ -12,14 +12,16 @@ Local Open Scope int_scope. Definition abgroup_Z@{} : AbGroup@{Set}. Proof. - snrapply Build_AbGroup. - - refine (Build_Group Int int_add 0 int_neg _); repeat split. - + exact _. - + exact int_add_assoc. - + exact int_add_0_r. - + exact int_add_neg_l. - + exact int_add_neg_r. + snrapply Build_AbGroup'. + - exact Int. + - exact 0. + - exact int_neg. + - exact int_add. + - exact _. - exact int_add_comm. + - exact int_add_assoc. + - exact int_add_0_l. + - exact int_add_neg_l. Defined. (** For every group [G] and element [g : G], the map sending an integer to that power of [g] is a homomorphism. See [ab_mul] for the homomorphism [G -> G] when [G] is abelian. *) diff --git a/theories/Algebra/Rings/CRing.v b/theories/Algebra/Rings/CRing.v index a4f2ee3cd01..91fd19cd668 100644 --- a/theories/Algebra/Rings/CRing.v +++ b/theories/Algebra/Rings/CRing.v @@ -23,17 +23,21 @@ Global Instance cring_plus {R : CRing} : Plus R := plus_abgroup R. Global Instance cring_zero {R : CRing} : Zero R := zero_abgroup R. Global Instance cring_negate {R : CRing} : Negate R := negate_abgroup R. -Definition Build_CRing' (R : AbGroup) - `(!One R, !Mult R, !Commutative (.*.), !LeftDistribute (.*.) (+), @IsMonoid R (.*.) 1) +Definition Build_CRing' (R : AbGroup) `(!One R, !Mult R) + (comm : Commutative (.*.)) (assoc : Associative (.*.)) + (dist_l : LeftDistribute (.*.) (+)) (unit_l : LeftIdentity (.*.) 1) : CRing. Proof. snrapply Build_CRing. - - snrapply (Build_Ring R). - 1-3,5: exact _. - intros x y z. - lhs rapply commutativity. - lhs rapply simple_distribute_l. - f_ap. + - rapply (Build_Ring R); only 1: exact _. + 2: repeat split; only 1-3: exact _. + + intros x y z. + lhs nrapply comm. + lhs rapply dist_l. + f_ap. + + intros x. + lhs rapply comm. + apply unit_l. - exact _. Defined. diff --git a/theories/Algebra/Rings/Localization.v b/theories/Algebra/Rings/Localization.v index 0ff826727d5..957da4537ec 100644 --- a/theories/Algebra/Rings/Localization.v +++ b/theories/Algebra/Rings/Localization.v @@ -286,6 +286,17 @@ Section Localization. Defined. (** *** Ring laws *) + + (** Commutativity of addition *) + Instance commutative_plus_localization_type + : Commutative plus_localization_type. + Proof. + intros x; srapply Localization_type_ind_hprop; intros y; revert x. + srapply Localization_type_ind_hprop; intros x. + apply loc_frac_eq, fraction_eq_simple; simpl. + rewrite (rng_mult_comm (denominator y) (denominator x)). + f_ap; apply rng_plus_comm. + Defined. (** Left additive identity *) Instance leftidentity_plus_localization_type @@ -301,19 +312,6 @@ Section Localization. apply rng_mult_one_l. Defined. - Instance rightidentity_plus_localization_type - : RightIdentity plus_localization_type zero_localization_type. - Proof. - srapply Localization_type_ind_hprop; intros f. - apply loc_frac_eq, fraction_eq_simple; simpl. - f_ap. - - rewrite rng_mult_zero_l. - rewrite rng_plus_zero_r. - apply rng_mult_one_r. - - symmetry. - apply rng_mult_one_r. - Defined. - Instance leftinverse_plus_localization_type : LeftInverse plus_localization_type negate_localization_type zero_localization_type. Proof. @@ -325,17 +323,6 @@ Section Localization. apply rng_plus_negate_l. Defined. - Instance rightinverse_plus_localization_type - : RightInverse plus_localization_type negate_localization_type zero_localization_type. - Proof. - srapply Localization_type_ind_hprop; intros f. - apply loc_frac_eq, fraction_eq_simple; simpl. - refine (rng_mult_one_r _ @ _). - refine (_ @ (rng_mult_zero_l _)^). - rewrite rng_mult_negate_l. - apply rng_plus_negate_r. - Defined. - Instance associative_plus_localization_type : Associative plus_localization_type. Proof. @@ -355,16 +342,6 @@ Section Localization. apply rng_mult_comm. Defined. - Instance commutative_plus_localization_type - : Commutative plus_localization_type. - Proof. - intros x; srapply Localization_type_ind_hprop; intros y; revert x. - srapply Localization_type_ind_hprop; intros x. - apply loc_frac_eq, fraction_eq_simple; simpl. - rewrite (rng_mult_comm (denominator y) (denominator x)). - f_ap; apply rng_plus_comm. - Defined. - Instance leftidentity_mult_localization_type : LeftIdentity mult_localization_type one_localization_type. Proof. @@ -373,14 +350,6 @@ Section Localization. f_ap; [|symmetry]; apply rng_mult_one_l. Defined. - Instance rightidentity_mult_localization_type - : RightIdentity mult_localization_type one_localization_type. - Proof. - srapply Localization_type_ind_hprop; intros f. - apply loc_frac_eq, fraction_eq_simple; simpl. - f_ap; [|symmetry]; apply rng_mult_one_r. - Defined. - Instance associative_mult_localization_type : Associative mult_localization_type. Proof. @@ -422,35 +391,11 @@ Section Localization. all: f_ap. Defined. - Instance rightdistribute_localization_type - : RightDistribute mult_localization_type plus_localization_type. - Proof. - intros x y z. - rewrite 3 (commutative_mult_localization_type _ z). - snrapply leftdistribute_localization_type. - Defined. - - Instance isring_localization_type : IsRing Localization_type - := ltac:(repeat split; exact _). - Definition rng_localization : CRing. Proof. - snrapply Build_CRing. - { snrapply Build_Ring. - - snrapply Build_AbGroup. - + snrapply Build_Group. - * exact Localization_type. - * exact plus_localization_type. - * exact zero_localization_type. - * exact negate_localization_type. - * exact _. - + exact _. - - exact mult_localization_type. - - exact one_localization_type. - - exact leftdistribute_localization_type. - - exact rightdistribute_localization_type. - - exact _. } - exact _. + snrapply Build_CRing'. + 1: rapply (Build_AbGroup' Localization_type). + all: exact _. Defined. Definition loc_in : R $-> rng_localization. diff --git a/theories/Algebra/Rings/Z.v b/theories/Algebra/Rings/Z.v index 8f8c8a25098..0d9cf3b124b 100644 --- a/theories/Algebra/Rings/Z.v +++ b/theories/Algebra/Rings/Z.v @@ -10,16 +10,13 @@ Require Import WildCat.Core. Definition cring_Z : CRing. Proof. snrapply Build_CRing'. - 6: repeat split. - exact abgroup_Z. - exact 1%int. - exact int_mul. - exact int_mul_comm. - - exact int_dist_l. - - exact _. - exact int_mul_assoc. + - exact int_dist_l. - exact int_mul_1_l. - - exact int_mul_1_r. Defined. Local Open Scope mc_scope.