The Lean Language Reference

17.11. Linear Arithmetic Solver

grind also contains a linear arithmetic linarith solver parametrized by type classes. It self-configures depending on the availability of these type classes, so not all need to be provided. The capabilities of the linarith solver will of course degrade when some are not available. The solver ignores any type supported by cutsat. This module is useful for reasoning about Real, ordered vector spaces, etc.

The main type classes for module structures are NatModule (every Semiring is a NatModule) and IntModule (every Ring is an IntModule). These may interact with the three order classes Preorder, PartialOrder, and LinearOrder. (Typically a Preorder is enough when the context already includes a contradiction, but to prove linear inequality goals you will need a LinearOrder.) To express that the additive structure in a module is compatible with the order we need OrderedAdd. We have limited support for ordered rings at present, represented by the typeclass OrderedRing.

🔗type class
Lean.Grind.NatModule.{u} (M : Type u) : Type u
Lean.Grind.NatModule.{u} (M : Type u) : Type u

A module over the natural numbers, i.e. a type with zero, addition, and scalar multiplication by natural numbers, satisfying appropriate compatibilities.

Equivalently, an additive commutative monoid.

Use IntModule if the type has negation.

Instance Constructor

Lean.Grind.NatModule.mk.{u}

Extends

Methods

zero : M
Inherited from
  1. Lean.Grind.AddCommMonoid M
add : M  M  M
Inherited from
  1. Lean.Grind.AddCommMonoid M
add_zero :  (a : M), a + 0 = a
Inherited from
  1. Lean.Grind.AddCommMonoid M
add_comm :  (a b : M), a + b = b + a
Inherited from
  1. Lean.Grind.AddCommMonoid M
add_assoc :  (a b c : M), a + b + c = a + (b + c)
Inherited from
  1. Lean.Grind.AddCommMonoid M
nsmul : HMul Nat M M

Scalar multiplication by natural numbers.

zero_nsmul :  (a : M), 0 * a = 0

Scalar multiplication by zero is zero.

one_nsmul :  (a : M), 1 * a = a

Scalar multiplication by one is the identity.

add_nsmul :  (n m : Nat) (a : M), (n + m) * a = n * a + m * a

Scalar multiplication is distributive over addition in the natural numbers.

nsmul_zero :  (n : Nat), n * 0 = 0

Scalar multiplication of zero is zero.

nsmul_add :  (n : Nat) (a b : M), n * (a + b) = n * a + n * b

Scalar multiplication is distributive over addition in the module.

🔗type class
Lean.Grind.IntModule.{u} (M : Type u) : Type u
Lean.Grind.IntModule.{u} (M : Type u) : Type u

A module over the integers, i.e. a type with zero, addition, negation, subtraction, and scalar multiplication by integers, satisfying appropriate compatibilities.

Equivalently, an additive commutative group.

Instance Constructor

Lean.Grind.IntModule.mk.{u}

Extends

Methods

zero : M
Inherited from
  1. Lean.Grind.AddCommGroup M
add : M  M  M
Inherited from
  1. Lean.Grind.AddCommGroup M
add_zero :  (a : M), a + 0 = a
Inherited from
  1. Lean.Grind.AddCommGroup M
add_comm :  (a b : M), a + b = b + a
Inherited from
  1. Lean.Grind.AddCommGroup M
add_assoc :  (a b c : M), a + b + c = a + (b + c)
Inherited from
  1. Lean.Grind.AddCommGroup M
neg : M  M
Inherited from
  1. Lean.Grind.AddCommGroup M
sub : M  M  M
Inherited from
  1. Lean.Grind.AddCommGroup M
neg_add_cancel :  (a : M), -a + a = 0
Inherited from
  1. Lean.Grind.AddCommGroup M
sub_eq_add_neg :  (a b : M), a - b = a + -b
Inherited from
  1. Lean.Grind.AddCommGroup M
nsmul : HMul Nat M M

Scalar multiplication by natural numbers.

zsmul : HMul Int M M

Scalar multiplication by integers.

zero_zsmul :  (a : M), 0 * a = 0

Scalar multiplication by zero is zero.

one_zsmul :  (a : M), 1 * a = a

Scalar multiplication by one is the identity.

add_zsmul :  (n m : Int) (a : M), (n + m) * a = n * a + m * a

Scalar multiplication is distributive over addition in the integers.

zsmul_zero :  (n : Int), n * 0 = 0

Scalar multiplication of zero is zero.

zsmul_add :  (n : Int) (a b : M), n * (a + b) = n * a + n * b

Scalar multiplication by integers is distributive over addition in the module.

zsmul_natCast_eq_nsmul :  (n : Nat) (a : M), n * a = n * a

Scalar multiplication by natural numbers is consistent with scalar multiplication by integers.

🔗type class
Lean.Grind.Preorder.{u} (α : Type u) : Type u
Lean.Grind.Preorder.{u} (α : Type u) : Type u

A preorder is a reflexive, transitive relation with a < b defined in the obvious way.

Instance Constructor

Lean.Grind.Preorder.mk.{u}

Extends

Methods

le : α  α  Prop
Inherited from
  1. LE α
  2. LT α
lt : α  α  Prop
Inherited from
  1. LE α
  2. LT α
le_refl :  (a : α), a  a

The less-than-or-equal relation is reflexive.

le_trans :  {a b c : α}, a  b  b  c  a  c

The less-than-or-equal relation is transitive.

lt_iff_le_not_le :  {a b : α}, a < b  a  b  ¬b  a

The less-than relation is determined by the less-than-or-equal relation.

🔗type class
Lean.Grind.PartialOrder.{u} (α : Type u) : Type u
Lean.Grind.PartialOrder.{u} (α : Type u) : Type u

A partial order is a preorder with the additional property that a b and b a implies a = b.

Instance Constructor

Lean.Grind.PartialOrder.mk.{u}

Extends

Methods

le : α  α  Prop
Inherited from
  1. Lean.Grind.Preorder α
lt : α  α  Prop
Inherited from
  1. Lean.Grind.Preorder α
le_refl :  (a : α), a  a
Inherited from
  1. Lean.Grind.Preorder α
le_trans :  {a b c : α}, a  b  b  c  a  c
Inherited from
  1. Lean.Grind.Preorder α
lt_iff_le_not_le :  {a b : α}, a < b  a  b  ¬b  a
Inherited from
  1. Lean.Grind.Preorder α
le_antisymm :  {a b : α}, a  b  b  a  a = b

The less-than-or-equal relation is antisymmetric.

🔗type class
Lean.Grind.LinearOrder.{u} (α : Type u) : Type u
Lean.Grind.LinearOrder.{u} (α : Type u) : Type u

A linear order is a partial order with the additional property that every pair of elements is comparable.

Instance Constructor

Lean.Grind.LinearOrder.mk.{u}

Extends

Methods

le : α  α  Prop
Inherited from
  1. Lean.Grind.PartialOrder α
lt : α  α  Prop
Inherited from
  1. Lean.Grind.PartialOrder α
le_refl :  (a : α), a  a
Inherited from
  1. Lean.Grind.PartialOrder α
le_trans :  {a b c : α}, a  b  b  c  a  c
Inherited from
  1. Lean.Grind.PartialOrder α
lt_iff_le_not_le :  {a b : α}, a < b  a  b  ¬b  a
Inherited from
  1. Lean.Grind.PartialOrder α
le_antisymm :  {a b : α}, a  b  b  a  a = b
Inherited from
  1. Lean.Grind.PartialOrder α
le_total :  (a b : α), a  b  b  a

For every two elements a and b, either a b or b a.

🔗type class
Lean.Grind.OrderedAdd.{u} (M : Type u) [HAdd M M M] [Lean.Grind.Preorder M] : Prop
Lean.Grind.OrderedAdd.{u} (M : Type u) [HAdd M M M] [Lean.Grind.Preorder M] : Prop

Addition is compatible with a preorder if a b a + c b + c.

Instance Constructor

Lean.Grind.OrderedAdd.mk.{u}

Methods

add_le_left_iff :  {a b : M} (c : M), a  b  a + c  b + c

a + c b + c iff a b.

🔗type class
Lean.Grind.OrderedRing.{u} (R : Type u) [Lean.Grind.Semiring R] [Lean.Grind.Preorder R] : Prop
Lean.Grind.OrderedRing.{u} (R : Type u) [Lean.Grind.Semiring R] [Lean.Grind.Preorder R] : Prop

A ring which is also equipped with a preorder is considered a strict ordered ring if addition, negation, and multiplication are compatible with the preorder, and 0 < 1.

Instance Constructor

Lean.Grind.OrderedRing.mk.{u}

Extends

Methods

add_le_left_iff :  {a b : R} (c : R), a  b  a + c  b + c
Inherited from
  1. Lean.Grind.OrderedAdd R
zero_lt_one : 0 < 1

In a strict ordered semiring, we have 0 < 1.

mul_lt_mul_of_pos_left :  {a b c : R}, a < b  0 < c  c * a < c * b

In a strict ordered semiring, we can multiply an inequality a < b on the left by a positive element 0 < c to obtain c * a < c * b.

mul_lt_mul_of_pos_right :  {a b c : R}, a < b  0 < c  a * c < b * c

In a strict ordered semiring, we can multiply an inequality a < b on the right by a positive element 0 < c to obtain a * c < b * c.

The core functionality of linarith is a model based solver for linear inequalities with integer coefficients. You can disable this solver using the option grind -linarith.

The following examples demonstrate goals that can be decided by the linarith solver.

variable [IntModule α] [LinearOrder α] [OrderedAdd α] example (a b : α) : 2*a + b b + a + a := α:Type u_1inst✝²:IntModule αinst✝¹:LinearOrder αinst✝:OrderedAdd αa:αb:α2 * a + b b + a + a All goals completed! 🐙 example (a b : α) (h : a b) : 3 * a + b 4 * b := α:Type u_1inst✝²:IntModule αinst✝¹:LinearOrder αinst✝:OrderedAdd αa:αb:αh:a b3 * a + b 4 * b All goals completed! 🐙 example (a b c : α) (_ : a = b + c) (_ : 2 * b c) : 2 * a 3 * c := α:Type u_1inst✝²:IntModule αinst✝¹:LinearOrder αinst✝:OrderedAdd αa:αb:αc:αx✝¹:a = b + cx✝:2 * b c2 * a 3 * c All goals completed! 🐙 example (a b c d e : α) : 2*a + b 0 b 0 c 0 d 0 e 0 a 3*c c 6*e d - 5*e 0 a + b + 3*c + d + 2*e < 0 False := α:Type u_1inst✝²:IntModule αinst✝¹:LinearOrder αinst✝:OrderedAdd αa:αb:αc:αd:αe:α2 * a + b 0 b 0 c 0 d 0 e 0 a 3 * c c 6 * e d - 5 * e 0 a + b + 3 * c + d + 2 * e < 0 False All goals completed! 🐙

At present we only use the CommRing structure to do basic normalization (e.g. identifying linear atoms a * b and b * a), and to allow constants (with the fact 0 < 1) and scalar multiplication on both sides.

variable [CommRing R] [LinearOrder R] [OrderedRing R] example (a b : R) (h : a * b 1) : b * 3 * a + 1 4 := R:Type u_1inst✝²:CommRing Rinst✝¹:LinearOrder Rinst✝:OrderedRing Ra:Rb:Rh:a * b 1b * 3 * a + 1 4 All goals completed! 🐙 example (a b c d e f : R) : 2*a + b 1 b 0 c 0 d 0 e*f 0 a 3*c c 6*e*f d - f*e*5 0 a + b + 3*c + d + 2*e*f < 0 False := R:Type u_1inst✝²:CommRing Rinst✝¹:LinearOrder Rinst✝:OrderedRing Ra:Rb:Rc:Rd:Re:Rf:R2 * a + b 1 b 0 c 0 d 0 e * f 0 a 3 * c c 6 * e * f d - f * e * 5 0 a + b + 3 * c + d + 2 * e * f < 0 False All goals completed! 🐙

Planned future features

  • Support for NatModule (by embedding in the Grothendieck envelope, as we already do for semirings),

  • Better communication between the ring and linarith solvers. There is currently very little communication between these two solvers.

  • Non-linear arithmetic over ordered rings.