Automation for proving inequalities in commutative (semi)rings

This file provides automation for proving certain kinds of inequalities in commutative semirings: goals of the form A ≤ B and A < B for which the ring-normal forms of A and B differ by a nonnegative (resp. positive) constant.

For example, ⊢ x + 3 + y < y + x + 4 is in scope because the normal forms of the LHS and RHS are, respectively, 3 + (x + y) and 4 + (x + y), which differ by an additive constant.

Main declarations

• Mathlib.Tactic.Ring.proveLE: prove goals of the form A ≤ B (subject to the scope constraints described)
• Mathlib.Tactic.Ring.proveLT: prove goals of the form A < B (subject to the scope constraints described)

Implementation notes

The automation is provided in the MetaM monad; that is, these functions are not user-facing. It would not be hard to provide user-facing versions (see the test file), but the scope of this automation is rather specialized and might be confusing to users. It is also subsumed by linarith.

Rather than having the metaprograms Mathlib.Tactic.Ring.evalLE and Mathlib.Tactic.Ring.evalLT perform all type class inference at the point of use, we record in advance, as abbrevs, a few type class deductions which will certainly be necessary. They add no new information (they can already be proved by inferInstance).

This helps in speeding up the metaprograms in this file substantially -- about a 50% reduction in heartbeat count in representative test cases -- since otherwise a substantial fraction of their runtime is devoted to type class inference.

@[reducible, inline]

abbrev Mathlib.Tactic.Ring.cs_of_ocs (α : Type u_1) [OrderedCommSemiring α] : CommSemiring α

OrderedCommSemiring implies CommSemiring.

Equations

• Mathlib.Tactic.Ring.cs_of_ocs α = inferInstance

@[reducible, inline]

abbrev Mathlib.Tactic.Ring.amwo_of_ocs (α : Type u_1) [OrderedCommSemiring α] : AddMonoidWithOne α

OrderedCommSemiring implies AddMonoidWithOne.

Equations

• Mathlib.Tactic.Ring.amwo_of_ocs α = inferInstance

@[reducible, inline]

abbrev Mathlib.Tactic.Ring.le_of_ocs (α : Type u_1) [OrderedCommSemiring α] : LE α

OrderedCommSemiring implies LE.

Equations

• Mathlib.Tactic.Ring.le_of_ocs α = inferInstance

@[reducible, inline]

abbrev Mathlib.Tactic.Ring.cs_of_socs (α : Type u_1) [StrictOrderedCommSemiring α] : CommSemiring α

StrictOrderedCommSemiring implies CommSemiring.

Equations

• Mathlib.Tactic.Ring.cs_of_socs α = inferInstance

@[reducible, inline]

abbrev Mathlib.Tactic.Ring.amwo_of_socs (α : Type u_1) [StrictOrderedCommSemiring α] : AddMonoidWithOne α

StrictOrderedCommSemiring implies AddMonoidWithOne.

Equations

• Mathlib.Tactic.Ring.amwo_of_socs α = inferInstance

@[reducible, inline]

abbrev Mathlib.Tactic.Ring.lt_of_socs (α : Type u_1) [StrictOrderedCommSemiring α] : LT α

StrictOrderedCommSemiring implies LT.

Equations

• Mathlib.Tactic.Ring.lt_of_socs α = inferInstance

The lemmas like add_le_add_right in the root namespace are stated under minimal type classes, typically just [CovariantClass α α (swap (· + ·)) (· ≤ ·)] or similar. Here we restate these lemmas under stronger type class assumptions ([OrderedCommSemiring α] or similar), which helps in speeding up the metaprograms in this file (Mathlib.Tactic.Ring.proveLT and Mathlib.Tactic.Ring.proveLE) substantially -- about a 50% reduction in heartbeat count in representative test cases -- since otherwise a substantial fraction of their runtime is devoted to type class inference.

These metaprograms at least require CommSemiring, LE/LT, and all CovariantClass/ContravariantClass permutations for addition, and in their main use case (in linear_combination) the Preorder type class is also required, so it is rather little loss of generality simply to require OrderedCommSemiring/StrictOrderedCommSemiring.

theorem Mathlib.Tactic.Ring.add_le_add_right {α : Type u_1} [OrderedCommSemiring α] {b : α} {c : α} (bc : b ≤ c) (a : α) : b + a ≤ c + a

theorem Mathlib.Tactic.Ring.add_le_of_nonpos_left {α : Type u_1} [OrderedCommSemiring α] (a : α) {b : α} (h : b ≤ 0) : b + a ≤ a

theorem Mathlib.Tactic.Ring.le_add_of_nonneg_left {α : Type u_1} [OrderedCommSemiring α] (a : α) {b : α} (h : 0 ≤ b) : a ≤ b + a

theorem Mathlib.Tactic.Ring.add_lt_add_right {α : Type u_1} [StrictOrderedCommSemiring α] {b : α} {c : α} (bc : b < c) (a : α) : b + a < c + a

theorem Mathlib.Tactic.Ring.add_lt_of_neg_left {α : Type u_1} [StrictOrderedCommSemiring α] (a : α) {b : α} (h : b < 0) : b + a < a

theorem Mathlib.Tactic.Ring.lt_add_of_pos_left {α : Type u_1} [StrictOrderedCommSemiring α] (a : α) {b : α} (h : 0 < b) : a < b + a

inductive Mathlib.Tactic.Ring.ExceptType : Type

Inductive type carrying the two kinds of errors which can arise in the metaprograms Mathlib.Tactic.Ring.evalLE and Mathlib.Tactic.Ring.evalLT.

• tooSmall: Mathlib.Tactic.Ring.ExceptType
• notComparable: Mathlib.Tactic.Ring.ExceptType

def Mathlib.Tactic.Ring.evalLE {v : Lean.Level} {α : Q(Type v)} : (x : Q(OrderedCommSemiring «$α»)) → {a b : Q(«$α»)} → Mathlib.Tactic.Ring.ExSum q(Mathlib.Tactic.Ring.cs_of_ocs «$α») a → Mathlib.Tactic.Ring.ExSum q(Mathlib.Tactic.Ring.cs_of_ocs «$α») b → Lean.MetaM (Except Mathlib.Tactic.Ring.ExceptType Q(«$a» ≤ «$b»))

In a commutative semiring, given Ring.ExSum objects va, vb which differ by a positive (additive) constant, construct a proof of $a < $b, where a (resp. b) is the expression in the semiring to which va (resp. vb) evaluates.

Equations

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

def Mathlib.Tactic.Ring.evalLT {v : Lean.Level} {α : Q(Type v)} : (x : Q(StrictOrderedCommSemiring «$α»)) → {a b : Q(«$α»)} → Mathlib.Tactic.Ring.ExSum q(Mathlib.Tactic.Ring.cs_of_socs «$α») a → Mathlib.Tactic.Ring.ExSum q(Mathlib.Tactic.Ring.cs_of_socs «$α») b → Lean.MetaM (Except Mathlib.Tactic.Ring.ExceptType Q(«$a» < «$b»))

In a commutative semiring, given Ring.ExSum objects va, vb which differ by a positive (additive) constant, construct a proof of $a < $b, where a (resp. b) is the expression in the semiring to which va (resp. vb) evaluates.

Equations

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

theorem Mathlib.Tactic.Ring.le_congr {α : Type u_1} [LE α] {a : α} {b : α} {c : α} {d : α} (h1 : a = b) (h2 : b ≤ c) (h3 : d = c) : a ≤ d

theorem Mathlib.Tactic.Ring.lt_congr {α : Type u_1} [LT α] {a : α} {b : α} {c : α} {d : α} (h1 : a = b) (h2 : b < c) (h3 : d = c) : a < d

def Mathlib.Tactic.Ring.proveLE (g : Lean.MVarId) : Lean.MetaM Unit

Prove goals of the form A ≤ B in an ordered commutative semiring, if the ring-normal forms of A and B differ by a nonnegative (additive) constant.

Equations

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

def Mathlib.Tactic.Ring.proveLT (g : Lean.MVarId) : Lean.MetaM Unit

Prove goals of the form A < B in an ordered commutative semiring, if the ring-normal forms of A and B differ by a positive (additive) constant.

Equations

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