Zulip Chat Archive

Stream: maths

Topic: norm_cast failure


view this post on Zulip 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_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

view this post on Zulip 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 :-)

view this post on Zulip 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