# Documentation

Mathlib.Tactic.Ring.RingNF

# ring_nf tactic #

A tactic which uses ring to rewrite expressions. This can be used non-terminally to normalize ring expressions in the goal such as ⊢ P (x + x + x)⊢ P (x + x + x) ~> ⊢ P (x * 3)⊢ P (x * 3), as well as being able to prove some equations that ring cannot because they involve ring reasoning inside a subterm, such as sin (x + y) + sin (y + x) = 2 * sin (x + y).

def Mathlib.Tactic.Ring.ExBase.isAtom :
{a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 : Q(«$arg»)} → Bool

True if this represents an atomic expression.

Equations
• = match x with | => true | x => false
def Mathlib.Tactic.Ring.ExProd.isAtom :
{a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 : Q(«$arg»)} → Bool

True if this represents an atomic expression.

Equations
• One or more equations did not get rendered due to their size.
def Mathlib.Tactic.Ring.ExSum.isAtom :
{a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 : Q(«$arg»)} → Bool

True if this represents an atomic expression.

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

The normalization style for ring_nf.

Instances For
Equations
• the reducibility setting to use when comparing atoms for defeq

• if true, atoms inside ring expressions will be reduced recursively

recursive : Bool
• The normalization style.

Configuration for ring_nf.

Instances For
Equations
Equations

Function elaborating RingNF.Config.

Equations
• One or more equations did not get rendered due to their size.
• A basically empty simp context, passed to the simp traversal in RingNF.rewrite.

• A cleanup routine, which simplifies normalized polynomials to a more human-friendly format.

The read-only state of the RingNF monad.

Instances For
@[inline]

The monad for RingNF contains, in addition to the AtomM state, a simp context for the main traversal and a simp function (which has another simp context) to simplify normalized polynomials.

Equations
def Mathlib.Tactic.RingNF.rewrite (parent : Lean.Expr) (root : ) :

A tactic in the RingNF.M monad which will simplify expression parent to a normal form.

• root: true if this is a direct call to the function. RingNF.M.run sets this to false in recursive mode.
Equations
• One or more equations did not get rendered due to their size.
theorem Mathlib.Tactic.RingNF.add_assoc_rev {R : Type u_1} [inst : ] (a : R) (b : R) (c : R) :
a + (b + c) = a + b + c
theorem Mathlib.Tactic.RingNF.mul_assoc_rev {R : Type u_1} [inst : ] (a : R) (b : R) (c : R) :
a * (b * c) = a * b * c
theorem Mathlib.Tactic.RingNF.mul_neg {R : Type u_1} [inst : Ring R] (a : R) (b : R) :
a * -b = -(a * b)
theorem Mathlib.Tactic.RingNF.add_neg {R : Type u_1} [inst : Ring R] (a : R) (b : R) :
a + -b = a - b
theorem Mathlib.Tactic.RingNF.nat_rawCast_0 {R : Type u_1} [inst : ] :
= 0
theorem Mathlib.Tactic.RingNF.nat_rawCast_1 {R : Type u_1} [inst : ] :
= 1
theorem Mathlib.Tactic.RingNF.nat_rawCast_2 {R : Type u_1} [inst : ] {n : } [inst : ] :
theorem Mathlib.Tactic.RingNF.int_rawCast_2 {n : } {R : Type u_1} [inst : Ring R] [inst : ] :
theorem Mathlib.Tactic.RingNF.rat_rawCast_2 {n : } {d : } {R : Type u_1} [inst : ] :
= n / d

Runs a tactic in the RingNF.M monad, given initial data:

• s: a reference to the mutable state of ring, for persisting across calls. This ensures that atom ordering is used consistently.
• cfg: the configuration options
• x: the tactic to run
Equations
• One or more equations did not get rendered due to their size.

The recursive context.

The atom evaluator calls either RingNF.rewrite recursively, or nothing depending on cfg.recursive.

Use ring_nf to rewrite the main goal.

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

Use ring_nf to rewrite hypothesis h.

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

Simplification tactic for expressions in the language of commutative (semi)rings, which rewrites all ring expressions into a normal form.

• ring_nf! will use a more aggressive reducibility setting to identify atoms.
• ring_nf (config := cfg) allows for additional configuration:
• red: the reducibility setting (overridden by !)
• recursive: if true, ring_nf will also recurse into atoms
• ring_nf works as both a tactic and a conv tactic. In tactic mode, ring_nf at h can be used to rewrite in a hypothesis.
Equations
• One or more equations did not get rendered due to their size.

Simplification tactic for expressions in the language of commutative (semi)rings, which rewrites all ring expressions into a normal form.

• ring_nf! will use a more aggressive reducibility setting to identify atoms.
• ring_nf (config := cfg) allows for additional configuration:
• red: the reducibility setting (overridden by !)
• recursive: if true, ring_nf will also recurse into atoms
• ring_nf works as both a tactic and a conv tactic. In tactic mode, ring_nf at h can be used to rewrite in a hypothesis.
Equations
• One or more equations did not get rendered due to their size.

Simplification tactic for expressions in the language of commutative (semi)rings, which rewrites all ring expressions into a normal form.

• ring_nf! will use a more aggressive reducibility setting to identify atoms.
• ring_nf (config := cfg) allows for additional configuration:
• red: the reducibility setting (overridden by !)
• recursive: if true, ring_nf will also recurse into atoms
• ring_nf works as both a tactic and a conv tactic. In tactic mode, ring_nf at h can be used to rewrite in a hypothesis.
Equations
• One or more equations did not get rendered due to their size.

Tactic for solving equations of commutative (semi)rings, allowing variables in the exponent.

• This version of ring1 uses ring_nf to simplify in atoms.
• The variant ring1_nf! will use a more aggressive reducibility setting to determine equality of atoms.
Equations
• One or more equations did not get rendered due to their size.

Tactic for solving equations of commutative (semi)rings, allowing variables in the exponent.

• This version of ring1 uses ring_nf to simplify in atoms.
• The variant ring1_nf! will use a more aggressive reducibility setting to determine equality of atoms.
Equations
• One or more equations did not get rendered due to their size.

Elaborator for the ring_nf tactic.

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

Simplification tactic for expressions in the language of commutative (semi)rings, which rewrites all ring expressions into a normal form.

• ring_nf! will use a more aggressive reducibility setting to identify atoms.
• ring_nf (config := cfg) allows for additional configuration:
• red: the reducibility setting (overridden by !)
• recursive: if true, ring_nf will also recurse into atoms
• ring_nf works as both a tactic and a conv tactic. In tactic mode, ring_nf at h can be used to rewrite in a hypothesis.
Equations
• One or more equations did not get rendered due to their size.

Tactic for evaluating expressions in commutative (semi)rings, allowing for variables in the exponent.

• ring! will use a more aggressive reducibility setting to determine equality of atoms.
• ring1 fails if the target is not an equality.

For example:

example (n : ℕ) (m : ℤ) : 2^(n+1) * m = 2 * 2^n * m := by ring
example (a b : ℤ) (n : ℕ) : (a + b)^(n + 2) = (a^2 + b^2 + a * b + b * a) * (a + b)^n := by ring
example (x y : ℕ) : x + id y = y + id x := by ring!

Equations

Tactic for evaluating expressions in commutative (semi)rings, allowing for variables in the exponent.

• ring! will use a more aggressive reducibility setting to determine equality of atoms.
• ring1 fails if the target is not an equality.

For example:

example (n : ℕ) (m : ℤ) : 2^(n+1) * m = 2 * 2^n * m := by ring
example (a b : ℤ) (n : ℕ) : (a + b)^(n + 2) = (a^2 + b^2 + a * b + b * a) * (a + b)^n := by ring
example (x y : ℕ) : x + id y = y + id x := by ring!

Equations

The tactic ring evaluates expressions in commutative (semi)rings. This is the conv tactic version, which rewrites a target which is a ring equality to True.

See also the ring tactic.

Equations

The tactic ring evaluates expressions in commutative (semi)rings. This is the conv tactic version, which rewrites a target which is a ring equality to True.

See also the ring tactic.

Equations