Commit 2023-12-11 11:08 9f2bb70b

View on Github →

fix: correct bad handling of rat literals in ring_nf (#8836) Reported on Zulip:

import Mathlib.Data.Real.Basic

local macro_rules | `($x ^ $y) => `(HPow.hPow $x $y) -- Porting note: See issue lean4[#2220](https://github.com/leanprover-community/mathlib4/pull/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.

Estimated changes