ring tactic

A tactic for solving equations in commutative (semi)rings, where the exponents can also contain variables. Based on http://www.cs.ru.nl/~freek/courses/tt-2014/read/10.1.1.61.3041.pdf .

More precisely, expressions of the following form are supported:

• constants (non-negative integers)
• variables
• coefficients (any rational number, embedded into the (semi)ring)
• addition of expressions
• multiplication of expressions (a * b)
• scalar multiplication of expressions (n • a; the multiplier must have type ℕ or ℤ)
• exponentiation of expressions (the exponent must have type ℕ)
• subtraction and negation of expressions (if the base is a full ring)

The extension to exponents means that something like 2 * 2^n * b = b * 2^(n+1) can be proved, even though it is not strictly speaking an equation in the language of commutative rings.

Implementation notes

The basic approach to prove equalities is to normalise both sides and check for equality. We use Mathlib.Tactic.Ring.Common to implement the normal forms and normalization procedure.

This file defines the evaluation of basic operations such as addition and multipication of the rational coefficients as embedded inside the (semi)ring. This is done using norm_num.

It further implements the core ring1 tactic.

Caveats and future work

The normalized form of an expression is the one that is useful for the tactic, but not as nice to read. To remedy this, the user-facing normalization calls ringNFCore.

Subtraction cancels out identical terms, but division does not. That is: a - a = 0 := by ring solves the goal, but a / a := 1 by ring doesn't. Note that 0 / 0 is generally defined to be 0, so division cancelling out is not true in general.

Multiplication of powers can be simplified a little bit further: 2 ^ n * 2 ^ n = 4 ^ n := by ring could be implemented in a similar way that 2 * a + 2 * a = 4 * a := by ring already works. This feature wasn't needed yet, so it's not implemented yet.

Tags

ring, semiring, exponent, power

@[reducible]

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

ExBase BaseType sα e stores the structure of a normalized expression e, which appears as the base of an exponent expression e^n. The sum constructor is only used when the exponent n is not a constant.

Equations

• Mathlib.Tactic.Ring.ExBase sα = Mathlib.Tactic.Ring.Common.ExBase Mathlib.Tactic.Ring.RatCoeff sα

@[reducible]

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

ExProd BaseType sα e stores the structure of a normalized monomial expression e. A monomial here is a product of powers of ExBase expressions, terminated by a (nonzero) constant coefficient. The data of the constant coefficient is stored in the BaseType.

Equations

• Mathlib.Tactic.Ring.ExProd sα = Mathlib.Tactic.Ring.Common.ExProd Mathlib.Tactic.Ring.RatCoeff sα

@[reducible]

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

ExSum BaseType sα e stores the structure of a normalized polynomial expression e, which is a sum of monomials.

Equations

• Mathlib.Tactic.Ring.ExSum sα = Mathlib.Tactic.Ring.Common.ExSum Mathlib.Tactic.Ring.RatCoeff sα

theorem Mathlib.Tactic.Ring.cast_pos {R : Type u_1} [CommSemiring R] {a : R} {n : ℕ} : Meta.NormNum.IsNat a n → a = n.rawCast + 0

theorem Mathlib.Tactic.Ring.cast_zero {R : Type u_1} [CommSemiring R] {a : R} : Meta.NormNum.IsNat a 0 → a = 0

theorem Mathlib.Tactic.Ring.cast_neg {n : ℕ} {R : Type u_2} [Ring R] {a : R} : Meta.NormNum.IsInt a (Int.negOfNat n) → a = (Int.negOfNat n).rawCast + 0

theorem Mathlib.Tactic.Ring.cast_nnrat {n d : ℕ} {R : Type u_2} [DivisionSemiring R] {a : R} : Meta.NormNum.IsNNRat a n d → a = NNRat.rawCast n d + 0

theorem Mathlib.Tactic.Ring.cast_rat {n : ℤ} {d : ℕ} {R : Type u_2} [DivisionRing R] {a : R} : Meta.NormNum.IsRat a n d → a = Rat.rawCast n d + 0

def Mathlib.Tactic.Ring.ExProd.mkNat {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) (n : ℕ) : (e : Q(«$α»)) × ExProd sα e

Constructs the expression corresponding to .const n. (The .const constructor does not check that the expression is correct.)

def Mathlib.Tactic.Ring.ExProd.mkNegNat {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) : Q(Ring «$α») → (n : ℕ) → (e : Q(«$α»)) × ExProd sα e

Constructs the expression corresponding to .const (-n). (The .const constructor does not check that the expression is correct.)

def Mathlib.Tactic.Ring.ExProd.mkNNRat {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) : Q(DivisionSemiring «$α») → (q : ℚ) → (n d : Q(ℕ)) → (h : Lean.Expr) → (e : Q(«$α»)) × ExProd sα e

Constructs the expression corresponding to .const q h for q = n / d and h a proof that (d : α) ≠ 0. (The .const constructor does not check that the expression is correct.)

Equations

• Mathlib.Tactic.Ring.ExProd.mkNNRat sα x✝ q n d h = ⟨q(NNRat.rawCast «$n» «$d»), Mathlib.Tactic.Ring.Common.ExProd.const { value := q, hyp := some h }⟩

def Mathlib.Tactic.Ring.ExProd.mkNegNNRat {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) : Q(DivisionRing «$α») → (q : ℚ) → (n d : Q(ℕ)) → (h : Lean.Expr) → (e : Q(«$α»)) × ExProd sα e

Constructs the expression corresponding to .const q h for q = -(n / d) and h a proof that (d : α) ≠ 0. (The .const constructor does not check that the expression is correct.)

Equations

• Mathlib.Tactic.Ring.ExProd.mkNegNNRat sα x✝ q n d h = ⟨q(Rat.rawCast (Int.negOfNat «$n») «$d»), Mathlib.Tactic.Ring.Common.ExProd.const { value := q, hyp := some h }⟩

def Mathlib.Tactic.Ring.evalCast {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {e : Q(«$α»)} : Meta.NormNum.Result e → Option (Common.Result (ExSum sα) e)

Converts a proof by norm_num that e is a numeral, into a normalization as a monomial:

• e = 0 if norm_num returns IsNat e 0
• e = Nat.rawCast n + 0 if norm_num returns IsNat e n
• e = Int.rawCast n + 0 if norm_num returns IsInt e n
• e = NNRat.rawCast n d + 0 if norm_num returns IsNNRat e n d
• e = Rat.rawCast n d + 0 if norm_num returns IsRat e n d

Scalar multiplication by ℕ

theorem Mathlib.Tactic.Ring.natCast_nat {R : Type u_1} [CommSemiring R] (n : ℕ) : ↑n.rawCast = n.rawCast

theorem Mathlib.Tactic.Ring.natCast_mul {R : Type u_1} [CommSemiring R] {b₁ b₃ : R} {a₁ a₃ : ℕ} (a₂ : ℕ) : ↑a₁ = b₁ → ↑a₃ = b₃ → ↑(a₁ ^ a₂ * a₃) = b₁ ^ a₂ * b₃

theorem Mathlib.Tactic.Ring.natCast_zero {R : Type u_1} [CommSemiring R] : ↑0 = 0

theorem Mathlib.Tactic.Ring.natCast_add {R : Type u_1} [CommSemiring R] {b₁ b₂ : R} {a₁ a₂ : ℕ} : ↑a₁ = b₁ → ↑a₂ = b₂ → ↑(a₁ + a₂) = b₁ + b₂

partial def Mathlib.Tactic.Ring.ExBase.evalNatCast {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {v : Lean.Level} {β : Q(Type v)} (sβ : Q(CommSemiring «$β»)) {a : Q(ℕ)} (va : ExBase sβ a) : AtomM (Common.Result (ExBase sα) q(↑«$a»))

Applies Nat.cast to a nat polynomial to produce a polynomial in α.

• An atom e causes ↑e to be allocated as a new atom.
• A sum delegates to ExSum.evalNatCast.

partial def Mathlib.Tactic.Ring.ExProd.evalNatCast {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {v : Lean.Level} {β : Q(Type v)} (sβ : Q(CommSemiring «$β»)) {a : Q(ℕ)} (va : ExProd sβ a) : AtomM (Common.Result (ExProd sα) q(↑«$a»))

Applies Nat.cast to a nat monomial to produce a monomial in α.

• ↑c = c if c is a numeric literal
• ↑(a ^ n * b) = ↑a ^ n * ↑b

partial def Mathlib.Tactic.Ring.ExSum.evalNatCast {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {v : Lean.Level} {β : Q(Type v)} (sβ : Q(CommSemiring «$β»)) {a : Q(ℕ)} (va : ExSum sβ a) : AtomM (Common.Result (ExSum sα) q(↑«$a»))

Applies Nat.cast to a nat polynomial to produce a polynomial in α.

• ↑0 = 0
• ↑(a + b) = ↑a + ↑b

Scalar multiplication by ℤ

theorem Mathlib.Tactic.Ring.natCast_int {R : Type u_2} [CommRing R] (n : ℕ) : ↑n.rawCast = n.rawCast

theorem Mathlib.Tactic.Ring.intCast_negOfNat_Int {R : Type u_2} [CommRing R] (n : ℕ) : ↑(Int.negOfNat n).rawCast = (Int.negOfNat n).rawCast

theorem Mathlib.Tactic.Ring.intCast_mul {R : Type u_2} [CommRing R] {b₁ b₃ : R} {a₁ a₃ : ℤ} (a₂ : ℕ) : ↑a₁ = b₁ → ↑a₃ = b₃ → ↑(a₁ ^ a₂ * a₃) = b₁ ^ a₂ * b₃

theorem Mathlib.Tactic.Ring.intCast_zero {R : Type u_2} [CommRing R] : ↑0 = 0

theorem Mathlib.Tactic.Ring.intCast_add {R : Type u_2} [CommRing R] {b₁ b₂ : R} {a₁ a₂ : ℤ} : ↑a₁ = b₁ → ↑a₂ = b₂ → ↑(a₁ + a₂) = b₁ + b₂

def Mathlib.Tactic.Ring.ExBase.evalIntCast {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {v : Lean.Level} {β : Q(Type v)} (sβ : Q(CommSemiring «$β»)) {a : Q(ℤ)} (rα : Q(CommRing «$α»)) (va : ExBase sβ a) : AtomM (Common.Result (ExBase sα) q(↑«$a»))

Applies Int.cast to an int polynomial to produce a polynomial in α.

• An atom e causes ↑e to be allocated as a new atom.
• A sum delegates to ExSum.evalIntCast.

Equations

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

def Mathlib.Tactic.Ring.ExProd.evalIntCast {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {v : Lean.Level} {β : Q(Type v)} (sβ : Q(CommSemiring «$β»)) {a : Q(ℤ)} (rα : Q(CommRing «$α»)) (va : ExProd sβ a) : AtomM (Common.Result (ExProd sα) q(↑«$a»))

Applies Int.cast to an int monomial to produce a monomial in α.

• ↑c = c if c is a numeric literal
• ↑(a ^ n * b) = ↑a ^ n * ↑b

Equations

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

def Mathlib.Tactic.Ring.ExSum.evalIntCast {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {v : Lean.Level} {β : Q(Type v)} (sβ : Q(CommSemiring «$β»)) {a : Q(ℤ)} (rα : Q(CommRing «$α»)) (va : ExSum sβ a) : AtomM (Common.Result (ExSum sα) q(↑«$a»))

Applies Int.cast to an int polynomial to produce a polynomial in α.

• ↑0 = 0
• ↑(a + b) = ↑a + ↑b

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Ring.ExSum.evalIntCast sα sβ rα Mathlib.Tactic.Ring.Common.ExSum.zero = pure { expr := q(0), val := Mathlib.Tactic.Ring.Common.ExSum.zero, proof := q(⋯) }

def Mathlib.Tactic.Ring.ExBase.cast {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {v : Lean.Level} {β : Q(Type v)} {sβ : Q(CommSemiring «$β»)} {a : Q(«$α»)} : ExBase sα a → (a : Q(«$β»)) × ExBase sβ a

Converts ExBase sα to ExBase sβ, assuming sα and sβ are defeq.

Equations

• Mathlib.Tactic.Ring.ExBase.cast sα (Mathlib.Tactic.Ring.Common.ExBase.atom i) = ⟨a, Mathlib.Tactic.Ring.Common.ExBase.atom i⟩
• Mathlib.Tactic.Ring.ExBase.cast sα (Mathlib.Tactic.Ring.Common.ExBase.sum a_1) = match Mathlib.Tactic.Ring.ExSum.cast sα a_1 with | ⟨fst, vb⟩ => ⟨fst, Mathlib.Tactic.Ring.Common.ExBase.sum vb⟩

def Mathlib.Tactic.Ring.ExProd.cast {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {v : Lean.Level} {β : Q(Type v)} {sβ : Q(CommSemiring «$β»)} {a : Q(«$α»)} : ExProd sα a → (a : Q(«$β»)) × ExProd sβ a

Converts ExProd sα to ExProd sβ, assuming sα and sβ are defeq.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Ring.ExProd.cast sα (Mathlib.Tactic.Ring.Common.ExProd.const { value := i, hyp := h }) = ⟨a, Mathlib.Tactic.Ring.Common.ExProd.const { value := i, hyp := h }⟩

def Mathlib.Tactic.Ring.ExSum.cast {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {v : Lean.Level} {β : Q(Type v)} {sβ : Q(CommSemiring «$β»)} {a : Q(«$α»)} : ExSum sα a → (a : Q(«$β»)) × ExSum sβ a

Converts ExSum sα to ExSum sβ, assuming sα and sβ are defeq.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Ring.ExSum.cast sα Mathlib.Tactic.Ring.Common.ExSum.zero = ⟨q(0), Mathlib.Tactic.Ring.Common.ExSum.zero⟩

theorem Mathlib.Tactic.Ring.smul_eq_mul {α : Type u_2} [Mul α] {a a' : α} (h : a = a') (b : α) : a • b = a' * b

theorem Mathlib.Tactic.Ring.Nat.smul_eq_mul {R : Type u_1} [CommSemiring R] {n n' : ℕ} {r : R} (hr : ↑n = r) (hn : n' = n) (a : R) : n' • a = r * a

theorem Mathlib.Tactic.Ring.Int.smul_eq_mul {R : Type u_1} {n n' : ℤ} {r : R} [CommRing R] (hr : ↑n = r) (hn : n' = n) (a : R) : n' • a = r * a

def Mathlib.Tactic.Ring.RatCoeff.toResult {u : Lean.Level} {α : Q(Type u)} {a : Q(«$α»)} : RatCoeff a → Meta.NormNum.Result a

Turn coefficient data into a NormNum.Result.

Equations

• { value := q, hyp := h }.toResult = Mathlib.Meta.NormNum.Result.ofRawRat q a h

def Mathlib.Tactic.Ring.RatCoeff.ofResult {u : Lean.Level} {α : Q(Type u)} {a : Q(«$α»)} (res : Meta.NormNum.Result a) : Option (Common.Result RatCoeff a)

Turn a NormNum.Result into coefficient data.

Equations

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

def Mathlib.Tactic.Ring.RingCompute.add {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {a b : Q(«$α»)} (za : RatCoeff a) (zb : RatCoeff b) : Lean.MetaM (Common.Result RatCoeff q(«$a» + «$b») × Option Q(Meta.NormNum.IsNat («$a» + «$b») 0))

Add two rational number expressions. If the result is zero, returns a proof of this fact.

Equations

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

def Mathlib.Tactic.Ring.RingCompute.mul {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {a b : Q(«$α»)} (za : RatCoeff a) (zb : RatCoeff b) : Lean.MetaM (Common.Result RatCoeff q(«$a» * «$b»))

Evaluate the product of two rational number expressions.

Equations

• Mathlib.Tactic.Ring.RingCompute.mul sα za zb = do let res ← za.toResult.mul zb.toResult q(«$sα».toSemiring) let __do_lift ← liftM (Mathlib.Tactic.Ring.RatCoeff.ofResult res) pure __do_lift

partial def Mathlib.Tactic.Ring.RingCompute.cast {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) (cα : Common.Cache sα) (v : Lean.Level) (β : Q(Type v)) (sβ : Q(CommSemiring «$β»)) (_smul : Q(SMul «$β» «$α»)) (x : Q(«$β»)) : AtomM ((y : Q(«$α»)) × Common.ExSum RatCoeff sα q(«$y») × Q(∀ (a : «$α»), «$x» • a = «$y» * a))

Cast ℕ and ℤ normalized expressions ExSums into α, used to evaluate scalar multiplications.

def Mathlib.Tactic.Ring.RingCompute.neg {u : Lean.Level} {α : Q(Type u)} {a : Q(«$α»)} (_crα : Q(CommRing «$α»)) (za : RatCoeff a) : Lean.MetaM (Common.Result RatCoeff q(-«$a»))

Negate rational number expressions.

Equations

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

def Mathlib.Tactic.Ring.RingCompute.pow {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {a : Q(«$α»)} {b : Q(ℕ)} (za : RatCoeff a) (vb : Common.ExProdNat q(«$b»)) : OptionT Lean.MetaM (Common.Result RatCoeff q(«$a» ^ «$b»))

Raise a rational number expression to the power of a natural number.

Fails if the exponent is not a literal.

def Mathlib.Tactic.Ring.RingCompute.inv {u : Lean.Level} {α : Q(Type u)} (_sα : Q(CommSemiring «$α»)) {a : Q(«$α»)} (czα : Option Q(CharZero «$α»)) (_sfα : Q(Semifield «$α»)) (za : RatCoeff a) : AtomM (Option (Common.Result RatCoeff q(«$a»⁻¹)))

Evaluate the inverse of a natural number expression.

Equations

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

def Mathlib.Tactic.Ring.RingCompute.derive {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) (x : Q(«$α»)) : Lean.MetaM (Common.Result (Common.ExSum RatCoeff sα) q(«$x»))

Try to evaluate an expression as a rational constant using norm_num.

Equations

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

def Mathlib.Tactic.Ring.RingCompute.isOne {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {x : Q(«$α»)} (zx : RatCoeff x) : Option Q(Meta.NormNum.IsNat «$x» 1)

Decide if x is 1 and provide a proof if so.

Equations

• Mathlib.Tactic.Ring.RingCompute.isOne sα { value := q, hyp := h } = if (q == 1) = true then have this := ⋯; pure q(⋯) else failure

def Mathlib.Tactic.Ring.ringCompare {u : Lean.Level} {α : Q(Type u)} : Common.RingCompare RatCoeff

The comarisons on the basetype used to compare normalized ring expressions.

Equations

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

partial def Mathlib.Tactic.Ring.ringCompute {u : Lean.Level} {α : Q(Type u)} {sα : Q(CommSemiring «$α»)} (cα : Common.Cache sα) : Common.RingCompute RatCoeff sα

The data used by the ring tactic to normalize the constant coefficients.

def Mathlib.Tactic.Ring.rcℕ : Common.RingCompute Common.btℕ Common.sℕ

The data used by ring-like tactics to normalize constant coefficients of natural number expressions.

Equations

• Mathlib.Tactic.Ring.rcℕ = Mathlib.Tactic.Ring.ringCompute Mathlib.Tactic.Ring.Common.Cache.nat

class Mathlib.Tactic.Ring.CSLift (α : Type u) (β : outParam (Type u)) : Type u

CSLift α β is a typeclass used by ring for lifting operations from α (which is not a commutative semiring) into a commutative semiring β by using an injective map lift : α → β.

• lift : α → β

  lift is the "canonical injection" from α to β

• inj : Function.Injective lift

  lift is an injective function

class Mathlib.Tactic.Ring.CSLiftVal {α : Type u} {β : outParam (Type u)} [CSLift α β] (a : α) (b : outParam β) : Prop

CSLiftVal a b means that b = lift a. This is used by ring to construct an expression b from the input expression a, and then run the usual ring algorithm on b.

• eq : b = CSLift.lift a

  The output value b is equal to the lift of a. This can be supplied by the default instance which sets b := lift a, but ring will treat this as an atom so it is more useful when there are other instances which distribute addition or multiplication.

@[instance 100]

instance Mathlib.Tactic.Ring.instCSLiftValLift {α β : Type u_2} [CSLift α β] (a : α) : CSLiftVal a (CSLift.lift a)

theorem Mathlib.Tactic.Ring.of_lift {α β : Type u_2} [inst : CSLift α β] {a b : α} {a' b' : β} [h1 : CSLiftVal a a'] [h2 : CSLiftVal b b'] (h : a' = b') : a = b

theorem Mathlib.Tactic.Ring.of_eq {α : Sort u_2} {a b c : α} : a = c → b = c → a = b

opaque Mathlib.Tactic.Ring.ringCleanupRef : IO.Ref (Lean.Expr → Lean.MetaM Lean.Expr)

This is a routine which is used to clean up the unsolved subgoal of a failed ring1 application. It is overridden in Mathlib/Tactic/Ring/RingNF.lean to apply the ring_nf simp set to the goal.

def Mathlib.Tactic.Ring.proveEq (g : Lean.MVarId) : AtomM Unit

Frontend of ring1: attempt to close a goal g, assuming it is an equation of semirings.

Equations

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

def Mathlib.Tactic.Ring.ring1 : Lean.ParserDescr

ring1 solves the goal when it is an equality in commutative (semi)rings, allowing variables in the exponent.

This version of ring fails if the target is not an equality.

• ring1! uses a more aggressive reducibility setting to determine equality of atoms.

Equations

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

def Mathlib.Tactic.Ring.tacticRing1! : Lean.ParserDescr

ring1 solves the goal when it is an equality in commutative (semi)rings, allowing variables in the exponent.

This version of ring fails if the target is not an equality.

• ring1! uses a more aggressive reducibility setting to determine equality of atoms.

Equations

• Mathlib.Tactic.Ring.tacticRing1! = Lean.ParserDescr.node `Mathlib.Tactic.Ring.tacticRing1! 1024 (Lean.ParserDescr.nonReservedSymbol "ring1!" false)