Zulip Chat Archive

Stream: general

Topic: cannot compute cube root


view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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 (NZQRC\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 81/38^{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 71/37^{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 R\Bbb R.


Last updated: May 15 2021 at 00:39 UTC