Algebra/*: Use int_iter for grp_pow

theories/Algebra/AbGroups/AbelianGroup.v

@@ -228,6 +228,20 @@ Proof.
     1-2: exact negate_involutive.
 Defined.
 
+(** This goal comes up twice in the proof of [ab_mul], so we factor it out. *)
+Local Definition ab_mul_helper {A : AbGroup} (a b x y z : A)
+  (p : x = y + z)
+  : a + b + x = a + y + (b + z).
+Proof.
+  lhs_V srapply grp_assoc.
+  rhs_V srapply grp_assoc.
+  apply grp_cancelL.
+  rhs srapply grp_assoc.
+  rhs nrapply (ap (fun g => g + z) (ab_comm y b)).
+  rhs_V srapply grp_assoc.
+  apply grp_cancelL, p.
+Defined.
+
 (** Multiplication by [n : Int] defines an endomorphism of any abelian group [A]. *)
 Definition ab_mul {A : AbGroup} (n : Int) : GroupHomomorphism A A.
 Proof.
@@ -236,26 +250,11 @@ Proof.
   intros a b.
   induction n; cbn.
   - exact (grp_unit_l _)^.
-  - destruct n.
-    + reflexivity.
-    + rhs_V srapply (associativity a).
-      rhs srapply (ap _ (associativity _ b _)).
-      rewrite (commutativity (nat_iter _ _ _) b).
-      rhs_V srapply (ap _ (associativity b _ _)).
-      rhs srapply (associativity a).
-      apply grp_cancelL.
-      exact IHn.
-  - destruct n.
-    + rewrite (commutativity (-a)).
-      exact (grp_inv_op a b).
-    + rhs_V srapply (associativity (-a)).
-      rhs srapply (ap _ (associativity _ (-b) _)).
-      rewrite (commutativity (nat_iter _ _ _) (-b)).
-      rhs_V srapply (ap _ (associativity (-b) _ _)).
-      rhs srapply (associativity (-a)).
-      rewrite (commutativity (-a) (-b)), <- (grp_inv_op a b).
-      apply grp_cancelL.
-      exact IHn.
+  - rewrite 3 grp_pow_int_add_1.
+    by apply ab_mul_helper.
+  - rewrite 3 grp_pow_int_sub_1.
+    rewrite (grp_inv_op a b), (commutativity (-b) (-a)).
+    by apply ab_mul_helper.
 Defined.
 
 (** [ab_mul n] is natural. *)

theories/Algebra/Groups/Group.v

@@ -478,98 +478,61 @@ End GroupMovement.
 
 (** For a given [g : G] we can define the function [Int -> G] sending an integer to that power of [g]. *)
 Definition grp_pow {G : Group} (g : G) (n : Int) : G
-  := match n with
-     | posS n => nat_iter n (g *.) g
-     | zero => mon_unit
-     | negS n => nat_iter n ((- g) *.) (- g)
-     end.
+  := int_iter (g *.) n mon_unit.
 
 (** Any homomorphism respects [grp_pow]. In other words, [fun g => grp_pow g n] is natural. *)
 Lemma grp_pow_natural {G H : Group} (f : GroupHomomorphism G H) (n : Int) (g : G)
   : f (grp_pow g n) = grp_pow (f g) n.
 Proof.
-  induction n.
-  - apply grp_homo_unit.
-  - destruct n; simpl in IHn |- *.
-    + reflexivity.
-    + lhs snrapply grp_homo_op.
-      apply ap.
-      exact IHn.
-  - destruct n; simpl in IHn |- *.
-    + apply grp_homo_inv.
-    + lhs snrapply grp_homo_op.
-      apply ap011.
-      * apply grp_homo_inv.
-      * exact IHn.
+  lhs snrapply (int_iter_commute_map _ ((f g) *.)).
+  1: nrapply grp_homo_op.
+  apply (ap (int_iter _ n)), grp_homo_unit.
 Defined.
 
 (** All powers of the unit are the unit. *)
 Definition grp_pow_unit {G : Group} (n : Int)
   : grp_pow (G:=G) mon_unit n = mon_unit.
 Proof.
-  induction n.
+  snrapply (int_iter_invariant n _ (fun g => g = mon_unit)); cbn.
+  1, 2: apply paths_ind_r.
+  - apply grp_unit_r.
+  - lhs nrapply grp_unit_r. apply grp_inv_unit.
   - reflexivity.
-  - destruct n; simpl. 
-    + reflexivity.
-    + by lhs nrapply grp_unit_l.
-  - destruct n; simpl in IHn |- *.
-    + apply grp_inv_unit.
-    + destruct IHn^.
-      rhs_V apply (@grp_inv_unit G).
-      apply grp_unit_r.
 Defined.
 
 (** Note that powers don't preserve the group operation as it is not commutative. This does hold in an abelian group so such a result will appear later. *)
 
-(** Helper functions for [grp_pow_int_add]. This is how we can unfold [grp_pow] once. *)
-
+(** The next two results tell us how [grp_pow] unfolds. *)
 Definition grp_pow_int_add_1 {G : Group} (n : Int) (g : G)
-  : grp_pow g (n.+1)%int = g * grp_pow g n.
-Proof.
-  induction n; simpl.
-  - exact (grp_unit_r g)^.
-  - destruct n; reflexivity.
-  - destruct n.
-    + apply (grp_inv_r g)^.
-    + rhs srapply associativity.
-      rewrite grp_inv_r. 
-      apply (grp_unit_l _)^.
-Defined.
+  : grp_pow g (n.+1)%int = g * grp_pow g n
+  := int_iter_succ_l _ _ _.
 
 Definition grp_pow_int_sub_1 {G : Group} (n : Int) (g : G)
-  : grp_pow g (n.-1)%int = (- g) * grp_pow g n.
-Proof.
-  induction n; simpl.
-  - exact (grp_unit_r (-g))^.
-  - destruct n.
-    + apply (grp_inv_l g)^.
-    + rhs srapply associativity.
-      rewrite grp_inv_l.
-      apply (grp_unit_l _)^.
-  - destruct n; reflexivity.
-Defined.
+  : grp_pow g (n.-1)%int = (- g) * grp_pow g n
+  := int_iter_pred_l _ _ _.
 
 (** [grp_pow] commutes negative exponents to powers of the inverse *)
 Definition grp_pow_int_sign_commute {G : Group} (n : Int) (g : G)
   : grp_pow g (int_neg n) = grp_pow (- g) n.
 Proof.
-  induction n.
+  lhs nrapply int_iter_neg.
+  destruct n.
+  - cbn. by rewrite grp_inv_inv.
+  - reflexivity.
   - reflexivity.
-  - destruct n; reflexivity.
-  - destruct n; simpl; rewrite grp_inv_inv; reflexivity.
 Defined.
 
 (** [grp_pow] satisfies an additive law of exponents. *)
 Definition grp_pow_int_add {G : Group} (m n : Int) (g : G)
   : grp_pow g (n + m)%int = grp_pow g n * grp_pow g m.
 Proof.
+  lhs nrapply int_iter_add.
   induction n; cbn.
   1: exact (grp_unit_l _)^.
-  1: rewrite int_add_succ_l, 2 grp_pow_int_add_1.
-  2: rewrite int_add_pred_l, 2 grp_pow_int_sub_1.
-  1,2: rhs_V srapply associativity; 
-       snrapply (ap (_ *.));
-       exact IHn.
+  1: rewrite int_iter_succ_l, grp_pow_int_add_1.
+  2: rewrite int_iter_pred_l, grp_pow_int_sub_1; cbn.
+  1,2 : rhs_V srapply associativity;
+        apply ap, IHn.
 Defined.
 
 (** ** The category of Groups *)

theories/Algebra/Rings/Z.v

@@ -32,7 +32,7 @@ Global Instance issemigrouppreserving_mult_rng_int_mult (R : Ring)
   : IsSemiGroupPreserving (A:=cring_Z) (Aop:=(.*.)) (Bop:=(.*.)) (rng_int_mult R 1).
 Proof.
   intros x y.
-  cbn.
+  cbn; unfold sg_op.
   induction x as [|x|x].
   - simpl.
     by rhs nrapply rng_mult_zero_l.
@@ -59,6 +59,7 @@ Proof.
   1: exact (rng_int_mult R 1).
   repeat split.
   1,2: exact _.
+  apply rng_plus_zero_r.
 Defined.
 
 (** The integers are the initial commutative ring *)

theories/Spaces/Int.v

@@ -634,6 +634,22 @@ Proof.
     apply eisretr.
 Defined.
 
+Definition int_iter_invariant (n : Int) {A} (f : A -> A) `{!IsEquiv f}
+  (P : A -> Type)
+  (Psucc : forall x, P x -> P (f x))
+  (Ppred : forall x, P x -> P (f^-1 x))
+  : forall x, P x -> P (int_iter f n x).
+Proof.
+  induction n as [|n IHn|n IHn]; intro x.
+  - exact idmap.
+  - intro H.
+    rewrite int_iter_succ_l.
+    apply Psucc, IHn, H.
+  - intro H.
+    rewrite int_iter_pred_l.
+    apply Ppred, IHn, H.
+Defined.
+
 (** ** Exponentiation of loops *)
 
 Definition loopexp {A : Type} {x : A} (p : x = x) (z : Int) : (x = x)