The bound tactic

bound is an aesop wrapper that proves inequalities by straightforward recursion on structure, assuming that intermediate terms are nonnegative or positive as needed. It also has some support for guessing where it is unclear where to recurse, such as which side of a min or max to use as the bound or whether to assume a power is less than or greater than one.

The functionality of bound overlaps with positivity and gcongr, but can jump back and forth between 0 ≤ x and x ≤ y-type inequalities. For example, bound proves 0 ≤ c → b ≤ a → 0 ≤ a * c - b * c by turning the goal into b * c ≤ a * c, then using mul_le_mul_of_nonneg_right. bound also uses specialized lemmas for goals of the form 1 ≤ x, 1 < x, x ≤ 1, x < 1.

Additional hypotheses can be passed as bound [h0, h1 n, ...]. This is equivalent to declaring them via have before calling bound.

See test/Bound.lean for tests.

Calc usage

Since bound requires the inequality proof to exactly match the structure of the expression, it is often useful to iterate between bound and rw / simp using calc. Here is an example:

-- Calc example: A weak lower bound for `z ↦ z^2 + c`
lemma le_sqr_add {c z : ℂ} (cz : abs c ≤ abs z) (z3 : 3 ≤ abs z) :
    2 * abs z ≤ abs (z^2 + c) := by
  calc abs (z^2 + c)
    _ ≥ abs (z^2) - abs c := by bound
    _ ≥ abs (z^2) - abs z := by bound
    _ ≥ (abs z - 1) * abs z := by rw [mul_comm, mul_sub_one, ← pow_two, ← abs.map_pow]
    _ ≥ 2 * abs z := by bound

Aesop rules

bound uses threes types of aesop rules: apply, forward, and closing tactics. To register a lemma as an apply rule, tag it with @[bound]. It will be automatically converted into either a norm apply or safe apply rule depending on the number and type of its hypotheses:

1. Nonnegativity/positivity/nonpositivity/negativity hypotheses get score 1 (those involving 0).
2. Other inequalities get score 10.
3. Disjunctions a ∨ b get score 100, plus the score of a and b.

Score 0 lemmas turn into norm apply rules, and score 0 < s lemmas turn into safe apply s rules. The score is roughly lexicographic ordering on the counts of the three type (guessing, general, involving-zero), and tries to minimize the complexity of hypotheses we have to prove. See Mathlib.Tactic.Bound.Attribute for the full algorithm.

To register a lemma as a forward rule, tag it with @[bound_forward]. The most important builtin forward rule is le_of_lt, so that strict inequalities can be used to prove weak inequalities. Another example is HasFPowerSeriesOnBall.r_pos, so that bound knows that any power series present in the context have positive radius of convergence. Custom @[bound_forward] rules that similarly expose inequalities inside structures are often useful.

Guessing apply rules

There are several cases where there are two standard ways to recurse down an inequality, and it is not obvious which is correct without more information. For example, a ≤ min b c is registered as a safe apply 4 rule, since we always need to prove a ≤ b ∧ a ≤ c. But if we see min a b ≤ c, either a ≤ c or b ≤ c suffices, and we don't know which.

In these cases we declare a new lemma with an ∨ hypotheses that covers the two cases. Tagging it as @[bound] will add a +100 penalty to the score, so that it will be used only if necessary. Aesop will then try both ways by splitting on the resulting ∨ hypothesis.

Currently the two types of guessing rules are

1. min and max rules, for both ≤ and <
2. pow and rpow monotonicity rules which branch on 1 ≤ a or a ≤ 1.

Closing tactics

We close numerical goals with norm_num and linarith.

.mpr lemmas of iff statements for use as Aesop apply rules

Once Aesop can do general terms directly, we can remove these:

https://github.com/leanprover-community/aesop/issues/107

theorem Mathlib.Tactic.Bound.mul_lt_mul_left_of_pos_of_lt {α : Type} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [PosMulStrictMono α] [PosMulReflectLT α] (a0 : 0 < a) : b < c → a * b < a * c

theorem Mathlib.Tactic.Bound.mul_lt_mul_right_of_pos_of_lt {α : Type} {a : α} {b : α} {c : α} [Mul α] [Zero α] [Preorder α] [MulPosStrictMono α] [MulPosReflectLT α] (c0 : 0 < c) : a < b → a * c < b * c

theorem Mathlib.Tactic.Bound.Nat.cast_pos_of_pos {R : Type} [OrderedSemiring R] [Nontrivial R] {n : ℕ} : 0 < n → 0 < ↑n

theorem Mathlib.Tactic.Bound.Nat.one_le_cast_of_le {α : Type} [AddCommMonoidWithOne α] [PartialOrder α] [AddLeftMono α] [ZeroLEOneClass α] [CharZero α] {n : ℕ} : 1 ≤ n → 1 ≤ ↑n

Apply rules for bound

Most bound lemmas are registered in-place where the lemma is declared. These are only the lemmas that do not require additional imports within this file.

Forward rules for bound

Guessing rules: when we don't know how to recurse

theorem Mathlib.Tactic.Bound.le_max_of_le_left_or_le_right {α : Type} [LinearOrder α] {a : α} {b : α} {c : α} : a ≤ b ∨ a ≤ c → a ≤ max b c

theorem Mathlib.Tactic.Bound.lt_max_of_lt_left_or_lt_right {α : Type} [LinearOrder α] {a : α} {b : α} {c : α} : a < b ∨ a < c → a < max b c

theorem Mathlib.Tactic.Bound.min_le_of_left_le_or_right_le {α : Type} [LinearOrder α] {a : α} {b : α} {c : α} : a ≤ c ∨ b ≤ c → min a b ≤ c

theorem Mathlib.Tactic.Bound.min_lt_of_left_lt_or_right_lt {α : Type} [LinearOrder α] {a : α} {b : α} {c : α} : a < c ∨ b < c → min a b < c

Closing tactics

TODO: Kim Morrison noted that we could check for ℕ or ℤ and try omega as well.

def Mathlib.Tactic.Bound.boundNormNum : Aesop.RuleTac

Close numerical goals with norm_num

Equations

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

def Mathlib.Tactic.Bound.boundLinarith : Aesop.RuleTac

Close numerical and other goals with linarith

Equations

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

bound tactic implementation

def Mathlib.Tactic.Bound.boundConfig : Aesop.Options

Aesop configuration for bound

Equations

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

def «tacticBound[_]» : Lean.ParserDescr

bound tactic for proving inequalities via straightforward recursion on expression structure.

An example use case is

-- Calc example: A weak lower bound for `z ↦ z^2 + c`
lemma le_sqr_add {c z : ℂ} (cz : abs c ≤ abs z) (z3 : 3 ≤ abs z) :
    2 * abs z ≤ abs (z^2 + c) := by
  calc abs (z^2 + c)
    _ ≥ abs (z^2) - abs c := by bound
    _ ≥ abs (z^2) - abs z := by bound
    _ ≥ (abs z - 1) * abs z := by rw [mul_comm, mul_sub_one, ← pow_two, ← abs.map_pow]
    _ ≥ 2 * abs z := by bound

bound is built on top of aesop, and uses

1. Apply lemmas registered via the @[bound] attribute
2. Forward lemmas registered via the @[bound_forward] attribute
3. Local hypotheses from the context
4. Optionally: additional hypotheses provided as bound [h₀, h₁] or similar. These are added to the context as if by have := hᵢ.

The functionality of bound overlaps with positivity and gcongr, but can jump back and forth between 0 ≤ x and x ≤ y-type inequalities. For example, bound proves 0 ≤ c → b ≤ a → 0 ≤ a * c - b * c by turning the goal into b * c ≤ a * c, then using mul_le_mul_of_nonneg_right. bound also contains lemmas for goals of the form 1 ≤ x, 1 < x, x ≤ 1, x < 1. Conversely, gcongr can prove inequalities for more types of relations, supports all positivity functionality, and is likely faster since it is more specialized (not built atop aesop).

Equations

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