## Stream: maths

### Topic: norm_cast failure

#### Kevin Buzzard (Jun 21 2020 at 15:49):

I think that with_top.coe_add and with_top.coe_eq_coe might be missing norm_cast attributes. But even with that I can't get norm_cast to do the job completely. What am I missing?

import tactic

attribute [norm_cast] with_top.coe_eq_coe
attribute [norm_cast] with_top.coe_zero

example (n : ℤ) (h : (n : with_top ℤ) + n = 0) : (n : with_top ℤ) = 0 :=
begin
-- can I avoid these two lines with some attribute tagging?
change (↑n : with_top ℤ) + ↑n = (0 : ℤ) at h,
change (n : with_top ℤ) = (0 : ℤ),
-- now it all works
norm_cast at h,
norm_cast,
end


#### Kevin Buzzard (Jun 21 2020 at 15:50):

Oh! Got it -- I bet int isn't a canonically ordered semiring, and that's the assumption for coe_zero. As you were :-)

#### Kevin Buzzard (Jun 21 2020 at 16:06):

attribute [norm_cast] with_top.coe_add
attribute [norm_cast] with_top.coe_eq_coe

@[norm_cast] lemma with_top.coe_zero' {α : Type*}
[add_monoid α] : ((0 : α) : with_top α) = 0 := rfl

@[norm_cast] lemma with_top.coe_eq_zero' {α : Type*}
[add_monoid α] {a : α} : (a : with_top α) = 0 ↔ a = 0 :=
by rw [←with_top.coe_zero', with_top.coe_eq_coe]


I think that with_top got left out when the norm_cast revolution happened.

Last updated: May 10 2021 at 08:14 UTC