ring-like tactics

The core normalization procedure for ring-like tactics that solve 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 (living in BaseType; for ring this is a rational embedded into the semiring)
• addition of expressions
• multiplication of expressions (a * b)
• scalar multiplication of expressions (r • a)
• 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. The normalisation is guided by building a value in the type ExSum at the meta level, together with a proof (at the base level) that the original value is equal to the normalised version.

The outline of the file:

• Define a mutual inductive family of types ExSum, ExProd, ExBase, which can represent expressions with +, *, ^ and some parametric BaseType. The mutual induction ensures that associativity and distributivity are applied, by restricting which kinds of subexpressions appear as arguments to the various operators.
• Represent addition, multiplication and exponentiation in the ExSum type, thus allowing us to map expressions to ExSum (the eval function drives this). We apply associativity and distributivity of the operators here (helped by Ex* types) and commutativity as well (by sorting the subterms; unfortunately not helped by anything). Any expression not of the above formats is treated as an atom (the same as a variable).

There are some details we glossed over which make the plan more complicated:

• The order on atoms is not initially obvious. We construct a list containing them in order of initial appearance in the expression, then use the index into the list as a key to order on.
• For pow, the exponent must be a natural number, while the base can be any semiring α. We swap out operations for the base ring α with those for the exponent ring ℕ as soon as we deal with exponents. Unfortunately this has to be done with a separate inductive type due to universe issues outlined later in this file.

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

def Mathlib.Tactic.Ring.Common.sℕ : Q(CommSemiring ℕ)

A typed expression of type CommSemiring ℕ used when we are working on ring subexpressions of type ℕ.

Equations

• Mathlib.Tactic.Ring.Common.sℕ = q(Nat.instCommSemiring)

structure Mathlib.Tactic.Ring.RatCoeff {u : Lean.Level} {α : Q(Type u)} (e : Q(«$α»)) : Type

The data used by ring to represent coefficients. e is a raw rat cast.

We include e as a parameter even though it is unused in this definition because it lets us use Qq type annotations in the RingCompute structure, and so that it can be used with the Result type defined below.

• value : ℚ

  The value represented by e. Should not be zero.

• hyp : Option Lean.Expr

  If value is not an integer, then hyp should be a proof of (value.den : α) ≠ 0.

@[implicit_reducible]

instance Mathlib.Tactic.Ring.Common.instInhabitedRatCoeff {a✝ : Lean.Level} {a✝¹ : Q(Type a✝)} {a✝² : Q($a✝)} : Inhabited (RatCoeff a✝²)

Equations

• Mathlib.Tactic.Ring.Common.instInhabitedRatCoeff = { default := Mathlib.Tactic.Ring.Common.instInhabitedRatCoeff.default }

def Mathlib.Tactic.Ring.Common.instInhabitedRatCoeff.default {a✝ : Lean.Level} {a✝¹ : Q(Type a✝)} {a✝² : Q($a✝)} : RatCoeff a✝²

Equations

• Mathlib.Tactic.Ring.Common.instInhabitedRatCoeff.default = { value := default, hyp := default }

@[reducible, inline]

abbrev Mathlib.Tactic.Ring.Common.btℕ (e : Q(ℕ)) : Type

The data used to represent coefficients in exponents. This is the same data that ring uses.

Equations

• Mathlib.Tactic.Ring.Common.btℕ e = Mathlib.Tactic.Ring.RatCoeff q(«$e»)

@[implicit_reducible]

instance Mathlib.Tactic.Ring.Common.instInhabitedBtℕ (e : Lean.Expr) : Inhabited (btℕ e)

Equations

• Mathlib.Tactic.Ring.Common.instInhabitedBtℕ e = { default := { value := 0, hyp := none } }

The ExNat types

The Ex{Base,Prod,Sum}Nat types are equivalent to Ex{Base,Prod,Sum} btℕ sℕ. ExProdNat is only used to represent exponents in ExProds. We cannot use ExProd btℕ sℕ in the mul constructor of ExProd because BaseType is a parameter and not an index. Making BaseType an index (i.e. moving it to the right of the colon) would require including it as an argument to each constructor, raising the universe level of ExProd from Type to Type 1; that is:

inductive ExProd : ∀ {u : Lean.Level} {α : Q(Type u)} (BaseType : Q($α) → Type)
    (sα : Q(CommSemiring $α)) (e : Q($α)), Type
  | const {u : Lean.Level} {α : Q(Type u)} {BaseType} {sα} {e : Q($α)} (value : BaseType e) :
      ExProd BaseType sα e
  | mul {u : Lean.Level} {α : Q(Type u)} {BaseType} {sα} {x : Q($α)} {e : Q(ℕ)} {b : Q($α)} :
    ExBase BaseType sα x → ExProd btℕ sℕ e → ExProd BaseType sα b →
      ExProd BaseType sα q($x ^ $e * $b)

would fail to compile because ExProd lives in Type 1.

Lean does not support monadic computation in Type 1 in its core monad types, so we cannot tolerate this universe bump.

inductive Mathlib.Tactic.Ring.Common.ExBaseNat (e : Q(ℕ)) : Type

ExBaseNat e stores the structure of a normalized expression e : Q(ℕ), 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.

Used to represent normalized natural number expressions in exponents.

ExBaseNat q($e) is equivalent to ExBase btℕ sℕ q($e), and one can cast between the two.

• atom {e : Q(ℕ)} (id : ℕ) : ExBaseNat e

  An atomic expression e with id id.

  Atomic expressions are those which ring cannot parse any further. For instance, a + (a % b) has a and (a % b) as atoms. The ring1 tactic does not normalize the subexpressions in atoms, but ring_nf does.

  Atoms in fact represent equivalence classes of expressions, modulo definitional equality. The field index : ℕ should be a unique number for each class, while e : Q($α) contains a representative of this class.

• sum {e : Q(ℕ)} : ExSumNat e → ExBaseNat e

  A sum of monomials.

inductive Mathlib.Tactic.Ring.Common.ExProdNat (e : Q(ℕ)) : Type

ExProdNat e stores the structure of a normalized monomial expression e : Q(ℕ). A monomial here is a product of powers of ExBaseNat expressions, terminated by a (nonzero) constant coefficient.

Used to represent normalized natural number expressions in exponents.

ExProdNat q($e) is equivalent to ExProd btℕ sℕ q($e), and one can cast between the two.

• const {e : Q(ℕ)} (value : btℕ e) : ExProdNat e

  A coefficient value, holding the data that ring uses to represent rational coefficients. In this case these happen to always be natural numbers.

• mul {x e b : Q(ℕ)} : ExBaseNat x → ExProdNat e → ExProdNat b → ExProdNat q(«$x» ^ «$e» * «$b»)

  A product x ^ e * b is a monomial if b is a monomial. Here x is an ExBaseNat and e is an ExProdNat representing a monomial expression in ℕ (it is a monomial instead of a polynomial because we eagerly normalize x ^ (a + b) = x ^ a * x ^ b.)

inductive Mathlib.Tactic.Ring.Common.ExSumNat (e : Q(ℕ)) : Type

ExSumNat e stores the structure of a normalized polynomial expression e : Q(ℕ), which is a sum of monomials.

Used to represent normalized natural number expressions in exponents.

ExSumNat q($e) is equivalent to ExSum btℕ sℕ q($e), and one can cast between the two.

• zero : ExSumNat q(0)

  Zero is a polynomial. e is the expression 0.

• add {a b : Q(ℕ)} : ExProdNat a → ExSumNat b → ExSumNat q(«$a» + «$b»)

  A sum a + b is a polynomial if a is a monomial and b is another polynomial.

The BaseType parameter is used to specify how constant coefficients are stored. In the ring tactic we need only to store coefficients as normalizations to rational numbers, but in a future algebra tactic the base type may itself be a normalized ring expression.

inductive Mathlib.Tactic.Ring.Common.ExBase {u : Lean.Level} {α : Q(Type u)} (BaseType : Q(«$α») → Type) (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.

• atom {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {e : Q(«$α»)} (id : ℕ) : ExBase BaseType sα e

  An atomic expression e with id id.

  Atomic expressions are those which a ring-like tactic cannot parse any further. For instance, a + (a % b) has a and (a % b) as atoms. The ring1 tactic does not normalize the subexpressions in atoms, but ring_nf does.

  Atoms in fact represent equivalence classes of expressions, modulo definitional equality. The field index : ℕ should be a unique number for each class, while e : Q($α) contains a representative of this class.

• sum {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {e : Q(«$α»)} : ExSum BaseType sα e → ExBase BaseType sα e

  A sum of monomials.

inductive Mathlib.Tactic.Ring.Common.ExProd {u : Lean.Level} {α : Q(Type u)} (BaseType : Q(«$α») → Type) (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.

• const {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {e : Q(«$α»)} (value : BaseType e) : ExProd BaseType sα e

  A coefficient value, which must not be 0. e is a raw rat cast. If value is not an integer, then hyp should be a proof of (value.den : α) ≠ 0.

• mul {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {x : Q(«$α»)} {e : Q(ℕ)} {b : Q(«$α»)} : ExBase BaseType sα x → ExProdNat e → ExProd BaseType sα b → ExProd BaseType sα q(«$x» ^ «$e» * «$b»)

  A product x ^ e * b is a monomial if b is a monomial. Here x is an ExBase and e is an ExProdNat representing a monomial expression in ℕ (it is a monomial instead of a polynomial because we eagerly normalize x ^ (a + b) = x ^ a * x ^ b.)

inductive Mathlib.Tactic.Ring.Common.ExSum {u : Lean.Level} {α : Q(Type u)} (BaseType : Q(«$α») → Type) (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.

• zero {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} : ExSum BaseType sα q(0)

  Zero is a polynomial. e is the expression 0.

• add {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {a b : Q(«$α»)} : ExProd BaseType sα a → ExSum BaseType sα b → ExSum BaseType sα q(«$a» + «$b»)

  A sum a + b is a polynomial if a is a monomial and b is another polynomial.

structure Mathlib.Tactic.Ring.Common.Result {u : Lean.Level} {α : Q(Type u)} (E : Q(«$α») → Type u_1) (e : Q(«$α»)) : Type u_1

The result of evaluating an (unnormalized) expression e into the type family E (typically one of ExSum, ExProd, ExBase or BaseType) is a (normalized) element e' and a representation E e' for it, and a proof of e = e'.

• expr : Q(«$α»)

  The normalized result.

• val : E self.expr

  The data associated to the normalization.

• proof : Q(«$e» = unknown_1)

  A proof that the original expression is equal to the normalized result.

@[implicit_reducible]

instance Mathlib.Tactic.Ring.Common.instInhabitedResultOfSigmaQuoted {u : Lean.Level} {α : Q(Type u)} {E : Q(«$α») → Type} {e : Q(«$α»)} [Inhabited ((e : Q(«$α»)) × E e)] : Inhabited (Result E e)

Equations

• Mathlib.Tactic.Ring.Common.instInhabitedResultOfSigmaQuoted = match default with | ⟨e', v⟩ => { default := { expr := e', val := v, proof := default } }

structure Mathlib.Tactic.Ring.Common.RingCompare {u : Lean.Level} {α : Q(Type u)} (BaseType : Q(«$α») → Type) : Type

Defines how comparisons and binary equality are computed in the base type. These are seperated from RingCompute because they can often be defined without using instance caches.

• eq {x y : Q(«$α»)} : BaseType x → BaseType y → Bool

  Returns whether two coefficients are equal

• compare {x y : Q(«$α»)} : BaseType x → BaseType y → Ordering

  Returns whether x is less than, equal to or greater than y. Can be any total order.

structure Mathlib.Tactic.Ring.Common.RingCompute {u : Lean.Level} {α : Q(Type u)} (BaseType : Q(«$α») → Type) (sα : Q(CommSemiring «$α»)) extends Mathlib.Tactic.Ring.Common.RingCompare BaseType : Type

Stores all of the normalization procedures on the coefficient type.

ring implements these using norm_num algebra will implement these using ring

• eq {x y : Q(«$α»)} : BaseType x → BaseType y → Bool
• compare {x y : Q(«$α»)} : BaseType x → BaseType y → Ordering
• add {x y : Q(«$α»)} : BaseType x → BaseType y → Lean.MetaM (Result BaseType q(«$x» + «$y») × Option Q(Meta.NormNum.IsNat («$x» + «$y») 0))

  Evaluate the sum of two coefficents.

  If the result is zero returns a proof of this fact, which is used to remove zero terms.

• mul {x y : Q(«$α»)} : BaseType x → BaseType y → Lean.MetaM (Result BaseType q(«$x» * «$y»))

  Evaluate the product of two coefficents.

• cast (v : Lean.Level) (β : Q(Type v)) : Q(CommSemiring «$β») → (x✝ : Q(SMul «$β» «$α»)) → (x : Q(«$β»)) → AtomM ((y : Q(«$α»)) × ExSum BaseType sα q(«$y») × Q(∀ (a : «$α»), «$x» • a = «$y» * a))

  Given a commutative ring β with a scalar multiplication action on α and a x : β, cast x to α such that the scalar multiplication turns into normal multiplication. Typically one can think of α as being an algebra over β, but this file does not know about Algebras.

• neg {x : Q(«$α»)} (rα : Q(CommRing «$α»)) : BaseType x → Lean.MetaM (Result BaseType q(-«$x»))

  Evaluate the negation of a coefficient.

• pow {x : Q(«$α»)} {b : Q(ℕ)} : BaseType x → (vb : ExProdNat q(«$b»)) → OptionT Lean.MetaM (Result BaseType q(«$x» ^ «$b»))

  Raise a coefficient to some natural power.

  The exponent is not necessarily a natural literal. If the tactic can only raise coefficients to the power of a literal (e.g. ring), it should check for this and return none otherwise.

• inv {x : Q(«$α»)} (czα : Option Q(CharZero «$α»)) (fα : Q(Semifield «$α»)) : BaseType x → AtomM (Option (Result BaseType q(«$x»⁻¹)))

  Evaluate the inverse of a coefficient.

• derive (x : Q(«$α»)) : Lean.MetaM (Result (ExSum BaseType sα) q(«$x»))

  Evaluate an expression as a potential coefficient.

• isOne {x : Q(«$α»)} : BaseType x → Option Q(Meta.NormNum.IsNat «$x» 1)

  Decides whether a coefficient is 1 and returns a proof if so.

• one : Result BaseType q(Nat.rawCast 1)

  The number 1 represented as a BaseType.

@[implicit_reducible]

instance Mathlib.Tactic.Ring.Common.instCoeOutRingComputeRingCompare {u : Lean.Level} {α : Q(Type u)} (BaseType : Q(«$α») → Type) (sα : Q(CommSemiring «$α»)) : CoeOut (RingCompute BaseType sα) (RingCompare BaseType)

Equations

• Mathlib.Tactic.Ring.Common.instCoeOutRingComputeRingCompare BaseType sα = { coe := fun (x : Mathlib.Tactic.Ring.Common.RingCompute BaseType sα) => x.toRingCompare }

instance Mathlib.Tactic.Ring.Common.instNonemptyRingCompute (u : Lean.Level) (α : Q(Type u)) (BaseType : Q(«$α») → Type) [∀ (e : Q(«$α»)), Nonempty (BaseType e)] (sα : Q(CommSemiring «$α»)) : Nonempty (RingCompute BaseType sα)

@[implicit_reducible]

instance Mathlib.Tactic.Ring.Common.instInhabitedSigmaQuotedConstMkStr1NilLevelExBaseNat : Inhabited ((e : Q(ℕ)) × ExBaseNat e)

Equations

• Mathlib.Tactic.Ring.Common.instInhabitedSigmaQuotedConstMkStr1NilLevelExBaseNat = { default := ⟨default, Mathlib.Tactic.Ring.Common.ExBaseNat.atom 0⟩ }

@[implicit_reducible]

instance Mathlib.Tactic.Ring.Common.instInhabitedSigmaQuotedConstMkStr1NilLevelExSumNat : Inhabited ((e : Q(ℕ)) × ExSumNat e)

Equations

• Mathlib.Tactic.Ring.Common.instInhabitedSigmaQuotedConstMkStr1NilLevelExSumNat = { default := ⟨q(0), Mathlib.Tactic.Ring.Common.ExSumNat.zero⟩ }

@[implicit_reducible]

instance Mathlib.Tactic.Ring.Common.instInhabitedSigmaQuotedConstMkStr1NilLevelExProdNat : Inhabited ((e : Q(ℕ)) × ExProdNat e)

Equations

• Mathlib.Tactic.Ring.Common.instInhabitedSigmaQuotedConstMkStr1NilLevelExProdNat = { default := ⟨default, Mathlib.Tactic.Ring.Common.ExProdNat.const default⟩ }

@[implicit_reducible]

instance Mathlib.Tactic.Ring.Common.instInhabitedSigmaQuotedExBase {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} : Inhabited ((e : Q(«$α»)) × ExBase bt sα e)

Equations

• Mathlib.Tactic.Ring.Common.instInhabitedSigmaQuotedExBase = { default := ⟨default, Mathlib.Tactic.Ring.Common.ExBase.atom 0⟩ }

@[implicit_reducible]

instance Mathlib.Tactic.Ring.Common.instInhabitedSigmaQuotedExSum {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} : Inhabited ((e : Q(«$α»)) × ExSum bt sα e)

Equations

• Mathlib.Tactic.Ring.Common.instInhabitedSigmaQuotedExSum = { default := ⟨q(0), Mathlib.Tactic.Ring.Common.ExSum.zero⟩ }

@[implicit_reducible]

instance Mathlib.Tactic.Ring.Common.instInhabitedSigmaQuotedExProd {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} [(e : Q(«$α»)) → Inhabited (bt e)] : Inhabited ((e : Q(«$α»)) × ExProd bt sα e)

Equations

• Mathlib.Tactic.Ring.Common.instInhabitedSigmaQuotedExProd = { default := ⟨default, Mathlib.Tactic.Ring.Common.ExProd.const default⟩ }

partial def Mathlib.Tactic.Ring.Common.ExBaseNat.toExBase (e : Q(ℕ)) : ExBaseNat e → (e' : Q(ℕ)) × ExBase btℕ sℕ e'

Cast ExBaseNat to ExBase btℕ sℕ.

partial def Mathlib.Tactic.Ring.Common.ExProdNat.toExProd (e : Q(ℕ)) : ExProdNat e → (e' : Q(ℕ)) × ExProd btℕ sℕ e'

Cast ExProdNat to ExProd btℕ sℕ.

partial def Mathlib.Tactic.Ring.Common.ExSumNat.toExSum (e : Q(ℕ)) : ExSumNat e → (e' : Q(ℕ)) × ExSum btℕ sℕ e'

Cast ExSumNat to ExSum btℕ sℕ.

partial def Mathlib.Tactic.Ring.Common.ExBase.toExBaseNat (e : Q(ℕ)) : ExBase btℕ sℕ e → (e' : Q(ℕ)) × ExBaseNat e'

Cast ExBase btℕ sℕ to ExBaseNat.

partial def Mathlib.Tactic.Ring.Common.ExProd.toExProdNat (e : Q(ℕ)) : ExProd btℕ sℕ e → (e' : Q(ℕ)) × ExProdNat e'

Cast ExProd btℕ sℕ to ExProdNat.

partial def Mathlib.Tactic.Ring.Common.ExSum.toExSumNat (e : Q(ℕ)) : ExSum btℕ sℕ e → (e' : Q(ℕ)) × ExSumNat e'

Cast ExSum btℕ sℕ to ExSumNat.

def Mathlib.Tactic.Ring.Common.ExBase.toProd {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) {a : Q(«$α»)} {b : Q(ℕ)} (va : ExBase bt sα a) (vb : ExProdNat b) : Result (ExProd bt sα) q(«$a» ^ «$b» * Nat.rawCast 1)

Embed an exponent (an ExBase, ExProd pair) as an ExProd by multiplying by 1.

Equations

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

def Mathlib.Tactic.Ring.Common.ExProd.toSum {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {e : Q(«$α»)} (v : ExProd bt sα e) : ExSum bt sα q(«$e» + 0)

Embed ExProd in ExSum by adding 0.

Equations

• v.toSum = Mathlib.Tactic.Ring.Common.ExSum.add v Mathlib.Tactic.Ring.Common.ExSum.zero

partial def Mathlib.Tactic.Ring.Common.ExBase.eq (rcℕ : RingCompare btℕ) {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompare bt) {a b : Q(«$α»)} : ExBase bt sα a → ExBase bt sα b → Bool

Equality test for expressions. This is not a BEq instance because it is heterogeneous.

partial def Mathlib.Tactic.Ring.Common.ExProd.eq (rcℕ : RingCompare btℕ) {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompare bt) {a b : Q(«$α»)} : ExProd bt sα a → ExProd bt sα b → Bool

Equality test for expressions. This is not a BEq instance because it is heterogeneous.

partial def Mathlib.Tactic.Ring.Common.ExSum.eq (rcℕ : RingCompare btℕ) {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompare bt) {a b : Q(«$α»)} : ExSum bt sα a → ExSum bt sα b → Bool

Equality test for expressions. This is not a BEq instance because it is heterogeneous.

partial def Mathlib.Tactic.Ring.Common.ExBase.cmp (rcℕ : RingCompute btℕ sℕ) {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompare bt) {a b : Q(«$α»)} : ExBase bt sα a → ExBase bt sα b → Ordering

A total order on normalized expressions. This is not an Ord instance because it is heterogeneous.

partial def Mathlib.Tactic.Ring.Common.ExProd.cmp (rcℕ : RingCompute btℕ sℕ) {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompare bt) {a b : Q(«$α»)} : ExProd bt sα a → ExProd bt sα b → Ordering

A total order on normalized expressions. This is not an Ord instance because it is heterogeneous.

partial def Mathlib.Tactic.Ring.Common.ExSum.cmp (rcℕ : RingCompute btℕ sℕ) {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompare bt) {a b : Q(«$α»)} : ExSum bt sα a → ExSum bt sα b → Ordering

A total order on normalized expressions. This is not an Ord instance because it is heterogeneous.

def Mathlib.Tactic.Ring.Common.ExProd.coeff {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} [(e : Q(«$α»)) → Inhabited (bt e)] {e : Q(«$α»)} : have this := { default := ⟨default, default⟩ }; ExProd bt sα e → (c : Q(«$α»)) × bt c

Get the leading coefficient of an ExProd.

Equations

• (Mathlib.Tactic.Ring.Common.ExProd.const q).coeff = ⟨e, q⟩
• (Mathlib.Tactic.Ring.Common.ExProd.mul a a_1 v).coeff = v.coeff

inductive Mathlib.Tactic.Ring.Common.Overlap {u : Lean.Level} {α : Q(Type u)} (bt : Q(«$α») → Type) (sα : Q(CommSemiring «$α»)) (e : Q(«$α»)) : Type

Two monomials are said to "overlap" if they differ by a constant factor, in which case the constants just add. When this happens, the constant may be either zero (if the monomials cancel) or nonzero (if they add up); the zero case is handled specially.

• zero {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {e : Q(«$α»)} : Q(Meta.NormNum.IsNat «$e» 0) → Overlap bt sα e

  The expression e (the sum of monomials) is equal to 0.

• nonzero {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {e : Q(«$α»)} : Result (ExProd bt sα) e → Overlap bt sα e

  The expression e (the sum of monomials) is equal to another monomial (with nonzero leading coefficient).

Addition

theorem Mathlib.Tactic.Ring.Common.add_overlap_pf {R : Type u_1} [CommSemiring R] {a b c : R} (x : R) (e : ℕ) (pq_pf : a + b = c) : x ^ e * a + x ^ e * b = x ^ e * c

theorem Mathlib.Tactic.Ring.Common.add_overlap_pf_zero {R : Type u_1} [CommSemiring R] {a b : R} (x : R) (e : ℕ) : Meta.NormNum.IsNat (a + b) 0 → Meta.NormNum.IsNat (x ^ e * a + x ^ e * b) 0

def Mathlib.Tactic.Ring.Common.evalAddOverlap {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) (rcℕ : RingCompute btℕ sℕ) {a b : Q(«$α»)} (va : ExProd bt sα a) (vb : ExProd bt sα b) : OptionT Lean.MetaM (Overlap bt sα q(«$a» + «$b»))

Given monomials va, vb, attempts to add them together to get another monomial. If the monomials are not compatible, returns none. For example, xy + 2xy = 3xy is a .nonzero overlap, while xy + xz returns none and xy + -xy = 0 is a .zero overlap.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Ring.Common.evalAddOverlap rc rcℕ va vb = do liftM (Lean.checkSystem `Mathlib.Tactic.Ring.Common.evalAddOverlap.toString) OptionT.fail

theorem Mathlib.Tactic.Ring.Common.add_pf_zero_add {R : Type u_1} [CommSemiring R] (b : R) : 0 + b = b

theorem Mathlib.Tactic.Ring.Common.add_pf_add_zero {R : Type u_1} [CommSemiring R] (a : R) : a + 0 = a

theorem Mathlib.Tactic.Ring.Common.add_pf_add_overlap {R : Type u_1} [CommSemiring R] {a₁ a₂ b₁ b₂ c₁ c₂ : R} : a₁ + b₁ = c₁ → a₂ + b₂ = c₂ → a₁ + a₂ + (b₁ + b₂) = c₁ + c₂

theorem Mathlib.Tactic.Ring.Common.add_pf_add_overlap_zero {R : Type u_1} [CommSemiring R] {a₁ a₂ b₁ b₂ c : R} (h : Meta.NormNum.IsNat (a₁ + b₁) 0) (h₄ : a₂ + b₂ = c) : a₁ + a₂ + (b₁ + b₂) = c

theorem Mathlib.Tactic.Ring.Common.add_pf_add_lt {R : Type u_1} [CommSemiring R] {a₂ b c : R} (a₁ : R) : a₂ + b = c → a₁ + a₂ + b = a₁ + c

theorem Mathlib.Tactic.Ring.Common.add_pf_add_gt {R : Type u_1} [CommSemiring R] {a b₂ c : R} (b₁ : R) : a + b₂ = c → a + (b₁ + b₂) = b₁ + c

partial def Mathlib.Tactic.Ring.Common.evalAdd {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) (rcℕ : RingCompute btℕ sℕ) {a b : Q(«$α»)} (va : ExSum bt sα a) (vb : ExSum bt sα b) : Lean.MetaM (Result (ExSum bt sα) q(«$a» + «$b»))

Adds two polynomials va, vb together to get a normalized result polynomial.

• 0 + b = b
• a + 0 = a
• a * x + a * y = a * (x + y) (for x, y coefficients; uses evalAddOverlap)
• (a₁ + a₂) + (b₁ + b₂) = a₁ + (a₂ + (b₁ + b₂)) (if a₁.lt b₁)
• (a₁ + a₂) + (b₁ + b₂) = b₁ + ((a₁ + a₂) + b₂) (if not a₁.lt b₁)

Multiplication

theorem Mathlib.Tactic.Ring.Common.one_mul {R : Type u_1} [CommSemiring R] (a : R) : Nat.rawCast 1 * a = a

theorem Mathlib.Tactic.Ring.Common.mul_one {R : Type u_1} [CommSemiring R] (a : R) : a * Nat.rawCast 1 = a

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

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

theorem Mathlib.Tactic.Ring.Common.mul_pp_pf_overlap {R : Type u_1} [CommSemiring R] {a₂ b₂ c : R} {ea eb e : ℕ} (x : R) : ea + eb = e → a₂ * b₂ = c → x ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * c

partial def Mathlib.Tactic.Ring.Common.evalMulProd {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) (rcℕ : RingCompute btℕ sℕ) {a b : Q(«$α»)} (va : ExProd bt sα a) (vb : ExProd bt sα b) : Lean.MetaM (Result (ExProd bt sα) q(«$a» * «$b»))

Multiplies two monomials va, vb together to get a normalized result monomial.

• x * y = (x * y) (for x, y coefficients)
• x * (b₁ * b₂) = b₁ * (b₂ * x) (for x coefficient)
• (a₁ * a₂) * y = a₁ * (a₂ * y) (for y coefficient)
• (x ^ ea * a₂) * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂) (if ea and eb are identical except coefficient)
• (a₁ * a₂) * (b₁ * b₂) = a₁ * (a₂ * (b₁ * b₂)) (if a₁.lt b₁)
• (a₁ * a₂) * (b₁ * b₂) = b₁ * ((a₁ * a₂) * b₂) (if not a₁.lt b₁)

theorem Mathlib.Tactic.Ring.Common.mul_zero {R : Type u_1} [CommSemiring R] (a : R) : a * 0 = 0

theorem Mathlib.Tactic.Ring.Common.mul_add {R : Type u_1} [CommSemiring R] {a b₁ b₂ c₁ c₂ d : R} : a * b₁ = c₁ → a * b₂ = c₂ → c₁ + 0 + c₂ = d → a * (b₁ + b₂) = d

def Mathlib.Tactic.Ring.Common.evalMul₁ {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) (rcℕ : RingCompute btℕ sℕ) {a b : Q(«$α»)} (va : ExProd bt sα a) (vb : ExSum bt sα b) : Lean.MetaM (Result (ExSum bt sα) q(«$a» * «$b»))

Multiplies a monomial va to a polynomial vb to get a normalized result polynomial.

• a * 0 = 0
• a * (b₁ + b₂) = (a * b₁) + (a * b₂)

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Ring.Common.evalMul₁ rc rcℕ va Mathlib.Tactic.Ring.Common.ExSum.zero = pure { expr := q(0), val := Mathlib.Tactic.Ring.Common.ExSum.zero, proof := q(⋯) }

theorem Mathlib.Tactic.Ring.Common.zero_mul {R : Type u_1} [CommSemiring R] (b : R) : 0 * b = 0

theorem Mathlib.Tactic.Ring.Common.add_mul {R : Type u_1} [CommSemiring R] {a₁ a₂ b c₁ c₂ d : R} : a₁ * b = c₁ → a₂ * b = c₂ → c₁ + c₂ = d → (a₁ + a₂) * b = d

def Mathlib.Tactic.Ring.Common.evalMul {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) (rcℕ : RingCompute btℕ sℕ) {a b : Q(«$α»)} (va : ExSum bt sα a) (vb : ExSum bt sα b) : Lean.MetaM (Result (ExSum bt sα) q(«$a» * «$b»))

Multiplies two polynomials va, vb together to get a normalized result polynomial.

• 0 * b = 0
• (a₁ + a₂) * b = (a₁ * b) + (a₂ * b)

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Ring.Common.evalMul rc rcℕ Mathlib.Tactic.Ring.Common.ExSum.zero vb = pure { expr := q(0), val := Mathlib.Tactic.Ring.Common.ExSum.zero, proof := q(⋯) }

Negation

theorem Mathlib.Tactic.Ring.Common.neg_one_mul {R : Type u_2} [CommRing R] {a b : R} : -1 * a = b → -a = b

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

def Mathlib.Tactic.Ring.Common.evalNegProd {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) {a : Q(«$α»)} (rα : Q(CommRing «$α»)) (va : ExProd bt sα a) : Lean.MetaM (Result (ExProd bt sα) q(-«$a»))

Negates a monomial va to get another monomial.

• -c = (-c) (for c coefficient)
• -(a₁ * a₂) = a₁ * -a₂

Equations

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

theorem Mathlib.Tactic.Ring.Common.neg_zero {R : Type u_2} [CommRing R] : -0 = 0

theorem Mathlib.Tactic.Ring.Common.neg_add {R : Type u_2} [CommRing R] {a₁ a₂ b₁ b₂ : R} : -a₁ = b₁ → -a₂ = b₂ → -(a₁ + a₂) = b₁ + b₂

def Mathlib.Tactic.Ring.Common.evalNeg {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) {a : Q(«$α»)} (rα : Q(CommRing «$α»)) (va : ExSum bt sα a) : Lean.MetaM (Result (ExSum bt sα) q(-«$a»))

Negates a polynomial va to get another polynomial.

• -0 = 0 (for c coefficient)
• -(a₁ + a₂) = -a₁ + -a₂

Equations

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

Subtraction

theorem Mathlib.Tactic.Ring.Common.sub_pf {R : Type u_2} [CommRing R] {a b c d : R} : -b = c → a + c = d → a - b = d

def Mathlib.Tactic.Ring.Common.evalSub {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) (rcℕ : RingCompute btℕ sℕ) {a b : Q(«$α»)} (rα : Q(CommRing «$α»)) (va : ExSum bt sα a) (vb : ExSum bt sα b) : Lean.MetaM (Result (ExSum bt sα) q(«$a» - «$b»))

Subtracts two polynomials va, vb to get a normalized result polynomial.

• a - b = a + -b

Equations

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

Exponentiation

theorem Mathlib.Tactic.Ring.Common.pow_prod_atom {R : Type u_1} [CommSemiring R] (a : R) (b : ℕ) {e : R} (h : (a + 0) ^ b * Nat.rawCast 1 = e) : a ^ b = e

def Mathlib.Tactic.Ring.Common.evalPowProdAtom {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) {a : Q(«$α»)} {b : Q(ℕ)} (va : ExProd bt sα a) (vb : ExProdNat b) : Result (ExProd bt sα) q(«$a» ^ «$b»)

The fallback case for exponentiating polynomials is to use ExBase.toProd to just build an exponent expression. (This has a slightly different normalization than evalPowAtom because the input types are different.)

• x ^ e = (x + 0) ^ e * 1

Equations

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

theorem Mathlib.Tactic.Ring.Common.pow_atom {R : Type u_1} [CommSemiring R] (a : R) (b : ℕ) {e : R} (h : a ^ b * Nat.rawCast 1 = e) : a ^ b = e + 0

def Mathlib.Tactic.Ring.Common.evalPowAtom {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) {a : Q(«$α»)} {b : Q(ℕ)} (va : ExBase bt sα a) (vb : ExProdNat b) : Result (ExSum bt sα) q(«$a» ^ «$b»)

The fallback case for exponentiating polynomials is to use ExBase.toProd to just build an exponent expression.

• x ^ e = x ^ e * 1 + 0

Equations

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

theorem Mathlib.Tactic.Ring.Common.const_pos (n : ℕ) (h : Nat.ble 1 n = true) : 0 < n.rawCast

theorem Mathlib.Tactic.Ring.Common.mul_exp_pos {a₁ a₂ : ℕ} (n : ℕ) (h₁ : 0 < a₁) (h₂ : 0 < a₂) : 0 < a₁ ^ n * a₂

theorem Mathlib.Tactic.Ring.Common.add_pos_left {a₁ : ℕ} (a₂ : ℕ) (h : 0 < a₁) : 0 < a₁ + a₂

theorem Mathlib.Tactic.Ring.Common.add_pos_right {a₂ : ℕ} (a₁ : ℕ) (h : 0 < a₂) : 0 < a₁ + a₂

partial def Mathlib.Tactic.Ring.Common.ExBaseNat.evalPos {a : Q(ℕ)} (va : ExBaseNat a) : Option Q(0 < «$a»)

Attempts to prove that a polynomial expression in ℕ is positive.

• Atoms are not (necessarily) positive
• Sums defer to ExSum.evalPos

partial def Mathlib.Tactic.Ring.Common.ExProdNat.evalPos {a : Q(ℕ)} (va : ExProdNat a) : Option Q(0 < «$a»)

Attempts to prove that a monomial expression in ℕ is positive.

• 0 < c (where c is a numeral) is true by the normalization invariant (c is not zero)
• 0 < x ^ e * b if 0 < x and 0 < b

partial def Mathlib.Tactic.Ring.Common.ExSumNat.evalPos {a : Q(ℕ)} (va : ExSumNat a) : Option Q(0 < «$a»)

Attempts to prove that a polynomial expression in ℕ is positive.

• 0 < 0 fails
• 0 < a + b if 0 < a or 0 < b

theorem Mathlib.Tactic.Ring.Common.pow_one {R : Type u_1} [CommSemiring R] (a : R) : a ^ 1 = a

theorem Mathlib.Tactic.Ring.Common.pow_bit0 {R : Type u_1} [CommSemiring R] {a b c : R} {k : ℕ} : a ^ k = b → b * b = c → a ^ Nat.mul 2 k = c

theorem Mathlib.Tactic.Ring.Common.pow_bit1 {R : Type u_1} [CommSemiring R] {a b c : R} {k : ℕ} {d : R} : a ^ k = b → b * b = c → c * a = d → a ^ (Nat.mul 2 k).add 1 = d

partial def Mathlib.Tactic.Ring.Common.evalPowNat {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) (rcℕ : RingCompute btℕ sℕ) {a : Q(«$α»)} (va : ExSum bt sα a) (n : Q(ℕ)) : Lean.MetaM (Result (ExSum bt sα) q(«$a» ^ «$n»))

The main case of exponentiation of ring expressions is when va is a polynomial and n is a nonzero literal expression, like (x + y)^5. In this case we work out the polynomial completely into a sum of monomials.

• x ^ 1 = x
• x ^ (2*n) = x ^ n * x ^ n
• x ^ (2*n+1) = x ^ n * x ^ n * x

theorem Mathlib.Tactic.Ring.Common.one_pow {R : Type u_1} [CommSemiring R] {a : R} (b : ℕ) (ha : Meta.NormNum.IsNat a 1) : a ^ b = a

theorem Mathlib.Tactic.Ring.Common.mul_pow {R : Type u_1} [CommSemiring R] {a₂ c₂ : R} {ea₁ b c₁ : ℕ} {xa₁ : R} : ea₁ * b = c₁ → a₂ ^ b = c₂ → (xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ c₁ * c₂

theorem Mathlib.Tactic.Ring.Common.mul_pow_mul {R : Type u_1} [CommSemiring R] {a₂ c₂ : R} {ea₁ b c₁ : ℕ} {xa₁ c₃ d : R} : ea₁ * b = c₁ → a₂ ^ b = c₂ → xa₁ ^ c₁ * Nat.rawCast 1 = c₃ → c₃ * c₂ = d → (xa₁ ^ ea₁ * a₂) ^ b = d

def Mathlib.Tactic.Ring.Common.evalPowProd {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) (rcℕ : RingCompute btℕ sℕ) {a : Q(«$α»)} {b : Q(ℕ)} (va : ExProd bt sα a) (vb : ExProdNat b) : Lean.MetaM (Result (ExProd bt sα) q(«$a» ^ «$b»))

There are several special cases when exponentiating monomials:

• 1 ^ n = 1
• x ^ y = (x ^ y) when x is a constant (Note this may fail if e.g. y is not a constant)
• (a * b) ^ e = a ^ e * b ^ e

In all other cases we use evalPowProdAtom.

Equations

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

structure Mathlib.Tactic.Ring.Common.ExtractCoeff (e : Q(ℕ)) : Type

The result of extractCoeff is a numeral and a proof that the original expression factors by this numeral.

• k : Q(ℕ)

  A raw natural number literal.

• e' : Q(ℕ)

  The result of extracting the coefficient is a monic monomial.

• ve' : ExProdNat self.e'

  e' is a monomial.

• p : Q(«$e» = unknown_1 * unknown_2)

  The proof that e splits into the coefficient k and the monic monomial e'.

theorem Mathlib.Tactic.Ring.Common.coeff_one (k : ℕ) {e : ℕ} (h : Nat.rawCast 1 = e) : k.rawCast = e * k

theorem Mathlib.Tactic.Ring.Common.coeff_mul {a₃ c₂ k : ℕ} (a₁ a₂ : ℕ) : a₃ = c₂ * k → a₁ ^ a₂ * a₃ = a₁ ^ a₂ * c₂ * k

def Mathlib.Tactic.Ring.Common.extractCoeff (rcℕ : RingCompute btℕ sℕ) {a : Q(ℕ)} (va : ExProdNat a) : ExtractCoeff a

Given a monomial expression va, splits off the leading coefficient k and the remainder e', stored in the ExtractCoeff structure.

• c = 1 * c (if c is a constant)
• a * b = (a * b') * k if b = b' * k

Equations

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

theorem Mathlib.Tactic.Ring.Common.pow_one_cast {R : Type u_1} [CommSemiring R] (a : R) : a ^ Nat.rawCast 1 = a

theorem Mathlib.Tactic.Ring.Common.pow_one_cast_of_isNat {R : Type u_1} [CommSemiring R] (a : R) (b : ℕ) (hb : Meta.NormNum.IsNat b 1) : a ^ b = a

theorem Mathlib.Tactic.Ring.Common.zero_pow {R : Type u_1} [CommSemiring R] {b : ℕ} : 0 < b → 0 ^ b = 0

theorem Mathlib.Tactic.Ring.Common.single_pow {R : Type u_1} [CommSemiring R] {a c : R} {b : ℕ} : a ^ b = c → (a + 0) ^ b = c + 0

theorem Mathlib.Tactic.Ring.Common.pow_nat {R : Type u_1} [CommSemiring R] {a : R} {b c k : ℕ} {d e : R} : b = c * k → a ^ c = d → d ^ k = e → a ^ b = e

partial def Mathlib.Tactic.Ring.Common.evalPow₁ {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) (rcℕ : RingCompute btℕ sℕ) {a : Q(«$α»)} {b : Q(ℕ)} (va : ExSum bt sα a) (vb : ExProdNat b) : Lean.MetaM (Result (ExSum bt sα) q(«$a» ^ «$b»))

Exponentiates a polynomial va by a monomial vb, including several special cases.

• a ^ 1 = a
• 0 ^ e = 0 if 0 < e
• (a + 0) ^ b = a ^ b computed using evalPowProd
• a ^ b = (a ^ b') ^ k if b = b' * k and k > 1

Otherwise a ^ b is just encoded as a ^ b * 1 + 0 using evalPowAtom.

theorem Mathlib.Tactic.Ring.Common.pow_zero {R : Type u_1} [CommSemiring R] (a : R) {e : R} (h : Nat.rawCast 1 = e) : a ^ 0 = e + 0

theorem Mathlib.Tactic.Ring.Common.pow_add {R : Type u_1} [CommSemiring R] {a c₁ c₂ : R} {b₁ b₂ : ℕ} {d : R} : a ^ b₁ = c₁ → a ^ b₂ = c₂ → c₁ * c₂ = d → a ^ (b₁ + b₂) = d

def Mathlib.Tactic.Ring.Common.evalPow {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) (rcℕ : RingCompute btℕ sℕ) {a : Q(«$α»)} {b : Q(ℕ)} (va : ExSum bt sα a) (vb : ExSumNat b) : Lean.MetaM (Result (ExSum bt sα) q(«$a» ^ «$b»))

Exponentiates two polynomials va, vb.

• a ^ 0 = 1
• a ^ (b₁ + b₂) = a ^ b₁ * a ^ b₂

Equations

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

structure Mathlib.Tactic.Ring.Common.Cache {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) : Type

This cache contains data required by the ring tactic during execution.

• rα : Option Q(CommRing «$α»)

  A ring instance on α, if available.

• dsα : Option Q(Semifield «$α»)

  A division semiring instance on α, if available.

• czα : Option Q(CharZero «$α»)

  A characteristic zero ring instance on α, if available.

def Mathlib.Tactic.Ring.Common.mkCache {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) : Lean.MetaM (Cache sα)

Create a new cache for α by doing the necessary instance searches.

Equations

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

theorem Mathlib.Tactic.Ring.Common.toProd_pf {R : Type u_1} [CommSemiring R] {a a' : R} (p : a = a') {e : ℕ} (hone : Nat.rawCast 1 = e) : a = a' ^ e * Nat.rawCast 1

theorem Mathlib.Tactic.Ring.Common.atom_pf {R : Type u_1} [CommSemiring R] {b : R} (a : R) {e : ℕ} (hone : Nat.rawCast 1 = e) (hb : a ^ e * Nat.rawCast 1 = b) : a = b + 0

theorem Mathlib.Tactic.Ring.Common.atom_pf' {R : Type u_1} [CommSemiring R] {a a' b : R} (p : a = a') {e : ℕ} (hone : Nat.rawCast 1 = e) (hb : a' ^ e * Nat.rawCast 1 = b) : a = b + 0

def Mathlib.Tactic.Ring.Common.evalAtom {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) (rcℕ : RingCompute btℕ sℕ) (e : Q(«$α»)) : AtomM (Result (ExSum bt sα) e)

Evaluates an atom, an expression where ring can find no additional structure.

• a = a ^ 1 * 1 + 0

Equations

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

theorem Mathlib.Tactic.Ring.Common.inv_mul {R : Type u_2} [Semifield R] {a₁ : R} {a₂ : ℕ} {a₃ b₁ b₃ c : R} : a₁⁻¹ = b₁ → a₃⁻¹ = b₃ → b₃ * (b₁ ^ a₂ * Nat.rawCast 1) = c → (a₁ ^ a₂ * a₃)⁻¹ = c

theorem Mathlib.Tactic.Ring.Common.inv_zero {R : Type u_2} [Semifield R] : 0⁻¹ = 0

theorem Mathlib.Tactic.Ring.Common.inv_single {R : Type u_2} [Semifield R] {a b : R} : a⁻¹ = b → (a + 0)⁻¹ = b + 0

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

def Mathlib.Tactic.Ring.Common.evalInvAtom {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (dsα : Q(Semifield «$α»)) (a : Q(«$α»)) : AtomM (Result (ExBase bt sα) q(«$a»⁻¹))

Applies ⁻¹ to a polynomial to get an atom.

Equations

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

def Mathlib.Tactic.Ring.Common.ExProd.evalInv {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) (rcℕ : RingCompute btℕ sℕ) (dsα : Q(Semifield «$α»)) {a : Q(«$α»)} (czα : Option Q(CharZero «$α»)) (va : ExProd bt sα a) : AtomM (Result (ExProd bt sα) q(«$a»⁻¹))

Inverts a polynomial va to get a normalized result polynomial.

• c⁻¹ = (c⁻¹) if c is a constant
• (a ^ b * c)⁻¹ = a⁻¹ ^ b * c⁻¹

Equations

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

def Mathlib.Tactic.Ring.Common.ExSum.evalInv {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) (rcℕ : RingCompute btℕ sℕ) (dsα : Q(Semifield «$α»)) {a : Q(«$α»)} (czα : Option Q(CharZero «$α»)) (va : ExSum bt sα a) : AtomM (Result (ExSum bt sα) q(«$a»⁻¹))

Inverts a polynomial va to get a normalized result polynomial.

• 0⁻¹ = 0
• a⁻¹ = (a⁻¹) if a is a nontrivial sum

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Ring.Common.ExSum.evalInv rc rcℕ dsα czα Mathlib.Tactic.Ring.Common.ExSum.zero = pure { expr := q(0), val := Mathlib.Tactic.Ring.Common.ExSum.zero, proof := q(⋯) }

theorem Mathlib.Tactic.Ring.Common.div_pf {R : Type u_2} [Semifield R] {a b c d : R} : b⁻¹ = c → a * c = d → a / b = d

def Mathlib.Tactic.Ring.Common.evalDiv {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) (rcℕ : RingCompute btℕ sℕ) {a b : Q(«$α»)} (rα : Q(Semifield «$α»)) (czα : Option Q(CharZero «$α»)) (va : ExSum bt sα a) (vb : ExSum bt sα b) : AtomM (Result (ExSum bt sα) q(«$a» / «$b»))

Divides two polynomials va, vb to get a normalized result polynomial.

• a / b = a * b⁻¹

Equations

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

theorem Mathlib.Tactic.Ring.Common.add_congr {R : Type u_1} [CommSemiring R] {a a' b b' c : R} : a = a' → b = b' → a' + b' = c → a + b = c

theorem Mathlib.Tactic.Ring.Common.mul_congr {R : Type u_1} [CommSemiring R] {a a' b b' c : R} : a = a' → b = b' → a' * b' = c → a * b = c

theorem Mathlib.Tactic.Ring.Common.nsmul_congr {R : Type u_1} [CommSemiring R] {b b' c : R} {a a' : ℕ} : a = a' → b = b' → a' • b' = c → a • b = c

theorem Mathlib.Tactic.Ring.Common.zsmul_congr {R : Type u_2} [CommRing R] {b b' c : R} {a a' : ℤ} : a = a' → b = b' → a' • b' = c → a • b = c

theorem Mathlib.Tactic.Ring.Common.pow_congr {R : Type u_1} [CommSemiring R] {a a' c : R} {b b' : ℕ} : a = a' → b = b' → a' ^ b' = c → a ^ b = c

theorem Mathlib.Tactic.Ring.Common.neg_congr {R : Type u_2} [CommRing R] {a a' b : R} : a = a' → -a' = b → -a = b

theorem Mathlib.Tactic.Ring.Common.sub_congr {R : Type u_2} [CommRing R] {a a' b b' c : R} : a = a' → b = b' → a' - b' = c → a - b = c

theorem Mathlib.Tactic.Ring.Common.inv_congr {R : Type u_2} [Semifield R] {a a' b : R} : a = a' → a'⁻¹ = b → a⁻¹ = b

theorem Mathlib.Tactic.Ring.Common.div_congr {R : Type u_2} [Semifield R] {a a' b b' c : R} : a = a' → b = b' → a' / b' = c → a / b = c

theorem Mathlib.Tactic.Ring.Common.smul_congr {R : Type u_2} {α : Type u_3} [CommSemiring α] [SMul R α] {r : R} {a b t c : α} : a = b → (∀ (x : α), r • x = t * x) → t * b = c → r • a = c

def Mathlib.Tactic.Ring.Common.Cache.nat : Cache sℕ

A precomputed Cache for ℕ.

Equations

• Mathlib.Tactic.Ring.Common.Cache.nat = { rα := none, dsα := none, czα := some q(⋯) }

def Mathlib.Tactic.Ring.Common.isAtomOrDerivable {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) (c : Cache sα) (e : Q(«$α»)) : AtomM (Option (Option (Result (ExSum bt sα) e)))

Checks whether e would be processed by eval as a ring expression, or otherwise if it is an atom or something simplifiable via norm_num.

We use this in ring_nf to avoid rewriting atoms unnecessarily.

Returns:

• none if eval would process e as an algebraic ring expression
• some none if eval would treat e as an atom.
• some (some r) if eval would not process e as an algebraic ring expression, but NormNum.derive can nevertheless simplify e, with result r.

Equations

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

partial def Mathlib.Tactic.Ring.Common.eval (rcℕ : RingCompute btℕ sℕ) {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} (rc : RingCompute bt sα) (c : Cache sα) (e : Q(«$α»)) : AtomM (Result (ExSum bt sα) e)

Evaluates expression e of type α into a normalized representation as a polynomial. This is the main driver of ring, which calls out to evalAdd, evalMul etc.

• rc tells us how to normalize constants in α.
• rcℕ tells us how to normalize constants in exponents.