Zulip Chat Archive

Stream: maths

Topic: int.coe_nat_mul isn't nat.cast_mul


view this post on Zulip Kevin Buzzard (Jul 31 2018 at 22:58):

#check @int.coe_nat_mul -- int.coe_nat_mul : ∀ (m n : ℕ), ↑(m * n) = ↑m * ↑n -- this is in ℤ
#check @nat.cast_mul -- nat.cast_mul : ∀ {α : Type u_1} [_inst_1 : semiring α] (m n : ℕ), ↑(m * n) = ↑m * ↑n
example : semiring  := by apply_instance -- fine

example (m n : ) : ((m * n):) = m * n := nat.cast_mul m n -- fails

/- full error with pp.all true:
synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
  @coe_to_lift.{1 1} nat int (@coe_base.{1 1} nat int int.has_coe)
inferred
  @coe_to_lift.{1 1} nat int
    (@coe_base.{1 1} nat int
       (@nat.cast_coe.{0} int (@mul_zero_class.to_has_zero.{0} int (@semiring.to_mul_zero_class.{0} int int.semiring))
          (@monoid.to_has_one.{0} int (@semiring.to_monoid.{0} int int.semiring))
          (@distrib.to_has_add.{0} int (@semiring.to_distrib.{0} int int.semiring))))
-/

It seems that the coercion from nat to int isn't the one from nat to a general semiring. This means that I am having to write a bunch of functions twice, e.g.

theorem nat.cast_pow {α : Type*} [semiring α] (n : ) :  m : , (n : α) ^ m = (n ^ m : )
| 0 := nat.cast_one.symm
| (d+1) := show n * n ^ d = (n ^ d * n), by rw [nat.cast_pow,mul_comm,nat.cast_mul]

theorem nat.cast_pow' (n : ) :  m : , (n : ) ^ m = (n ^ m : )
| 0 := nat.cast_one.symm
| (d+1) := show n * n ^ d = (n ^ d * n), by rw [nat.cast_pow',mul_comm,int.coe_nat_mul]

Maybe the last one should be int.coe_nat_pow or something? Am I missing a trick? I'm trying to move smoothly between the naturals, the integers, and the integers mod p.

view this post on Zulip Kevin Buzzard (Jul 31 2018 at 23:02):

[I'm threatening to add some of these functions to my brief nat PR by the way]

view this post on Zulip Mario Carneiro (Aug 01 2018 at 01:30):

Yes. There are two coercions from N to Z, with different names. They are proven the same, so given one theorem the other isn't far away, but you have to have both sets of theorems

view this post on Zulip Mario Carneiro (Aug 01 2018 at 01:32):

There are also two power functions N -> N -> N, with different names, the specialization of monoid.pow and nat.pow, again they are proven the same and a simp lemma will translate one to the other

view this post on Zulip Mario Carneiro (Aug 01 2018 at 01:33):

In both cases you can put the blame on the fact that the special case is defined in lean core and mathlib can't undefine it, although I'm not sure I would remove int.coe_nat if I could


Last updated: May 09 2021 at 11:09 UTC