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_nf tactic. The process needs to be repeated since ring_nf 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_nf 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. We also use neg_one_zsmul in the forward direction to normalize (-1) • b to -b.

For the same reason (ℤ is itself an AddGroup), sub_eq_add_neg is applied once as a preprocessing step rather than being part of the main simp set: inside the loop it would also rewrite the subtractions that ring_nf reintroduces in ℤ scalars (e.g. k - n in (k - n) • a), and the two would undo each other forever. That cycle is harmless in goal mode, where fail_if_no_progress compares goal types, but rewriting a hypothesis allocates a fresh fvarId each round, which counts as progress, so add_group at h would never terminate. Preprocessing loses no proving power because nothing in the loop ever creates a new subtraction of group elements.

Other than this issue, the strategy parallels Thomas Browning and Patrick Massot's group tactic.

TODO

• Surface non-progress-related errors from repeat.
• Allow add_groups ifUnchanged behavior to be configurable.

Tags

group theory, additive group

def Mathlib.Tactic.AddGroup.addGroup : Lean.ParserDescr

add_group normalizes expressions in additive groups without assuming commutativity. Unlike abel, which does take advantage of commutativity, add_group instead only uses 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.

add_group at l1 l2 ... normalizes at the given locations.

For additive commutative groups, use the abel tactic instead. For multiplicative groups, use the group tactic instead.

Example:

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

Equations

• One or more equations did not get rendered due to their size.

We register add_group with the hint tactic.