something `nlinarith` can't do

Stream: general

[Heather Macbeth]

Here is something nlinarith can't do -- should it be able to do it? Would it be easy to add?

import data.real.basic

-- works
example (x y : ℝ) (h₁ : 0 ≤ y) (h₂ : y ≤ x) : y * x ≤ x * x := by nlinarith

-- fails
example (x y : ℝ) (h₁ : 0 ≤ y) (h₂ : y ≤ x) : y * x ≤ x ^ 2 := by nlinarith

[Heather Macbeth]

Also, today I learned:

example {α : Type*} [monoid α] (x : α) : x ^ 2 = x * x

is not true by rfl? (Instead there's a lemma.)

[Heather Macbeth]

Heather Macbeth said:

Here is something nlinarith can't do -- should it be able to do it? Would it be easy to add?

import data.real.basic

-- works
example (x y : ℝ) (h₁ : 0 ≤ y) (h₂ : y ≤ x) : y * x ≤ x * x := by nlinarith

-- fails
example (x y : ℝ) (h₁ : 0 ≤ y) (h₂ : y ≤ x) : y * x ≤ x ^ 2 := by nlinarith

Something a little strange about this example: I had thought that that adding intermediate hypotheses solved by ring would not work, because nlinarith subsumesring. But in fact this works:

example (x y : ℝ) (h₁ : 0 ≤ y) (h₂ : y ≤ x) : y * x ≤ x ^ 2 :=
begin
  have : x ^ 2 = x * x := by ring,
  rw this,
  nlinarith
end

[Adam Topaz]

example {α : Type*} [monoid α] (x : α) : x ^ 2 = x * (x * 1) := rfl

[Adam Topaz]

Makes sense, since $x^n$ is defined by recursion on $n$.

[Rob Lewis]

#4082

[Rob Lewis]

Feel free to tag me in linarith/nlinarith questions btw, I almost missed this.

[Heather Macbeth]

Thank you, this is great!

[Heather Macbeth]

Remarkably, this will be merged before the lecture I was preparing when I discovered this gap.

[Heather Macbeth]

(although it seems the web editor updates mathlib only once a day :-) )

[Bryan Gin-ge Chen]

I just triggered a web editor update which should be ready in 2 hours or so, in case you or your students want to use the new nlinarith there. (Sadly, the web editor build can't use leanproject yet.)

[Heather Macbeth]

Sorry @Bryan Gin-ge Chen, I was not complaining, just marvelling!

[Bryan Gin-ge Chen]

No worries, I didn't take it that way! I'm glad folks are making use of the web editor, despite all its warts.

[Heather Macbeth]

It's my first time using it in this way (to share a snippet with a newbie audience), but it seems perfect for the purpose.

[Heather Macbeth]

@Rob Lewis Here's something linarith can't do; could it be made to do it?

I'm continuing the thread from a couple of weeks ago because it seems similar -- it's something that ring can do, so it feels like it would be safe to tell linarith about it.

import data.real.basic

--fails
example {a b c : ℝ} (h : 0 ≤ b / a - c / a) : 0 ≤ (b - c) / a :=
by linarith

--works
example {a b c : ℝ} (h : 0 ≤ b / a - c / a) : 0 ≤ (b - c) / a :=
begin
  ring at ⊢ h,
  linarith
end

Adapted from an open PR of @Malo Jaffré (#4307).

[Patrick Massot]

This example if very officially out of scope for linarith (non-constant denominator).

[Heather Macbeth]

linarith does a normalization of hypotheses which is very similar to ring, but not quite the same. IANATW (I am not a tactic writer), but I don't see why the normalization of hypotheses can't be exactly the same as that done by ring.

[Heather Macbeth]

Here's what the ring converts the problem to (and it works):

example {a b c : ℝ} (h : 0 ≤ a⁻¹ * b - c * a⁻¹) : 0 ≤ a⁻¹ * b - a⁻¹ * c :=
by linarith

[Heather Macbeth]

also, it seems to work in Coq :)

Require Import Psatz Rbase.
Open Scope R_scope.

Lemma test (a b c : R) (h : 0 < b / a - c / a) :
  0 < (b - c) / a.
Proof.
  lra.
Qed.

[Rob Lewis]

Mmm. It's possible, I'm not sure if it's a tiny change to the linarith parser or a medium change.

[Rob Lewis]

This needs a medium change to the parsing step. As much as I hate that lra can do something linarith can't, it'll have to wait, unless this is blocking something big.

[Rob Lewis]

Heather Macbeth said:

linarith does a normalization of hypotheses which is very similar to ring, but not quite the same. IANATW (I am not a tactic writer), but I don't see why the normalization of hypotheses can't be exactly the same as that done by ring.

linarith doesn't use ring as a normalizer because it's expensive to do verified preprocessing. The normalization doesn't have to be proof producing since the rest of linarith produces and checks a certificate. So the parsing stage ("figure out the linear structure of this expression") is much lighter weight.

[Rob Lewis]

But the data structure it parses into is (unsurprisingly) badly suited for division.

[Heather Macbeth]

Rob Lewis said:

linarith doesn't use ring as a normalizer because it's expensive to do verified preprocessing. The normalization doesn't have to be proof producing since the rest of linarith produces and checks a certificate. So the parsing stage ("figure out the linear structure of this expression") is much lighter weight.

Thanks, very interesting!

[Heather Macbeth]

Rob Lewis said:

As much as I hate that lra can do something linarith can't, it'll have to wait, unless this is blocking something big.

One can use the workaround ring at ...., linarith forever, so it can certainly wait :)