# `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 * 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)`.

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

True if this represents an atomic expression.

Equations

- (Mathlib.Tactic.Ring.ExBase.atom id).isAtom = true
- x✝.isAtom = false

Instances For

source
def Mathlib.Tactic.Ring.ExProd.isAtom {u : Lean.Level} {arg : Q(Type u)} {sα : Q(CommSemiring «$arg»)} {a : Q(«$arg»)} :
ExProd sα a → Bool

True if this represents an atomic expression.

Equations

- One or more equations did not get rendered due to their size.
- x✝.isAtom = false

Instances For

source
def Mathlib.Tactic.Ring.ExSum.isAtom {u : Lean.Level} {arg : Q(Type u)} {sα : Q(CommSemiring «$arg»)} {a : Q(«$arg»)} :
ExSum sα a → Bool

True if this represents an atomic expression.

Equations

- (Mathlib.Tactic.Ring.ExSum.add va₁ Mathlib.Tactic.Ring.ExSum.zero).isAtom = va₁.isAtom
- (Mathlib.Tactic.Ring.ExSum.add va₁ va₂).isAtom = false
- x✝.isAtom = false

Instances For

source
inductive Mathlib.Tactic.RingNF.RingMode :
Type

The normalization style for `ring_nf`.

- SOP : RingMode

  Sum-of-products form, like `x + x * y * 2 + z ^ 2`.

- raw : RingMode

  Raw form: the representation `ring` uses internally.

Instances For

source
instance Mathlib.Tactic.RingNF.instInhabitedRingMode :
Inhabited RingMode
Equations

- Mathlib.Tactic.RingNF.instInhabitedRingMode = { default := Mathlib.Tactic.RingNF.instInhabitedRingMode.default }

source
def Mathlib.Tactic.RingNF.instInhabitedRingMode.default :
RingMode
Equations

- Mathlib.Tactic.RingNF.instInhabitedRingMode.default = Mathlib.Tactic.RingNF.RingMode.SOP

Instances For

source
instance Mathlib.Tactic.RingNF.instBEqRingMode :
BEq RingMode
Equations

- Mathlib.Tactic.RingNF.instBEqRingMode = { beq := Mathlib.Tactic.RingNF.instBEqRingMode.beq }

source
def Mathlib.Tactic.RingNF.instBEqRingMode.beq :
RingMode → RingMode → Bool
Equations

- Mathlib.Tactic.RingNF.instBEqRingMode.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source
instance Mathlib.Tactic.RingNF.instReprRingMode :
Repr RingMode
Equations

- Mathlib.Tactic.RingNF.instReprRingMode = { reprPrec := Mathlib.Tactic.RingNF.instReprRingMode.repr }

source
def Mathlib.Tactic.RingNF.instReprRingMode.repr :
RingMode → ℕ → Std.Format
Equations

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

Instances For

source
structure Mathlib.Tactic.RingNF.Config extends Mathlib.Tactic.AtomM.Recurse.Config :
Type

Configuration for `ring_nf`.

- red : Lean.Meta.TransparencyMode
- zetaDelta : Bool
- failIfUnchanged : Bool

  if true, then fail if no progress is made

- mode : RingMode

  The normalization style.

Instances For

source
instance Mathlib.Tactic.RingNF.instInhabitedConfig :
Inhabited Config
Equations

- Mathlib.Tactic.RingNF.instInhabitedConfig = { default := Mathlib.Tactic.RingNF.instInhabitedConfig.default }

source
def Mathlib.Tactic.RingNF.instInhabitedConfig.default :
Config
Equations

- Mathlib.Tactic.RingNF.instInhabitedConfig.default = { toConfig := default, failIfUnchanged := default, mode := default }

Instances For

source
def Mathlib.Tactic.RingNF.instBEqConfig.beq :
Config → Config → Bool
Equations

- Mathlib.Tactic.RingNF.instBEqConfig.beq { toConfig := a, failIfUnchanged := a_1, mode := a_2 } { toConfig := b, failIfUnchanged := b_1, mode := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
- Mathlib.Tactic.RingNF.instBEqConfig.beq x✝¹ x✝ = false

Instances For

source
instance Mathlib.Tactic.RingNF.instBEqConfig :
BEq Config
Equations

- Mathlib.Tactic.RingNF.instBEqConfig = { beq := Mathlib.Tactic.RingNF.instBEqConfig.beq }

source
def Mathlib.Tactic.RingNF.instReprConfig.repr :
Config → ℕ → Std.Format
Equations

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

Instances For

source
instance Mathlib.Tactic.RingNF.instReprConfig :
Repr Config
Equations

- Mathlib.Tactic.RingNF.instReprConfig = { reprPrec := Mathlib.Tactic.RingNF.instReprConfig.repr }

source
def Mathlib.Tactic.RingNF.elabConfig :
Lean.Syntax → Lean.Elab.Tactic.TacticM Config

Function elaborating `RingNF.Config`.

Equations

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

Instances For

source
def Mathlib.Tactic.RingNF.evalExpr (e : Lean.Expr) :
AtomM Lean.Meta.Simp.Result

Evaluates an expression `e` into a normalized representation as a polynomial.

This is a variant of `Mathlib.Tactic.Ring.eval`, the main driver of the `ring` tactic. It differs in

- operating on `Expr` (input) and `Simp.Result` (output), rather than typed `Qq` versions of these;
- throwing an error if the expression `e` is an atom for the `ring` tactic.

Equations

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

Instances For

source
theorem Mathlib.Tactic.RingNF.add_assoc_rev {R : Type u_1} [CommSemiring R] (a b c : R) :
a + (b + c) = a + b + c
source
theorem Mathlib.Tactic.RingNF.mul_assoc_rev {R : Type u_1} [CommSemiring R] (a b c : R) :
a * (b * c) = a * b * c
source
theorem Mathlib.Tactic.RingNF.mul_neg {R : Type u_2} [Ring R] (a b : R) :
a * -b = -(a * b)
source
theorem Mathlib.Tactic.RingNF.add_neg {R : Type u_2} [Ring R] (a b : R) :
a + -b = a - b
source
theorem Mathlib.Tactic.RingNF.nat_rawCast_0 {R : Type u_1} [CommSemiring R] :
Nat.rawCast 0 = 0
source
theorem Mathlib.Tactic.RingNF.nat_rawCast_1 {R : Type u_1} [CommSemiring R] :
Nat.rawCast 1 = 1
source
theorem Mathlib.Tactic.RingNF.nat_rawCast_2 {R : Type u_1} [CommSemiring R] {n : ℕ} [n.AtLeastTwo] :
n.rawCast = OfNat.ofNat n
source
theorem Mathlib.Tactic.RingNF.int_rawCast_neg {n : ℕ} {R : Type u_2} [Ring R] :
(Int.negOfNat n).rawCast = -n.rawCast
source
theorem Mathlib.Tactic.RingNF.nnrat_rawCast {n d : ℕ} {R : Type u_2} [DivisionSemiring R] :
NNRat.rawCast n d = n.rawCast / d.rawCast
source
theorem Mathlib.Tactic.RingNF.rat_rawCast_neg {n d : ℕ} {R : Type u_2} [DivisionRing R] :
Rat.rawCast (Int.negOfNat n) d = (Int.negOfNat n).rawCast / d.rawCast
source
def Mathlib.Tactic.RingNF.cleanup (cfg : Config) (r : Lean.Meta.Simp.Result) :
Lean.MetaM Lean.Meta.Simp.Result

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

Equations

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

Instances For

source
def Mathlib.Tactic.RingNF.ringNF :
Lean.ParserDescr

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 `!`)
  - `zetaDelta`: if true, local let variables can be unfolded (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.

This can be used non-terminally to normalize ring expressions in the goal such as `⊢ P (x + x + x)` ~> `⊢ 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)`.

Equations

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

Instances For

source
def Mathlib.Tactic.RingNF.tacticRing_nf!__ :
Lean.ParserDescr

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 `!`)
  - `zetaDelta`: if true, local let variables can be unfolded (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.

This can be used non-terminally to normalize ring expressions in the goal such as `⊢ P (x + x + x)` ~> `⊢ 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)`.

Equations

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

Instances For

source
def Mathlib.Tactic.RingNF.ringNFConv :
Lean.ParserDescr

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 `!`)
  - `zetaDelta`: if true, local let variables can be unfolded (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.

This can be used non-terminally to normalize ring expressions in the goal such as `⊢ P (x + x + x)` ~> `⊢ 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)`.

Equations

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

Instances For

source
def Mathlib.Tactic.RingNF.ring1NF :
Lean.ParserDescr

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.

Instances For

source
def Mathlib.Tactic.RingNF.tacticRing1_nf!_ :
Lean.ParserDescr

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.

Instances For

source
def Mathlib.Tactic.RingNF.elabRingNFConv :
Lean.Elab.Tactic.Tactic

Elaborator for the `ring_nf` tactic.

Equations

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

Instances For

source
def Mathlib.Tactic.RingNF.convRing_nf!_ :
Lean.ParserDescr

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 `!`)
  - `zetaDelta`: if true, local let variables can be unfolded (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.

This can be used non-terminally to normalize ring expressions in the goal such as `⊢ P (x + x + x)` ~> `⊢ 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)`.

Equations

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

Instances For

source
def Mathlib.Tactic.RingNF.ring :
Lean.ParserDescr

Tactic for evaluating expressions in commutative (semi)rings, allowing for variables in the exponent. If the goal is not appropriate for `ring` (e.g. not an equality) `ring_nf` will be suggested.

- `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!
    example (x : ℕ) (h : x * 2 > 5): x + x > 5 := by ring; assumption -- suggests ring_nf

Equations

- Mathlib.Tactic.RingNF.ring = Lean.ParserDescr.node `Mathlib.Tactic.RingNF.ring 1024 (Lean.ParserDescr.nonReservedSymbol "ring" false)

Instances For

source
def Mathlib.Tactic.RingNF.tacticRing! :
Lean.ParserDescr

Tactic for evaluating expressions in commutative (semi)rings, allowing for variables in the exponent. If the goal is not appropriate for `ring` (e.g. not an equality) `ring_nf` will be suggested.

- `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!
    example (x : ℕ) (h : x * 2 > 5): x + x > 5 := by ring; assumption -- suggests ring_nf

Equations

- Mathlib.Tactic.RingNF.tacticRing! = Lean.ParserDescr.node `Mathlib.Tactic.RingNF.tacticRing! 1024 (Lean.ParserDescr.nonReservedSymbol "ring!" false)

Instances For

source
def Mathlib.Tactic.RingNF.ringConv :
Lean.ParserDescr

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

- Mathlib.Tactic.RingNF.ringConv = Lean.ParserDescr.node `Mathlib.Tactic.RingNF.ringConv 1024 (Lean.ParserDescr.nonReservedSymbol "ring" false)

Instances For

source
def Mathlib.Tactic.RingNF.convRing! :
Lean.ParserDescr

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

- Mathlib.Tactic.RingNF.convRing! = Lean.ParserDescr.node `Mathlib.Tactic.RingNF.convRing! 1024 (Lean.ParserDescr.nonReservedSymbol "ring!" false)

Instances For

We register `ring` with the `hint` tactic.