ring for NNReal

Stream: mathlib4

[Heather Macbeth]

@Eric Wieser, now that #9915 (norm_num for NNRat-algebras) has been merged, is it on your radar to do the same generalization for ring? For example,

-- currently fails
example {x : ℝ≥0} : x / 2 + x / 2 = x := by ring

[Eric Wieser]

The reality is that I got norm_num mostly working with #9915, lost motivation, then @Aaron Liu fixed up the ring stuff to not crash with my changes

[Eric Wieser]

And in the end, the extent of my review of the changes to ring were "yes, this is still correct"

[Eric Wieser]

But I didn't spend any time thinking about how to generalize ring!

[Eric Wieser]

It looks pretty straightforward to adapt https://github.com/leanprover-community/mathlib4/blob/77ee539f65bc808ccd55f88bf61870dc200326f5/Mathlib/Tactic/Ring/Basic.lean#L1027-L1056

[Eric Wieser]

This weekend is a bad time for me, so it's all yours if you want @Aaron Liu!

[Aaron Liu]

#28494

[Heather Macbeth]

OK, that was clearly too easy! :). Do you want to do linarith next???

(I think the idea would be to write a nnrealToReal preprocessor, mimicking docs#Mathlib.Tactic.Linarith.natToInt.)

[Aaron Liu]

Heather Macbeth said:

OK, that was clearly too easy! :). Do you want to do linarith next???

Knowing how linarith works, that might be, complicated

[Heather Macbeth]

Which part? I was thinking the preprocessor would do this:

import Mathlib

example (x y : NNReal) (h : x + 3 ≤ y) : x + 5 ≤ 3 * y := by
  -- preprocess
  rw [← NNReal.coe_le_coe] at *
  push_cast at *
  have : (0:ℝ) ≤ x := NNReal.zero_le_coe
  have : (0:ℝ) ≤ y := NNReal.zero_le_coe
  -- now can work in `ℝ`
  linarith

IIUC that's how the Nat-to-Int preprocessor works.

[Aaron Liu]

oh are we special-casing NNReal?

[Aaron Liu]

will we also have to special-case all the other ordered semifields?

[Heather Macbeth]

We already special-case Nat, so there's a precedent. NNReal will be 95% of the use cases, so I don't think we should let the perfect be the enemy of the good.

[Aaron Liu]

I guess I can try it

[Heather Macbeth]

You could write something for general cancellative semirings, but that's actually not as good for special cases like Nat and NNReal, because it doesn't let you move into a concrete other ring (Int or Real) where the context might already contain relevant additional hypotheses.

[Aaron Liu]

I would argue that collecting facts from different types might be starting to get a little out of scope for linarith

[Heather Macbeth]

Wait, what? It already does it right?

[Aaron Liu]

I thought it does it once for each type

[Aaron Liu]

maybe I worded that badly

[Aaron Liu]

linarith won't take two facts in two different types, and use both of them to prove a goal I think

[Aaron Liu]

it only works on one type, and if there are facts from different types in the context then it will try each type independently and take the first success

[Heather Macbeth]

It preprocesses before splitting by type. See docs#Mathlib.Tactic.Linarith.runLinarith

[Aaron Liu]

did I get that right?

[Aaron Liu]

preprocessor is different

[Aaron Liu]

Anyways if I'm doing this for linarith then where should I put it? I doubt the linarith file imports NNReal.

[Heather Macbeth]

The principled answer would be to create an environment extension for linarith preprocessors. But I think that's overcomplicated here, where there's literally one piece of extensibility needed. Instead, perhaps you could use a trick I have seen in the ring code, although I'm not quite sure how it works:

[Heather Macbeth]

https://github.com/leanprover-community/mathlib4/blob/3fb2e061618391cf00f768e5d9c4e98e4540e6c6/Mathlib/Tactic/Ring/Basic.lean#L1211-L1216

[Heather Macbeth]

https://github.com/leanprover-community/mathlib4/blob/3fb2e061618391cf00f768e5d9c4e98e4540e6c6/Mathlib/Tactic/Ring/RingNF.lean#L122-L124

[Heather Macbeth]

Or the cheap version is to make people call it under a new name/syntax (linarith≥0 ...)

[Eric Wieser]

Heather Macbeth said:

OK, that was clearly too easy! :). Do you want to do linarith next???

(I think the idea would be to write a nnrealToReal preprocessor, mimicking docs#Mathlib.Tactic.Linarith.natToInt.)

I have an open PR that fixes a potential bug in this processor

[Heather Macbeth]

I see (#28290). OK, maybe we need to wait until that one's merged before writing variants.