Zulip Chat Archive

Stream: new members

Topic: Coercion issues


view this post on Zulip Jack J Garzella (Apr 30 2020 at 03:12):

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?

view this post on Zulip Alex J. Best (Apr 30 2020 at 03:19):

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).

view this post on Zulip Alex J. Best (Apr 30 2020 at 03:22):

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

view this post on Zulip Jack J Garzella (Apr 30 2020 at 16:06):

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?

view this post on Zulip Alex J. Best (Apr 30 2020 at 16:25):

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

view this post on Zulip Alex J. Best (Apr 30 2020 at 16:45):

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

view this post on Zulip Alex J. Best (Apr 30 2020 at 16:46):

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.

view this post on Zulip Kevin Buzzard (Apr 30 2020 at 17:32):

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]

Last updated: May 13 2021 at 04:21 UTC