## Stream: general

### Topic: cannot compute cube root

#### Formally Verified Waffle Maker (Oct 19 2020 at 23:09):

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 (Oct 19 2020 at 23:18):

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 (Oct 19 2020 at 23:22):

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 (Oct 19 2020 at 23:23):

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 (Oct 19 2020 at 23:26):

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 (Oct 20 2020 at 00:48):

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 (Oct 20 2020 at 07:05):

@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$.

Last updated: May 15 2021 at 00:39 UTC