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.
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
Augment a Module.NF R M
object l
, i.e. a list of pairs in R × M
, by prepending another
pair p : R × M
.
Instances For
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
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.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
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
Lists of expressions representing scalars and vectors, and operations on such lists #
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
.
Instances For
Given l
of type qNF R M
, i.e. a list of (Q($R) × Q($M)) × ℕ
s (two Expr
s 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 Expr
s.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given l
of type qNF R₁ M
, i.e. a list of (Q($R₁) × Q($M)) × ℕ
s (two Expr
s and a natural
number), apply an expression representing a function with domain R₁
to each of the Q($R₁)
components.
Equations
Instances For
Given two terms l₁
, l₂
of type qNF R M
, i.e. lists of (Q($R) × Q($M)) × ℕ
s (two Expr
s
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
Given two terms l₁
, l₂
of type qNF R M
, i.e. lists of (Q($R) × Q($M)) × ℕ
s (two Expr
s
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₁
.
Instances For
Given two terms l₁
, l₂
of type qNF R M
, i.e. lists of (Q($R) × Q($M)) × ℕ
s (two Expr
s
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
Given two terms l₁
, l₂
of type qNF R M
, i.e. lists of (Q($R) × Q($M)) × ℕ
s (two Expr
s
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₁
.
Instances For
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 #
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
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 Expr
s
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
.
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
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
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 algebraMap
s as new semirings are encountered), so we reinterpret the
most commonly occuring algebraMap
s (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
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
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)
Instances For
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)