cannot compute cube root

Stream: general

[Formally Verified Waffle Maker]

The line:

use 8^((1 : ℚ)/3),

in the code:

import data.real.basic
import tactic

open real


theorem eight_has_a_cube_root : ∃ n, n^3 = 8 :=
begin
    use 8^((1 : ℚ)/3),
    ring,
end

makes Lean complain:

failed to instantiate goal with (frozen_name has_pow.pow) 8 ((frozen_name has_div.div) (typed_expr (frozen_name rat) 1) 3)

Any help would be appreciated :smile:

[Bryan Gin-ge Chen]

The error message isn't very helpful here, but if you use the very similar tactic#existsi, you'll see the underlying problem:

import data.real.basic
import tactic
theorem eight_has_a_cube_root : ∃ n, n^3 = 8 :=
begin
    existsi 8^((1 : ℚ)/3),
/-
failed to synthesize type class instance for
⊢ has_pow ℕ ℚ
state:
⊢ ∃ (n : ℕ), n ^ 3 = 8
-/
    ring,
end

The problem is that Lean doesn't know how to raise a natural number to a rational power.

[Floris van Doorn]

Note that this works:

import analysis.special_functions.pow

open real

theorem eight_has_a_cube_root : ∃ n : ℝ, n^3 = 8 :=
begin
    use 8^((1 : ℝ)/3),
end

[Floris van Doorn]

I've imported the function where docs#real.has_pow was defined, changed the statement to talk about reals (which I think is what you wanted?) and use a real exponent.

[Floris van Doorn]

Here is the rest of the proof (with 7 instead of 8):

import analysis.special_functions.pow

open real

theorem seven_has_a_cube_root : ∃ n : ℝ, n^3 = 7 :=
begin
    use 7^((1 : ℝ)/3),
    rw [← rpow_nat_cast, ← real.rpow_mul]; norm_num
end

[Formally Verified Waffle Maker]

Floris van Doorn said:

Here is the rest of the proof (with 7 instead of 8):

import analysis.special_functions.pow

open real

theorem seven_has_a_cube_root : ∃ n : ℝ, n^3 = 7 :=
begin
    use 7^((1 : ℝ)/3),
    rw [← rpow_nat_cast, ← real.rpow_mul]; norm_num
end

Bryan Gin-ge Chen said:

The error message isn't very helpful here, but if you use the very similar tactic#existsi, you'll see the underlying problem:

import data.real.basic
import tactic
theorem eight_has_a_cube_root : ∃ n, n^3 = 8 :=
begin
    existsi 8^((1 : ℚ)/3),
/-
failed to synthesize type class instance for
⊢ has_pow ℕ ℚ
state:
⊢ ∃ (n : ℕ), n ^ 3 = 8
-/
    ring,
end

The problem is that Lean doesn't know how to raise a natural number to a rational power.

Thank you very much for your kind support! :pray:

[Kenny Lau]

@Formally Verified Waffle Maker there's some basic type theory to be known here. in maths we have partial functions, and numbers have flexible types ($\Bbb N \subset \Bbb Z \subset \Bbb Q \subset \Bbb R \subset \Bbb C$). but in Lean, a natural number cannot suddenly become a real number, so expressions like $8^{1/3}$ doesn't make sense (or at least shouldn't give you a natural number) because it would have to be defined for all natural numbers, and last time I checked $7^{1/3}$ is not a natural number. Here's the thing. Functions have fixed types as well. A function (such as cube root) have a fixed type for the input and a fixed type for the output (technically a lie, but let's go with this for now), so cube root has to have codomain $\Bbb R$.