unify ofNat and Nat.cast

Stream: mathlib4

[Timo Carlin-Burns]

With the addition of the OfNat typeclass for nat literals in Lean 4, we now have two names for the embedding of the natural numbers into a semiring: OfNat.ofNat and Nat.cast. The former is used by numerals, e.g. (5 : R) is notation for OfNat.ofNat 5. The latter is used for coercions, e.g. (↑n : R) for some variable n is notation for Nat.cast n. These two functions are defeq, but they are not reducibly defeq, which means we need to duplicate lemmas for each of them. (See #8006 for an example of how many lemmas we need to add.) I have a proof of concept which would unify the two by making Nat.cast an abbrev for OfNat.ofNat. Would this change be a good idea? (Note that this should probably wait until after lean4#2867 is fixed.)

Proof of concept

/-! Proof of concept for unifying coercions from ℕ and nat literals. -/

universe u

-- Redefine `NatCast` from Std in terms of `OfNat`
abbrev NatCast (R : Type u) : Type u := ∀ n, OfNat R n

-- `Nat.cast n` and `OfNat.ofNat n` will now be reducibly defeq so we don't have to duplicate theorems about them
abbrev Nat.cast [NatCast R] (n : Nat) : R := OfNat.ofNat n

instance [NatCast R] : Coe Nat R where
  coe n := Nat.cast n

-- This works as intended!
example [NatCast R] (n : Nat) : (n : R) = OfNat.ofNat n := by with_reducible rfl
example [NatCast R] : ((0 : Nat) : R) = (0 : R) := by with_reducible rfl
example [NatCast R] : ((1 : Nat) : R) = (1 : R) := by with_reducible rfl
example [NatCast R] : ((2 : Nat) : R) = (2 : R) := by with_reducible rfl

-- `Zero` and `One` from mathlib can remain unchanged
class Zero (R : Type u) : Type u where
  zero : R

class One (R : Type u) : Type u where
  one : R

instance Zero.instOfNat (R : Type u) [Zero R] : OfNat R 0 where
  ofNat := Zero.zero

instance One.instOfNat (R : Type u) [One R] : OfNat R 1 where
  ofNat := One.one

instance [OfNat R 0] : Zero R where
  zero := 0

instance [OfNat R 1] : One R where
  one := 1

-- The only change needed to `AddMonoidWithOne` is removing `extends NatCast`
class AddMonoidWithOne (R : Type u) extends Add R, Zero R, One R where
  add_zero (x : R) : x + 0 = x
  zero_add (x : R) : 0 + x = x
  add_assoc (x y z : R) : x + y + z = x + (y + z)
  natCast : Nat → R
  natCast_zero : natCast 0 = 0
  natCast_succ (n : Nat) : natCast n.succ = natCast n + 1

-- We need to avoid non-defeq diamonds with `Zero.instOfNat` and `One.instOfNat`,
-- so we use them directly and effectively ignore the provided `natCast` at inputs `0` and `1`.
instance AddMonoidWithOne.instOfNat (R : Type u) [AddMonoidWithOne R] : (n : Nat) → OfNat R n
  | 0 => Zero.instOfNat R
  | 1 => One.instOfNat R
  | (n + 2) => ⟨natCast (n + 2)⟩

-- What defeqs does does nat coercion into `AddMonoidWithOne` have?
example [AddMonoidWithOne R] : (0 : R) = Zero.zero := by rfl
example [AddMonoidWithOne R] : (1 : R) = One.one := by rfl
example [AddMonoidWithOne R] : (0 : R) = AddMonoidWithOne.natCast 0 := by rfl -- fails..
example [AddMonoidWithOne R] : (1 : R) = AddMonoidWithOne.natCast 1 := by rfl -- fails..
example [AddMonoidWithOne R] (n : Nat) : (n : R) = AddMonoidWithOne.natCast n := by rfl -- fails..
example [AddMonoidWithOne R] (n : Nat) : ((n + 2 : Nat) : R) = AddMonoidWithOne.natCast (n + 2) := by rfl -- succeeds!

[Eric Wieser]

I think this is a bad idea because OfNat.ofNat is, as I understand it, only ever allowed to contain raw literals

[Timo Carlin-Burns]

"allowed" in what sense? We already write lemmas about OfNat.ofNat applied to variables

[Kim Morrison]

Yes, you should not think of OfNat.ofNat as "the embedding of natural numbers into a semiring". Instead, it is a supporting structure for elaborating numerals.

There are two different concerns here (elaborating numerals, and coercing into semirings), which have a confusing overlap, but are best kept separate.

[Timo Carlin-Burns]

It's not clear to me that these concerns ought to be separate. While semirings are where this shows up in mathlib, this will be a problem for any type which supports coercions from Nat. I imagine any type (semiring or not) that would want a Coe Nat MyType instance would also want OfNat MyType n for all n.

[Eric Wieser]

"allowed" in the sense that users of this typeclass are allowed to assume this invariant in order to process numerals

[Eric Wieser]

Of course this could change, but this is a decision to be made in core, not something that can be safely changed in mathlib

[Timo Carlin-Burns]

It's hard for me to imagine the use case for this invariant. Are you saying existing meta code detects numerals by matching on @OfNat.ofNat _ x _ and then errors if x is not nat_lit n? It seems simpler to pattern match on @OfNat.ofNat _ (nat_lit n) _ anyway, and since core is not enforcing this invariant, that would also make the meta code more robust.

[Timo Carlin-Burns]

Also, I don't think this invariant is currently maintained in practice.

• Lemma statements often involve OfNat.ofNat x where x is a variable. e.g. docs#Int.Nat.cast_ofNat_Int
• Some lemma statements involve OfNat.ofNat (Nat.succ n), e.g. docs#PNat.val_ofNat.
• Some lemma statements involve OfNat.ofNat (n + 1), e.g. docs#Real.Gamma_ofNat_eq_factorial

If meta code assumes that OfNat.ofNat is only ever applied to nat literals, then it will break if used in the proof of any such lemma.

[Timo Carlin-Burns]

Bump.. Another user has bumped into the rough edge in the language that would be fixed by this proposal. I would like to help move some resolution to this issue forward, so if this one is being rejected, it would be very helpful to have it clearly explained what's wrong with it so I know what would need to be improved in a future proposal.

[Timo Carlin-Burns]

(Is the problem just that this thread is in the wrong stream since this proposal is broader than mathlib?)

[Mario Carneiro]

yes, this is not something mathlib can do anything about. It would need to be a lean4 RFC

[Timo Carlin-Burns]

Ahh thanks. So is the correct next step to make a post in the lean4 stream with "[RFC]" in the topic name?

[Mario Carneiro]

No, lean4 RFCs are issues on the lean4 repository. RFC threads here are more like pre-RFCs to gather support

[Mario Carneiro]

which you may also want to do if you want to present a strong proposal

[Kyle Miller]

One issue I'm seeing here is that the instance in @OfNat.ofNat R x _ should be determined by R and x. If you do anything to change x without being sure that the instance is the canonical one for this R, x pair, you're breaking an assumption about instance arguments.

The Nat.cast function does not have this dependency on the specific value being cast. It just depends on the ring.

[Kyle Miller]

Another issue is that OfNat.ofNat n is assumed to be a sort of atomic expression, one that has special support in various tactics (like simp) that normalize them to some extent.

[Timo Carlin-Burns]

Thanks Kyle for taking a look! You make a good point that simp would need to be updated. Let me make sure I understand the issue about the instance argument.

Kyle Miller said:

One issue I'm seeing here is that the instance in @OfNat.ofNat R x _ should be determined by R and x. If you do anything to change x without being sure that the instance is the canonical one for this R, x pair, you're breaking an assumption about instance arguments.

I'm not sure I understand. Is the scenario you're imagining that you try to rewrite by a non-defeq equality at x and this fails because there's a dependency on x? Is this an accurate MWE?

-- (These library definitions are copied from the proof of concept above)

abbrev NatCast' (R : Type u) : Type u := ∀ n, OfNat R n

abbrev Nat.cast' [NatCast' R] (n : Nat) : R := OfNat.ofNat n

instance [NatCast' R] : Coe Nat R where
  coe n := Nat.cast' n

class Zero (R : Type u) : Type u where
  zero : R

class One (R : Type u) : Type u where
  one : R

instance Zero.instOfNat (R : Type u) [Zero R] : OfNat R 0 where
  ofNat := Zero.zero

instance One.instOfNat (R : Type u) [One R] : OfNat R 1 where
  ofNat := One.one

class AddMonoidWithOne (R : Type u) extends Add R, Zero R, One R where
  add_zero (x : R) : x + 0 = x
  zero_add (x : R) : 0 + x = x
  add_assoc (x y z : R) : x + y + z = x + (y + z)
  natCast : Nat → R
  natCast_zero : natCast 0 = 0
  natCast_succ (n : Nat) : natCast n.succ = natCast n + 1

instance AddMonoidWithOne.instOfNat (R : Type u) [AddMonoidWithOne R] : (n : Nat) → OfNat R n
  | 0 => Zero.instOfNat R
  | 1 => One.instOfNat R
  | (n + 2) => ⟨natCast (n + 2)⟩

-- (End library definitions; begin example)

/-- A term which is equal to `2`, but not definitionally so. -/
noncomputable def my2 : Nat := Classical.choose (show ∃ n, n = 2 from ⟨2, rfl⟩)
theorem my2_spec : my2 = 2 := Classical.choose_spec (show ∃ n, n = 2 from ⟨2, rfl⟩)

example [AddMonoidWithOne R] : (Nat.cast' my2 : R) = 2 := by
  rw [my2_spec] -- no dependency on `my2` exposed because `Nat.cast'` is never unfolded

example [AddMonoidWithOne R] : (Nat.cast' my2 : R) = 2 := by
  rw [Nat.cast', my2_spec] -- dependency on `my2` is fine because `rw` works on all occurences

example [AddMonoidWithOne R] : (Nat.cast' my2 : R) = 2 := by
  rw [Nat.cast']
  conv in (@OfNat.ofNat _ my2) => rw [my2_spec] -- ERROR: motive is dependent

[Kyle Miller]

While that's a scenario I was imagining, it's not the one I was talking about. An assumption is that given R and x then Lean can use the instance it infers to fill in the _ in OfNat.ofNat R x _. There are many places in Lean that try to check this assumption (an error you might see is "inferred instance is not defeq to provided instance", or something like that).

Even if you replace x with a defeq term, if it's not syntactically of the right form there's a chance the instance it infers will not be the right one.

[Timo Carlin-Burns]

But as long as the synthesized instances are defeq there's no problem, right? The design of AddMonoidWithOne.instOfNat above is precisely to avoid non-defeq instance diamonds for OfNat R 0 and OfNat R 1