sqrt(3^2) = 3

Stream: new members

[Lars Ericson]

I am trying to prove that the square root of 3^2 is 3. I am trying to introduce some facts:

lemma three_sqrt_squared_equals_three : (((3:ℝ) ^ 2) ^ (1/2: ℝ )) = (3: ℝ)  :=
begin
  have h1 := zero_le 3,                --OK
  have h2 := real.sqrt_sqr h1, -- ERROR
end

The second fact gives an error:

type mismatch at application
  real.sqrt_sqr h1
term
  h1
has type
  0 ≤ 3
but is expected to have type
  0 ≤ ?m_1
state:
h1 : 0 ≤ 3
⊢ (3 ^ 2) ^ (1 / 2) = 3

I need a lifeline.

[Alex J. Best]

zero_le 3 refers to the natural number 3, you probably want have h1 := zero_le (3: ℝ),

[Lars Ericson]

Alas this

import data.real.basic
import analysis.special_functions.pow

lemma three_sqrt_squared_equals_three : (((3:ℝ) ^ 2) ^ (1/2: ℝ )) = (3: ℝ)  :=
begin
  have h1 := zero_le (3:ℝ),
end

gives me a different error:

failed to synthesize type class instance for
⊢ canonically_ordered_add_monoid ℝ
state:
⊢ (3 ^ 2) ^ (1 / 2) = 3

[Alex J. Best]

Right, the real number 3 isn't automatically greater or equal to zero (unlike the natural number 3, where every natural number is nonnegative), so you need to prove it.
maybe have h1 : 0\le 3 := by norm_num does what you want

[Lars Ericson]

That resolves that issue but then the problem expands. I need a definitional equality for square root. This leads to deterministic timeout. If I say sorry for that, then I get almost there, but I get a error message at the end regarding the mix of types. The final goal state of

h3 : (3 ^ 2) ^ (1 / 2) = 3
⊢ (3 ^ 2) ^ (1 / 2) = 3

does not give a clear indication that there is a type mismatch between h3 and goal in :

import data.real.basic
import analysis.special_functions.pow

lemma sqrt_x_equals_sqrt_x (x : ℝ ): real.sqrt x =  x ^ (1 / 2) :=
begin
  sorry -- deterministic timeout for library_search! and suggest
end

lemma three_sqrt_squared_equals_three : (((3:ℝ) ^ 2) ^ (1/2: ℝ )) = (3: ℝ)  :=
begin
  have h1 : 0 ≤ (3:ℝ), by norm_num,
  have h2 := real.sqrt_sqr h1,
  have h3 := sqrt_x_equals_sqrt_x ((3:ℝ)^2),
  rw h2 at h3,
  rw eq_comm at h3,
  exact h3,
end

The error message at exact h3 is:

invalid type ascription, term has type
  @eq real
    (@has_pow.pow real nat (@monoid.has_pow real real.monoid)
       (@has_pow.pow real nat (@monoid.has_pow real real.monoid) 3 2)
       (@has_div.div nat nat.has_div 1 2))
    3
but is expected to have type
  @eq real
    (@has_pow.pow real real real.has_pow (@has_pow.pow real nat (@monoid.has_pow real real.monoid) 3 2)
       (@has_div.div real (@div_inv_monoid.to_has_div real (@division_ring.to_div_inv_monoid real real.division_ring)) 1
          2))
    3
state:
h1 : 0 ≤ 3,
h2 : real.sqrt (3 ^ 2) = 3,
h3 : (3 ^ 2) ^ (1 / 2) = 3
⊢ (3 ^ 2) ^ (1 / 2) = 3

[Alex J. Best]

Once again one of the problems here is the types of things not being what you think they are, you should get into the habit of using the widgets like in this gif Patrick made
Patrick Massot said:

nat_vs_int.gif

to check the types are what you expect.

In your first lemma, 1/2 is the natural number floor division 1/2 which is in fact 0. So the lemma isn't true

[Alex J. Best]

The version first lemma you really want is in mathlib as docs#real.sqrt_eq_rpow btw

[Lars Ericson]

Just out of curiosity, given that there is a spot-on theorem for this, why is library search timing out?

import data.real.basic
import analysis.special_functions.pow

lemma sqrt_x_equals_sqrt_x (x : ℝ ): real.sqrt x =  x ^ ((1:ℝ )/ (2: ℝ) ) :=
begin
  --rw real.sqrt_eq_rpow,
  library_search!
end

[Alex J. Best]

The theorem in the library is an equality of functions, whereas your statement is about the functions applied to some specific x