OfScientific pretty printing after `simp`

Stream: lean4

[Geoffrey Irving]

If I do simp, explicit numbers like 0.123712 expand and look worse:

import Mathlib

lemma with_number : (0.123712 : ℝ) < 0.8482312 := by
  -- Goal print as `0.123712 < 0.8482312`
  simp only
  -- Goal prints as `OfScientific.ofScientific 123712 true 6 < OfScientific.ofScientific 8482312 true 7`
  norm_num

Is there a way to keep the pretty printing nice? (I'm tightening some bounds of very nonlinear things, and it results in explicit numbers popping up.)

[Kyle Miller]

The reason this is happening is that the OfScientific literals contain raw natural number literals, but after simp only they become normalized as literals using OfNat. This is potentially a bug in OfScientific literals.

Something you could do is add your own pretty printer for OfScientific that can handle OfNat literals.

[Eric Wieser]

This is potentially a bug in OfScientific literals.

Do you mean a bug in simp, in that it should not be doing this normalization?

[Eric Wieser]

Or that it should not contain raw numerals in the first place?

[Kyle Miller]

I was think it's the OfScientific literal containing a raw nat, but you could point your finger at simp too. It's aware of OfNat.ofNat, so maybe it should be aware of OfScientific.ofScientific too.

[Mario Carneiro]

I think OfScientific should be using raw nats

[Mario Carneiro]

so I would point the blame at simp here

[Kyle Miller]

@Geoffrey Irving Want to make a Lean 4 issue documenting the fact that simp only does this to these literals? Make sure it doesn't use mathlib -- you can use Float instead of Real. No need for the issue to suggest a solution -- we just want to track the problem.

[Geoffrey Irving]

Yep, will do.

[Eric Wieser]

Is #simp 0.5 a sufficient repro?

[Kyle Miller]

@Geoffrey Irving Here's a free delaborator for you in the meantime, hacked from the core one:

import Mathlib

open Lean PrettyPrinter Delaborator SubExpr in
@[delab app.OfScientific.ofScientific]
def delabOfScientific : Delab := whenPPOption getPPCoercions <| withOverApp 5 do
  let expr ← getExpr
  guard <| expr.getAppNumArgs == 5
  let some m := (expr.getArg! 2).nat? | failure
  let some e := (expr.getArg! 4).nat? | failure
  let s ← match expr.getArg! 3 with
    | Expr.const ``Bool.true _  => pure true
    | Expr.const ``Bool.false _ => pure false
    | _ => failure
  let str := toString m
  if s && e == str.length then
    return Syntax.mkScientificLit ("0." ++ str)
  else if s && e < str.length then
    let mStr := str.extract 0 ⟨str.length - e⟩
    let eStr := str.extract ⟨str.length - e⟩ ⟨str.length⟩
    return Syntax.mkScientificLit (mStr ++ "." ++ eStr)
  else
    return Syntax.mkScientificLit (str ++ "e" ++ (if s then "-" else "") ++ toString e)

[Geoffrey Irving]

Neat, thank you!

[Kyle Miller]

I only had to modify the let ... m := ... and let ... e := ... lines

[Geoffrey Irving]

Github issue: https://github.com/leanprover/lean4/issues/3194