Proving 64 = (4:ℝ) ^ (3:ℝ)

Stream: new members

[Kunhao Zheng]

Hi! I've been in difficulty when I tried to prove this equality, I've browsed through the other topics and found some subtlety in type theory, but I think this one is provable as they are both of type ℝ, but I don't know exactly how when norm_cast failed.

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

example : ↑ ( 1 * 2 ) = (1:ℝ) * 2 :=
begin
  norm_cast,
end

example : ↑ ( 1 ^ 2 ) = (1:ℝ) ^ 2 :=
begin
  norm_cast,
end

example : ↑ ( 1 ^ 2 ) = (1:ℝ) ^ (2:ℝ) :=
begin
  simp,
end

These simple examples above work magically( The 3rd one will panic when I use norm_cast), but when it comes to

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

example : ↑ ( 4 ^ 3 ) = (4:ℝ) ^ (3:ℝ) :=
begin
  nth_rewrite 0 [pow_succ'],
  simp,
  simp [pow_succ],
  sorry
end

example : (64:ℝ) = 4^(3:ℝ) :=
begin
  suffices : (64:ℝ) = 4^3, {
      rw this,
      norm_cast,
      sorry
    },
    linarith,
end

Cheating like norm_cast or simp won't work...
If possible, how can I see what's going on under the hood when I apply norm_cast or simp? I think maybe that helps to inspect how it succeeds in the simple ones.

[Mario Carneiro]

My suggestion: rewrite it to 4^((3:nat):real) with norm_cast, use a lemma to turn it into 4^(3:nat) and then norm_num

[Kunhao Zheng]

I've found some lemma which lift the first argument of pow, like nat.cast_pow, but I didn't find what I need that can lift the exponent.

[Shing Tak Lam]

docs#real.rpow_nat_cast

[Kunhao Zheng]

Shing Tak Lam said:

docs#real.rpow_nat_cast

Thank you! @Shing Tak Lam and @Mario Carneiro, that saved my day. I managed to finish this proof by following the hint.

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

example : (64:ℝ) = 4^(3:ℝ) :=
begin
  suffices : (64:ℝ) = 4^((3:ℕ):ℝ), {
      rw this,
      norm_cast,
  },
  suffices : (64:ℝ) = 4^(3:ℕ), {
      rw this,
      rw eq_comm,
      exact real.rpow_nat_cast (4:ℝ) 3,
  },
  norm_num,
end

[Eric Wieser]

This is a nice opportunity to use calc blocks:

example : (64 : ℝ) = 4^(3 : ℝ) :=
calc (64 : ℝ) = 4^(3 : ℕ) : by norm_num
          ... = 4^((3 : ℕ) : ℝ) : by rw real.rpow_nat_cast
          ... = 4^(3 : ℝ) : by norm_cast