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 * 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
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.

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
  • One or more equations did not get rendered due to their size.
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
source
instance Mathlib.Tactic.RingNF.instBEqRingMode :
BEq RingMode
Equations
source
instance Mathlib.Tactic.RingNF.instReprRingMode :
Repr RingMode
Equations
source
structure Mathlib.Tactic.RingNF.Config :
Type

Configuration for ring_nf.

  • red : Lean.Meta.TransparencyMode

    the reducibility setting to use when comparing atoms for defeq

  • recursive : Bool

    if true, atoms inside ring expressions will be reduced recursively

  • mode : RingMode

    The normalization style.

Instances For
source
instance Mathlib.Tactic.RingNF.instInhabitedConfig :
Inhabited Config
Equations
source
instance Mathlib.Tactic.RingNF.instBEqConfig :
BEq Config
Equations
source
instance Mathlib.Tactic.RingNF.instReprConfig :
Repr Config
Equations
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.
source
structure Mathlib.Tactic.RingNF.Context :
Type

The read-only state of the RingNF monad.

source
@[reducible, inline]
abbrev Mathlib.Tactic.RingNF.M (α : Type) :
Type

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
source
def Mathlib.Tactic.RingNF.rewrite (parent : Lean.Expr) (root : Bool := true) :
M Lean.Meta.Simp.Result

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.
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.rat_rawCast_pos {n d : ℕ} {R : Type u_2} [DivisionRing R] :
Rat.rawCast (Int.ofNat 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.M.run {α : Type} (s : IO.Ref AtomM.State) (cfg : Config) (x : M α) :
Lean.MetaM α

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.
source
partial def Mathlib.Tactic.RingNF.M.run.rctx (s : IO.Ref AtomM.State) (cfg : Config) (nctx : Context) :
AtomM.Context

The recursive context.

source
partial def Mathlib.Tactic.RingNF.M.run.evalAtom (s : IO.Ref AtomM.State) (cfg : Config) (nctx : Context) (e : Lean.Expr) :
Lean.MetaM Lean.Meta.Simp.Result

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

source
def Mathlib.Tactic.RingNF.ringNFTarget (s : IO.Ref AtomM.State) (cfg : Config) :
Lean.Elab.Tactic.TacticM Unit

Use ring_nf to rewrite the main goal.

Equations
  • One or more equations did not get rendered due to their size.
source
def Mathlib.Tactic.RingNF.ringNFLocalDecl (s : IO.Ref AtomM.State) (cfg : Config) (fvarId : Lean.FVarId) :
Lean.Elab.Tactic.TacticM Unit

Use ring_nf to rewrite hypothesis h.

Equations
  • One or more equations did not get rendered due to their size.
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 !)
    • 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.
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 !)
    • 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.
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 !)
    • 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.
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.
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.
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.
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 !)
    • 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.
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
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
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
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