linear_combination for inequalities

Stream: mathlib4

[Heather Macbeth]

#16841 extends the tactic linear_combination to prove inequalities! From the test file:

example (a b : ℚ) (h1 : a ≤ 1) (h2 : b = 1) : (a + b) / 2 ≤ 1 := by
  linear_combination (h1 + h2) / 2

example {x y : ℤ} (hx : x + 3 ≤ 2) (hy : y + 2 * x ≥ 3) : y > 3 := by
  linear_combination hy + 2 * hx

example {x y z : ℚ} (h1 : 4 * x + y + 3 * z ≤ 25) (h2 : -x + 2 * y + z = 3)
    (h3 : 5 * x + 7 * z = 43) :
    x ≤ 4 := by
  linear_combination (14 * h1 - 7 * h2 - 5 * h3) / 38

example {t : ℚ} (ht : t ≥ 10) : t ^ 2 - 3 * t - 17 ≥ 5 := by
  linear_combination (t + 7) * ht

[Martin Dvořák]

It seems that my duality project is henceforth redundant. JOKE

[Heather Macbeth]

Some rudimentary profiling suggests that on "tiny" problems, linear_combination-for-inequalities is as fast as a rewrite or a proof term, and several times faster than linarith:

import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Mathlib.Data.Real.Basic

variable {a b : ℝ}

-- 730 heartbeats
example (h : a < b) : 0 < b - a := by linarith

-- 223 heartbeats
example (h : a < b) : 0 < b - a := by linear_combination h

-- 278 heartbeats
example (h : a < b) : 0 < b - a := by rwa [sub_pos]

-- 279 heartbeats
example (h : a < b) : 0 < b - a := sub_pos.mpr h

[Heather Macbeth]

This kind of goal is my primary motivation for this feature, so I would be very interested in

• suggestions for measuring this speedup more precisely (on small problems #time has high variance and I am hesitant to draw conclusions)
• suggestions for speeding up further!

[Heather Macbeth]

I thought of one other way to profile small problems: repeat 50 times and #time the whole thing.

import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Mathlib.Data.Real.Basic

variable {a b : ℝ}

syntax "test_tactic" " [" term "]" : tactic

macro_rules | (tactic | test_tactic [$arg])=> (tactic | linear_combination ($arg))
-- macro_rules | (tactic | test_tactic [$arg])=> (tactic | linarith only [$arg])

example (h : a < b) : True := by
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
have : 0 < b - a := by test_tactic [h]
trivial

I assume this is not the right way to do it? (For the record: 761 ms for 50 identical linariths, 483 ms for 50 identical linear_combinations.)

[Kim Morrison]

Use repeat rather than actually repeating. :-)

[Kim Morrison]

And you might add a zero or two!

[Heather Macbeth]

@Kim Morrison What is the syntax? I see the repeat tactic but this doesn't seem to take a parameter for number of iterations? docs#Lean.Parser.Tactic.tacticRepeat_

[Daniel Weber]

I don't know about repeat, but I think you can use iterate (docs#Lean.Parser.Tactic.tacticIterate____)

[Heather Macbeth]

OK, that actually seems pretty stable! For 500 iterations, 1.2 seconds for rwa [sub_pos], 5.2 seconds for linear_combination h, 8.3 seconds for linarith only [h]:

import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LinearCombination
import Mathlib.Data.Real.Basic

variable {a b : ℝ}

#time
set_option maxRecDepth 1600 in
example (h : a < b) : True := by
  iterate 500
    have H : 0 < b - a := by linear_combination h
    clear H
  trivial

[Heather Macbeth]

I assume that when the same tactic call is repeated 500 times, things like typeclass search are cached, so it really is just the tactic execution and typechecking which are being tested?

(Which may not reflect "real-world" conditions ... Is there a way of clearing any cached typeclass searches between iterations?)

[Kim Morrison]

(Oops, sorry, iterate!)

[Damiano Testa]

There is also docs#Mathlib.CountHeartbeats.tacticCount_heartbeats!_In__ that might be useful.

[Heather Macbeth]

Yup, that's how I got these heartbeat counts, but the heartbeat numbers seem not to match my impression of time elapsed.

[Heather Macbeth]

The prerequisites for #16841 (linear_combination-for-inequalities) have all been merged, and this tactic is ready for review!

[Heather Macbeth]

Merged, thanks to Rob!

How do we feel about large-scale squeezing of linarith to linear_combination? See #18841 for the result of doing this in 100 places: it's a modest speedup. On the other hand, it's a slight loss in readability.

We could also have a policy that is "conditional" rather than absolute; for example the policy could be "linariths which depend on only one hypothesis are fair game for squeezing".

[Johan Commelin]

I left some comments. I think squeezing linarith only might be a good rule.

Also, we could rename linear_combination to lincombi if we think that linarith has an unfair advantage for short proofs.

[Michael Rothgang]

I also left some comments: TL;DR is that many changes are clear wins imho, some are neutral to good, and a few I'm less sure about (including because of the length).

[Michael Rothgang]

I think squeezing which avoids extra haves/several lines is clearly better. If the new code is shorter, I think it's also clearly better.

[Heather Macbeth]

Thank you Johan and Michael for going through the diff! But I am realising from your comments that I presented the PR in a way which obscures the linarith/linear_combination discussion, because I also mixed in some golfing which would have worked with either linarith or linear_combination. Let me move that golfing to a separate PR so we have a better basis for the discussion.