[Merged by Bors] - fix: correct bad handling of rat literals in `ring_nf` #8836

eric-wieser · 2023-12-06T01:41:41Z

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

This removes the unwanted Int.ofNat and coercions.

The docstring was apparently incorrect on Rat.rawCast (according to @digama0).
With that in mind, it's just a case of fixing the local lemmas used to clean up, to reflect the actual invariant instead of the previously-documented one.

This also fixes a hang when using mode = .raw, by using only a single pass to prevent 1 recursively expanding to Nat.rawCast 1 + 0.

Mathlib/Tactic/NormNum/Result.lean

Co-authored-by: Mario Carneiro <mcarneir@andrew.cmu.edu>

Mathlib/Tactic/NormNum/Result.lean

eric-wieser · 2023-12-06T02:40:40Z

Mathlib/Tactic/Ring/RingNF.lean

+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


The docstring in the other file says that Int.rawCast (.ofNat n) is not allowed to ever appear; so arguably rat_rawCast is a bad lemma because it introduces this illegal form, even if only temporarily.

I think the version I had that preserved the invariant was a little clearer.

We're taking things out of raw cast form here, so it's fine to break those invariants. (More precisely we are temporarily weakening one of the invariants to allow the Int.rawCast (.ofNat n) form.) The main reason I like this version better is that it's more orthogonal, we only need one case each for negation and division and the int cast. Otherwise we need a cartesian product of cases for all the ways that you can build literals.

Just for comparison, my proposal is

Suggested change

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

theorem int_rawCast_neg {R} [Ring R] : (Int.rawCast (.negOfNat n) : R) = -Nat.rawCast n := by simp

theorem rat_rawCast_pos {R} [DivisionRing R] :

(Rat.rawCast (.ofNat n) d : R) = Nat.rawCast n / Nat.rawCast d := by simp

theorem rat_rawCast_neg {R} [DivisionRing R] :

(Rat.rawCast (.negOfNat n) d : R) = Int.rawCast (.negOfNat n) / Nat.rawCast d := by simp

which has two benefits:

It never transitions through an invalid use of Int.rawCast

It doesn't accept invalid uses of Rat.rawCast

This is hardly a cartesian explosion, since we only have three types here anyway.

Bhavik posted the following example on Zulip:

import Mathlib.Data.Real.Basic example {n : ℝ} : (n + 1 / 2) ^ 2 * (n + 1 + 1 / 3) ≤ (n + 1 / 3) * (n + 1) ^ 2 := by ring_nf; sorry

On 86251e6, the remaining goal displays as ⊢ 1 / 3 + n * (OfNat.ofNat 19 / 12) + n ^ 2 * (OfNat.ofNat 7 / 3) + n ^ 3 ≤ 1 / 3 + n * (OfNat.ofNat 5 / 3) + n ^ 2 * (OfNat.ofNat 7 / 3) + n ^ 3 in the infoview. Applying Eric's suggestion, it is ⊢ 1 / 3 + n * (19 / 12) + n ^ 2 * (7 / 3) + n ^ 3 ≤ 1 / 3 + n * (5 / 3) + n ^ 2 * (7 / 3) + n ^ 3

(Note, regarding the two simp lemma strategies, I don't really care that much about it. Use whichever one you prefer.)

@collares, do you have any ideas for how to write a test for that? It seems the one I added doesn't spot the issue.

I ended up using guard_mgs with trace_state

…g_nf

digama0 · 2023-12-07T11:19:54Z

test/ring.lean

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


Suggested change

sorry

exact test_sorry

test_sorry has the interesting effect of complaining about unused hypotheses

you will have to use _hn etc as well. The reason is because the linter doesn't fire on proofs that contain sorry.

Indeed, I've already pushed such a change.

alexjbest · 2023-12-07T17:23:05Z

test/ring.lean

+  -- `conv_lhs` prevents `ring_nf` picking a bad normalization for both sides.
+  conv_lhs => ring_nf
+
+-- We can't use `guard_target =ₛ` here, as while it does detect stray `OfNat`s, it also complains


it sounds like we need a guard_target mode for pretty printed output rather than expr equality

Or some intermediate "syntactically equal except for ~~instances~~ implicit arguments"

digama0 · 2023-12-11T11:07:49Z

bors r+

@digama0

Reported [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ring_nf.20returns.20ugly.20literals/near/400988184): > ```lean > 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: > ```lean > ↑(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 > ``` This removes the unwanted `Int.ofNat` and coercions. The docstring was apparently incorrect on `Rat.rawCast` (according to @digama0). With that in mind, it's just a case of fixing the local lemmas used to clean up, to reflect the actual invariant instead of the previously-documented one. This also fixes a hang when using `mode = .raw`, by using only a single pass to prevent `1` recursively expanding to `Nat.rawCast 1 + 0`. Co-authored-by: Mario Carneiro <di.gama@gmail.com>

mathlib-bors · 2023-12-11T12:14:52Z

Pull request successfully merged into master.

Build succeeded:

@digama0

Reported [on Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/ring_nf.20returns.20ugly.20literals/near/400988184): > ```lean > 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: > ```lean > ↑(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 > ``` This removes the unwanted `Int.ofNat` and coercions. The docstring was apparently incorrect on `Rat.rawCast` (according to @digama0). With that in mind, it's just a case of fixing the local lemmas used to clean up, to reflect the actual invariant instead of the previously-documented one. This also fixes a hang when using `mode = .raw`, by using only a single pass to prevent `1` recursively expanding to `Nat.rawCast 1 + 0`. Co-authored-by: Mario Carneiro <di.gama@gmail.com>

fix: correct bad handling of rat literals in ring_nf

bdaa6ff

eric-wieser added bug Something isn't working awaiting-review t-meta Tactics, attributes or user commands labels Dec 6, 2023

whitespace

28267bf

digama0 reviewed Dec 6, 2023

View reviewed changes

Mathlib/Tactic/NormNum/Result.lean Outdated Show resolved Hide resolved

eric-wieser and others added 2 commits December 6, 2023 01:48

add a test

6500524

Update Mathlib/Tactic/NormNum/Result.lean

f3cb812

Co-authored-by: Mario Carneiro <mcarneir@andrew.cmu.edu>

leanprover-community deleted a comment from github-actions bot Dec 6, 2023

eric-wieser commented Dec 6, 2023

View reviewed changes

Mathlib/Tactic/NormNum/Result.lean Outdated Show resolved Hide resolved

tweak simp theorems, add singlePass

aaf5d46

eric-wieser commented Dec 6, 2023

View reviewed changes

eric-wieser added 4 commits December 6, 2023 12:18

Wrap lines

7b76536

Merge remote-tracking branch 'origin/master' into eric-wieser/fix-rin…

86251e6

…g_nf

fix

b785e87

add a test to verify that doesn't appear

6502f97

digama0 reviewed Dec 7, 2023

View reviewed changes

tidy

53d0526

alexjbest reviewed Dec 7, 2023

View reviewed changes

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Dec 11, 2023

mathlib-bors bot changed the title ~~fix: correct bad handling of rat literals in ring_nf~~ [Merged by Bors] - fix: correct bad handling of rat literals in ring_nf Dec 11, 2023

mathlib-bors bot closed this Dec 11, 2023

mathlib-bors bot deleted the eric-wieser/fix-ring_nf branch December 11, 2023 12:14

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - fix: correct bad handling of rat literals in `ring_nf` #8836

[Merged by Bors] - fix: correct bad handling of rat literals in `ring_nf` #8836

eric-wieser commented Dec 6, 2023 •

edited

Loading

eric-wieser Dec 6, 2023

digama0 Dec 6, 2023

eric-wieser Dec 6, 2023

collares Dec 7, 2023

digama0 Dec 7, 2023

eric-wieser Dec 7, 2023

eric-wieser Dec 7, 2023

digama0 Dec 7, 2023

eric-wieser Dec 7, 2023

digama0 Dec 7, 2023

eric-wieser Dec 7, 2023

alexjbest Dec 7, 2023

eric-wieser Dec 7, 2023 •

edited

Loading

digama0 commented Dec 11, 2023

mathlib-bors bot commented Dec 11, 2023

[Merged by Bors] - fix: correct bad handling of rat literals in ring_nf #8836

[Merged by Bors] - fix: correct bad handling of rat literals in ring_nf #8836

Conversation

eric-wieser commented Dec 6, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eric-wieser Dec 7, 2023 • edited Loading

Choose a reason for hiding this comment

digama0 commented Dec 11, 2023

mathlib-bors bot commented Dec 11, 2023

[Merged by Bors] - fix: correct bad handling of rat literals in `ring_nf` #8836

[Merged by Bors] - fix: correct bad handling of rat literals in `ring_nf` #8836

eric-wieser commented Dec 6, 2023 •

edited

Loading

eric-wieser Dec 7, 2023 •

edited

Loading