A tactic for normalization over modules

This file provides the two 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. The module tactic does this and then runs the ring tactic on each of these coefficient-wise equalities, failing if this does not resolve them.

The scalar type R 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).

Theory of lists of pairs (scalar, vector)

This section contains the lemmas which are orchestrated by the match_scalars and module tactics to prove goals in modules. The basic object which these lemmas concern is NF R M, a type synonym for a list of ordered pairs in R × M, where typically M is an R-module.

def Mathlib.Tactic.Module.NF (R : Type u_1) (M : Type u_2) : Type (max u_2 u_1)

Basic theoretical "normal form" object of the match_scalars and module tactics: a type synonym for a list of ordered pairs in R × M, where typically M is an R-module. This is the form to which the tactics reduce module expressions.

(It is not a full "normal form" because the scalars, i.e. R components, are not themselves ring-normalized. But this partial normal form is more convenient for our purposes.)

Equations

• Mathlib.Tactic.Module.NF R M = List (R × M)

@[match_pattern]

def Mathlib.Tactic.Module.NF.cons {R : Type u_2} {M : Type u_3} (p : R × M) (l : Mathlib.Tactic.Module.NF R M) : Mathlib.Tactic.Module.NF R M

Augment a Module.NF R M object l, i.e. a list of pairs in R × M, by prepending another pair p : R × M.

Equations

• p ::ᵣ l = p :: l

def Mathlib.Tactic.Module.NF.«term_::ᵣ_» : Lean.TrailingParserDescr

Augment a Module.NF R M object l, i.e. a list of pairs in R × M, by prepending another pair p : R × M.

Equations

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

def Mathlib.Tactic.Module.NF.eval {R : Type u_2} {M : Type u_3} [Add M] [Zero M] [SMul R M] (l : Mathlib.Tactic.Module.NF R M) : M

Evaluate a Module.NF R M object l, i.e. a list of pairs in R × M, to an element of M, by forming the "linear combination" it specifies: scalar-multiply each R term to the corresponding M term, then add them all up.

Equations

• l.eval = (List.map (fun (x : R × M) => match x with | (r, x) => r • x) l).sum

@[simp]

theorem Mathlib.Tactic.Module.NF.eval_cons {R : Type u_2} {M : Type u_3} [AddMonoid M] [SMul R M] (p : R × M) (l : Mathlib.Tactic.Module.NF R M) : (p ::ᵣ l).eval = p.1 • p.2 + l.eval

theorem Mathlib.Tactic.Module.NF.atom_eq_eval {M : Type u_3} [AddMonoid M] (x : M) : x = Mathlib.Tactic.Module.NF.eval [(1, x)]

theorem Mathlib.Tactic.Module.NF.zero_eq_eval (M : Type u_3) [AddMonoid M] : 0 = Mathlib.Tactic.Module.NF.eval []

theorem Mathlib.Tactic.Module.NF.add_eq_eval₁ {R : Type u_2} {M : Type u_3} [AddMonoid M] [SMul R M] (a₁ : R × M) {a₂ : R × M} {l₁ : Mathlib.Tactic.Module.NF R M} {l₂ : Mathlib.Tactic.Module.NF R M} {l : Mathlib.Tactic.Module.NF R M} (h : l₁.eval + (a₂ ::ᵣ l₂).eval = l.eval) : (a₁ ::ᵣ l₁).eval + (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval

theorem Mathlib.Tactic.Module.NF.add_eq_eval₂ {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (r₁ : R) (r₂ : R) (x : M) {l₁ : Mathlib.Tactic.Module.NF R M} {l₂ : Mathlib.Tactic.Module.NF R M} {l : Mathlib.Tactic.Module.NF R M} (h : l₁.eval + l₂.eval = l.eval) : ((r₁, x) ::ᵣ l₁).eval + ((r₂, x) ::ᵣ l₂).eval = ((r₁ + r₂, x) ::ᵣ l).eval

theorem Mathlib.Tactic.Module.NF.add_eq_eval₃ {R : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {a₁ : R × M} (a₂ : R × M) {l₁ : Mathlib.Tactic.Module.NF R M} {l₂ : Mathlib.Tactic.Module.NF R M} {l : Mathlib.Tactic.Module.NF R M} (h : (a₁ ::ᵣ l₁).eval + l₂.eval = l.eval) : (a₁ ::ᵣ l₁).eval + (a₂ ::ᵣ l₂).eval = (a₂ ::ᵣ l).eval

theorem Mathlib.Tactic.Module.NF.add_eq_eval {R : Type u_2} {M : Type u_3} {R₁ : Type u_4} {R₂ : Type u_5} [AddCommMonoid M] [Semiring R] [Module R M] [Semiring R₁] [Module R₁ M] [Semiring R₂] [Module R₂ M] {l₁ : Mathlib.Tactic.Module.NF R M} {l₂ : Mathlib.Tactic.Module.NF R M} {l : Mathlib.Tactic.Module.NF R M} {l₁' : Mathlib.Tactic.Module.NF R₁ M} {l₂' : Mathlib.Tactic.Module.NF R₂ M} {x₁ : M} {x₂ : M} (hx₁ : x₁ = l₁'.eval) (hx₂ : x₂ = l₂'.eval) (h₁ : l₁.eval = l₁'.eval) (h₂ : l₂.eval = l₂'.eval) (h : l₁.eval + l₂.eval = l.eval) : x₁ + x₂ = l.eval

theorem Mathlib.Tactic.Module.NF.sub_eq_eval₁ {R : Type u_2} {M : Type u_3} [SMul R M] [AddGroup M] (a₁ : R × M) {a₂ : R × M} {l₁ : Mathlib.Tactic.Module.NF R M} {l₂ : Mathlib.Tactic.Module.NF R M} {l : Mathlib.Tactic.Module.NF R M} (h : l₁.eval - (a₂ ::ᵣ l₂).eval = l.eval) : (a₁ ::ᵣ l₁).eval - (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval

theorem Mathlib.Tactic.Module.NF.sub_eq_eval₂ {R : Type u_2} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] (r₁ : R) (r₂ : R) (x : M) {l₁ : Mathlib.Tactic.Module.NF R M} {l₂ : Mathlib.Tactic.Module.NF R M} {l : Mathlib.Tactic.Module.NF R M} (h : l₁.eval - l₂.eval = l.eval) : ((r₁, x) ::ᵣ l₁).eval - ((r₂, x) ::ᵣ l₂).eval = ((r₁ - r₂, x) ::ᵣ l).eval

theorem Mathlib.Tactic.Module.NF.sub_eq_eval₃ {R : Type u_2} {M : Type u_3} [Ring R] [AddCommGroup M] [Module R M] {a₁ : R × M} (a₂ : R × M) {l₁ : Mathlib.Tactic.Module.NF R M} {l₂ : Mathlib.Tactic.Module.NF R M} {l : Mathlib.Tactic.Module.NF R M} (h : (a₁ ::ᵣ l₁).eval - l₂.eval = l.eval) : (a₁ ::ᵣ l₁).eval - (a₂ ::ᵣ l₂).eval = ((-a₂.1, a₂.2) ::ᵣ l).eval

theorem Mathlib.Tactic.Module.NF.sub_eq_eval {R : Type u_2} {M : Type u_3} {R₁ : Type u_4} {R₂ : Type u_5} {S₁ : Type u_6} {S₂ : Type u_7} [AddCommGroup M] [Ring R] [Module R M] [Semiring R₁] [Module R₁ M] [Semiring R₂] [Module R₂ M] [Semiring S₁] [Module S₁ M] [Semiring S₂] [Module S₂ M] {l₁ : Mathlib.Tactic.Module.NF R M} {l₂ : Mathlib.Tactic.Module.NF R M} {l : Mathlib.Tactic.Module.NF R M} {l₁' : Mathlib.Tactic.Module.NF R₁ M} {l₂' : Mathlib.Tactic.Module.NF R₂ M} {l₁'' : Mathlib.Tactic.Module.NF S₁ M} {l₂'' : Mathlib.Tactic.Module.NF S₂ M} {x₁ : M} {x₂ : M} (hx₁ : x₁ = l₁''.eval) (hx₂ : x₂ = l₂''.eval) (h₁' : l₁'.eval = l₁''.eval) (h₂' : l₂'.eval = l₂''.eval) (h₁ : l₁.eval = l₁'.eval) (h₂ : l₂.eval = l₂'.eval) (h : l₁.eval - l₂.eval = l.eval) : x₁ - x₂ = l.eval

instance Mathlib.Tactic.Module.NF.instNeg {R : Type u_2} {M : Type u_3} [Neg R] : Neg (Mathlib.Tactic.Module.NF R M)

Equations

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

theorem Mathlib.Tactic.Module.NF.eval_neg {R : Type u_2} {M : Type u_3} [AddCommGroup M] [Ring R] [Module R M] (l : Mathlib.Tactic.Module.NF R M) : (-l).eval = -l.eval

theorem Mathlib.Tactic.Module.NF.zero_sub_eq_eval {R : Type u_2} {M : Type u_3} [AddCommGroup M] [Ring R] [Module R M] (l : Mathlib.Tactic.Module.NF R M) : 0 - l.eval = (-l).eval

theorem Mathlib.Tactic.Module.NF.neg_eq_eval {S : Type u_1} {R : Type u_2} {M : Type u_3} [AddCommGroup M] [Semiring S] [Module S M] [Ring R] [Module R M] {l : Mathlib.Tactic.Module.NF R M} {l₀ : Mathlib.Tactic.Module.NF S M} (hl : l.eval = l₀.eval) {x : M} (h : x = l₀.eval) : -x = (-l).eval

instance Mathlib.Tactic.Module.NF.instSMulOfMul {R : Type u_2} {M : Type u_3} [Mul R] : SMul R (Mathlib.Tactic.Module.NF R M)

Equations

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

@[simp]

theorem Mathlib.Tactic.Module.NF.smul_apply {R : Type u_2} {M : Type u_3} [Mul R] (r : R) (l : Mathlib.Tactic.Module.NF R M) : r • l = List.map (fun (x : R × M) => match x with | (a, x) => (r * a, x)) l

theorem Mathlib.Tactic.Module.NF.eval_smul {R : Type u_2} {M : Type u_3} [AddCommMonoid M] [Semiring R] [Module R M] {l : Mathlib.Tactic.Module.NF R M} {x : M} (h : x = l.eval) (r : R) : (r • l).eval = r • x

theorem Mathlib.Tactic.Module.NF.smul_eq_eval {S : Type u_1} {R : Type u_2} {M : Type u_3} {R₀ : Type u_4} [AddCommMonoid M] [Semiring R] [Module R M] [Semiring R₀] [Module R₀ M] [Semiring S] [Module S M] {l : Mathlib.Tactic.Module.NF R M} {l₀ : Mathlib.Tactic.Module.NF R₀ M} {s : S} {r : R} {x : M} (hx : x = l₀.eval) (hl : l.eval = l₀.eval) (hs : r • x = s • x) : s • x = (r • l).eval

theorem Mathlib.Tactic.Module.NF.eq_cons_cons {R : Type u_2} {M : Type u_3} [AddMonoid M] [SMul R M] {r₁ : R} {r₂ : R} (m : M) {l₁ : Mathlib.Tactic.Module.NF R M} {l₂ : Mathlib.Tactic.Module.NF R M} (h1 : r₁ = r₂) (h2 : l₁.eval = l₂.eval) : ((r₁, m) ::ᵣ l₁).eval = ((r₂, m) ::ᵣ l₂).eval

theorem Mathlib.Tactic.Module.NF.eq_cons_const {R : Type u_2} {M : Type u_3} [AddCommMonoid M] [Semiring R] [Module R M] {r : R} (m : M) {n : M} {l : Mathlib.Tactic.Module.NF R M} (h1 : r = 0) (h2 : l.eval = n) : ((r, m) ::ᵣ l).eval = n

theorem Mathlib.Tactic.Module.NF.eq_const_cons {R : Type u_2} {M : Type u_3} [AddCommMonoid M] [Semiring R] [Module R M] {r : R} (m : M) {n : M} {l : Mathlib.Tactic.Module.NF R M} (h1 : 0 = r) (h2 : n = l.eval) : n = ((r, m) ::ᵣ l).eval

theorem Mathlib.Tactic.Module.NF.eq_of_eval_eq_eval {R : Type u_2} {M : Type u_3} {R₁ : Type u_4} {R₂ : Type u_5} [AddCommMonoid M] [Semiring R] [Module R M] [Semiring R₁] [Module R₁ M] [Semiring R₂] [Module R₂ M] {l₁ : Mathlib.Tactic.Module.NF R M} {l₂ : Mathlib.Tactic.Module.NF R M} {l₁' : Mathlib.Tactic.Module.NF R₁ M} {l₂' : Mathlib.Tactic.Module.NF R₂ M} {x₁ : M} {x₂ : M} (hx₁ : x₁ = l₁'.eval) (hx₂ : x₂ = l₂'.eval) (h₁ : l₁.eval = l₁'.eval) (h₂ : l₂.eval = l₂'.eval) (h : l₁.eval = l₂.eval) : x₁ = x₂

def Mathlib.Tactic.Module.NF.algebraMap {S : Type u_1} (R : Type u_2) {M : Type u_3} [CommSemiring S] [Semiring R] [Algebra S R] (l : Mathlib.Tactic.Module.NF S M) : Mathlib.Tactic.Module.NF R M

Operate on a Module.NF S M object l, i.e. a list of pairs in S × M, where S is some commutative semiring, by applying to each S-component the algebra-map from S into a specified S-algebra R.

Equations

• Mathlib.Tactic.Module.NF.algebraMap R l = List.map (fun (x : S × M) => match x with | (s, x) => ((algebraMap S R) s, x)) l

theorem Mathlib.Tactic.Module.NF.eval_algebraMap {S : Type u_1} (R : Type u_2) {M : Type u_3} [CommSemiring S] [Semiring R] [Algebra S R] [AddMonoid M] [SMul S M] [MulAction R M] [IsScalarTower S R M] (l : Mathlib.Tactic.Module.NF S M) : (Mathlib.Tactic.Module.NF.algebraMap R l).eval = l.eval

Lists of expressions representing scalars and vectors, and operations on such lists

@[reducible, inline]

abbrev Mathlib.Tactic.Module.qNF {u : Lean.Level} {v : Lean.Level} (R : Q(Type u)) (M : Q(Type v)) : Type

Basic meta-code "normal form" object of the match_scalars and module tactics: a type synonym for a list of ordered triples comprising expressions representing terms of two types R and M (where typically M is an R-module), together with a natural number "index".

The natural number represents the index of the M term in the AtomM monad: this is not enforced, but is sometimes assumed in operations. Thus when items ((a₁, x₁), k) and ((a₂, x₂), k) appear in two different Module.qNF objects (i.e. with the same ℕ-index k), it is expected that the expressions x₁ and x₂ are the same. It is also expected that the items in a Module.qNF list are in strictly increasing order by natural-number index.

By forgetting the natural number indices, an expression representing a Mathlib.Tactic.Module.NF object can be built from a Module.qNF object; this construction is provided as Mathlib.Tactic.Module.qNF.toNF.

Equations

• Mathlib.Tactic.Module.qNF R M = List ((Q(«$R») × Q(«$M»)) × ℕ)

def Mathlib.Tactic.Module.qNF.toNF {u : Lean.Level} {v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} (l : Mathlib.Tactic.Module.qNF R M) : Q(Mathlib.Tactic.Module.NF «$R» «$M»)

Given l of type qNF R M, i.e. a list of (Q($R) × Q($M)) × ℕs (two Exprs and a natural number), build an Expr representing an object of type NF R M (i.e. List (R × M)) in the in the obvious way: by forgetting the natural numbers and gluing together the Exprs.

Equations

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

def Mathlib.Tactic.Module.qNF.onScalar {v : Lean.Level} {M : Q(Type v)} {u₁ : Lean.Level} {u₂ : Lean.Level} {R₁ : Q(Type u₁)} {R₂ : Q(Type u₂)} (l : Mathlib.Tactic.Module.qNF R₁ M) (f : Q(«$R₁» → «$R₂»)) : Mathlib.Tactic.Module.qNF R₂ M

Given l of type qNF R₁ M, i.e. a list of (Q($R₁) × Q($M)) × ℕs (two Exprs and a natural number), apply an expression representing a function with domain R₁ to each of the Q($R₁) components.

Equations

• l.onScalar f = List.map (fun (x : (Q(«$R₁») × Q(«$M»)) × ℕ) => match x with | ((a, x), k) => ((q(«$f» «$a»), x), k)) l

@[irreducible]

def Mathlib.Tactic.Module.qNF.add {u : Lean.Level} {v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} (iR : Q(Semiring «$R»)) : Mathlib.Tactic.Module.qNF R M → Mathlib.Tactic.Module.qNF R M → Mathlib.Tactic.Module.qNF R M

Given two terms l₁, l₂ of type qNF R M, i.e. lists of (Q($R) × Q($M)) × ℕs (two Exprs and a natural number), construct another such term l, which will have the property that in the $R-module $M, the sum of the "linear combinations" represented by l₁ and l₂ is the linear combination represented by l.

The construction assumes, to be valid, that the lists l₁ and l₂ are in strictly increasing order by ℕ-component, and that if pairs (a₁, x₁) and (a₂, x₂) appear in l₁, l₂ respectively with the same ℕ-component k, then the expressions x₁ and x₂ are equal.

The construction is as follows: merge the two lists, except that if pairs (a₁, x₁) and (a₂, x₂) appear in l₁, l₂ respectively with the same ℕ-component k, then contribute a term (a₁ + a₂, x₁) to the output list with ℕ-component k.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Module.qNF.add iR [] x = x
• Mathlib.Tactic.Module.qNF.add iR x [] = x

@[irreducible]

def Mathlib.Tactic.Module.qNF.mkAddProof {u : Lean.Level} {v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} {iR : Q(Semiring «$R»)} {iM : Q(AddCommMonoid «$M»)} (iRM : Q(Module «$R» «$M»)) (l₁ : Mathlib.Tactic.Module.qNF R M) (l₂ : Mathlib.Tactic.Module.qNF R M) : let a := (Mathlib.Tactic.Module.qNF.add iR l₁ l₂).toNF; let a_1 := l₂.toNF; let a_2 := l₁.toNF; Q(Mathlib.Tactic.Module.NF.eval unknown_1 + Mathlib.Tactic.Module.NF.eval unknown_2 = Mathlib.Tactic.Module.NF.eval unknown_3)

Given two terms l₁, l₂ of type qNF R M, i.e. lists of (Q($R) × Q($M)) × ℕs (two Exprs and a natural number), recursively construct a proof that in the $R-module $M, the sum of the "linear combinations" represented by l₁ and l₂ is the linear combination represented by Module.qNF.add iR l₁ l₁.

@[irreducible]

def Mathlib.Tactic.Module.qNF.sub {u : Lean.Level} {v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} (iR : Q(Ring «$R»)) : Mathlib.Tactic.Module.qNF R M → Mathlib.Tactic.Module.qNF R M → Mathlib.Tactic.Module.qNF R M

Given two terms l₁, l₂ of type qNF R M, i.e. lists of (Q($R) × Q($M)) × ℕs (two Exprs and a natural number), construct another such term l, which will have the property that in the $R-module $M, the difference of the "linear combinations" represented by l₁ and l₂ is the linear combination represented by l.

The construction assumes, to be valid, that the lists l₁ and l₂ are in strictly increasing order by ℕ-component, and that if pairs (a₁, x₁) and (a₂, x₂) appear in l₁, l₂ respectively with the same ℕ-component k, then the expressions x₁ and x₂ are equal.

The construction is as follows: merge the first list and the negation of the second list, except that if pairs (a₁, x₁) and (a₂, x₂) appear in l₁, l₂ respectively with the same ℕ-component k, then contribute a term (a₁ - a₂, x₁) to the output list with ℕ-component k.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Module.qNF.sub iR [] x = x.onScalar q(Neg.neg)
• Mathlib.Tactic.Module.qNF.sub iR x [] = x

@[irreducible]

def Mathlib.Tactic.Module.qNF.mkSubProof {u : Lean.Level} {v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} (iR : Q(Ring «$R»)) (iM : Q(AddCommGroup «$M»)) (iRM : Q(Module «$R» «$M»)) (l₁ : Mathlib.Tactic.Module.qNF R M) (l₂ : Mathlib.Tactic.Module.qNF R M) : let a := (Mathlib.Tactic.Module.qNF.sub iR l₁ l₂).toNF; let a_1 := l₂.toNF; let a_2 := l₁.toNF; Q(Mathlib.Tactic.Module.NF.eval unknown_1 - Mathlib.Tactic.Module.NF.eval unknown_2 = Mathlib.Tactic.Module.NF.eval unknown_3)

Given two terms l₁, l₂ of type qNF R M, i.e. lists of (Q($R) × Q($M)) × ℕs (two Exprs and a natural number), recursively construct a proof that in the $R-module $M, the difference of the "linear combinations" represented by l₁ and l₂ is the linear combination represented by Module.qNF.sub iR l₁ l₁.

def Mathlib.Tactic.Module.qNF.matchRings {v : Lean.Level} {M : Q(Type v)} {iM : Q(AddCommMonoid «$M»)} {u₁ : Lean.Level} {R₁ : Q(Type u₁)} {iR₁ : Q(Semiring «$R₁»)} (iRM₁ : Q(Module «$R₁» «$M»)) {u₂ : Lean.Level} {R₂ : Q(Type u₂)} (iR₂ : Q(Semiring «$R₂»)) (iRM₂ : Q(Module «$R₂» «$M»)) (l₁ : Mathlib.Tactic.Module.qNF R₁ M) (l₂ : Mathlib.Tactic.Module.qNF R₂ M) (r : Q(«$R₂»)) (x : Q(«$M»)) : Lean.MetaM ((u : Lean.Level) × (R : Q(Type u)) × (iR : Q(Semiring «$R»)) × (x_1 : Q(Module «$R» «$M»)) × ((l₁' : Mathlib.Tactic.Module.qNF R M) × let a := l₁.toNF; let a_1 := l₁'.toNF; Q(Mathlib.Tactic.Module.NF.eval unknown_1 = Mathlib.Tactic.Module.NF.eval unknown_2)) × ((l₂' : Mathlib.Tactic.Module.qNF R M) × let a := l₂.toNF; let a_1 := l₂'.toNF; Q(Mathlib.Tactic.Module.NF.eval unknown_1 = Mathlib.Tactic.Module.NF.eval unknown_2)) × (r' : Q(«$R»)) × Q(«$r'» • «$x» = «$r» • «$x»))

Given an expression M representing a type which is an AddCommMonoid and a module over two semirings R₁ and R₂, find the "bigger" of the two semirings. That is, we assume that it will turn out to be the case that either (1) R₁ is an R₂-algebra and the R₂ scalar action on M is induced from R₁'s scalar action on M, or (2) vice versa; we return the semiring R₁ in the first case and R₂ in the second case.

Moreover, given expressions representing particular scalar multiplications of R₁ and/or R₂ on M (a List (R₁ × M), a List (R₂ × M), a pair (r, x) : R₂ × M), bump these up to the "big" ring by applying the algebra-map where needed.

Equations

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

Core of the module tactic

partial def Mathlib.Tactic.Module.parse {v : Lean.Level} {M : Q(Type v)} (iM : Q(AddCommMonoid «$M»)) (x : Q(«$M»)) : Mathlib.Tactic.AtomM ((u : Lean.Level) × (R : Q(Type u)) × (iR : Q(Semiring «$R»)) × (x_1 : Q(Module «$R» «$M»)) × (l : Mathlib.Tactic.Module.qNF R M) × let a := l.toNF; Q(«$x» = Mathlib.Tactic.Module.NF.eval unknown_1))

The main algorithm behind the match_scalars and module tactics: partially-normalizing an expression in an additive commutative monoid M into the form c1 • x1 + c2 • x2 + ... c_k • x_k, where x1, x2, ... are distinct atoms in M, and c1, c2, ... are scalars. The scalar type of the expression 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.

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).

TODO: implement a variant in which a semiring R is provided by the user, and the assumption is instead that for any semiring S which occurs, we have Algebra S R. The PR #16984 provides a proof-of-concept implementation of this variant, but it would need some polishing before joining Mathlib.

Possible TODO, if poor performance on large problems is witnessed: switch the implementation from AtomM to CanonM, per the discussion https://github.com/leanprover-community/mathlib4/pull/16593/files#r1749623191

partial def Mathlib.Tactic.Module.reduceCoefficientwise {u : Lean.Level} {v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} : {x : Q(AddCommMonoid «$M»)} → {x_1 : Q(Semiring «$R»)} → (iRM : Q(Module «$R» «$M»)) → (l₁ l₂ : Mathlib.Tactic.Module.qNF R M) → Lean.MetaM (List Lean.MVarId × let a := l₂.toNF; let a_1 := l₁.toNF; Q(Mathlib.Tactic.Module.NF.eval unknown_1 = Mathlib.Tactic.Module.NF.eval unknown_2))

Given expressions R and M representing types such that M's is a module over R's, and given two terms l₁, l₂ of type qNF R M, i.e. lists of (Q($R) × Q($M)) × ℕs (two Exprs and a natural number), construct a list of new goals: that the R-coefficient of an M-atom which appears in only one list is zero, and that the R-coefficients of an M-atom which appears in both lists are equal. Also construct (dependent on these new goals) a proof that the "linear combinations" represented by l₁ and l₂ are equal in M.

def Mathlib.Tactic.Module.matchScalarsAux (g : Lean.MVarId) : Mathlib.Tactic.AtomM (List Lean.MVarId)

Given a goal which is an equality in a type M (with M an AddCommMonoid), parse the LHS and RHS of the goal as linear combinations of M-atoms over some semiring R, and reduce the goal to the respective equalities of the R-coefficients of each atom.

This is an auxiliary function which produces slightly awkward goals in R; they are later cleaned up by the function Mathlib.Tactic.Module.postprocess.

Equations

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

def Mathlib.Tactic.Module.algebraMapThms : Array Lean.Name

Lemmas used to post-process the result of the match_scalars and module tactics by converting the algebraMap operations which (which proliferate in the constructed scalar goals) to more familiar forms: ℕ, ℤ and ℚ casts.

Equations

• Mathlib.Tactic.Module.algebraMapThms = #[`eq_natCast, `eq_intCast, `eq_ratCast]

def Mathlib.Tactic.Module.postprocess (mvarId : Lean.MVarId) : Lean.MetaM Lean.MVarId

Postprocessing for the scalar goals constructed in the match_scalars and module tactics. These goals feature a proliferation of algebraMap operations (because the scalars start in ℕ and get successively bumped up by algebraMaps as new semirings are encountered), so we reinterpret the most commonly occuring algebraMaps (those out of ℕ, ℤ and ℚ) into their standard forms (ℕ, ℤ and ℚ casts) and then try to disperse the casts using the various push_cast lemmas.

Equations

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

def Mathlib.Tactic.Module.matchScalars (g : Lean.MVarId) : Lean.MetaM (List Lean.MVarId)

Given a goal which is an equality in a type M (with M an AddCommMonoid), parse the LHS and RHS of the goal as linear combinations of M-atoms over some semiring R, and reduce the goal to the respective equalities of the R-coefficients of each atom.

Equations

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

def Mathlib.Tactic.Module.tacticMatch_scalars : Lean.ParserDescr

Given a goal which is an equality in a type M (with M an AddCommMonoid), parse the LHS and RHS of the goal as linear combinations of M-atoms over some semiring R, and reduce 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

This produces the goal ⊢ -2 * (a * 1) = a * (-2 * 1):

example [AddCommGroup M] [Ring R] [Module R M] (a : R) (x : M) :
    -(2:R) • a • x = a • (-2:ℤ) • x  := by
  match_scalars

The scalar type for the goals produced by the match_scalars tactic is the largest scalar type encountered; for example, if ℕ, ℚ and a characteristic-zero field K all occur as scalars, then the goals produced are equalities in K. A variant of push_cast is used internally in match_scalars to interpret scalars from the other types in this largest type.

If the set of scalar types encountered is not totally ordered (in the sense that for all rings R, S encountered, it holds that either Algebra R S or Algebra S R), then the match_scalars tactic fails.

Equations

• Mathlib.Tactic.Module.tacticMatch_scalars = Lean.ParserDescr.node `Mathlib.Tactic.Module.tacticMatch_scalars 1024 (Lean.ParserDescr.nonReservedSymbol "match_scalars" false)

def Mathlib.Tactic.Module.tacticModule : Lean.ParserDescr

Given a goal which is an equality in a type M (with M an AddCommMonoid), parse the LHS and RHS of the goal as linear combinations of M-atoms over some commutative semiring R, and prove the goal by checking that the LHS- and RHS-coefficients of each atom are the same up to ring-normalization in R.

(If the proofs of coefficient-wise equality will require more reasoning than just ring-normalization, use the tactic match_scalars instead, and then prove coefficient-wise equality by hand.)

Example uses of the module tactic:

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

example [AddCommGroup M] [CommRing R] [Module R M] (a b μ ν : R) (x y : M) :
    (μ - ν) • a • x = (a • μ • x + b • ν • y) - ν • (a • x + b • y) := by
  module

Equations

• Mathlib.Tactic.Module.tacticModule = Lean.ParserDescr.node `Mathlib.Tactic.Module.tacticModule 1024 (Lean.ParserDescr.nonReservedSymbol "module" false)