norm_num not solving inequality with sqrt

Stream: new members

[Tyler Josephson ⚛️]

Why can't norm_num solve these? (originally had a much more complicated goal, (54000 / 7) ^ (1 / 2) ≤ 100 (all reals), but pared down to the following #mwe:

import Mathlib

example : (2 : ℝ ) ^ ( (1 : ℝ) / 2) ≤ 3 := by norm_num

example : Real.sqrt (2 : ℝ ) ≤ 3 := by norm_num

[Kevin Buzzard]

For the same reason norm_num can't solve sqrt 2 <= 1.41421357, namely that lean is not a calculator yet, and has no algorithms for doing arbitrary precision arithmetic on the reals (or indeed any precision, when it comes to square roots, log, exp, sin, cos etc). Square both sides to turn it into a question about rationals, which it will have no trouble with.

[Kevin Buzzard]

There's work in progress by Geoffrey Irving to rectify this.

[Tyler Josephson ⚛️]

I still get an error on the first one, after squaring both sides:

example : ((2 : ℝ ) ^ ( (1 : ℝ) / 2))^2 ≤ 3^2 := by norm_num -- doesn't work

example : (Real.sqrt (2 : ℝ ))^2 ≤ 3^2 := by norm_num -- works

[Daniel Weber]

norm_num [← Real.rpow_mul_natCast]

works there

[Tyler Josephson ⚛️]

Can I use the above to get at the underlying goal? Feels like this is close.

example : Real.sqrt 2 ≤ 3 := by
  have sq : (Real.sqrt 2)^2 ≤ 3^2 := by norm_num
  sorry

[Daniel Weber]

You can directly do norm_num [Real.sqrt_le_iff]

[Tyler Josephson ⚛️]

Thanks! My original goal was

example : Real.sqrt (54000 / 7) ≤ 100 :=  by
  sorry

which gets bogged down by simplifying to √54000 / √7 ≤ 100 and getting stuck.
Could I direct it better with a have statement?

example : Real.sqrt (54000 / 7) ≤ 100 :=  by
  have sq: (Real.sqrt (54000 / 7))^2 ≤ (100)^2 :=  by norm_num
  sorry

[Ruben Van de Velde]

Huh, docs#Real.sqrt_div is a simp lemma. I wonder why

[Ruben Van de Velde]

This works:

import Mathlib

example : Real.sqrt (54000 / 7) ≤ 100 :=  by
  rw [Real.sqrt_le_iff]
  norm_num

[Kyle Miller]

Here's some previous discussion about "why can't norm_num do X".

Sometimes norm_num seems like it's got a bigger scope than it actually has since it interleaves simp between normalizations (you can use norm_num only to disable this, just like simp syntax). The tactic is an evaluator that takes numeric expressions and normalizes them as an integer or a rational. The expression Real.sqrt (54000 / 7) isn't rational, so norm_num can't do anything with it.

Potentially norm_num could devise a strategy to try to prove real inequalities, but that seems like it would work better as part of an algebraic number normalizer (something that represents numbers as roots of polynomials).