Rewriting an expression that involves `OfNat`

Stream: mathlib4

[Mitchell Lee]

Hello. I have run into the following issue several times in the past week and I want to know if there is any way around it.

Suppose that I want to prove a simple theorem such as

example {R M : Type*} [Ring R] [AddCommMonoid M] [Module R M] (m : M) : (100 : R) • m = 100 • m := sorry

Both sides of the equation appear exactly the same in the goal view. However, I tried rfl, simp, norm_cast, and push_cast and none of them worked. Even exact? cannot close the goal, and apply? suggests a wide variety of lemmas that don't seem likely to help at all.

After quite a bit of manual library searching, I figured out that this example can be closed with (nsmul_eq_smul_cast R 100 m).symm. Here is the type line of nsmul_eq_smul_cast:

theorem nsmul_eq_smul_cast (n : ℕ) (b : M) : n • b = (n : R) • b := ...

The reason exact? can't find this lemma is that (nsmul_eq_smul_cast R 100 m).symm has type ((100 : ℕ) : R) • m = 100 • m. This is definitionally equal to the desired equation (100 : R) • m = 100 • m, but it is not syntactically equal.

[Mitchell Lee]

The fact that (100 : R) and ((100 : ℕ) : R) are not syntactically equal has some other annoying consequences. For example, suppose that (100 : R) • m appears in a goal expression, and I would like to rewrite it to 100 • m. Or, to put it another way, how can we prove the example (100 : R) • m = 100 • m from earlier by rewriting the left-hand side into the right-hand side?

Because(100 : R) • m = 100 • m is a special case of nsmul_eq_smul_cast, one might try:

example {R M : Type*} [Ring R] [AddCommMonoid M] [Module R M] (m : M) : (100 : R) • m = 100 • m := by
  /- tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ↑?n • ?b -/
  rw [← nsmul_eq_smul_cast R 100 m]

Of course, this doesn't work, because the right-hand side of nsmul_eq_smul_cast R 100 m is not (100 : R) • m, but rather ((100 : ℕ) : R) • m. The best I can do is this:

example {R M : Type*} [Ring R] [AddCommMonoid M] [Module R M] (m : M) : (100 : R) • m = 100 • m := by
  rw [show (100 : R) = (100 : ℕ) by rfl, ← nsmul_eq_smul_cast R 100 m]

However, having to rewrite using (100 : R) = (100 : ℕ) is rather annoying, and I can't help but think there should be a better way to do this.

[Mitchell Lee]

Here is a combined snippet of code that demonstrates this difficulty:

import Mathlib

variable {R M : Type*} [Ring R] [AddCommMonoid M] [Module R M] (m : M)

example : (100 : R) • m = 100 • m := by
  /- `exact?` could not close the goal. Try `apply?` to see partial suggestions. -/
  exact?

example : (100 : R) • m = 100 • m :=
  (nsmul_eq_smul_cast R 100 m).symm

example : (100 : R) • m = 100 • m := by
  /- tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  ↑?n • ?b -/
  rw [← nsmul_eq_smul_cast R]

example : (100 : R) • m = 100 • m := by
  rw [show (100 : R) = (100 : ℕ) by rfl, ← nsmul_eq_smul_cast R]

[Timo Carlin-Burns]

This problem has kinda been my project for a number of months. I've PRed simp lemmas for OfNat.ofNat corresponding to every Nat.cast simp lemma, but I didn't get around to the non-simp ones. There are a lot of them and it isn't always easy to generalize them appropriately due to the Nat.AtLeastTwo typeclass adding an additional hypothesis. I made an RFC for unifying the two which would make exact? work properly for your use case, but there were some concerns posed and the discussion seems to have trailed off after I tried to clarify.

[Kyle Miller]

Here's a similar example of this issue that impacts even those who aren't using module theory:

example (x : ℝ) : x ^ (22 : ℝ) = x ^ (22 : ℕ) := by
  sorry

(In fact, ^ is a right action, so it's essentially the same issue.)

[Mitchell Lee]

Thank you so much for working to make this sort of thing easier @Timo Carlin-Burns

[Mitchell Lee]

Here is another situation in which this particular issue was quite painful: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Proving.20Hadamard.5E2.20.3D.20Identity.20in.202.5En.20dimensions/near/431612839
In order to get the rewriting to work, I had to write twice the identity matrix as (2 : ℕ), because writing it as just 2 made it much harder to apply some general matrix theorems.

And here's a snippet where I tried very hard not to write rw [show (2 : R) = (2 : ℕ) by rfl], but ended up having to do so anyways: https://github.com/leanprover-community/mathlib4/pull/7569#discussion_r1556964555

[Mitchell Lee]

This might be a stupid question, but why does instOfNatAtLeastTwo even exist? If it didn't, would it not still be possible to write things like (100 : R)?

[Kyle Miller]

It's to deal with making sure that docs#Zero and docs#One cover OfNat R 0 and OfNat R 1. The OfNat class is new in Lean 4, so Mathlib needs these classes to be integrated somehow. But simultaneously there are some good reasons for Zero and One. I'm not sure what the long-term solution will be.

[Kyle Miller]

(A reason to still have these classes: an algebraic structure cannot extend both OfNat R 0 and OfNat R 1 since there is a name collision in fields. They both want ofNat.)

[Mitchell Lee]

What I mean is this: I think it's quite useful to be able to type 0 and 1 and not have them be interpreted as a coercion. But when I type (100 : R), I'm totally okay with that just being an abbreviation for ((100 : ℕ) : R). What problems would occur if this were the case?

[Mitchell Lee]

And do these problems outweigh having to make two different versions of every theorem that involves natCast?

[Timo Carlin-Burns]

Is this the implementation you're suggesting? The problem is that (100 : R) is currently programmed to elaborate only if OfNat R 100 and doesn't fall back to (100 : Nat) and CoeHTCT Nat R

import Std

def MyRing := Rat

instance : OfNat MyRing 0 := inferInstanceAs (OfNat Rat 0)
instance : OfNat MyRing 1 := inferInstanceAs (OfNat Rat 1)
instance : CoeHTCT Nat MyRing := inferInstanceAs (CoeHTCT Nat Rat)

#check (0 : MyRing) -- OK
#check (1 : MyRing) -- OK
#check ((100 : Nat) : MyRing) -- OK
#check (100 : MyRing) -- ERROR: failed to synthesize instance `OfNat MyRing 100`

[Mitchell Lee]

I see.