Documentation

Mathlib.Tactic.Ring.Basic

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:

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:

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

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

A shortcut instance for CommSemiring used by ring.

Equations
Instances For

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

    Equations
    Instances For
      inductive Mathlib.Tactic.Ring.ExBase {u : Lean.Level} {α : Q(Type u)} :
      Q(CommSemiring «$α»)Q(«$α»)Type

      The base e of a normalized exponent expression.

      • atom: {u : Lean.Level} → {α : Q(Type u)} → { : Q(CommSemiring «$α»)} → {e : Q(«$α»)} → Mathlib.Tactic.Ring.ExBase 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 value : expr contains a representative of this class. The function resolve_atom determines the appropriate atom for a given expression.

      • sum: {u : Lean.Level} → {α : Q(Type u)} → { : Q(CommSemiring «$α»)} → {e : Q(«$α»)} → Mathlib.Tactic.Ring.ExSum eMathlib.Tactic.Ring.ExBase e

        A sum of monomials.

      Instances For
        inductive Mathlib.Tactic.Ring.ExProd {u : Lean.Level} {α : Q(Type u)} :
        Q(CommSemiring «$α»)Q(«$α»)Type

        A monomial, which is a product of powers of ExBase expressions, terminated by a (nonzero) constant coefficient.

        Instances For
          inductive Mathlib.Tactic.Ring.ExSum {u : Lean.Level} {α : Q(Type u)} :
          Q(CommSemiring «$α»)Q(«$α»)Type

          A polynomial expression, which is a sum of monomials.

          Instances For
            partial def Mathlib.Tactic.Ring.ExBase.eq {u : Lean.Level} {α : Q(Type u)} {sα : Q(CommSemiring «$α»)} {a : Q(«$α»)} {b : Q(«$α»)} :

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

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

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

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

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

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

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

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

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

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

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

            instance Mathlib.Tactic.Ring.instInhabitedSigmaQuotedExBase {u : Lean.Level} {α : Q(Type u)} {sα : Q(CommSemiring «$α»)} :
            Inhabited ((e : Q(«$α»)) × Mathlib.Tactic.Ring.ExBase e)
            Equations
            instance Mathlib.Tactic.Ring.instInhabitedSigmaQuotedExSum {u : Lean.Level} {α : Q(Type u)} {sα : Q(CommSemiring «$α»)} :
            Inhabited ((e : Q(«$α»)) × Mathlib.Tactic.Ring.ExSum e)
            Equations
            • Mathlib.Tactic.Ring.instInhabitedSigmaQuotedExSum = { default := q(0), Mathlib.Tactic.Ring.ExSum.zero }
            instance Mathlib.Tactic.Ring.instInhabitedSigmaQuotedExProd {u : Lean.Level} {α : Q(Type u)} {sα : Q(CommSemiring «$α»)} :
            Inhabited ((e : Q(«$α»)) × Mathlib.Tactic.Ring.ExProd e)
            Equations
            partial 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(«$α»)} :
            Mathlib.Tactic.Ring.ExBase a(a : Q(«$β»)) × Mathlib.Tactic.Ring.ExBase a

            Converts ExBase to ExBase, assuming and are defeq.

            partial 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(«$α»)} :
            Mathlib.Tactic.Ring.ExProd a(a : Q(«$β»)) × Mathlib.Tactic.Ring.ExProd a

            Converts ExProd to ExProd, assuming and are defeq.

            partial 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(«$α»)} :
            Mathlib.Tactic.Ring.ExSum a(a : Q(«$β»)) × Mathlib.Tactic.Ring.ExSum a

            Converts ExSum to ExSum, assuming and are defeq.

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

            The result of evaluating an (unnormalized) expression e into the type family E (one of ExSum, ExProd, ExBase) 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.

            Instances For
              instance Mathlib.Tactic.Ring.instInhabitedResultOfSigmaQuoted {u : Lean.Level} {α : Q(Type u)} {E : Q(«$α»)Type} {e : Q(«$α»)} [Inhabited ((e : Q(«$α»)) × E e)] :
              Equations
              • Mathlib.Tactic.Ring.instInhabitedResultOfSigmaQuoted = match default with | e', v => { default := { expr := e', val := v, proof := default } }
              def Mathlib.Tactic.Ring.ExProd.mkNat {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) (n : ) :
              (e : Q(«$α»)) × Mathlib.Tactic.Ring.ExProd e

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

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

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

                Instances For
                  def Mathlib.Tactic.Ring.ExProd.mkRat {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) :
                  Q(DivisionRing «$α»)Q()Q()Lean.Expr(e : Q(«$α»)) × Mathlib.Tactic.Ring.ExProd e

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

                  Equations
                  Instances For
                    def Mathlib.Tactic.Ring.ExBase.toProd {u : Lean.Level} {α : Q(Type u)} {sα : Q(CommSemiring «$α»)} {a : Q(«$α»)} {b : Q()} (va : Mathlib.Tactic.Ring.ExBase a) (vb : Mathlib.Tactic.Ring.ExProd Mathlib.Tactic.Ring.sℕ b) :
                    Mathlib.Tactic.Ring.ExProd q(«$a» ^ «$b» * Nat.rawCast 1)

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

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

                      Embed ExProd in ExSum by adding 0.

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

                        Get the leading coefficient of an ExProd.

                        Equations
                        Instances For
                          inductive Mathlib.Tactic.Ring.Overlap {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) (e : Q(«$α»)) :

                          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.

                          Instances For
                            theorem Mathlib.Tactic.Ring.add_overlap_pf {R : Type u_1} [CommSemiring R] {a : R} {b : R} {c : R} (x : R) (e : ) (pq_pf : a + b = c) :
                            x ^ e * a + x ^ e * b = x ^ e * c
                            theorem Mathlib.Tactic.Ring.add_overlap_pf_zero {R : Type u_1} [CommSemiring R] {a : R} {b : R} (x : R) (e : ) :
                            def Mathlib.Tactic.Ring.evalAddOverlap {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {a : Q(«$α»)} {b : Q(«$α»)} (va : Mathlib.Tactic.Ring.ExProd a) (vb : Mathlib.Tactic.Ring.ExProd 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.

                            Instances For
                              theorem Mathlib.Tactic.Ring.add_pf_zero_add {R : Type u_1} [CommSemiring R] (b : R) :
                              0 + b = b
                              theorem Mathlib.Tactic.Ring.add_pf_add_zero {R : Type u_1} [CommSemiring R] (a : R) :
                              a + 0 = a
                              theorem Mathlib.Tactic.Ring.add_pf_add_overlap {R : Type u_1} [CommSemiring R] {a₁ : R} {a₂ : R} {b₁ : R} {b₂ : R} {c₁ : R} {c₂ : R} :
                              a₁ + b₁ = c₁a₂ + b₂ = c₂a₁ + a₂ + (b₁ + b₂) = c₁ + c₂
                              theorem Mathlib.Tactic.Ring.add_pf_add_overlap_zero {R : Type u_1} [CommSemiring R] {a₁ : R} {a₂ : R} {b₁ : R} {b₂ : R} {c : R} (h : Mathlib.Meta.NormNum.IsNat (a₁ + b₁) 0) (h₄ : a₂ + b₂ = c) :
                              a₁ + a₂ + (b₁ + b₂) = c
                              theorem Mathlib.Tactic.Ring.add_pf_add_lt {R : Type u_1} [CommSemiring R] {a₂ : R} {b : R} {c : R} (a₁ : R) :
                              a₂ + b = ca₁ + a₂ + b = a₁ + c
                              theorem Mathlib.Tactic.Ring.add_pf_add_gt {R : Type u_1} [CommSemiring R] {a : R} {b₂ : R} {c : R} (b₁ : R) :
                              a + b₂ = ca + (b₁ + b₂) = b₁ + c
                              partial def Mathlib.Tactic.Ring.evalAdd {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {a : Q(«$α»)} {b : Q(«$α»)} (va : Mathlib.Tactic.Ring.ExSum a) (vb : Mathlib.Tactic.Ring.ExSum 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₁)
                              theorem Mathlib.Tactic.Ring.one_mul {R : Type u_1} [CommSemiring R] (a : R) :
                              theorem Mathlib.Tactic.Ring.mul_one {R : Type u_1} [CommSemiring R] (a : R) :
                              theorem Mathlib.Tactic.Ring.mul_pf_left {R : Type u_1} [CommSemiring R] {a₃ : R} {b : R} {c : R} (a₁ : R) (a₂ : ) :
                              a₃ * b = ca₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * c
                              theorem Mathlib.Tactic.Ring.mul_pf_right {R : Type u_1} [CommSemiring R] {a : R} {b₃ : R} {c : R} (b₁ : R) (b₂ : ) :
                              a * b₃ = ca * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * c
                              theorem Mathlib.Tactic.Ring.mul_pp_pf_overlap {R : Type u_1} [CommSemiring R] {a₂ : R} {b₂ : R} {c : R} {ea : } {eb : } {e : } (x : R) :
                              ea + eb = ea₂ * b₂ = cx ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * c
                              partial def Mathlib.Tactic.Ring.evalMulProd {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {a : Q(«$α»)} {b : Q(«$α»)} (va : Mathlib.Tactic.Ring.ExProd a) (vb : Mathlib.Tactic.Ring.ExProd 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.mul_zero {R : Type u_1} [CommSemiring R] (a : R) :
                              a * 0 = 0
                              theorem Mathlib.Tactic.Ring.mul_add {R : Type u_1} [CommSemiring R] {a : R} {b₁ : R} {b₂ : R} {c₁ : R} {c₂ : R} {d : R} :
                              a * b₁ = c₁a * b₂ = c₂c₁ + 0 + c₂ = da * (b₁ + b₂) = d
                              def Mathlib.Tactic.Ring.evalMul₁ {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {a : Q(«$α»)} {b : Q(«$α»)} (va : Mathlib.Tactic.Ring.ExProd a) (vb : Mathlib.Tactic.Ring.ExSum 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.evalMul₁ va Mathlib.Tactic.Ring.ExSum.zero = pure { expr := q(0), val := Mathlib.Tactic.Ring.ExSum.zero, proof := q() }
                              Instances For
                                theorem Mathlib.Tactic.Ring.zero_mul {R : Type u_1} [CommSemiring R] (b : R) :
                                0 * b = 0
                                theorem Mathlib.Tactic.Ring.add_mul {R : Type u_1} [CommSemiring R] {a₁ : R} {a₂ : R} {b : R} {c₁ : R} {c₂ : R} {d : R} :
                                a₁ * b = c₁a₂ * b = c₂c₁ + c₂ = d(a₁ + a₂) * b = d
                                def Mathlib.Tactic.Ring.evalMul {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {a : Q(«$α»)} {b : Q(«$α»)} (va : Mathlib.Tactic.Ring.ExSum a) (vb : Mathlib.Tactic.Ring.ExSum 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.evalMul Mathlib.Tactic.Ring.ExSum.zero vb = pure { expr := q(0), val := Mathlib.Tactic.Ring.ExSum.zero, proof := q() }
                                Instances For
                                  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₁ : R} {b₃ : R} {a₁ : } {a₃ : } (a₂ : ) :
                                  a₁ = b₁a₃ = b₃(a₁ ^ a₂ * a₃) = b₁ ^ a₂ * b₃
                                  theorem Mathlib.Tactic.Ring.natCast_add {R : Type u_1} [CommSemiring R] {b₁ : R} {b₂ : R} {a₁ : } {a₂ : } :
                                  a₁ = b₁a₂ = b₂(a₁ + a₂) = b₁ + b₂

                                  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.

                                  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

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

                                  • ↑0 = 0
                                  • ↑(a + b) = ↑a + ↑b
                                  theorem Mathlib.Tactic.Ring.smul_nat {a : } {b : } {c : } :
                                  a * b = ca b = c
                                  theorem Mathlib.Tactic.Ring.smul_eq_cast {R : Type u_1} [CommSemiring R] {a' : R} {b : R} {c : R} {a : } :
                                  a = a'a' * b = ca b = c

                                  Constructs the scalar multiplication n • a, where both n : ℕ and a : α are normalized polynomial expressions.

                                  • a • b = a * b if α = ℕ
                                  • a • b = ↑a * b otherwise
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    theorem Mathlib.Tactic.Ring.neg_one_mul {R : Type u_2} [Ring R] {a : R} {b : R} :
                                    (Int.negOfNat 1).rawCast * a = b-a = b
                                    theorem Mathlib.Tactic.Ring.neg_mul {R : Type u_2} [Ring R] (a₁ : R) (a₂ : ) {a₃ : R} {b : R} :
                                    -a₃ = b-(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * b
                                    def Mathlib.Tactic.Ring.evalNegProd {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {a : Q(«$α»)} (rα : Q(Ring «$α»)) (va : Mathlib.Tactic.Ring.ExProd a) :

                                    Negates a monomial va to get another monomial.

                                    • -c = (-c) (for c coefficient)
                                    • -(a₁ * a₂) = a₁ * -a₂
                                    Instances For
                                      theorem Mathlib.Tactic.Ring.neg_zero {R : Type u_2} [Ring R] :
                                      -0 = 0
                                      theorem Mathlib.Tactic.Ring.neg_add {R : Type u_2} [Ring R] {a₁ : R} {a₂ : R} {b₁ : R} {b₂ : R} :
                                      -a₁ = b₁-a₂ = b₂-(a₁ + a₂) = b₁ + b₂
                                      def Mathlib.Tactic.Ring.evalNeg {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {a : Q(«$α»)} (rα : Q(Ring «$α»)) (va : Mathlib.Tactic.Ring.ExSum 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.evalNeg Mathlib.Tactic.Ring.ExSum.zero = pure { expr := q(0), val := Mathlib.Tactic.Ring.ExSum.zero, proof := q() }
                                      Instances For
                                        theorem Mathlib.Tactic.Ring.sub_pf {R : Type u_2} [Ring R] {a : R} {b : R} {c : R} {d : R} :
                                        -b = ca + c = da - b = d
                                        def Mathlib.Tactic.Ring.evalSub {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {a : Q(«$α»)} {b : Q(«$α»)} (rα : Q(Ring «$α»)) (va : Mathlib.Tactic.Ring.ExSum a) (vb : Mathlib.Tactic.Ring.ExSum 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.
                                        Instances For
                                          theorem Mathlib.Tactic.Ring.pow_prod_atom {R : Type u_1} [CommSemiring R] (a : R) (b : ) :
                                          a ^ b = (a + 0) ^ b * Nat.rawCast 1

                                          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
                                          Instances For
                                            theorem Mathlib.Tactic.Ring.pow_atom {R : Type u_1} [CommSemiring R] (a : R) (b : ) :
                                            a ^ b = a ^ b * Nat.rawCast 1 + 0

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

                                            • x ^ e = x ^ e * 1 + 0
                                            Equations
                                            Instances For
                                              theorem Mathlib.Tactic.Ring.const_pos (n : ) (h : Nat.ble 1 n = true) :
                                              0 < n.rawCast
                                              theorem Mathlib.Tactic.Ring.mul_exp_pos {a₁ : } {a₂ : } (n : ) (h₁ : 0 < a₁) (h₂ : 0 < a₂) :
                                              0 < a₁ ^ n * a₂
                                              theorem Mathlib.Tactic.Ring.add_pos_left {a₁ : } (a₂ : ) (h : 0 < a₁) :
                                              0 < a₁ + a₂
                                              theorem Mathlib.Tactic.Ring.add_pos_right {a₂ : } (a₁ : ) (h : 0 < a₂) :
                                              0 < a₁ + a₂

                                              Attempts to prove that a polynomial expression in is positive.

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

                                              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

                                              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.pow_one {R : Type u_1} [CommSemiring R] (a : R) :
                                              a ^ 1 = a
                                              theorem Mathlib.Tactic.Ring.pow_bit0 {R : Type u_1} [CommSemiring R] {a : R} {b : R} {c : R} {k : } :
                                              a ^ k = bb * b = ca ^ Nat.mul 2 k = c
                                              theorem Mathlib.Tactic.Ring.pow_bit1 {R : Type u_1} [CommSemiring R] {a : R} {b : R} {c : R} {k : } {d : R} :
                                              a ^ k = bb * b = cc * a = da ^ (Nat.mul 2 k).add 1 = d
                                              partial def Mathlib.Tactic.Ring.evalPowNat {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {a : Q(«$α»)} (va : Mathlib.Tactic.Ring.ExSum a) (n : Q()) :

                                              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.mul_pow {R : Type u_1} [CommSemiring R] {a₂ : R} {c₂ : R} {ea₁ : } {b : } {c₁ : } {xa₁ : R} :
                                              ea₁ * b = c₁a₂ ^ b = c₂(xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ c₁ * c₂

                                              There are several special cases when exponentiating monomials:

                                              • 1 ^ n = 1
                                              • x ^ y = (x ^ y) when x and y are constants
                                              • (a * b) ^ e = a ^ e * b ^ e

                                              In all other cases we use evalPowProdAtom.

                                              Instances For

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

                                                Instances For
                                                  theorem Mathlib.Tactic.Ring.coeff_mul {a₃ : } {c₂ : } {k : } (a₁ : ) (a₂ : ) :
                                                  a₃ = c₂ * ka₁ ^ a₂ * a₃ = a₁ ^ a₂ * c₂ * k

                                                  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
                                                  Instances For
                                                    theorem Mathlib.Tactic.Ring.zero_pow {R : Type u_1} [CommSemiring R] {b : } :
                                                    0 < b0 ^ b = 0
                                                    theorem Mathlib.Tactic.Ring.single_pow {R : Type u_1} [CommSemiring R] {a : R} {c : R} {b : } :
                                                    a ^ b = c(a + 0) ^ b = c + 0
                                                    theorem Mathlib.Tactic.Ring.pow_nat {R : Type u_1} [CommSemiring R] {a : R} {b : } {c : } {k : } {d : R} {e : R} :
                                                    b = c * ka ^ c = dd ^ k = ea ^ b = e
                                                    partial def Mathlib.Tactic.Ring.evalPow₁ {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {a : Q(«$α»)} {b : Q()} (va : Mathlib.Tactic.Ring.ExSum a) (vb : Mathlib.Tactic.Ring.ExProd Mathlib.Tactic.Ring.sℕ 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.pow_zero {R : Type u_1} [CommSemiring R] (a : R) :
                                                    a ^ 0 = Nat.rawCast 1 + 0
                                                    theorem Mathlib.Tactic.Ring.pow_add {R : Type u_1} [CommSemiring R] {a : R} {c₁ : R} {c₂ : R} {b₁ : } {b₂ : } {d : R} :
                                                    a ^ b₁ = c₁a ^ b₂ = c₂c₁ * c₂ = da ^ (b₁ + b₂) = d

                                                    Exponentiates two polynomials va, vb.

                                                    • a ^ 0 = 1
                                                    • a ^ (b₁ + b₂) = a ^ b₁ * a ^ b₂
                                                    Equations
                                                    Instances For
                                                      structure Mathlib.Tactic.Ring.Cache {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) :

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

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

                                                        A ring instance on α, if available.

                                                      • dα : Option Q(DivisionRing «$α»)

                                                        A division ring instance on α, if available.

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

                                                        A characteristic zero ring instance on α, if available.

                                                      Instances For

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

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          theorem Mathlib.Tactic.Ring.cast_pos {R : Type u_1} [CommSemiring R] {a : R} {n : } :
                                                          Mathlib.Meta.NormNum.IsNat a na = n.rawCast + 0
                                                          theorem Mathlib.Tactic.Ring.cast_neg {n : } {R : Type u_2} [Ring R] {a : R} :
                                                          theorem Mathlib.Tactic.Ring.cast_rat {n : } {d : } {R : Type u_2} [DivisionRing R] {a : R} :

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

                                                          Instances For
                                                            theorem Mathlib.Tactic.Ring.toProd_pf {R : Type u_1} [CommSemiring R] {a : R} {a' : R} (p : a = a') :
                                                            theorem Mathlib.Tactic.Ring.atom_pf' {R : Type u_1} [CommSemiring R] {a : R} {a' : R} (p : a = a') :

                                                            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.
                                                            Instances For
                                                              theorem Mathlib.Tactic.Ring.inv_mul {R : Type u_2} [DivisionRing R] {a₁ : R} {a₂ : } {a₃ : R} {b₁ : R} {b₃ : R} {c : R} :
                                                              a₁⁻¹ = b₁a₃⁻¹ = b₃b₃ * (b₁ ^ a₂ * Nat.rawCast 1) = c(a₁ ^ a₂ * a₃)⁻¹ = c
                                                              theorem Mathlib.Tactic.Ring.inv_single {R : Type u_2} [DivisionRing R] {a : R} {b : R} :
                                                              a⁻¹ = b(a + 0)⁻¹ = b + 0
                                                              theorem Mathlib.Tactic.Ring.inv_add {R : Type u_1} [CommSemiring R] {b₁ : R} {b₂ : R} {a₁ : } {a₂ : } :
                                                              a₁ = b₁a₂ = b₂(a₁ + a₂) = b₁ + b₂
                                                              def Mathlib.Tactic.Ring.evalInvAtom {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) (dα : Q(DivisionRing «$α»)) (a : Q(«$α»)) :

                                                              Applies ⁻¹ to a polynomial to get an atom.

                                                              Equations
                                                              Instances For
                                                                def Mathlib.Tactic.Ring.ExProd.evalInv {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) (dα : Q(DivisionRing «$α»)) {a : Q(«$α»)} (czα : Option Q(CharZero «$α»)) (va : Mathlib.Tactic.Ring.ExProd 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.
                                                                Instances For
                                                                  def Mathlib.Tactic.Ring.ExSum.evalInv {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) (dα : Q(DivisionRing «$α»)) {a : Q(«$α»)} (czα : Option Q(CharZero «$α»)) (va : Mathlib.Tactic.Ring.ExSum a) :

                                                                  Inverts a polynomial va to get a normalized result polynomial.

                                                                  • 0⁻¹ = 0
                                                                  • a⁻¹ = (a⁻¹) if a is a nontrivial sum
                                                                  Instances For
                                                                    theorem Mathlib.Tactic.Ring.div_pf {R : Type u_2} [DivisionRing R] {a : R} {b : R} {c : R} {d : R} :
                                                                    b⁻¹ = ca * c = da / b = d
                                                                    def Mathlib.Tactic.Ring.evalDiv {u : Lean.Level} {α : Q(Type u)} (sα : Q(CommSemiring «$α»)) {a : Q(«$α»)} {b : Q(«$α»)} (rα : Q(DivisionRing «$α»)) (czα : Option Q(CharZero «$α»)) (va : Mathlib.Tactic.Ring.ExSum a) (vb : Mathlib.Tactic.Ring.ExSum 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.
                                                                    Instances For
                                                                      theorem Mathlib.Tactic.Ring.add_congr {R : Type u_1} [CommSemiring R] {a : R} {a' : R} {b : R} {b' : R} {c : R} :
                                                                      a = a'b = b'a' + b' = ca + b = c
                                                                      theorem Mathlib.Tactic.Ring.mul_congr {R : Type u_1} [CommSemiring R] {a : R} {a' : R} {b : R} {b' : R} {c : R} :
                                                                      a = a'b = b'a' * b' = ca * b = c
                                                                      theorem Mathlib.Tactic.Ring.nsmul_congr {R : Type u_1} [CommSemiring R] {b : R} {b' : R} {c : R} {a : } {a' : } :
                                                                      a = a'b = b'a' b' = ca b = c
                                                                      theorem Mathlib.Tactic.Ring.pow_congr {R : Type u_1} [CommSemiring R] {a : R} {a' : R} {c : R} {b : } {b' : } :
                                                                      a = a'b = b'a' ^ b' = ca ^ b = c
                                                                      theorem Mathlib.Tactic.Ring.neg_congr {R : Type u_2} [Ring R] {a : R} {a' : R} {b : R} :
                                                                      a = a'-a' = b-a = b
                                                                      theorem Mathlib.Tactic.Ring.sub_congr {R : Type u_2} [Ring R] {a : R} {a' : R} {b : R} {b' : R} {c : R} :
                                                                      a = a'b = b'a' - b' = ca - b = c
                                                                      theorem Mathlib.Tactic.Ring.inv_congr {R : Type u_2} [DivisionRing R] {a : R} {a' : R} {b : R} :
                                                                      a = a'a'⁻¹ = ba⁻¹ = b
                                                                      theorem Mathlib.Tactic.Ring.div_congr {R : Type u_2} [DivisionRing R] {a : R} {a' : R} {b : R} {b' : R} {c : R} :
                                                                      a = a'b = b'a' / b' = ca / b = c

                                                                      A precomputed Cache for .

                                                                      Equations
                                                                      Instances For

                                                                        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.
                                                                        Instances For

                                                                          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.

                                                                          class Mathlib.Tactic.Ring.CSLift (α : Type u) (β : outParam (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 Mathlib.Tactic.Ring.CSLift.lift

                                                                            lift is an injective function

                                                                          Instances
                                                                            theorem Mathlib.Tactic.Ring.CSLift.inj {α : Type u} {β : outParam (Type u)} [self : Mathlib.Tactic.Ring.CSLift α β] :
                                                                            Function.Injective Mathlib.Tactic.Ring.CSLift.lift

                                                                            lift is an injective function

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

                                                                            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.

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

                                                                            Instances

                                                                              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]
                                                                              Equations
                                                                              • =
                                                                              theorem Mathlib.Tactic.Ring.of_lift {α : Type u_2} {β : Type u_2} [inst : Mathlib.Tactic.Ring.CSLift α β] {a : α} {b : α} {a' : β} {b' : β} [h1 : Mathlib.Tactic.Ring.CSLiftVal a a'] [h2 : Mathlib.Tactic.Ring.CSLiftVal b b'] (h : a' = b') :
                                                                              a = b
                                                                              theorem Mathlib.Tactic.Ring.of_eq {α : Sort u_2} {a : α} {b : α} {c : α} :
                                                                              a = cb = ca = b

                                                                              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 to apply the ring_nf simp set to the goal.

                                                                              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.
                                                                              Instances For
                                                                                def Mathlib.Tactic.Ring.proveEq.ringCore {v : Lean.Level} {α : Q(Type v)} (sα : Q(CommSemiring «$α»)) (e₁ : Q(«$α»)) (e₂ : Q(«$α»)) :
                                                                                Mathlib.Tactic.AtomM Q(«$e₁» = «$e₂»)

                                                                                The core of proveEq takes expressions e₁ e₂ : α where α is a CommSemiring, and returns a proof that they are equal (or fails).

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

                                                                                  Tactic for solving equations of commutative (semi)rings, allowing variables in the exponent.

                                                                                  • This version of ring fails if the target is not an equality.
                                                                                  • The variant ring1! 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

                                                                                    Tactic for solving equations of commutative (semi)rings, allowing variables in the exponent.

                                                                                    • This version of ring fails if the target is not an equality.
                                                                                    • The variant ring1! will use a more aggressive reducibility setting to determine equality of atoms.
                                                                                    Equations
                                                                                    Instances For