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.

Instances For

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

    Instances For
      partial def Mathlib.Tactic.Ring.ExBase.eq :
      {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExBase a_1Mathlib.Tactic.Ring.ExBase bBool

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

      partial def Mathlib.Tactic.Ring.ExProd.eq :
      {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExProd a_1Mathlib.Tactic.Ring.ExProd bBool

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

      partial def Mathlib.Tactic.Ring.ExSum.eq :
      {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExSum a_1Mathlib.Tactic.Ring.ExSum bBool

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

      partial def Mathlib.Tactic.Ring.ExBase.cmp :
      {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExBase a_1Mathlib.Tactic.Ring.ExBase bOrdering

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

      partial def Mathlib.Tactic.Ring.ExProd.cmp :
      {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExProd a_1Mathlib.Tactic.Ring.ExProd bOrdering

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

      partial def Mathlib.Tactic.Ring.ExSum.cmp :
      {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → Mathlib.Tactic.Ring.ExSum a_1Mathlib.Tactic.Ring.ExSum bOrdering

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

      instance Mathlib.Tactic.Ring.instInhabitedSigmaQuotedExBase :
      {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → Inhabited ((e : Q(«$arg»)) × Mathlib.Tactic.Ring.ExBase e)
      instance Mathlib.Tactic.Ring.instInhabitedSigmaQuotedExSum :
      {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → Inhabited ((e : Q(«$arg»)) × Mathlib.Tactic.Ring.ExSum e)
      instance Mathlib.Tactic.Ring.instInhabitedSigmaQuotedExProd :
      {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → Inhabited ((e : Q(«$arg»)) × Mathlib.Tactic.Ring.ExProd e)
      partial def Mathlib.Tactic.Ring.ExBase.cast :
      {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 : Q(«$arg»)} → {a_2 : Lean.Level} → {arg_1 : Q(Type a_2)} → { : Q(CommSemiring «$arg_1»)} → Mathlib.Tactic.Ring.ExBase a_1(a : Q(«$arg_1»)) × Mathlib.Tactic.Ring.ExBase a

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

      partial def Mathlib.Tactic.Ring.ExProd.cast :
      {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 : Q(«$arg»)} → {a_2 : Lean.Level} → {arg_1 : Q(Type a_2)} → { : Q(CommSemiring «$arg_1»)} → Mathlib.Tactic.Ring.ExProd a_1(a : Q(«$arg_1»)) × Mathlib.Tactic.Ring.ExProd a

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

      partial def Mathlib.Tactic.Ring.ExSum.cast :
      {a : Lean.Level} → {arg : Q(Type a)} → { : Q(CommSemiring «$arg»)} → {a_1 : Q(«$arg»)} → {a_2 : Lean.Level} → {arg_1 : Q(Type a_2)} → { : Q(CommSemiring «$arg_1»)} → Mathlib.Tactic.Ring.ExSum a_1(a : Q(«$arg_1»)) × Mathlib.Tactic.Ring.ExSum a

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

      instance Mathlib.Tactic.Ring.instInhabitedResult :
      {a : Lean.Level} → {α : Q(Type a)} → {E : Q(«$α»)Type} → {e : Q(«$α»)} → [inst : Inhabited ((e : Q(«$α»)) × E e)] → Inhabited (Mathlib.Tactic.Ring.Result E e)
      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 : ) :
      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} {b₁ : R} {c₁ : R} {a₂ : R} {b₂ : 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} {b₁ : R} {a₂ : 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
      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] {ea : } {eb : } {e : } {a₂ : R} {b₂ : R} {c : R} (x : R) :
      ea + eb = ea₂ * b₂ = cx ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * c
      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} {c₁ : R} {b₂ : R} {c₂ : R} {d : R} :
      a * b₁ = c₁a * b₂ = c₂c₁ + 0 + c₂ = da * (b₁ + b₂) = d
      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} {b : R} {c₁ : R} {a₂ : R} {c₂ : R} {d : R} :
      a₁ * b = c₁a₂ * b = c₂c₁ + c₂ = d(a₁ + a₂) * b = d
      theorem Mathlib.Tactic.Ring.natCast_mul {R : Type u_1} [CommSemiring R] {a₁ : } {b₁ : R} {a₃ : } {b₃ : R} (a₂ : ) :
      a₁ = b₁a₃ = b₃↑(a₁ ^ a₂ * a₃) = b₁ ^ a₂ * b₃
      theorem Mathlib.Tactic.Ring.natCast_add {R : Type u_1} [CommSemiring R] {a₁ : } {b₁ : R} {a₂ : } {b₂ : R} :
      a₁ = b₁a₂ = b₂↑(a₁ + a₂) = b₁ + 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 : } {a' : R} {b : R} {c : R} :
      a = a'a' * b = ca b = c
      theorem Mathlib.Tactic.Ring.neg_one_mul {R : Type u_1} [Ring R] {a : R} {b : R} :
      Int.rawCast (Int.negOfNat 1) * a = b-a = b
      theorem Mathlib.Tactic.Ring.neg_mul {R : Type u_1} [Ring R] (a₁ : R) (a₂ : ) {a₃ : R} {b : R} :
      -a₃ = b-(a₁ ^ a₂ * a₃) = a₁ ^ a₂ * b
      theorem Mathlib.Tactic.Ring.neg_zero {R : Type u_1} [Ring R] :
      -0 = 0
      theorem Mathlib.Tactic.Ring.neg_add {R : Type u_1} [Ring R] {a₁ : R} {a₂ : R} {b₁ : R} {b₂ : R} :
      -a₁ = b₁-a₂ = b₂-(a₁ + a₂) = b₁ + b₂
      theorem Mathlib.Tactic.Ring.sub_pf {R : Type u_1} [Ring R] {a : R} {b : R} {c : R} {d : R} :
      -b = ca + c = da - b = d
      theorem Mathlib.Tactic.Ring.pow_prod_atom {R : Type u_1} [CommSemiring R] (a : R) (b : ) :
      a ^ b = (a + 0) ^ b * Nat.rawCast 1
      theorem Mathlib.Tactic.Ring.pow_atom {R : Type u_1} [CommSemiring R] (a : R) (b : ) :
      a ^ b = a ^ b * Nat.rawCast 1 + 0
      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₂
      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} {k : } {b : R} {c : R} :
      a ^ k = bb * b = ca ^ Nat.mul 2 k = c
      theorem Mathlib.Tactic.Ring.pow_bit1 {R : Type u_1} [CommSemiring R] {a : R} {k : } {b : R} {c : R} {d : R} :
      a ^ k = bb * b = cc * a = da ^ Nat.add (Nat.mul 2 k) 1 = d
      theorem Mathlib.Tactic.Ring.mul_pow {R : Type u_1} [CommSemiring R] {ea₁ : } {b : } {c₁ : } {a₂ : R} {c₂ : R} {xa₁ : R} :
      ea₁ * b = c₁a₂ ^ b = c₂(xa₁ ^ ea₁ * a₂) ^ b = xa₁ ^ c₁ * c₂

      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} {b : } {c : R} :
          a ^ b = c(a + 0) ^ b = c + 0
          theorem Mathlib.Tactic.Ring.pow_nat {R : Type u_1} [CommSemiring R] {b : } {c : } {k : } {a : R} {d : R} {e : R} :
          b = c * ka ^ c = dd ^ k = ea ^ b = e
          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} {b₁ : } {c₁ : R} {b₂ : } {c₂ : R} {d : R} :
          a ^ b₁ = c₁a ^ b₂ = c₂c₁ * c₂ = da ^ (b₁ + b₂) = d
          theorem Mathlib.Tactic.Ring.cast_rat {n : } {d : } {R : Type u_1} [DivisionRing R] {a : R} :
          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') :
          theorem Mathlib.Tactic.Ring.inv_mul {R : Type u_1} [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_1} [DivisionRing R] {a : R} {b : R} :
          a⁻¹ = b(a + 0)⁻¹ = b + 0
          theorem Mathlib.Tactic.Ring.inv_add {R : Type u_1} [CommSemiring R] {a₁ : } {b₁ : R} {a₂ : } {b₂ : R} :
          a₁ = b₁a₂ = b₂↑(a₁ + a₂) = b₁ + b₂
          theorem Mathlib.Tactic.Ring.div_pf {R : Type u_1} [DivisionRing R] {a : R} {b : R} {c : R} {d : R} :
          b⁻¹ = ca * c = da / b = d
          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] {a : } {a' : } {b : R} {b' : R} {c : R} :
          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} {b : } {b' : } {c : R} :
          a = a'b = b'a' ^ b' = ca ^ b = c
          theorem Mathlib.Tactic.Ring.neg_congr {R : Type u_1} [Ring R] {a : R} {a' : R} {b : R} :
          a = a'-a' = b-a = b
          theorem Mathlib.Tactic.Ring.sub_congr {R : Type u_1} [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_1} [DivisionRing R] {a : R} {a' : R} {b : R} :
          a = a'a'⁻¹ = ba⁻¹ = b
          theorem Mathlib.Tactic.Ring.div_congr {R : Type u_1} [DivisionRing R] {a : R} {a' : R} {b : R} {b' : R} {c : R} :
          a = a'b = b'a' / b' = ca / b = c
          theorem Mathlib.Tactic.Ring.of_eq {R : Type u_1} {a : R} {c : R} {b : R} :
          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.

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