A short introduction to the grind tactic

6. Satellite solvers🔗

As mentioned earlier, grind employs several satellite solvers to solve problems of a specific nature. Examples of this are cutsat for linear integer arithmetic, ring for algebraic expressions in rings and linarith for linear arithmetic problems not solved by cutsat.

These might have the same names as Mathlib tactics, they are however implemented independently because they are also supposed to support projects that don't depend on Mathlib. As these are basically tactics in their own right, we won't go into how they work here and instead focus on how you can customize them for your project.

In order for these tactic to work in your projects, you often have to implement certain instances.

For cutsat this is for example:

🔗type class
Lean.Grind.ToInt.{u} (α : Type u)
  (range : outParam Lean.Grind.IntInterval) : Type u
Lean.Grind.ToInt.{u} (α : Type u)
  (range :
    outParam Lean.Grind.IntInterval) :
  Type u

ToInt α I asserts that α can be embedded faithfully into an interval I in the integers.

Instance Constructor

Lean.Grind.ToInt.mk.{u}

Methods

toInt : α → ℤ

The embedding function.

toInt_inj : ∀ (x y : α), ↑x = ↑y → x = y

The embedding function is injective.

toInt_mem : ∀ (x : α), ↑x ∈ range

The embedding function lands in the interval.

For ring there are multiple relevant instances. One example here is:

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

A commutative ring, i.e. a ring with commutative multiplication.

Instance Constructor

Lean.Grind.CommRing.mk.{u}

Extends

Methods

add : α → α → α
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
mul : α → α → α
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
natCast : NatCast α
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
ofNat : (n : ℕ) → OfNat α n
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
nsmul : SMul ℕ α
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
npow : HPow α ℕ α
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
add_zero : ∀ (a : α), a + 0 = a
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
add_comm : ∀ (a b : α), a + b = b + a
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
add_assoc : ∀ (a b c : α), a + b + c = a + (b + c)
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
mul_assoc : ∀ (a b c : α), a * b * c = a * (b * c)
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
mul_one : ∀ (a : α), a * 1 = a
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
one_mul : ∀ (a : α), 1 * a = a
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
left_distrib : ∀ (a b c : α), a * (b + c) = a * b + a * c
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
right_distrib : ∀ (a b c : α), (a + b) * c = a * c + b * c
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
zero_mul : ∀ (a : α), 0 * a = 0
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
mul_zero : ∀ (a : α), a * 0 = 0
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
pow_zero : ∀ (a : α), a ^ 0 = 1
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
pow_succ : ∀ (a : α) (n : ℕ), a ^ (n + 1) = a ^ n * a
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
ofNat_succ : ∀ (a : ℕ), OfNat.ofNat (a + 1) = OfNat.ofNat a + 1
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
ofNat_eq_natCast : ∀ (n : ℕ), OfNat.ofNat n = ↑n
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
nsmul_eq_natCast_mul : ∀ (n : ℕ) (a : α), n • a = ↑n * a
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
neg : α → α
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
sub : α → α → α
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
intCast : IntCast α
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
zsmul : SMul ℤ α
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
neg_add_cancel : ∀ (a : α), -a + a = 0
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
sub_eq_add_neg : ∀ (a b : α), a - b = a + -b
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
neg_zsmul : ∀ (i : ℤ) (a : α), -i • a = -(i • a)
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
zsmul_natCast_eq_nsmul : ∀ (n : ℕ) (a : α), ↑n • a = n • a
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
intCast_ofNat : ∀ (n : ℕ), ↑(OfNat.ofNat n) = OfNat.ofNat n
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
intCast_neg : ∀ (i : ℤ), ↑(-i) = -↑i
Inherited from
  1. Lean.Grind.Ring α
  2. Lean.Grind.CommSemiring α
mul_comm : ∀ (a b : α), a * b = b * a

Multiplication is commutative.

If your project is based on Mathlib, you shouldn't have to do anything because Mathlib already derives these instances from the standard Mathlib notions. For example, Mathlib has CommRing.toGrindCommRing.