Documentation

Mathlib.Tactic.Module

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)

Instances For

@[match_pattern]

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

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

Instances For

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.

Instances For

def Mathlib.Tactic.Module.NF.eval {R : Type u_2} {M : Type u_3} [Add M] [Zero M] [SMul R M] (l : 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

Instances For

@[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 : 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 = eval [(1, x)]

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

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₁ l₂ l : 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) (x : M) {l₁ l₂ l : 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₁ l₂ l : 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₁ l₂ l : NF R M} {l₁' : NF R₁ M} {l₂' : NF R₂ M} {x₁ 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₁ l₂ l : 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) (x : M) {l₁ l₂ l : 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₁ l₂ l : 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₁ l₂ l : NF R M} {l₁' : NF R₁ M} {l₂' : NF R₂ M} {l₁'' : NF S₁ M} {l₂'' : NF S₂ M} {x₁ 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

@[implicit_reducible]

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

Neg (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 : 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 : 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 : NF R M} {l₀ : NF S M} (hl : l.eval = l₀.eval) {x : M} (h : x = l₀.eval) :

-x = (-l).eval

@[implicit_reducible]

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

SMul R (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 : 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 : 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 : NF R M} {l₀ : 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} (m : M) {l₁ l₂ : 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 : 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 : 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₁ l₂ : NF R M} {l₁' : NF R₁ M} {l₂' : NF R₂ M} {x₁ 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 : NF S M) :

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

Instances For

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 : NF S M) :

(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 v : Lean.Level} (R : Q(Type u)) (M : Q(Type v)) :

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»)) × ℕ)

Instances For

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

Q(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.

Instances For

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

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

Instances For

@[irreducible]

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

qNF R M → qNF R M → 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✝

Instances For

@[irreducible]

def Mathlib.Tactic.Module.qNF.mkAddProof {u 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₁ l₂ : qNF R M) :

have a := (add iR l₁ l₂).toNF; have a_1 := l₂.toNF; have a_2 := l₁.toNF; Q(«$a_2».eval + «$a_1».eval = «$a».eval)

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

Equations

One or more equations did not get rendered due to their size.
Mathlib.Tactic.Module.qNF.mkAddProof iRM [] l₂ = q(⋯)
Mathlib.Tactic.Module.qNF.mkAddProof iRM l₁ [] = q(⋯)

Instances For

@[irreducible]

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

qNF R M → qNF R M → 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✝

Instances For

@[irreducible]

def Mathlib.Tactic.Module.qNF.mkSubProof {u 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₁ l₂ : qNF R M) :

have a := (sub iR l₁ l₂).toNF; have a_1 := l₂.toNF; have a_2 := l₁.toNF; Q(«$a_2».eval - «$a_1».eval = «$a».eval)

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

Equations

One or more equations did not get rendered due to their size.
Mathlib.Tactic.Module.qNF.mkSubProof iR iM iRM [] l₂ = q(⋯)
Mathlib.Tactic.Module.qNF.mkSubProof iR iM iRM l₁ [] = q(⋯)

Instances For

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₁ : qNF R₁ M) (l₂ : 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₁' : qNF R M) × have a := l₁.toNF; have a_1 := l₁'.toNF; Q(«$a_1».eval = «$a».eval)) × ((l₂' : qNF R M) × have a := l₂.toNF; have a_1 := l₂'.toNF; Q(«$a_1».eval = «$a».eval)) × (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.

Instances For

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»)) :

AtomM ((u : Lean.Level) × (R : Q(Type u)) × (iR : Q(Semiring «$R»)) × (x_1 : Q(Module «$R» «$M»)) × (l : qNF R M) × have a := l.toNF; Q(«$x» = «$a».eval))

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 https://github.com/leanprover-community/mathlib4/pull/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 v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} {x✝ : Q(AddCommMonoid «$M»)} {x✝¹ : Q(Semiring «$R»)} (iRM : Q(Module «$R» «$M»)) (l₁ l₂ : qNF R M) :

Lean.MetaM (List Lean.MVarId × have a := l₂.toNF; have a_1 := l₁.toNF; Q(«$a_1».eval = «$a».eval))

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

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.

Instances For

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]

Instances For

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

Instances For

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.

Instances For

def Mathlib.Tactic.Module.tacticMatch_scalars :

Lean.ParserDescr

Given a goal parseable as a linear combination ⊢ a • x + ... + b • y = c • x + ... + d • y, match_scalars splits up the goal into equalities of the scalars for each respective atom. This means the example goal above is replaced by goals ⊢ a = c (from x), ..., ⊢ b = d (from y).

The module tactic is equivalent to match_scalars <;> ring1.

match_scalars can parse into expressions made of the operators +, -, • and the numeral 0. Any other subexpressions (including variables) are treated as atoms. If the goal is an equality in the type M, then match_scalars requires an AddCommMonoid M instance. If the goal contains a scalar multiplication (a : R) • (x : M), this requires a Semiring R and Module R M instance. If any of the instances are missing, match_scalars fails.

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 with the appropriate casts (from ℕ, ℤ, ℚ) and algebraMaps (otherwise) inserted. Inserted casts are simplified by lemmas tagged @[push_cast]. 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 match_scalars fails.

Examples:

example [AddCommMonoid M] [Semiring R] [Module R M] (a b : R) (x : M) :
    a • x + b • x = (b + a) • x := by
  match_scalars
  -- one goal: `⊢ a * 1 + b * 1 = (b + a) * 1`

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
  -- two goals:
  -- `⊢ a * (a * 1) + b * (b * 1) = 1` (from the `x` atom)
  -- `⊢ a * -(b * 1) + b * (a * 1) = 0` (from the `y` atom)

example [AddCommGroup M] [Ring R] [Module R M] (a : R) (x : M) :
    -(2:R) • a • x = a • (-2:ℤ) • x := by
  match_scalars
  -- one goal: `⊢ -2 * (a * 1) = a * (-2 * 1)`

Equations

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

Instances For

def Mathlib.Tactic.Module.tacticModule :

Lean.ParserDescr

Given a goal parseable as a linear combination ⊢ a • x + ... + b • y = c • x + ... + d • y, module proves the equalities of the scalars for each respective atom, by ring normalization. This means the example goal above is solved if ring can prove ⊢ a = c (from x), ..., ⊢ b = d (from y).

module is equivalent to match_scalars <;> ring1. If ring1 fails to prove one of the equalities, you can instead use match_scalars followed by specialized proofs for each scalar.

Examples:

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)

Instances For