def Lean.Meta.Sym.Simp.simpArith (d : Discharger := dischargeNone) (lhsOnly : Bool := false) (distrib : Bool := true) : Simproc

Normalizes ring and semiring terms and relations into polynomial normal form (Sym.Arith.normalize?), simplifying the atoms with simp. Intended as a pre simproc: it sees the maximal arithmetic subtree first and reifies it once.

A normal form is final (done := true): simp does not re-enter it, so the normalizer never runs on its own output, and it is cached so that reaching it again costs a lookup. Terms and relations differ in what post sees:

• A normalized term is not visited by post. Rewrite rules on arithmetic operators are what the normalizer supersedes.
• A normalized relation (=, ≤, <) is handed to post here, exactly once, and the result is chained in. This is how t = t and ground comparisons are closed (evalGround), and how rewrite rules on relations apply after normalization. Its two sides are cached as normal forms. If post rewrites the relation, that step is not final and simp continues on the result as usual.

The discharger d proves the side conditions x ≠ 0 under which x * x⁻¹ is cancelled in a field. With lhsOnly := true, relations over rings are normalized to p = 0, p ≤ 0, p < 0 instead of being split by sign, and with distrib := false products of non-constant polynomials are kept as atoms; see Arith.normalize?.

Equations

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

def Lean.Meta.Sym.Simp.simpNatRel : Simproc

Decides the Nat relations that are trivially unsatisfiable or valid after normalization by simpArith, like Nat.Linear does in simp +arith: a + k = 0, 0 = a + k, and a + k ≤ 0 become False for a positive numeral k, and 0 ≤ a becomes True. The other ground cases (k = 0, 0 ≤ k) are handled by evalGround. Intended as a post simproc, after simpArith has cancelled the common part of the two sides.

Equations

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