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

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

True if this represents an atomic expression.

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

True if this represents an atomic expression.

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

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.

Configuration for ring_nf.

Equations

Function elaborating RingNF.Config.

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

The read-only state of the RingNF monad.

@[reducible, 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

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} [CommSemiring R] (a : R) (b : R) (c : R) :
a + (b + c) = a + b + c
theorem Mathlib.Tactic.RingNF.mul_assoc_rev {R : Type u_1} [CommSemiring R] (a : R) (b : R) (c : R) :
a * (b * c) = a * b * c
theorem Mathlib.Tactic.RingNF.mul_neg {R : Type u_2} [Ring R] (a : R) (b : R) :
a * -b = -(a * b)
theorem Mathlib.Tactic.RingNF.add_neg {R : Type u_2} [Ring R] (a : R) (b : R) :
a + -b = a - b
theorem Mathlib.Tactic.RingNF.nat_rawCast_2 {R : Type u_1} [CommSemiring R] {n : } [n.AtLeastTwo] :
n.rawCast = OfNat.ofNat n
theorem Mathlib.Tactic.RingNF.int_rawCast_neg {n : } {R : Type u_2} [Ring R] :
(Int.negOfNat n).rawCast = -n.rawCast
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
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

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.

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.

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.

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.

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.

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.

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.

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

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

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