norm_cast

Stream: general

[Sebastien Gouezel]

I have never used norm_cast. I just met a stupid goal for which I thought it could be useful, so I tried it but nothing happened. Am I doing something wrong, or is it just that the relevant lemmas are not tagged yet?

example : ((0 : ℕ) : with_top ℕ) < (1 : with_top ℕ) :=
begin
  change ((0 : ℕ) : with_top ℕ) < (1 : ℕ),
  rw with_top.coe_lt_coe,
  exact zero_lt_one
end

[Paul-Nicolas Madelaine]

in this case it's just that the relevant lemmas for the 'with_top' type are not tagged yet

[Paul-Nicolas Madelaine]

local attribute [elim_cast] with_top.coe_lt_coe

example : ((0 : ℕ) : with_top ℕ) < (1 : with_top ℕ) :=
begin
  change ((0 : ℕ) : with_top ℕ) < (1 : ℕ),
  exact_mod_cast zero_lt_one
end

[Paul-Nicolas Madelaine]

the first line of the proof should also be useless once the numerals handling is fixed

[Johan Commelin]

I don't know if this has been asked before. But could we have norm_cast? and friends to report which normalization lemmas are used?

[Rob Lewis]

Future work :) but what's the scenario where you really want this? It's a much less useful report than squeeze_simp.

[Johan Commelin]

Sometimes norm_cast is a bit too aggresive. It doesn't happen often at all. In those cases, one option is to fall back to rw

[Johan Commelin]

For example, I had the following goal:

↑((multiplicity ↑p (r.num)).get _) < ↑((multiplicity ↑p ↑(r.denom)).get _)

[Johan Commelin]

On the left hand side, r.num is in ℤ, hence the this is multiplicity wrt integer division. On the right, norm_cast reduces to multiplicty of nats. But then you can't apply things like multiplicity_le_multiplicity_iff anymore, because you now have multiplicity wrt different semirings

[Johan Commelin]

One way to solve this is suffices : blah, {norm_cast}, or some hack like that.

[Johan Commelin]

Aha, so this is why I would like norm_cast?

[Johan Commelin]

Because it would open the door to norm_cast [-evil_lemma]

[Johan Commelin]

And that would allow users to finetune the end result, while keeping the readable and intuitive norm_cast tactic in their script

[Rob Lewis]

Thanks to @Gabriel Ebner for cleaning up the long-standing norm_cast PR! It's finally landed. For the most part, the change should be transparent, unless you're really abusing the tool. The one big difference is that now you tag all your lemmas @[norm_cast] instead of choosing a label yourself.

[Rob Lewis]

You can override the labeling function with @[norm_cast elim], for example, if you know what you're doing.

[Patrick Massot]

Seeing this landing is really great. Many thanks to Paul-Nicolas, Rob and Gabriel!

[Rob Lewis]

Oh, yeah, I obviously should have thanked @Paul-Nicolas Madelaine in my first post! This is almost entirely his work.

[Kevin Buzzard]

norm_cast is an absolutely essential tool for some of the codewars questions