Commit 2024-09-25 08:58 7c93f866

View on Github →

feat: match_scalars and module tactics (#16593) This PR contributes two new tactics match_scalars and module. Given a goal which is an equality in a type M (with M an AddCommMonoid), the match_scalars tactic parses the LHS and RHS of the goal as linear combinations of M-atoms over some semiring R, and reduces the goal to the respective equalities of the R-coefficients of each atom. For example, this produces the goal ⊢ a * 1 + b * 1 = (b + a) * 1:

example [AddCommMonoid M] [Semiring R] [Module R M] (a b : R) (x : M) :
    a • x + b • x = (b + a) • x := by
  match_scalars

This produces the two goals ⊢ a * (a * 1) + b * (b * 1) = 1 (from the x atom) and ⊢ a * -(b * 1) + b * (a * 1) = 0 (from the y atom):

example [AddCommGroup M] [Ring R] [Module R M] (a b : R) (x : M) :
    a • (a • x - b • y) + (b • a • y + b • b • x) = x := by
  match_scalars

The module tactic runs the match_scalars tactic and then runs the ring tactic on each of the coefficient-wise equalities which are created, failing if this does not resolve them. For example, it solves the following goals:

example [AddCommMonoid M] [CommSemiring R] [Module R M] (a b : R) (x : M) :
    a • x + b • x = (b + a) • x := by
  module
example [AddCommMonoid M] [Field K] [CharZero K] [Module K M] (x : M) :
    (2:K)⁻¹ • x + (3:K)⁻¹ • x + (6:K)⁻¹ • x = x := by
  module
example [AddCommGroup M] [CommRing R] [Module R M] (a : R) (v w : M) :
    (1 + a ^ 2) • (v + w) - a • (a • v - w) = v + (1 + a + a ^ 2) • w := by
  module

The scalar type R in these tactics is not pre-determined: instead it starts as ℕ (when each atom is initially given a scalar (1:ℕ)) and gets bumped up into bigger semirings when such semirings are encountered. However, to permit this, it is assumed that there is a "linear order" on all the semirings which appear in the expression: for any two semirings R and S which occur, we have either Algebra R S or Algebra S R).

Estimated changes