linarith

Stream: mathlib4

[Dan Velleman]

I'm finding linarith to be somewhat unpredictable. Here's an example:

import Mathlib

example (n : Nat) (h1 : ¬n = 1) (h2 : n ≥ 1) : n ≥ 2 := by
  by_contra h3
  suffices n = 1 by exact h1 this
  linarith

example (n : Nat) (h1 : ¬n = 1) (h2 : n ≥ 1) : n ≥ 2 := by
  have h4 : n ≥ 1 := h2
  by_contra h3
  suffices n = 1 by exact h1 this
  linarith

In the first example, linarith works, and in the second it doesn't. Why?

(I know these examples are somewhat convoluted, but it took me a while to find a MWE to illustrate the inconsistency I've been seeing.)

[Jireh Loreaux]

There was some discussion at the porting meeting last week of a not-easy-to-fix bug in linarith related to when it throws away certain hypotheses. A quick fix to the bug would make linarith take a huge performance hit, but I don't think anyone who knows enough about the algorithm has had the time to sit down and debug it. I'm not sure if that's what is going on here or not though.

[Heather Macbeth]

Also, linarith doesn't yet deal with fractions -- it needs the same second pass that norm_num, ring and positivity have had (thanks @Thomas Murrills!).

[Heather Macbeth]

So this kind of Lean 3 linarith capability isn't available yet:

import tactic.linarith

example {a b : ℚ} (h : (a + b) / 2 ≤ b) : a ≤ b := by linarith

[Heather Macbeth]

However, I think this example is probably none of those things, but instead the kind of bug @Mario Carneiro has been fixing in other tactics, about updates to the goal state not being handled correctly by the tactic.

[Mario Carneiro]

PSA: Please don't use import Mathlib in MWEs

[Heather Macbeth]

Looking at the trace using

set_option trace.linarith true
set_option trace.linarith.detail true

the issue seems to be that in the second one, the "assumed-for-the-sake-of-contradiction" hypothesis isn't picked up by linarith:

[linarith] Preprocessing: split conjunctions

[linarith] [ℕ, n ≥ 1, ¬n ≥ 2, 1 < n]

[linarith] Preprocessing: filter terms that are not proofs of comparisons

[linarith] [n ≥ 1, 1 < n]

[Heather Macbeth]

Whereas in the first one it is:

[linarith] Preprocessing: split conjunctions

[linarith] [ℕ, n ≥ 1, ¬n ≥ 2, 1 < n]

[linarith] Preprocessing: filter terms that are not proofs of comparisons

[linarith] [n ≥ 1, ¬n ≥ 2, 1 < n]

[Mario Carneiro]

!4#2173

[Dan Velleman]

I think I figured out what was happening in my examples. In the first example, when linarith is called, h3 is:

(app (const `Not []) (app (app (app (app (const `GE.ge [0])  etc.

But in the second one, it is:

(app (const `Not []) (mdata [(noImplicitLambda, true)] (app (app (app (app (const `GE.ge [0]) etc.

linarith doesn't look past the mdata, so it doesn't see that it is a negated ≥ statement.

The have h4 tactic adds the mdata to the goal (why?), and then by_contra leaves it there and adds a Not.

I wonder if this is a common pitfall in tactic writing--like forgetting to call withMainContext. I have certainly made both mistakes myself, resulting in tactics that sometimes work and sometimes don't.

[David Renshaw]

a previous example of this coming up: !4#1930

[Heather Macbeth]

and another:
https://github.com/leanprover-community/mathlib4/pull/1394/commits/52866b88dcd432ab2b1f3f9459d2788d3ea33dd6

[Thomas Murrills]

Are there “general rules” for when you need whnfR and when you don’t? It seems like you need it whenever you match on the actual form of an expression to either guard or extract data, at least.

Are there other cases? Do you e.g. need it after constructing expressions which you might assign metavariables to?

[Thomas Murrills]

And is there a general heuristic for “whose” responsibility it is to call whnfR: the thing that makes the expression, or the thing that eats it? Could we avoid some headaches by putting it in things like e.g. isEq, or is it expensive to perform/check if already performed?

[Mario Carneiro]

Thomas Murrills said:

And is there a general heuristic for “whose” responsibility it is to call whnfR: the thing that makes the expression, or the thing that eats it?

The thing that matches the expression is responsible for doing whatever reduction is necessary to recognize whatever is being identified

[Jannis Limperg]

There are a few different issues here:

• When you match on an expression, you should ask yourself whether to match structurally or up to computation.
• If structurally, you should ask yourself whether you want to ignore mdata. It's been suggested before that matching functions should ignore mdata by default, but currently this needs to be done explicitly.
• If up to computation, you should ask yourself which transparency is appropriate. You also need to make sure that you call the appropriate whnf variant multiple times if you match more than one level deep.

It's unfortunate that this is so complex (and some of the APIs could be improved), but the issue is partly inherent to the system: dependent type theory blesses and burdens us with pervasive computation.

[Tchsurvives]

Heather Macbeth said:

So this kind of Lean 3 linarith capability isn't available yet:

import tactic.linarith

example {a b : ℚ} (h : (a + b) / 2 ≤ b) : a ≤ b := by linarith

It seems that linarith is still unable to handle fractions, if it’s a porting issue, could someone point me somewhere? I am interested in implementing it

[Alex J. Best]

#3801 should have fixed this, the following now works in mathlib4 for me

import Mathlib.Tactic.Linarith

example {a b : ℚ} (h : (a + b) / 2 ≤ b) : a ≤ b := by linarith

do you have a failing example?

[Mario Carneiro]

!4#3801

[Tchsurvives]

Alex J. Best said:

do you have a failing example?

I was trying to do lean tutorials (00_first_proofs.lean) and this failed for me

example {x y : ℝ} : (∀ ε > 0, y ≤ x + ε) →  y ≤ x := by
  contrapose!
  intro hxy
  use (y-x)/2
  apply And.intro
  have key := calc
    y ≤ x + (y-x)/2 := by sorry
    _ = x/2 + y/2 := by ring
    _ < y := by linarith  -- this failed

[Tchsurvives]

oh wait, strangely the example you provided doesn't work for me either. might be my version version 4.0.0-nightly-2023-04-20, commit f9da1d8b55ca

[Alex J. Best]

Yeah that mathlib PR was only merged a couple of weeks back, so you probably need to update mathlib

[Tchsurvives]

Alex J. Best said:

Yeah that mathlib PR was only merged a couple of weeks back, so you probably need to update mathlib

You were right! Thanks alot it works now!!