norm_cast failure

Stream: maths

[Kevin Buzzard]

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_add
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,
  rwa add_self_eq_zero at h,
end

[Kevin Buzzard]

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]

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.