linarith regression on real numbers

Stream: mathlib4

[Mauricio Collares]

import Mathlib.Data.Real.Pi.Bounds
-- set_option trace.linarith true
example : 49 ≤ 16 * Real.pi - 1 := by linarith only [Real.pi_gt_3141592]

doesn't work in Lean 4, but

import data.real.pi.bounds
example : 49 ≤ 16 * real.pi - 1 := by linarith only [real.pi_gt_3141592]

worked in Lean 3.

[Notification Bot]

A message was moved here from #mathlib4 > linarith regression by Mauricio Collares.

[Sébastien Gouëzel]

Note that

import Mathlib.Data.Real.Pi.Bounds
example : 49 ≤ 16 * Real.pi - 1 := by
  have : 3.141592 < Real.pi := Real.pi_gt_3141592
  norm_num at this
  linarith

works, but fails without the norm_num line, so it's a OfScientific issue.

[Sébastien Gouëzel]

More minimal example:

import Mathlib.Data.Real.Pi.Bounds
example (a : ℝ) (ha : 1.0 ≤ a) : 1 ≤ a := by
  norm_num at ha
  linarith

fails without the norm_num.

[Anne Baanen]

Interestingly, set_option trace.linarith suggests that it does almost succeed:

[linarith] linarith is running on the following hypotheses:

[linarith] [ℝ, 1.0 ≤ a, 1 > a]

[linarith] Preprocessing: split conjunctions

[linarith] [ℝ, 1.0 ≤ a, 1 > a]

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

[linarith] [1.0 ≤ a, 1 > a]

[linarith] Preprocessing: replace negations of comparisons

[linarith] [1.0 ≤ a, 1 > a]

[linarith] Preprocessing: move nats to ints

[linarith] [1.0 ≤ a, 1 > a]

[linarith] Preprocessing: strengthen strict inequalities over int

[linarith] [1.0 ≤ a, 1 > a]

[linarith] Preprocessing: make comparisons with zero

[linarith] [1.0 - a ≤ 0, a - 1 < 0]

[linarith] Preprocessing: cancel denominators

[linarith] [1.0 - a ≤ 0, a - 1 < 0]

[linarith] after preprocessing, linarith has 2 facts:

[linarith] [1.0 - a ≤ 0, a - 1 < 0]

[linarith] hypotheses appear in 1 different types

[linarith] linarith has found a contradiction: []

[linarith] The expression
      0
    should be both 0 and negative

[Anne Baanen]

Ah nevermind, that's because the simplex algorithm oracle returns an empty proof when it fails.

[Anne Baanen]

linarith (config := { oracle := Linarith.CertificateOracle.fourierMotzkin }) will fail rather than returning an empty proof.

[Anne Baanen]

Okay, I don't know enough about the implementation of linarith to diagnose what's going wrong beyond that point.

[Eric Wieser]

Anne Baanen said:

Ah nevermind, that's because the simplex algorithm oracle returns an empty proof when it fails.

This sounds like a bug

[Bhavik Mehta]

Has there been any progress on this regression?

[Kim Morrison]

@Vasily Nesterov, perhaps? I'm not sure who "last touched" linarith.

[Bhavik Mehta]

I have a workaround following Sébastien's idea - applying norm_num everywhere makes the linariths succeed. But it's weird that this is necessary at all!

[Vasilii Nesterov]

Anne Baanen писал/а:

Ah nevermind, that's because the simplex algorithm oracle returns an empty proof when it fails.

Hi, is this what happens in this particular example?

import Mathlib.Data.Real.Pi.Bounds

set_option trace.linarith true

example (a : ℝ) (ha : 1.0 ≤ a) : 1 ≤ a := by
  linarith

For me it prints

[linarith] linarith is running on the following hypotheses:

[linarith] [ℝ, 1.0 ≤ a, 1 > a]

[linarith] Preprocessing: split conjunctions

[linarith] [ℝ, 1.0 ≤ a, 1 > a]

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

[linarith] [1.0 ≤ a, 1 > a]

[linarith] Preprocessing: replace negations of comparisons

[linarith] [1.0 ≤ a, 1 > a]

[linarith] Preprocessing: move nats to ints

[linarith] [1.0 ≤ a, 1 > a]

[linarith] Preprocessing: strengthen strict inequalities over int

[linarith] [1.0 ≤ a, 1 > a]

[linarith] Preprocessing: make comparisons with zero

[linarith] [1.0 - a ≤ 0, a - 1 < 0]

[linarith] Preprocessing: cancel denominators

[linarith] [1.0 - a ≤ 0, a - 1 < 0]

[linarith] after preprocessing, linarith has 2 facts:

[linarith] [1.0 - a ≤ 0, a - 1 < 0]

[linarith] hypotheses appear in 1 different types

[linarith] Simplex Algorithm failed

as expected. It used to return empty proof, but I thought I fixed it quite a while ago.

[Vasilii Nesterov]

Ah, I see that the topic is also quite old :)

Anyway, it's fixed now.

[Mauricio Collares]

Pedantically clarifying the status of this thread: The empty proof is indeed fixed (thanks a lot!), but the Lean 3 regression (i.e., the fact that the simplex algorithm fails if norm_num is not applied to the hypothesis, possibly due to linarith lacking appropriate support for OfScientific) still persists.

[Heather Macbeth]

I looked into this bug with decimals in linarith. There are two issues:

1. The cancel_denoms preprocessor ought to be triggered by a decimal (because a decimal is implicitly a rational number), but it's not -- currently the preprocessor is only run on expressions literally containing a /.
2. The cancel_denoms preprocessor doesn't currently know how to realise a decimal as a fraction (i.e. to turn 1.423 into 1423/1000), which is a necessary prep step before actually cancelling denominators.

A proposed fix is at #19174. I could have just taught cancel_denoms to handle decimals (which is what was done in mathlib3), but it seems more natural to me to actually let cancel_denoms preprocess all numbers using norm_num1. So now the following would also be handled (which were not handled in mathlib3):

• 10 / (8 + 2)
• 10 / 10 ^ 1
• 10⁻¹ * 10

Not sure what the performance impact will be -- benchmarking it now.

[Heather Macbeth]

Since norm_num1 will anyway have to handle any other arithmetic-expressions-on-numbers later (during the ring run in the discharger step), it seems plausible that no serious performance impact would result from instead handling them earlier (in the cancel-denoms preprocessor step) ... but we'll see!