norm_cast and ofNat

Stream: mathlib4

[Yury G. Kudryashov]

Should norm_cast recognize OfNat.ofNat as a coercion so that it can normalize expressions like ENNReall.ofReal (OfNat.ofNat n)?

[Yury G. Kudryashov]

In some sense, ofNat is a cast from nat literals to a type with OfNat instance.

[Alex J. Best]

Isn't the issue more that ENNReal.ofReal isn't a cast? Rather than it being ofNat or any other coercion to reals?

[Alex J. Best]

Like

import Mathlib


example (n : ℕ) : (↑(↑n : ℚ) : ℝ) = x := by
  norm_cast -- gets rid of a cast

example (n : ℕ) : (ENNReal.ofReal (↑n : ℝ) : ENNReal) = x := by
  norm_cast -- does nothing


example (n : ℚ) : (ENNReal.ofReal (↑n : ℝ) : ENNReal) = x := by
  norm_cast  --- same

[Yury G. Kudryashov]

Second example works if you add @[norm_cast] to docs#ENNReal.ofReal_coe_nat (done locally)

[Yury G. Kudryashov]

And we don't have a lemma about ofReal and Rat.cast.

[Yury G. Kudryashov]

Because we don't have ENNReal.ofRat.

[Alex J. Best]

So if you add that attribute what goes wrong with ofNat? #mwe please

[Yury G. Kudryashov]

docs#ENNReal.ofReal_ofNat can't be a norm_cast lemma.

[Alex J. Best]

I still don't understand what isn't working that you think should be though?

[Alex J. Best]

Like this works fine

import Mathlib

attribute [norm_cast] ENNReal.ofReal_coe_nat
example (n : ℕ) : (ENNReal.ofReal (7  : ℝ) : ENNReal) = x := by
  norm_cast

[Alex J. Best]

If you have ofNats in the goal applied to anything other than nat literals then I don't know how they would get there

[Yury G. Kudryashov]

I was proving a generic lemma about OfNat.ofNat but probably you're right: all these lemmas should be done by defeq to a Nat.cast lemma.

[Yury G. Kudryashov]

I was working on #8163. I added norm_cast to ofReal_coe_nat, then tried the next lemma and failed.