lots of linarith

Stream: mathlib4

[Matthew Ballard]

The new leader in instructions is now CategoryTheory.ComposableArrows and the load seems to be mainly due to the proliferation of by linarith auto-params.

#9594 uses a macro which tries assumption before linarith and decreases the time by about 15%.

Is there more light-weight tactic for Nat inequalities?

[Heather Macbeth]

This might be a great place to compare performance of linarith and omega?

[Matthew Ballard]

Where does omega live?

[Heather Macbeth]

https://github.com/leanprover/std4/blob/main/Std/Tactic/Omega.lean

[Johan Commelin]

Yes, in my work on showing that the nerve is a quasicategory, I used omega instead. It seems to work quite well.

[Johan Commelin]

But I haven't yet tested the change in mathlib. Curious what will happen!

[Matthew Ballard]

Lots of errors and warnings. Let me make sure I am not doing something wrong

[Matthew Ballard]

`(tactic| first | assumption | omega | linarith)

cuts things by 50-60%

[Matthew Ballard]

Oh wait.

[Matthew Ballard]

I hit a timeout which might have cut the testing short

[Matthew Ballard]

No, cut by 50% after restoring the code generation in the file. Oddly I needed to bump heartbeats on a new declaration

[Matthew Ballard]

Both the heartbeat bumps involve aesop as the auto-param, which then calls this auto-param multiple times

[Heather Macbeth]

Is there anything which omega doesn't solve?

[Matthew Ballard]

Strict inequality?

[Matthew Ballard]

I got a lot of errors with just omega as the auto-param. A quick glance made it seem that those were the majority of the problems

[Heather Macbeth]

Huh, I thought strict inequalities were in scope.

[Matthew Ballard]

I pushed the changes to the PR. Feel free to play with it. There is a docBlame complaint about the macro that I cannot for the life of me fix. I must be doing something silly

[Heather Macbeth]

About to hop on a plane, so only backseat driving from me today :)

[Matthew Ballard]

Free wifi on Delta :)

[Matthew Ballard]

Odds are nontrivial that I am doing something silly though

[Matthew Ballard]

omega doesn't like auto-params

[Matthew Ballard]

import Std.Tactic.Omega

example (i n : Nat) (hi : i ≤ n := by omega) : i < n + 1 := by omega
/-
error:
omega did not find a contradiction:
[1, -1] ∈ [1, ∞)
[0, 1] ∈ [0, ∞)
[1] ∈ [0, ∞)
-/

[Heather Macbeth]

Maybe this is std4#510 again

[Matthew Ballard]

Do we have to do some special incantation to docs#Lean.Meta.getLocalHyps in the presence of auto-params?

[Matthew Ballard]

Yeah that looks correct

[Matthew Ballard]

Huh. It seems like std4#510 doesn't fix this.

[Eric Rodriguez]

Aren't autoParams a different type as oppposed to just metadata?

[Eric Rodriguez]

It may need special support

[Matthew Ballard]

Maybe. I was just pretending

[Matthew Ballard]

This hacky thing makes the example work

import Std.Tactic.Omega

open Lean Elab Tactic in
elab "clean_up"  : tactic =>
  withMainContext do
    let ctx ← Lean.MonadLCtx.getLCtx
    ctx.forM fun decl: Lean.LocalDecl => do
      let declExpr := decl.toExpr
      let declType := decl.type.cleanupAnnotations
      liftMetaTactic fun mvarId => do
        let mvarIdNew ← mvarId.assert (←mkFreshId) declType declExpr
        let (_, mvarIdNew) ← mvarIdNew.intro1P
        return [mvarIdNew]

example (i n : Nat) (hi : i ≤ n := by omega) : i < n + 1 := by
  clean_up
  omega

[Johan Commelin]

cc @Scott Morrison I guess...

[Matthew Ballard]

With a little bit of omega we are speeding up

Benchmark                                            Metric             Change
  ==============================================================================
+ build                                                tactic execution    -7.8%
+ ~Mathlib.Algebra.Homology.ExactSequence              instructions       -10.0%
+ ~Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four   instructions       -69.8%
+ ~Mathlib.CategoryTheory.ComposableArrows             instructions       -46.3%

[Matthew Ballard]

Using the current fallback to linarith implementation

[Matthew Ballard]

Wall clock is -3% also

[Geoffrey Irving]

I'm curious watching this thread: why would omega be faster than linarith? Isn't it way more complicated?

[Matthew Ballard]

All I know was that I was told to use omega so I wouldn't mind being enlightened also

[Joachim Breitner]

But parts of the complications are put there to make it fast :-)

[Josha Dekker]

I don’t want to sidetrack the conversation, but the reason why we don’t do:

• run linarith
• extract the necessary proof steps, use them directly

is that the number of lines required for the proof would be large, right? Would there be some other way around this? E.g. use a companion-file to keep track of long proofs extracted from linarith for a given file? I see the problems with that approach as well, I’m just curious whether there are some thoughts on possible solutions for this?

[Geoffrey Irving]

Joachim Breitner said:

But parts of the complications are put there to make it fast :-)

Sure, but doesn't that imply that linarith could be sped up as well?

[Matthew Ballard]

Joachim Breitner said:

But parts of the complications are put there to make it fast :-)

Myles Garrett driven design

[Geoffrey Irving]

If we moved linarith to std, would it also get way faster? :)

[Mario Carneiro]

Geoffrey Irving said:

I'm curious watching this thread: why would omega be faster than linarith? Isn't it way more complicated?

omega is not using norm_num, which means that all the numeric literals have to be literals. It is written in std which means that it lacks a lot of the features from mathlib tactics, but that also makes it faster

[Mario Carneiro]

It also does not understand anything about the mathlib algebraic hierarchy, which it can get away with because it only works on Nat and Int where the operations are known. So that means no typeclass search which is big

[Patrick Massot]

Josha Dekker said:

I don’t want to sidetrack the conversation, but the reason why we don’t do:

• run linarith
• extract the necessary proof steps, use them directly

In principle it would output a linear_combination call, but this require work (and linear_combination is still only for equalities so far).

[Heather Macbeth]

... which someone should fix

[Eric Rodriguez]

I was talking with some people about making better use of certificate-based proofs in mathlib, as I think a lot of people already love polyrith and extending those methods would be incredible :)

[Heather Macbeth]

Rob pointed out to me a while ago that linarith already constructs the thing that could be the certificate, we just don't have the linear-combination-for-inequalities tactic to record it

[Rob Lewis]

Extending linear_combination to handle inequalities is definitely a known tactic improvement that wouldn't be crazy hard. It's waiting for someone with the time to do it. linarith should then factor through (the backend of) this implementation

[Kim Morrison]

omega is also often faster because it can take shortcuts that linarith can't. In particular, because it works over the integers whenever it notices a common factor in coefficients, it gets to divide through, rounding constant terms in the "favourable" direction. Often this gives a contradiction when linarith would still be dealing with rationals.

[Kim Morrison]

Separately, the implementation of omega tries to short-circuit early wherever possible. I suspect that if you add an "easy" contradiction e.g. x + y < 1 && x + y > 1 to a large and difficult problem then omega will reliably be fast but linarith will sometimes still "do the work". In practice this makes a big difference, so most problems are actually easy, and the only difficult is avoiding working on the irrelevant facts too early.

[Kim Morrison]

@Matthew Ballard, if you are finding first | omega | linarith is necessary in this file, I would love to have the list of examples where omega is failing.

[Matthew Ballard]

I added one to std4#510 - it is auto/opt params

[Matthew Ballard]

I have a fix in #9594 (also above) which cleans those up and adds them to the context before calling omega

[Matthew Ballard]

I am sure there is a more idiomatic way to strip those out from the hypotheses in the context :)

[Kim Morrison]

std4#518

[Matthew Ballard]

Using std4#518 to fully swap out

  Benchmark                                                           Metric             Change
  =============================================================================================
+ build                                                               tactic execution    -8.8%
+ ~Mathlib.Algebra.Homology.ExactSequence                             instructions       -66.9%
+ ~Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four                  instructions       -75.9%
+ ~Mathlib.CategoryTheory.ComposableArrows                            instructions       -53.4%
- ~Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit   instructions        19.5%

with -3% build wall-clock

[Kim Morrison]

That's over all of Mathlib?!

[Matthew Ballard]

Yes #9594

[Kim Morrison]

Nice!

[Kim Morrison]

Do you know what the deal is in FilteredColimitCommutesFiniteLimit?

[Matthew Ballard]

No idea

[Mario Carneiro]

It would be great to have a more targeted head-to-head demonstrating linarith being slower than omega, that smells like some missing optimization work

[Matthew Ballard]

I imagine you can specialize ComposableArrows to Type u

[Mario Carneiro]

I definitely second Scott's observation that linarith needs to get better at handling easy cases; I see people using linarith so often to prove really silly things like 2 + 2 = 4

[Mario Carneiro]

I mean a microbenchmark, a single problem rather than a whole file

[Matthew Ballard]

OK

[Rob Lewis]

Improving zify would be a huge help on its own. This takes .26 sec over Nat and .15 over Int. (Compare to .07 for omega, and negligible time for norm_num.)

example : (100:ℤ)*100 = 10000 := by
  linarith

[Eric Rodriguez]

oh, linarith only works on Nat/Int because of zify?

[Rob Lewis]

linarith needs subtraction, so it only works on Nat because of zify. Support for Int is native but the algorithm isn't complete in this setting.

[Matthew Ballard]

import Std.Tactic.Omega
import Mathlib.Tactic.Linarith

set_option profiler.threshold 1 in
set_option profiler true in
example (i j n : Nat) (hij : i ≤ j) (hj : j ≤ n) : i ≤ n := by omega
/-
tactic execution of Std.Tactic.Omega.omegaSyntax took 11.7ms
type checking took 9.1ms
-/

set_option profiler.threshold 1 in
set_option profiler true in
example (i j n : Nat) (hij : i ≤ j) (hj : j ≤ n) : i ≤ n := by linarith
/-
simp took 1.53ms
simp took 1.32ms
simp took 1.52ms
typeclass inference of CovariantClass took 2.16ms
typeclass inference of NeZero took 1.58ms
ring took 4.8ms
typeclass inference of CovariantClass took 2.88ms
tactic execution of linarith took 23.1ms
type checking took 3.82ms
-/

There were lots of things like this in ComposableArrows

[Eric Rodriguez]

Rob Lewis said:

linarith needs subtraction, so it only works on Nat because of zify. Support for Int is native but the algorithm isn't complete in this setting.

could this all be replaced with qify/rify?

[Rob Lewis]

In that example too, linarith spends half its time in zify. It's still not as fast as omega but much closer

[Matthew Ballard]

The overall drop in instructions across the file was a little over a half from the swap

[Rob Lewis]

Eric Rodriguez said:

Rob Lewis said:

linarith needs subtraction, so it only works on Nat because of zify. Support for Int is native but the algorithm isn't complete in this setting.

could this all be replaced with qify/rify?

My impression is that zify does extra things, in particular to try to make sense of nat subtraction when possible. And you don't want to translate nat problems to rat for linarith, because it has some tricks that only apply on int

[Matthew Ballard]

One could probably shrink this file down to nothing with a more simple-minded tactic that just tried using reflexivity and transitivity.

[Eric Rodriguez]

what tricks are those? taking advantage of stuff like 1 < x is the same as 2 ≤ x? I should hope rify and qify deal with nat-subtraction too.

[Rob Lewis]

what tricks are those? taking advantage of stuff like 1 < x is the same as 2 ≤ x?

Yes, exactly.

[Rob Lewis]

You're right, rify does do conditional simplification. I don't know why the implementations of rify and zify are different. rify seems to be much slower, compare:

import Std.Tactic.Omega
import Mathlib.Tactic.Linarith
import Mathlib.Tactic.Rify

set_option profiler.threshold 1 in
set_option profiler true in
example (n : ℕ) (hn : 1 < n) : 0 < n - 1 := by
  -- rify [hn]
  zify [hn]

[Kim Morrison]

Obviously omega has to do something equivalent to zify, as well. My initial draft of the frontend for omega in fact did use zify, but it was obviously too slow. One obstacle is simply that zify uses the simplifier, and will traverse deep subexpressions in irrelevant hypotheses looking for things to do. The omega frontend instead inspects hypotheses structurally from the top down, stopping as soon as it reaches a subexpression which is not "in scope".

[Yaël Dillies]

So we could "just" do that in zify too?

[Kim Morrison]

Quite likely!