sqrt{25} = 5 ?

Stream: new members

[RedPig]

Trying some simple example on LEAN but somehow struggle to generalize the proof, in the below examples, the first example works but the second fails. The main reason is that norm_num is able to do $\sqrt{1} = 1$ but can not do $\sqrt{25} = 5$. How shall we do it then, I guess we need to prove $\sqrt{25} = 5$. Or do I miss something simple here?

import Mathlib

theorem evaluate_f1 (f : ℝ → ℝ) (h₀ : ∀ x, f x =  3 * Real.sqrt (2 * x - 7) - 8) : f 4 = -5 := by
 simp [h₀]
 norm_num

import Mathlib

theorem evaluate_f2 (f : ℝ → ℝ) (h₀ : ∀ x, f x =  3 * Real.sqrt (2 * x - 7) - 8) : f 16 = 7:= by
 simp [h₀]
 norm_num

[Jireh Loreaux]

I'm not saying it's ideal, but you can do this:

import Mathlib

theorem evaluate_f2 (f : ℝ → ℝ) (h₀ : ∀ x, f x =  3 * Real.sqrt (2 * x - 7) - 8) : f 16 = 7:= by
  simp [h₀]
  rw [show (2 : ℝ) * 16 - 7 = 5 ^ 2 by norm_num, Real.sqrt_sq (by norm_num)]
  norm_num

[Bjørn Kjos-Hanssen]

Or this

import Mathlib

theorem evaluate_f2 (f : ℝ → ℝ) (h₀ : ∀ x, f x =  3 * Real.sqrt (2 * x - 7) - 8) : f 16 = 7:= by
 simp [h₀]
 norm_num
 have : √(25)=5 := by
  refine Real.sqrt_eq_cases.mpr ?_
  norm_num
 rw [this]
 ring_nf

[Ruben Van de Velde]

Sounds like someone should write a norm_num extension

[Jireh Loreaux]

What should it do on √12? Nothing? Or should it return 2 * √3? (I don't see a way to make the latter efficient)

[Jireh Loreaux]

And what about OfScientific?

[RedPig]

Jireh Loreaux said:

What should it do on √12? Nothing? Or should it return 2 * √3?

will it be useful to leverage sympy to do it? sp.simplify can do it in python as $2\sqrt{3}$

[Ruben Van de Velde]

Approximate to 3.46

[Jireh Loreaux]

?? But then it can't return a proof?

[Ruben Van de Velde]

More seriously, an extension that only covers perfect squares would be a useful first step

[Jireh Loreaux]

It should be relatively easy to adapt the existing extension for Nat.sqrt.

[RedPig]

Jireh Loreaux said:

?? But then it can't return a proof?

or use sympy to suggest the form and use LEAN to prove it? I don't think this is the way to go but just saying out my thought.

[Jireh Loreaux]

My comment was directed at Ruben's suggestion, not yours, sorry for the confusion.

[Ruben Van de Velde]

I think the overhead of calling out to sympy is probably not worth it, either in time or complexity

[Ruben Van de Velde]

Though it's an interesting idea

[RedPig]

another question: currently the proofs stuck at
$3 * √25 - 8 = 7$
from a human perspective, we should be able to reformat it as
$3 * √25 = 7 + 8$
and then
$3 * √25 = 15$
and then
$√25 = 5$

Is there function in LEAN can auto-transform in this way or it is all need to be manual?

[Jireh Loreaux]

How would Lean know that this is the form you want? (i.e., how would it know you wouldn't want 3 = 15 / √25, or any other variation?)

[Kyle Miller]

Somewhere in Zulip there is a simproc that can reduce squares to k * sqrt s with s square-free. It's not appropriate for normnum (other than for perfect squares) since normnum is for calculating a normal form that's integral or rational.

[Kyle Miller]

(I believe the simproc is just for Nat.sqrt)

[Kyle Miller]

Found it, and it was for Real.sqrt: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Should.20these.20surds.20be.20simplified.20with.20norm_num.3F/near/444362938

[Kevin Buzzard]

RedPig said:

another question: currently the proofs stuck at
$3 * √25 - 8 = 7$
from a human perspective, we should be able to reformat it as
$3 * √25 = 7 + 8$
and then
$3 * √25 = 15$
and then
$√25 = 5$

Is there function in LEAN can auto-transform in this way or it is all need to be manual?

import Mathlib.Tactic

example : 3 * √25 - 8 = 7 := by
  suffices √25 = 5 by polyrith
  rw [Real.sqrt_eq_cases]; norm_num

i.e. if you tell it the form you want, it's plain sailing.

[Eric Wieser]

(deleted)

[Bjørn Kjos-Hanssen]

polyrith doesn't seem to work in the Lean 4 playground, but linarith does the job too.

[Kevin Buzzard]

Huh, I thought it worked for me locally. Maybe polyrith doesn't work at all in the playground?

[Kevin Buzzard]

import Mathlib.Tactic

example : 3 * √25 - 8 = 7 := by
  suffices √25 = 5 by linear_combination 3 * this
  rw [Real.sqrt_eq_cases]; norm_num

works in the playground (i.e. replace polyrith with its output).

[Eric Wieser]

I don't think the playground is allowed network access