real.rpow_sub_one

Stream: new members

[Julia Ramos Alves]

Hello to all. I was trying to solve for the following goal:

⊢ 1 / 3 * real.pi ^ 3 / real.pi = 1 / 3 * real.pi ^ 2

with rw ← real.rpow_sub_one, , but I get the following error:

rewrite tactic failed, did not find instance of the pattern in the target expression
  ?m_1 ^ ?m_2 / ?m_1

Does anyone understand why that happens?

[Kevin Buzzard]

Because you're not posting #mwe s, it's difficult to diagnose such an error. Here's a conjecture: rpow is about a ^ b with b : real, but you have a ^ b with b : something else (e.g. perhaps int or nat). What you have posted doesn't give me enough information to know whether this is correct (because the real three and the integer 3 and the natural 3 all show up as 3).

[Ruben Van de Velde]

extract_goal could help create a #mwe

[Julia Ramos Alves]

Does this now give enough information? (I have tried extract_goal )

import analysis.fourier
import measure_theory.integral.interval_integral
import data.real.basic
import analysis.special_functions.integrals

example (x : ℝ) : 1 / 3 * real.pi ^ 3 / real.pi = 1 / 3 * real.pi ^ 2 :=
begin
  rw ← real.rpow_sub_one,
end

Probably not all imports concern this specific goal, but these are all I have. I believe the problem must be indeed that 3 is being treated as a nat, but I don't know how to fix that.

[Kevin Buzzard]

For sure that 3 in the power is a nat -- the default 3 is a nat. You can check yourself by clicking on it:
three.png

[Kevin Buzzard]

There are different ways you can make it a real 3. If you have the power to manually change the goal, you can tell Lean you mean the real 3 like this:

import analysis.fourier
import measure_theory.integral.interval_integral
import data.real.basic
import analysis.special_functions.integrals

example (x : ℝ) : 1 / 3 * (real.pi ^ (3 : ℝ) / real.pi) = 1 / 3 * real.pi ^ 2 :=
begin
  rw ← real.rpow_sub_one, -- works
  sorry, sorry,
end

Note that another reason your rewrite wasn't working was that associativity is not right for you -- default associativity is left-to-right so this is (1 / 3 * real.pi ^ 3) / real.pi, which is a different reason why the rewrite will fail. I've fixed it in the above.

[Kevin Buzzard]

Another approach is to rewrite the theorem saying that a ^ (b : real) = a ^ b for b : nat, e.g.

example (x : ℝ) : 1 / 3 * (real.pi ^ 3 / real.pi) = 1 / 3 * real.pi ^ 2 :=
begin
  rw ← real.rpow_nat_cast,
  rw ← real.rpow_sub_one, -- works
  sorry, sorry,
end

[Kevin Buzzard]

import analysis.fourier
import measure_theory.integral.interval_integral
import data.real.basic
import analysis.special_functions.integrals

-- me figuring out the first rewrite
-- example (a b c : ℝ) : a * b / c = a * (b / c) := by library_search

example (x : ℝ) : 1 / 3 * real.pi ^ 3 / real.pi = 1 / 3 * real.pi ^ 2 :=
begin
  rw mul_div_assoc, -- sort out the brackets
  rw ← real.rpow_nat_cast, -- get the right 3
  rw ← real.rpow_sub_one real.pi_ne_zero, -- works
  norm_num,
end