feat: add_group tactic

Mathlib/Tactic/AddGroup.lean

@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2020 Patrick Massot. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas Browning, Patrick Massot
+-/
+module
+
+public import Mathlib.Algebra.Order.Sub.Basic  -- shake: keep (tactic dependency)
+public meta import Mathlib.Tactic.FailIfNoProgress
+public import Mathlib.Tactic.Group  -- for zsmul_trick lemmas generated by @[to_additive]
+public import Mathlib.Tactic.Ring
+
+/-!
+# `add_group` tactic
+
+Normalizes expressions in the language of additive groups. The basic idea is to use the simplifier
+to put everything into a sum of integer scalar multiples (`zsmul` which takes an integer and an
+additive group element), then simplify the scalars using the `ring` tactic. The process needs to be
+repeated since `ring` can normalize a scalar to zero, leading to a summand that can be removed
+before collecting scalars again. The simplifier step also uses some extra lemmas to avoid
+some `ring` invocations.
+
+Note: Unlike the multiplicative `group` tactic which uses `← zpow_neg_one` to convert `a⁻¹` to
+`a ^ (-1 : ℤ)`, the additive version cannot use `← neg_one_zsmul` to convert `-a` to
+`(-1 : ℤ) • a` because `(-1 : ℤ)` is itself `-(1 : ℤ)`, causing simp to loop (since `ℤ` is also
+an `AddGroup`). Instead, we handle negation via `neg_add_rev` to distribute negation over sums,
+`zsmul_neg`/`neg_zsmul` for `n • (-a)`, and custom trick lemmas for combining `-b` with adjacent
+`zsmul` terms.
+
+## Tags
+
+group theory, additive group
+-/
+
+public meta section
+
+namespace Mathlib.Tactic.AddGroup
+
+open Lean
+open Lean.Meta
+open Lean.Parser.Tactic
+open Lean.Elab.Tactic
+
+-- The next three lemmas are not general purpose lemmas, they are intended for use only by
+-- the `add_group` tactic.
+-- They handle the case where a negated element `-b` appears adjacent to a `zsmul` of the same
+-- element, or adjacent to another negated copy.
+theorem zsmul_neg_trick {G : Type*} [AddGroup G] (a b : G) (n : ℤ) :
+    a + n • b + (-b) = a + (n + (-1)) • b := by
+  rw [add_assoc, ← neg_one_zsmul b, ← add_zsmul]
+
+theorem zsmul_neg_trick' {G : Type*} [AddGroup G] (a b : G) (n : ℤ) :
+    a + (-b) + n • b = a + ((-1) + n) • b := by
+  rw [add_assoc, ← neg_one_zsmul b, ← add_zsmul]
+
+theorem neg_neg_trick {G : Type*} [AddGroup G] (a b : G) :
+    a + (-b) + (-b) = a + (-2 : ℤ) • b := by
+  have h : -b = (-1 : ℤ) • b := (neg_one_zsmul b).symm
+  rw [h, add_assoc, ← add_zsmul]; norm_num
+
+/-- Auxiliary tactic for the `add_group` tactic. Calls the simplifier only. -/
+syntax (name := aux_add_group₁) "aux_add_group₁" (location)? : tactic
+
+macro_rules
+| `(tactic| aux_add_group₁ $[at $location]?) =>
+  `(tactic| simp -decide -failIfUnchanged only
+    [neg_add_rev, neg_zero, zsmul_neg, ← neg_zsmul,
+      add_zero, zero_add,
+      ← natCast_zsmul, ← mul_zsmul',
+      Int.natCast_add, Int.natCast_mul, neg_neg,
+      zsmul_zero, zero_zsmul, one_zsmul,
+      ← add_assoc,
+      ← add_zsmul, ← add_one_zsmul, ← one_add_zsmul,
+      Mathlib.Tactic.Group.zsmul_trick,
+      Mathlib.Tactic.Group.zsmul_trick_zero,
+      Mathlib.Tactic.Group.zsmul_trick_zero',
+      zsmul_neg_trick, zsmul_neg_trick',
+      add_neg_cancel_right, neg_add_cancel_right,
+      neg_neg_trick,
+      tsub_self, sub_self, add_neg_cancel, neg_add_cancel]
+  $[at $location]?)
+
+/-- Auxiliary tactic for the `add_group` tactic. Calls `ring_nf` to normalize scalars. -/
+syntax (name := aux_add_group₂) "aux_add_group₂" (location)? : tactic
+
+macro_rules
+| `(tactic| aux_add_group₂ $[at $location]?) =>
+  `(tactic| ring_nf -failIfUnchanged $[at $location]?)
+
+/-- `add_group` normalizes expressions in additive groups that occur in the goal. `add_group` does
+not assume commutativity, instead using only the additive group axioms without any information about
+which group is manipulated. If the goal is an equality, and after normalization the two sides are
+equal, `add_group` closes the goal.
+
+For multiplicative groups, use the `group` tactic instead.
+For additive commutative groups, use the `abel` tactic instead.
+
+* `add_group at l1 l2 ...` normalizes at the given locations.
+
+Example:
+```lean
+example {G : Type} [AddGroup G] (a b c d : G) (h : c = (a + 2 • b) + (-(b + b) + (-a)) + d) :
+    a + c + (-d) = a := by
+  add_group at h -- normalizes `h` which becomes `h : c = d`
+  rw [h]         -- the goal is now `a + d + (-d) = a`
+  add_group      -- which is then normalized and closed
+```
+-/
+syntax (name := add_group) "add_group" (location)? : tactic
+
+macro_rules
+| `(tactic| add_group $[$loc]?) =>
+  `(tactic| repeat (fail_if_no_progress (aux_add_group₁ $[$loc]? <;> aux_add_group₂ $[$loc]?)))
+
+end Mathlib.Tactic.AddGroup
+
+/-!
+We register `add_group` with the `hint` tactic.
+-/
+
+register_hint 900 add_group

MathlibTest/AddGroup.lean

@@ -0,0 +1,56 @@
+module
+import Mathlib.Tactic.AddGroup
+
+variable {G : Type} [AddGroup G]
+
+example (a b c : G) : c + (a + b) + (-b + -a) + c = c + c := by add_group
+
+example (a b c : G) : (b + -c) + c + (a + b) + (-b + -a) + c = b + c := by add_group
+
+example (a b c : G) : -c + (b + -c) + c + (a + b) + (-b + -a + -b) + c = 0 := by add_group
+
+-- NB the Hall-Witt identity is here in the Group.lean test, but this involves commutators
+-- which have no additive analogue, so this test was not additivised.
+
+example (a : G) : 2 • a + a = 3 • a := by add_group
+
+example (n m : ℕ) (a : G) : n • a + m • a = (n + m) • a := by add_group
+
+example (a b c : G) : c + (a + 2 • b) + (-(b + b) + -a) + c = c + c := by add_group
+
+example (n : ℕ) (a : G) : n • a + n • (-a) = 0 := by add_group
+
+example (a : G) : 2 • a + -a + -a = 0 := by add_group
+
+example (n m : ℕ) (a : G) : n • a + m • a = (m + n) • a := by add_group
+
+example (n : ℕ) (a : G) : (n - n) • a = 0 := by add_group
+
+example (n : ℤ) (a : G) : (n - n) • a = 0 := by add_group
+
+example (n : ℤ) (a : G) (h : (n * (n + 1) - n - n ^ 2) • a = a) : a = 0 := by
+  add_group at h
+  exact h.symm
+
+example (a b c d : G) (h : c = (a + 2 • b) + (-(b + b) + -a) + d) : a + c + -d = a := by
+  add_group at h
+  rw [h]
+  add_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) : (m - n) • a + (m - n) • b + (n - m) • b + (n - m) • a = 0 := by
+  add_group
+
+example (n : ℤ) (a b : G) :
+    n • a + n • b + n • a + n • a + (-n) • a + (-n) • a + (-n) • b + (-n) • a = 0 := by add_group
+
+-- Test that add_group deals with `-(0)` properly
+
+example (x y : G) : -((-x) + (x + y) + (-y)) = 0 := by add_group
+
+set_option linter.unusedTactic false in
+example (x : G) (h : x = 0) : x = 0 := by
+  add_group
+  exact h