Coercion issues

Stream: new members

[Jack J Garzella]

I'm trying to prove the following statement

lemma power_inverse :
∀ (a : real) (b : nat)
(ha : 0 ≤ a),
(a ^ (1 / b)) ^ b = a :=

and it looks to me from the docs that real.rpow_mul is a lemma that I might want to use. But when I tried to start the proof as follows:

begin
rw [(eq.symm (real.rpow_mul ha (1 / b) b))],
...
end

it seems that lean can't figure out the coersions of 1/b and b and I get a rewrite tactic failed, did not find instance of the pattern in the target expression \n (a ^ (1 / ↑b)) ^ ↑b. But if I replace the b with ↑b, then it gives me a don't know how to synthesize placeholder error.

Can anyone help me deal with these coercions? Or, is there a more automatic way to do things like this that I'm missing?

[Alex J. Best]

Whenever you get stuck with coercions like this its important to work out exactly what types everything is.
You can do this in a couple of ways, by setting set_option pp.all true will show you everything, but in this case you can also add dsimp [(^)], to see what ^ is being used here. In either case you'll see its taking real to a nat power, which is not what you intended. 1/b is being interpreted as the nat 1/b (likely just 0).

[Alex J. Best]

So a corrected (but not completely correct yet) statement would be

lemma power_inverse :
∀ (a : real) (b : nat)
(ha : 0 ≤ a),
(a ^ (1 / (b : ℝ))) ^ (b : ℝ) = a :=
begin
intros,
rw [← real.rpow_mul ha],
end

[Jack J Garzella]

Thanks so much! All of this was extremely helpful! I've now successfully proven my lemma, which looks like this:

lemma power_inverse :
∀ (a : real) (b : nat)
(ha : 0 ≤ a) (hb : (b : ℝ) ≠ 0),
(a ^ (1 / (b : ℝ))) ^ (b : ℝ) = a :=
begin
intros,
rw [←real.rpow_mul ha],
simp,
calc a ^ ((↑b)⁻¹ * ↑b) = a ^ ((1 : ℝ)) : by rw [field.inv_mul_cancel hb]
      ...               = a : by simp
end

The proof I used though is a bit verbose, and I'd like to make it shorter. In particular,
1) I can't figure out how to get simp to use the field.inv_mul_cancel lemma (which is marked @[simp])
2) It might be nice to have hb be of type b ≠ 0 rather than (b : ℝ) ≠ 0, but I don't know how to easily make b promote it's type.
How might I go about solving these?

[Alex J. Best]

Well if you want to make it short you can just use an explicit chain of rewrites in place of invoking simp, and not use a calc block (but calc blocks look nice)

lemma power_inverse :
∀ (a : real) (b : nat)
(ha : 0 ≤ a) (hb : (b : ℝ) ≠ 0),
(a ^ (1 / (b : ℝ))) ^ (b : ℝ) = a :=
begin
intros,
rw [←real.rpow_mul ha, one_div_eq_inv, inv_mul_cancel hb, real.rpow_one],
end

[Alex J. Best]

If you want simp to use inv_mul_cancel I believe you'll need to supply hb to simp,

lemma power_inverse :
∀ (a : real) (b : nat)
(ha : 0 ≤ a) (hb : (b : ℝ) ≠ 0),
(a ^ (1 / (b : ℝ))) ^ (b : ℝ) = a :=
begin
intros,
rw [←real.rpow_mul ha],
simp [hb],
end

[Alex J. Best]

Though in fact simp uses a different lemma inv_mul_cancel' in this case instead of the one you has in mind, which applies instead to groups with zero, rather than just division rings.

[Kevin Buzzard]

import analysis.calculus.specific_functions

lemma power_inverse :
∀ (a : real) (b : nat)
(ha : 0 ≤ a) (hb : (b : ℝ) ≠ 0),
(a ^ (1 / (b : ℝ))) ^ (b : ℝ) = a :=
λ _ _ ha hb, by simp [(real.rpow_mul ha _ _).symm, hb]