Numeric literals

Stream: lean4

[Patrick Massot]

I suspect I already asked this, but I’m not sure. Is there any way to tell Lean: “in this file, all numeric literals should be interpreted as real numbers”? This is for teaching purposes of course.

[Kim Morrison]

@[default_instance]
instance instOfNatReal (n : Nat) : OfNat Real n where
  ofNat := n

[Kim Morrison]

This at least interprets natural number literals as reals.

[Kim Morrison]

Presumably something similar with OfScientific works for decimals.

[Kim Morrison]

I'd be happy to see a command in Mathlib interpret_numeric_literals_as_reals which runs this locally.

[Kyle Miller]

There's a caveat to @[default_instance], which is that they can't be local, scoped, or later removed, so once you do this it's a permanent change to downstream modules.

[Patrick Massot]

Thanks Kim.

[Patrick Massot]

Indeed it works, but I wasn’t careful enough with what I wished for. I forgot I also had powers in this file. And the exponents should be natural numbers.

[Patrick Massot]

One sample challenge is to remove the type annotation in

example : (4 : ℝ) = 1^3 + 1^2 - 1 + 3 := by norm_num

[Patrick Massot]

In this specific example I get away with a local

local macro_rules
| `($x = $y) => `(@Eq Real $x $y)

but it seems really really brittle.

[Patrick Massot]

The larger context is

example (x : ℝ) (hyp : x^3 + x^2 - x + 3 = 0) : x ≠ 1 := by
  intro hx
  have H : (4 : ℝ) = 0 :=
    calc
      4 = 1^3 + 1^2 - 1 + 3 := by norm_num
      _ = x^3 + x^2 - x + 3 := by rw [← hx]
      _ = 0 := by congr
  linarith only [H]

This is part of explaining negation and I really don’t want students to hit the error you get without the type annotation on the have line.

[Patrick Massot]

I tried

@[default_instance]
instance instOfNatReal (n : Nat) : OfNat Real n where
  ofNat := n

local macro_rules | `($x ^ $y:num)   => `(@HPow.hPow Real Nat Real (@instHPow.{0, 0} Real Nat (@Monoid.toNatPow.{0} Real Real.instMonoid)) $x (@OfNat.ofNat.{0} Nat $y (instOfNatNat $y))) in

example : 4 = 1^3 + 1^2 - 1 + 3 := by norm_num

but it does not work. I think the statement is the intended one, but norm_num no longer works.