add smart constructors for AbGroup and CRing, drop laws for Loc

Signed-off-by: Ali Caglayan <[email protected]>

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.

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

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.
 

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.

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.