cube root of 8 is equal to 2

Stream: new members

[Alex Gu]

I'm not sure how to show this simple result, is there a short proof of it?

theorem c8 : (8 : ℝ) ^ (1 / 3 : ℝ) = 2 := by sorry

[Kenny Lau]

@Alex Gu Please remember to put the correct imports for an #mwe:

import Mathlib

theorem c8 : (8 : ℝ) ^ (1 / 3 : ℝ) = 2 := by
  rw [one_div, Real.rpow_inv_eq]
  all_goals norm_num

[Alex Gu]

thanks! and sorry about that :)

[Louis Cabarion]

Here’s how I solved it step by step:

1. Type apply?.
2. The first suggestion seems to yield easy subgoals:

Try this: refine (Real.eq_rpow_inv ?_ ?_ ?_).mp ?_
Remaining subgoals:
⊢ 0 ≤ 8
⊢ 0 ≤ 2
⊢ 1 / 3 ≠ 0
⊢ 8 = 2 ^ (1 / 3)⁻¹

3. Click the suggested refine line. Now you have refine (Real.eq_rpow_inv ?_ ?_ ?_).mp ?_ with four subgoals.
4. Since all the subgoals are equalities and inequalities which involve only normalised numerical expressions, norm_num will take care of them. Use norm_num four times and watch each goal get solved.
5. Finally, clean up everything:

import Mathlib

theorem c8 : (8 : ℝ) ^ (1 / 3 : ℝ) = 2 := by
  refine (Real.eq_rpow_inv ?_ ?_ ?_).mp ?_ <;> norm_num

[Louis Cabarion]

Alternative:

import Mathlib

theorem c8 : (8 : ℝ) ^ (1 / 3 : ℝ) = 2 :=
  (Real.eq_rpow_inv (by simp) (by simp) (by simp)).mp (by norm_num)

[Louis Cabarion]

@Kenny Lau Out of curiosity, could you share a step-by-step account of how you arrived at that proof (assuming you didn’t already know the lemma names by heart)?

[Kenny Lau]

Thanks for the invitation.

1. I first tried simp?, and saw that the goal became ⊢ 8 ^ 3⁻¹ = 2, so I took the lemma one_div and rewrited using it as the first step.
2. Then I see that I want a lemma about something to the power of an inverse, and I know the library spelling for these operations (rpow is special for real power), so I typed rpow_inv and hit Ctrl+Space, which gives me a list of suggestions, and the second one is exactly what I need:

image.png

3. Then I see that all the 4 goals generated are within the scope of norm_num, so that's what I did next.

[Kyle Miller]

Another way is to realize that if you cube both sides then you can cancel things, then everything's the kind of number that norm_num can handle.

import Mathlib

theorem c8 : (8 : ℝ) ^ (1 / 3 : ℝ) = 2 := by
  suffices ((8 : ℝ) ^ (1 / 3 : ℝ)) ^ (3 : ℝ) = 2 ^ (3 : ℝ) by
    rwa [Real.rpow_left_inj] at this <;> norm_num
    positivity
  rw [← Real.rpow_mul] <;> norm_num

[Weiyi Wang]

I am surprised this isn't a norm_num one-liner. Can we make it happen?

[Kenny Lau]

i think this will complicate things and might require something about computable reals which to my understanding is a bit of a far away goal

[Weiyi Wang]

Oh right, forgot about noncomputable reals :grimacing:

[Aaron Liu]

Weiyi Wang said:

I am surprised this isn't a norm_num one-liner. Can we make it happen?

yes

[Aaron Liu]

you don't need any computable reals either

[Aaron Liu]

but it'll only work when doing a rational power of a rational number where the answer is rational

[Kenny Lau]

(where everything is positive)

[Aaron Liu]

I guess we could support negative powers too

[Kenny Lau]

(edit: where the base is positive)

[Kyle Miller]

@Weiyi Wang The design of norm_num is to be able to normalize numeric expressions, and it chooses to only do it for families of expressions that it can always normalize. That limits it to mostly numeric expressions involving integers and rationals, and not powers with a non-integer exponent. (Here, "natural", "integer", etc. refer to the numbers inside a given number system, like Real. It doesn't have to be Nat, Int, Rat, etc.)

I'd suggested adding some root normalization once and Mario pushed back. I might have forgotten the context by now though.

[Aaron Liu]

negative bases too

[Kenny Lau]

mathlib doesn't have that refactor yet

[Kenny Lau]

I do support a refactor to make (-8)^(1/3) = -2, at the cost of the purists

[Louis Cabarion]

@Alex Gu A shorter proof:

import Mathlib

theorem c8 : (8 : ℝ) ^ (1 / 3 : ℝ) = 2 := by
  rw [← Real.eq_rpow_inv] <;> norm_num

[Aaron Liu]

Niven's theorem guarantees that when everything is rational there are only like 2 extra cases for negative base

[Kyle Miller]

You can make a simproc, it doesn't have to be norm_num.

[Aaron Liu]

this feels like it's in-scope for norm_num

[Aaron Liu]

it could also be a simproc

[Aaron Liu]

Kenny Lau said:

I do support a refactor to make (-8)^(1/3) = -2, at the cost of the purists

how will you make it continuous

[Kenny Lau]

Aaron Liu said:

Kenny Lau said:

I do support a refactor to make (-8)^(1/3) = -2, at the cost of the purists

how will you make it continuous

I claim that nobody cares about the function (-8)^x

[Aaron Liu]

Kenny Lau said:

mathlib doesn't have that refactor yet

you don't need a refactor to evaluate (-8)^(1/3) = 1

[Kenny Lau]

?

[Aaron Liu]

I think it's true

[Aaron Liu]

I found docs#Mathlib.Meta.NormNum.evalRPow but right now it only does Int exponents

[Louis Cabarion]

Here is the step by step procedure:

1. Type rw??.
2. Shift-click "8 ^ (1 / 3) = 2" in the InfoView.
3. Note the rewrite suggestion:

8 = 2 ^ (1 / 3)⁻¹
⊢ 0 ≤ 8
⊢ 0 ≤ 2
⊢ 1 / 3 ≠ 0

4. Click on that suggestion and get rw [← Real.eq_rpow_inv ?_ ?_ ?_].
5. Note that we now have four goals easily solved by norm_num.
6. Tidy up:

import Mathlib

theorem c8 : (8 : ℝ) ^ (1 / 3 : ℝ) = 2 := by
  rw [← Real.eq_rpow_inv] <;> norm_num

[Kenny Lau]

(-8)^(1/3) = exp (y log x) cos (π y) = exp (log (-8) / 3) cos (π/3) = exp ((log(8) + i π)/3) cos (π/3) and wolfram alpha says its real part is 1/2 @Aaron Liu

[Kenny Lau]

and this is too deep in the junk value territory for me to care

[Aaron Liu]

Kenny Lau said:

(-8)^(1/3) = exp (y log x) cos (π y) = exp (log (-8) / 3) cos (π/3) = exp ((log(8) + i π)/3) cos (π/3) and wolfram alpha says its real part is 1/2 Aaron Liu

Must have been off by one somewhere

[Eric Wieser]

#26935 might be of interest WRT the cbrt (-8) question

[Eric Wieser]

@Kenny Lau, (-8)^(1/3) = 1 I think

[Aaron Liu]

so I wasn't off by one after all

[Kenny Lau]

image.png

[Kenny Lau]

I see that I have misinterpreted this docstring

[Kenny Lau]

I think for clarity the docstring should

spoiler

change log x to log |x|

[Aaron Liu]

Kenny Lau said:

I think for clarity the docstring should

spoiler

change log x to log |x|

Did you read the docstring of docs#Real.log

[Kenny Lau]

yes