refactor: split the group tactic into group and group_exp

Mathlib.lean

@@ -5043,6 +5043,7 @@ import Mathlib.Tactic.GCongr.ForwardAttr
 import Mathlib.Tactic.Generalize
 import Mathlib.Tactic.GeneralizeProofs
 import Mathlib.Tactic.Group
+import Mathlib.Tactic.GroupExp
 import Mathlib.Tactic.GuardGoalNums
 import Mathlib.Tactic.GuardHypNums
 import Mathlib.Tactic.Have

Mathlib/Data/Int/Defs.lean

@@ -46,6 +46,10 @@ protected lemma le_iff_lt_or_eq : a ≤ b ↔ a < b ∨ a = b := by rw [Int.le_i
 
 end Order
 
+-- We want to use these lemmas earlier than the lemmas simp can prove them with
+@[simp, nolint simpNF] protected alias add_neg_cancel := Int.add_right_neg
+@[simp, nolint simpNF] protected alias neg_add_cancel := Int.add_left_neg
+
 -- TODO: Tag in Lean
 attribute [simp] natAbs_pos
 

Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

@@ -8,6 +8,7 @@ import Mathlib.Data.ZMod.Aut
 import Mathlib.Data.ZMod.QuotientGroup
 import Mathlib.GroupTheory.SpecificGroups.Dihedral
 import Mathlib.GroupTheory.Subgroup.Simple
+import Mathlib.Tactic.GroupExp
 
 /-!
 # Cyclic groups
@@ -559,7 +560,7 @@ theorem commutative_of_cyclic_center_quotient [IsCyclic G'] (f : G →* G') (hf
     _ = y ^ m * (y ^ n * (y ^ (-m) * a)) * (y ^ (-n) * b) := by rw [mem_center_iff.1 ha]
     _ = y ^ m * y ^ n * y ^ (-m) * (a * (y ^ (-n) * b)) := by simp [mul_assoc]
     _ = y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a) := by rw [mem_center_iff.1 hb]
-    _ = b * a := by group
+    _ = b * a := by group_exp
 
 /-- A group is commutative if the quotient by the center is cyclic. -/
 @[to_additive

Mathlib/NumberTheory/LucasLehmer.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro, Kim Morrison, Ainsley Pahljina
 -/
 import Mathlib.RingTheory.Fintype
 import Mathlib.Tactic.NormNum
+import Mathlib.Tactic.Ring
 import Mathlib.Tactic.Zify
 
 /-!

Mathlib/Tactic.lean

@@ -108,6 +108,7 @@ import Mathlib.Tactic.GCongr.ForwardAttr
 import Mathlib.Tactic.Generalize
 import Mathlib.Tactic.GeneralizeProofs
 import Mathlib.Tactic.Group
+import Mathlib.Tactic.GroupExp
 import Mathlib.Tactic.GuardGoalNums
 import Mathlib.Tactic.GuardHypNums
 import Mathlib.Tactic.Have

Mathlib/Tactic/Group.lean

@@ -3,19 +3,19 @@ Copyright (c) 2020. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning, Patrick Massot
 -/
-import Mathlib.Tactic.Ring
 import Mathlib.Tactic.FailIfNoProgress
+import Mathlib.Algebra.Group.Basic
 import Mathlib.Algebra.Group.Commutator
 
 /-!
 # `group` tactic
 
 Normalizes expressions in the language of groups. The basic idea is to use the simplifier
 to put everything into a product of group powers (`zpow` which takes a group element and an
-integer), then simplify the exponents using the `ring` tactic. The process needs to be repeated
-since `ring` can normalize an exponent to zero, leading to a factor that can be removed
-before collecting exponents again. The simplifier step also uses some extra lemmas to avoid
-some `ring` invocations.
+integer), then simplify the exponents using a few carefully chosen `simp` lemmas.
+
+This is a cheaper version of the `group_exp` tactic that doesn't use `ring_nf` to normalize
+exponents.
 
 ## Tags
 
@@ -44,46 +44,23 @@ theorem zpow_trick_one' {G : Type*} [Group G] (a b : G) (n : ℤ) :
     a * b ^ n * b = a * b ^ (n + 1) := by rw [mul_assoc, mul_zpow_self]
 
 /-- Auxiliary tactic for the `group` tactic. Calls the simplifier only. -/
-syntax (name := aux_group₁) "aux_group₁" (location)? : tactic
+syntax (name := group) "group" (location)? : tactic
 
 macro_rules
-| `(tactic| aux_group₁ $[at $location]?) =>
+| `(tactic| group $[at $location]?) =>
   `(tactic| simp -decide -failIfUnchanged only
-    [commutatorElement_def, mul_one, one_mul,
+    [commutatorElement_def,
       ← zpow_neg_one, ← zpow_natCast, ← zpow_mul,
-      Int.ofNat_add, Int.ofNat_mul,
+      Int.ofNat_zero, Int.ofNat_add, Int.ofNat_mul,
       Int.mul_neg, Int.neg_mul, neg_neg,
       one_zpow, zpow_zero, zpow_one, mul_zpow_neg_one,
       ← mul_assoc,
       ← zpow_add, ← zpow_add_one, ← zpow_one_add, zpow_trick, zpow_trick_one, zpow_trick_one',
-      tsub_self, sub_self, add_neg_cancel, neg_add_cancel]
+      Nat.sub_self, Int.sub_self,
+      one_mul, Int.one_mul,
+      mul_one, Int.mul_one,
+      Int.add_neg_cancel,
+      Int.neg_add_cancel]
   $[at $location]?)
 
-/-- Auxiliary tactic for the `group` tactic. Calls `ring_nf` to normalize exponents. -/
-syntax (name := aux_group₂) "aux_group₂" (location)? : tactic
-
-macro_rules
-| `(tactic| aux_group₂ $[at $location]?) =>
-  `(tactic| ring_nf $[at $location]?)
-
-/-- Tactic for normalizing expressions in multiplicative groups, without assuming
-commutativity, using only the group axioms without any information about which group
-is manipulated.
-
-(For additive commutative groups, use the `abel` tactic instead.)
-
-Example:
-```lean
-example {G : Type} [Group G] (a b c d : G) (h : c = (a*b^2)*((b*b)⁻¹*a⁻¹)*d) : a*c*d⁻¹ = a := by
-  group at h -- normalizes `h` which becomes `h : c = d`
-  rw [h]     -- the goal is now `a*d*d⁻¹ = a`
-  group      -- which then normalized and closed
-```
--/
-syntax (name := group) "group" (location)? : tactic
-
-macro_rules
-| `(tactic| group $[$loc]?) =>
-  `(tactic| repeat (fail_if_no_progress (aux_group₁ $[$loc]? <;> aux_group₂ $[$loc]?)))
-
 end Mathlib.Tactic.Group

Mathlib/Tactic/GroupExp.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2020. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas Browning, Patrick Massot
+-/
+import Mathlib.Tactic.Group
+import Mathlib.Tactic.Ring
+
+/-!
+# `group_exp` tactic
+
+Normalizes expressions in the language of groups. The basic idea is to use the simplifier
+to put everything into a product of group powers (`zpow` which takes a group element and an
+integer), then simplify the exponents using the `ring` tactic. The process needs to be repeated
+since `ring` can normalize an exponent to zero, leading to a factor that can be removed
+before collecting exponents again. The simplifier step also uses some extra lemmas to avoid
+some `ring` invocations.
+
+## Tags
+
+group theory
+-/
+
+namespace Mathlib.Tactic.Group
+open Lean Meta Parser.Tactic Elab.Tactic
+
+/-- Tactic for normalizing expressions in multiplicative groups, without assuming
+commutativity, using only the group axioms without any information about which group
+is manipulated.
+
+(For additive commutative groups, use the `abel` tactic instead.)
+
+Example:
+```lean
+example {G : Type} [Group G] (a b c d : G) (h : c = (a*b^2)*((b*b)⁻¹*a⁻¹)*d) : a*c*d⁻¹ = a := by
+  group at h -- normalizes `h` which becomes `h : c = d`
+  rw [h]     -- the goal is now `a*d*d⁻¹ = a`
+  group      -- which then normalized and closed
+```
+-/
+syntax (name := group_exp) "group_exp" (location)? : tactic
+
+macro_rules
+| `(tactic| group_exp $[$loc]?) =>
+  `(tactic| repeat (fail_if_no_progress (group $[$loc]? <;> ring_nf $[$loc]?)))
+
+end Mathlib.Tactic.Group

MathlibTest/Group.lean

@@ -13,38 +13,14 @@ example (a b c : G) : c⁻¹*(b*c⁻¹)*c*(a*b)*(b⁻¹*a⁻¹*b⁻¹)*c = 1 :=
 -- https://en.wikipedia.org/wiki/Three_subgroups_lemma#Proof_and_the_Hall%E2%80%93Witt_identity
 example (g h k : G) : g*⁅⁅g⁻¹,h⁆,k⁆*g⁻¹*k*⁅⁅k⁻¹,g⁆,h⁆*k⁻¹*h*⁅⁅h⁻¹,k⁆,g⁆*h⁻¹ = 1 := by group
 
-example (a : G) : a^2*a = a^3 := by group
-
 example (n m : ℕ) (a : G) : a^n*a^m = a^(n+m) := by group
 
-example (a b c : G) : c*(a*b^2)*((b*b)⁻¹*a⁻¹)*c = c*c := by group
-
 example (n : ℕ) (a : G) : a^n*(a⁻¹)^n = 1 := by group
 
-example (a : G) : a^2*a⁻¹*a⁻¹ = 1 := by group
-
-example (n m : ℕ) (a : G) : a^n*a^m = a^(m+n) := by group
-
 example (n : ℕ) (a : G) : a^(n-n) = 1 := by group
 
 example (n : ℤ) (a : G) : a^(n-n) = 1 := by group
 
-example (n : ℤ) (a : G) (h : a^(n*(n+1)-n-n^2) = a) : a = 1 := by
-  group at h
-  exact h.symm
-
-example (a b c d : G) (h : c = (a*b^2)*((b*b)⁻¹*a⁻¹)*d) : a*c*d⁻¹ = a := by
-  group at h
-  rw [h]
-  group
-
--- The next example can be expanded to require an arbitrarily high number of alternations
--- between simp and ring
-
-example (n m : ℤ) (a b : G) : a^(m-n)*b^(m-n)*b^(n-m)*a^(n-m) = 1 := by group
-
-example (n : ℤ) (a b : G) : a^n*b^n*a^n*a^n*a^(-n)*a^(-n)*b^(-n)*a^(-n) = 1 := by group
-
 -- Test that group deals with `1⁻¹` properly
 
 example (x y : G) : (x⁻¹ * (x * y) * y⁻¹)⁻¹ = 1 := by group

MathlibTest/GroupExp.lean

@@ -0,0 +1,27 @@
+import Mathlib.Tactic.GroupExp
+
+variable {G : Type} [Group G]
+
+example (a : G) : a^2*a = a^3 := by group_exp
+
+example (a b c : G) : c*(a*b^2)*((b*b)⁻¹*a⁻¹)*c = c*c := by group_exp
+
+example (a : G) : a^2*a⁻¹*a⁻¹ = 1 := by group_exp
+
+example (n m : ℕ) (a : G) : a^n*a^m = a^(m+n) := by group_exp
+
+example (n : ℤ) (a : G) (h : a^(n*(n+1)-n-n^2) = a) : a = 1 := by
+  group_exp at h
+  exact h.symm
+
+example (a b c d : G) (h : c = (a*b^2)*((b*b)⁻¹*a⁻¹)*d) : a*c*d⁻¹ = a := by
+  group_exp at h
+  rw [h]
+  group_exp
+
+-- The next example can be expanded to require an arbitrarily high number of alternations
+-- between simp and ring
+
+example (n m : ℤ) (a b : G) : a^(m-n)*b^(m-n)*b^(n-m)*a^(n-m) = 1 := by group_exp
+
+example (n : ℤ) (a b : G) : a^n*b^n*a^n*a^n*a^(-n)*a^(-n)*b^(-n)*a^(-n) = 1 := by group_exp

scripts/noshake.json

@@ -105,6 +105,7 @@
   "Mathlib.Tactic.Generalize",
   "Mathlib.Tactic.GeneralizeProofs",
   "Mathlib.Tactic.Group",
+  "Mathlib.Tactic.GroupExp",
   "Mathlib.Tactic.GuardHypNums",
   "Mathlib.Tactic.HaveI",
   "Mathlib.Tactic.Hint",