sqrt 4 = 2

Stream: mathlib4

[Li Xuanji]

I was trying to prove that $\sqrt 4 = 2$ and $\sqrt{18} = 3 \sqrt 2$. Are these the shortest proofs? I feel like they should both be one-liners

example : Real.sqrt 4 = 2 := by {
  rw [Real.sqrt_eq_iff_sq_eq]
  repeat norm_num
}

example : Real.sqrt 18 = 3*Real.sqrt 2 := by {
  rw [Real.sqrt_eq_iff_sq_eq]
  ring_nf
  field_simp
  norm_num
  norm_num
  simp
  exact Real.sqrt_nonneg 2
}

[Kyle Miller]

This turns out to be a little simpler:

example : Real.sqrt 4 = 2 := by {
  rw [Real.sqrt_eq_cases]
  norm_num
}

example : Real.sqrt 18 = 3*Real.sqrt 2 := by {
  rw [Real.sqrt_eq_cases]
  ring_nf
  norm_num
}

[Kyle Miller]

(@Mario Carneiro Is normalizing square roots of rationals in the purview of norm_num? I think I remember you mentioning it at some point as a future feature, or future non-feature, I can't remember which.)

[Kyle Miller]

I tried making an argument where it suffices to square both sides, but then that pushes some difficulty to needing to say that square roots are non-negative.

theorem Real.eq_of_sq_eq {x y : ℝ} (hx : 0 ≤ x) (hy : 0 ≤ y) (h : x^2 = y^2) : x = y := by
  rw [← sqrt_sq hx, ← sqrt_sq hy, h]

example : Real.sqrt 4 = 2 := by {
  apply Real.eq_of_sq_eq <;> norm_num
  apply Real.sqrt_nonneg
}

example : Real.sqrt 18 = 3*Real.sqrt 2 := by {
  apply Real.eq_of_sq_eq <;> ring_nf <;> norm_num
  apply Real.sqrt_nonneg
}

[Kyle Miller]

Those can be compressed to the one-liner general proof apply Real.eq_of_sq_eq <;> ring_nf <;> norm_num [Real.sqrt_nonneg] (you can pass Real.sqrt_nonneg to norm_num since it is a fine simp lemma)

[Damiano Testa]

The first equality can also be proved by splitting the equality in two steps, before seeking help from automation:

example : Real.sqrt 4 = 2 := Eq.trans (by norm_num) (Real.sqrt_sq zero_le_two)

[Li Xuanji]

Thanks! With Kyle's proof being more uniform I wrote a small tactic to dispatch these

-- sqrt_eq_cases for y = √ x
theorem eq_sqrt_cases (x y : ℝ) : y = Real.sqrt x ↔ y * y = x ∧ 0 ≤ y ∨ x < 0 ∧ y = 0 := by
  have r : y = Real.sqrt x ↔ Real.sqrt x = y := by exact eq_comm
  rw [r]
  exact Real.sqrt_eq_cases

macro "norm_sqrt_eq" : tactic => `(tactic| rw [Real.sqrt_eq_cases] <;> ring_nf <;> repeat norm_num )
macro "norm_eq_sqrt" : tactic => `(tactic| rw [eq_sqrt_cases] <;> ring_nf <;> repeat norm_num )

-- Normalize square roots of rational literals
macro "norm_sqrt" : tactic => `(tactic| first | norm_sqrt_eq | norm_eq_sqrt)

example : Real.sqrt 25 = 5 := by norm_sqrt
example : Real.sqrt 4 = 2 := by norm_sqrt
example : Real.sqrt 18 = 3*Real.sqrt 2 := by norm_sqrt
example : 2 = Real.sqrt 4:= by norm_sqrt
example : Real.sqrt (1/4) = 1/2 := by norm_sqrt
example : Real.sqrt (1/2) = Real.sqrt 2 / 2 := by norm_sqrt

[Emilie (Shad Amethyst)]

Isn't norm_eq_sqrt just rw [eq_comm]; norm_sqrt_eq?

[Damiano Testa]

Also, if you use macro_rules and finishing with done you can probably get away with a single tactic that tries either approach and only uses the first that works. (Untested, as I'm on mobile)

[Emilie (Shad Amethyst)]

I feel like ideally such a macro would replace Real.sqrt x in the current proof with y, and in the examples the proofs could then be closed with rfl

[Emilie (Shad Amethyst)]

But this is kind of what norm_num should be for to begin with...
I really need to learn how to write more advanced tactics

[Mario Carneiro]

Kyle Miller said:

(Mario Carneiro Is normalizing square roots of rationals in the purview of norm_num? I think I remember you mentioning it at some point as a future feature, or future non-feature, I can't remember which.)

I think this should be a separate tactic, it has much more in common with ring than norm_num because I don't think there are canonical forms in full generality (it will start to look like the algebraic numbers stuff from the CAD discussion)

[Li Xuanji]

I feel like ideally such a macro would replace Real.sqrt x in the current proof with y, and in the examples the proofs could then be closed with rfl

Yes, but idk how to write a tactic which will do that computation. (Happy to learn if someone wants to give it a try though)

[Emilie (Shad Amethyst)]

Unfortunately this is something that I only know how to do in Coq, not in Lean. I really would like to learn how to do that, though

[Eric Wieser]

Mario, would you be opposed to norm_num being taught how to find the square root of squares?

[Mario Carneiro]

no, that would be fine

[Mario Carneiro]

the trouble is only when you have to expand the set of normal forms

[Mario Carneiro]

since then every other norm_num extension has to interact with it

[Eric Wieser]

You mean like I tried to do in #9915?

[Mario Carneiro]

yes

[Kyle Miller]

Could this be a globally enabled simproc?

[Li Xuanji]

I didn't know about simproc! Gonna play with it. The reduceFoo example looks useful to learn from too.