ring_nf returns ugly literals

Stream: mathlib4

[Bhavik Mehta]

import Mathlib.Data.Real.Basic

local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4#2220

example {n : ℝ} : (n + 1 / 2) ^ 2 * (n + 1 + 1 / 3) ≤ (n + 1 / 3) * (n + 1) ^ 2 := by
  ring_nf

After the ring_nf call, the goal looks like:

 ↑(Int.ofNat 1) / ↑3 + n * (↑(Int.ofNat 19) / ↑12) + n ^ 2 * (↑(Int.ofNat 7) / ↑3) + n ^ 3 ≤
  ↑(Int.ofNat 1) / ↑3 + n * (↑(Int.ofNat 5) / ↑3) + n ^ 2 * (↑(Int.ofNat 7) / ↑3) + n ^ 3

which seems unnecessarily ugly. For comparison, ring_nf SOP in Lean 3 gives

n ^ 3 + n ^ 2 * (7 / 3) + n * (19 / 12) + 1 / 3 ≤ n ^ 3 + n ^ 2 * (7 / 3) + n * (5 / 3) + 1 / 3

which is clearer. This can be remedied in Lean 4 by using a bunch of simp lemmas:

simp only [Int.ofNat_eq_coe, Int.int_cast_ofNat, Nat.cast_ofNat, Int.cast_one, Nat.cast_one]

turns the goal into

1 / 3 + n * (19 / 12) + n ^ 2 * (7 / 3) + n ^ 3 ≤ 1 / 3 + n * (5 / 3) + n ^ 2 * (7 / 3) + n ^ 3

which is something I would be satisfied with, but can we make ring_nf alone give something like this instead?

[Bhavik Mehta]

(This came up in porting the exponential ramsey project)

[Patrick Massot]

I also faced this in the rpow_simp tactic post-processor here.

[Patrick Massot]

I even created those lemmas for this purpose, but maybe they are equivalent to the lemmas you cite.

[Bhavik Mehta]

Ah yeah, I think those lemmas are implied by some subset of the ones I gave. But really, it seems like ring_nf shouldn't need this post-processing step at all (it didn't in Lean 3)

[Patrick Massot]

Sure, I was only agreeing with you here.

[Mario Carneiro]

yes this seems to be a bug, something is wrong with the simp lemmas

[Bhavik Mehta]

Is this something that's being worked on, or is it worth me making an issue on mathlib4 to track it?

[Mario Carneiro]

best make an issue

[Mauricio Collares]

Is it weird that ring_nf (config := {mode := .raw}) takes forever here?

[Eric Wieser]

A simpler mwe:

import Mathlib.Data.Real.Basic

example : 0 ≤ (1 / 2 : ℝ) := by
  ring_nf
  sorry

[Eric Wieser]

Mauricio Collares said:

Is it weird that ring_nf (config := {mode := .raw}) takes forever here?

It seems like there's an infinite loop somewhere...

[Eric Wieser]

I think

/--
A "raw rat cast" is an expression of the form:

* `(Nat.rawCast lit : α)` where `lit` is a raw natural number literal
* `(Int.rawCast (Int.negOfNat lit) : α)` where `lit` is a nonzero raw natural number literal
* `(Rat.rawCast n d : α)` where `n` is a raw int cast, `d` is a raw nat cast, and `d` is not 1 or 0.

is being violated, as the Rat.rawCast does not have raw casts as arguments

[Eric Wieser]

The Int.ofNat seem to be coming from here. Should that be using Nat.rawCast instead? Or is there no strict convention here?

[Eric Wieser]

(cc @Mario Carneiro)

[Mario Carneiro]

there is a strict convention indeed, but there are some smart constructors that will remove those indirections in some cases

[Mario Carneiro]

And I believe this one is using the smart constructor (Result.isRat' calls Result.isInt which strips off the .ofNat)

[Mario Carneiro]

Oh wait, the doc string is wrong

[Eric Wieser]

The one I quote above?

[Mario Carneiro]

in the last case n and d should be raw int/nat numerals, not raw casts

[Eric Wieser]

The ofNat is definitely not being stripped off

[Eric Wieser]

What is a "raw int numeral"?

[Mario Carneiro]

that is, ofNat (nat_lit N) or negOfNat (nat_lit N)

[Eric Wieser]

Ah, so if the docstring is wrong then it really is just a missing simp lemma

[Eric Wieser]

Though maybe that doesn't explain why mode := .raw hangs

[Mario Carneiro]

the simp lemma rat_rawCast_2 looks suspicious / needs to be coupled with something else

[Eric Wieser]

I'll make a patch

[Mario Carneiro]

I'm testing these lemmas now (in place of the existing simp lemmas)

theorem int_rawCast_pos {R} [Ring R] : (Int.rawCast (.ofNat n) : R) = Nat.rawCast n := by simp
theorem int_rawCast_neg {R} [Ring R] : (Int.rawCast (.negOfNat n) : R) = -Nat.rawCast n := by simp
theorem rat_rawCast {R} [DivisionRing R] :
    (Rat.rawCast n d : R) = Int.rawCast n / Nat.rawCast d := by simp

[Mario Carneiro]

hm, it seems to work on the original problem but mode := .raw still hangs

[Eric Wieser]

#8836

[Eric Wieser]

(your message above only just arrived for me)

[Eric Wieser]

I wouldn't expect this to make any diference to .raw, because .raw skips out on using any of these lemmas anyway

[Mario Carneiro]

It seems that in .raw mode you have to set singlePass := true or else it will revisit raw expressions and expand 1 to Nat.rawCast 1 + 0 infinitely

[Mario Carneiro]

I pushed to your branch

[Eric Wieser]

I think this should be good to go now