push_cast and numerals

Stream: maths

[Chris Hughes]

push_cast with ((2 : nat) : int) then I get 1 + 1. Getting rid of the norm_cast attribute on int.coe_nat_succ fixes this problem, and push_cast gives me (2 : int). I can see there's been some attempt to fix it by setting a lower priority to the norm_cast attribute on int.coe_nat_succ, but this fix is obviously not working any more. One fix I found, was to get rid of the norm_cast attribute on int.coe_nat_succ and put the attribute on nat.succ_eq_add_one, but this seems like it might be evil.

[Gabriel Ebner]

norm_cast works just fine with ((2 : ℕ) : ℤ) because it has special handling for numerals. I didn't know about push_cast. I guess push_cast should use the same numeral handling then? @Rob Lewis Thoughts?

[Rob Lewis]

push_cast doesn't use special handling for anything. It's just simp with push_cast, where push_cast is a simp set derived from norm_cast lemmas.

I'm surprised that this works, why does coe_nat_succ match the numeral? bit0 isn't reducible, is it?

import tactic

set_option pp.numerals false

#simp only [int.coe_nat_succ] : ((2 : ℕ) : ℤ)