Polynomial normalization of ring and semiring terms #
normalize? rewrites a term of a CommRing, Ring, CommSemiring, or Semiring into the
polynomial normal form of Poly.toExpr, with a proof by reflection: the certificate compares
the Init polynomial of the input with the polynomial of the output (Expr.eq_of_toPoly_eq,
Expr.eq_of_toPolyC_eq, eq_normS, and their _nc variants for the non-commutative
structures, where monomials keep the order of their factors).
In a field of characteristic zero, the inverses of numerals are not atoms: the normal form is
p * d⁻¹ with p an integer polynomial and d a numeral, in lowest terms, and a relation
becomes denominator-free (a / 2 = b / 3 is 3 * a = 2 * b). The certificate reifies c⁻¹ as a
variable and eliminates it (Expr.eq_of_toPolyQ_eq, Init/Grind/Ring/FieldSolver.lean).
In any field, x * x⁻¹ for an atom x is cancelled when the discharge? callback proves
x ≠ 0 (Expr.eq_of_cancelInvs_eq); this is the only step whose result depends on the local
context, and it is marked contextDependent.
The normalizer owns the traversal of the arithmetic tree (visit): it recurses bottom-up
through the operators its structure interprets and hands every atom (maximal non-arithmetic
subterm) to the simpAtom callback, so that a simplifier can rewrite the atoms and the normal
form is stated for the simplified atoms. The congruence proof for that step is built with
Sym.Simp.mkCongr. Each node is reified once, and its polynomial is computed from its
children's with the SafePoly mirrors of the toPoly cases, so the polynomial of a node is the
kernel's toPoly of its reification by construction. A cast of a numeral (↑(2 : Nat),
↑(-2 : Int)) is rewritten to the numeral of the carrier on the way, also when it is the whole
term, so that a numeral has one representation.
With distrib := false, a product of two non-constant polynomials is not expanded: its factors
are normalized and certified where they are, and the product is an atom (see normalize?).
A certificate (certify) numbers the atoms it mentions in Expr.lt order, so the normal form
of a term does not depend on the order in which its atoms occur, and two terms denoting the same
polynomial over the same atoms normalize to the same (maximally shared) expression.
The input is not assumed to be canonicalized. The instance of each operator is compared, after
canonExpr, with the structure's canonical one; a node with another instance is an atom. The
proof is stated for the original term, and the kernel closes the gap between the goal's
instances and the canonical ones of the output while checking the expected type, as it does for
grind.
Equations
true for (commutative or not) rings, false for semirings.
Equations
Instances For
true for the commutative structures.
Equations
Instances For
- kind : Kind
- distrib : Bool
See
normalize?. - polyCfg : PolyConfig
The
PolyConfigof the structure: characteristic, (non-)commutativity, and the budget options. - charZero : Bool
truefor a field of characteristic zero, where numeral inverses are rational coefficients.
Instances For
The variables
c⁻¹for a numeralc ≥ 1with the field'sInvinstance, withc.The side conditions
x ≠ 0asked for so far, keyed byx, with the proof when discharged.
Instances For
Equations
Instances For
Equations
- Lean.Meta.Sym.Arith.getKind = do let __do_lift ← read pure __do_lift.kind
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.
Equations
- One or more equations did not get rendered due to their size.
Both ring kinds; takes precedence over the instance derived from MonadCommRing.
Equations
- One or more equations did not get rendered due to their size.
Both semiring kinds; takes precedence over the instance derived from MonadCommSemiring.
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.
If e is an application of an arithmetic operator supported by the normalizer, or a cast of a
numeral, returns its carrier type.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Rewrite steps #
The steps applied by visit that are not congruences: k • a ↦ ↑k * a, casts of numerals, and
the field rewrites.
Field rewrites applied by the walk, all without side conditions (Init/Grind/Ring/Field.lean):
a / b ↦ a * b⁻¹, (a * b)⁻¹ ↦ a⁻¹ * b⁻¹, (a ^ n)⁻¹ ↦ a⁻¹ ^ n, (-a)⁻¹ ↦ -a⁻¹, a⁻¹⁻¹ ↦ a,
0⁻¹ ↦ 0, 1⁻¹ ↦ 1. After them, x⁻¹ for an atom or numeral x is an atom of the
polynomial; the certificate eliminates numeral inverses in characteristic zero (getInvVars)
and cancels x * x⁻¹ under a discharged x ≠ 0 (decideInvAtoms).
Certificate helpers #
Visiting the arithmetic tree #
visit traverses the arithmetic tree of e (the nodes the structure interprets, by head symbol
and canonical instance) bottom-up. It simplifies the atoms with simpAtom, reifies each node
once, computes its polynomial from its children's, and, with distrib := false, keeps a product
of non-constant polynomials as an atom after normalizing its factors.
Certificates #
certify turns a visited node into the proof that its term equals the denotation of its
polynomial, by reflection on the Init polynomial functions (Expr.eq_of_toPoly_eq and
variants). It renames the variables of the node to a compact range in Expr.lt order, so each
certificate only touches its own atoms.
Relations #
lhs = rhs, lhs ≤ rhs, lhs < rhs over a ring or semiring are normalized by
moving everything to one side and splitting by sign (x + y = z + 2 * x becomes y = z + x),
or, with lhsOnly, by keeping everything on the left (y + -1 * z + -1 * x = 0).
With lhsOnly, an equation k * m + k' = 0 or k * m₁ = k * m₂ over a commutative ring of
nonzero characteristic c is solved for the monomial when k is invertible modulo c
(eq_norm_mul_exprC): in Fin 5, 4 * x + 2 = 0 becomes x = 2.
Rings use eq_norm_expr, le_norm_expr, lt_norm_expr (CommSolver.lean); in a field of
characteristic zero the numerator of lhs - rhs is split instead (eq_normQ_expr,
le_normQ_expr, lt_normQ_expr in FieldSolver.lean, the last two under IsLinearOrder), so
the result has no numeral inverses; inverse atoms with a discharged side condition are cancelled
(eq_normA_expr, le_normA_expr, lt_normA_expr). Semirings have no
subtraction: both sides are normalized as terms after removing their common part c
(eq_normS twice, the relation between lhs' + c and rhs' + c by congruence), and c is
cancelled with AddRightCancel.add_right_cancel_iff, OrderedAdd.add_le_left_iff, or
OrderedAdd.add_lt_left_iff.
Equations
Equations
Equations
- Lean.Meta.Sym.Arith.instBEqRelKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)
Instances For
Entry points #
Normalizes e into polynomial normal form after simplifying its atoms with simpAtom:
either an arithmetic term (see normalizeTerm?), a relation lhs = rhs, lhs ≤ rhs,
lhs < rhs whose carrier type is a CommRing or CommSemiring (see "Relations"), or an
Int divisibility constraint k ∣ e with a numeral k (see normalizeDvd?).
e must be maximally shared. The result cases are those of normalizeTerm?. A normalized
relation is done as well; a simplifier that wants post to see normalized relations (to
close t = t, say) must apply it itself, as Sym.Simp.simpArith does.
discharge? is asked for the side conditions x ≠ 0 under which x * x⁻¹ is cancelled in a
field; by default none is proved.
With lhsOnly := true, a relation over a ring is normalized to p = 0, p ≤ 0, or p < 0
with p the polynomial of lhs - rhs, instead of being split by sign (see "Relations"); the
exceptions follow simp +arith: equations between atoms and numerals (x = y, x = 3,
3 = x) and equations already of the form p = 0 are left alone, and x - y = 0 and
x + k = 0 are written x = y and x = -k. This is the normal form of the grind
normalizer. Semirings have no subtraction and are unaffected.
With distrib := false, multiplication is not distributed over addition: a product is
expanded only when one factor is a scalar (a constant, or a numeral inverse in a field of
characteristic zero) or both are monomials, a power only when its base is a monomial, and in a
field (a * b)⁻¹ and (a ^ n)⁻¹ are not rewritten. Any other product, power, or inverse is an
atom whose factors are normalized separately, so x * (y + 1) stays x * (y + 1) while
2 * (y + 1) becomes 2 * y + 2. This keeps the nonlinear atoms that decision procedures for
linear arithmetic see, as a simplifier that only linearizes would.
Equations
- One or more equations did not get rendered due to their size.