RFC: drop `Nat.AtLeastTwo`

Status quo

In Lean 4, numerical literals (e.g., (3 : α)) are in fact expressions of the form OfNat.ofNat 3 and depend on a typeclass instance

instance : OfNat α n

available for this particular type & numerical literal.

In Mathlib, there are a few commonly used OfNat instances:

• [One M] : OfNat M 1;
• [Zero M] : OfNat M 0;
• [NatCast R] {n} [n.AtLeastTwo] : OfNat R n.

There are also instances like [NeZero n] : OfNat PNat n, which are probably out of the scope of this discussion.

Why Nat.AtLeastTwo?

If we just drop [n.AtLeastTwo] in the [NatCast R] : OfNat R n instance, then for a ring R, we'll have 2 different instances for [OfNat R 0] and [OfNat R 1]. While we can ensure definitional equality for each specific type, this won't work for a generic ring.

Why change?

• Leo is working on grind and Groebner bases, and he uses [∀ n, OfNat α n] everywhere. If we want his code to work for Mathlib type, then we need to ensure [∀ n, OfNat α n] for our types or negotiate another approach.

• set_option pp.all true in
  #check (10 : ℝ)
  

  gives

  @OfNat.ofNat.{0} Real 10
    (@instOfNatAtLeastTwo.{0} Real 10 Real.instNatCast
      (@instNatAtLeastTwo (@OfNat.ofNat.{0} Nat 8 (instOfNatNat 8)))) : Real
  

• def thirtySeven : ℝ := 30 + 7 generates auxiliary declarations thirtySeven._proof_1 : (28 + 2).AtLeastTwo etc

Proposal 1

Drop [Nat.AtLeastTwo] and simplify one ofNat _ 0 to another.

Downside: it's easy to arrive at a situation when a lemma seems to apply but it doesn't, because it uses a wrong zero or one. This manifest as 1 = 1 not being solved by rfl. While we can ensure defeq for each concrete type (e.g., Real, by removing irreducible_def), we can't make it work for {M : Type*} [AddMonoidWithOne M] without rewriting the definition of AddMonoidWithOne (or modifying some other part of the system).

Proposal 2

Drop [Nat.AtLeastTwo _] and rewrite AddMonoidWithOne so that it no longer extends Zero (via AddMonoid) or One, and repeats the AddMonoid axioms using zero and one coming from ∀ n, OfNat M n.

We should write a linter that verifies that no instance of AddMonoidWithOne (or another class down the road) conflicts with Zero/One instance coming from other source.

Details of API changes

NatCast

We no longer use NatCast to generate OfNat instances. Instead, we have

instance [∀ n, OfNat M n] : NatCast M where
  natCast n := OfNat.ofNat n

IntCast

TODO: probably, no changes are required here.

AddMonoidWithOne

Instead of extending NatCast M and AddMonoid M, we use something like

class AddMonoidWithOne (M : Type*) extends AddSemigroup M where
  [toOfNat : ∀ n, OfNat M n]
  zero_add : ∀ x : M, 0 + x = x
  add_zero : ∀ x : M, x + 0 = x
  -- nsmul etc

When creating an instance [AddMonoidWithOne M], if either of [Zero M] or [One M] already exists, then we use something like

  toOfNat n
    | 0 => 0
    | 1 => 1
    | m + 2 => ⟨myFun m⟩

Semiring etc

The API changes above mean that we can no longer extend multiplicative and additive typeclasses in Semiring etc. We'll have to extend AddMonoidWithOne R, then add the relevant multiplicative fields (incl. npow stuff, if needed). This code duplication may be the main drawback of this approach.

A possible way to avoid this is to have a structure (does it have to be a class?) that takes [One _]/[Zero _] as an argument and gives all the remaining fields of Monoid _ / Group _ (I guess, these are the two most common cases).

Linter

For each instance, if the corresponding class has a projection to ∀ n, OfNat M n, then for each k = 0, 1, the linter should

• try to generate OfNat M k (a.k.a. Zero M or One m) with the same typeclass assumption but without using this instance;
• if the search fails, then OK;
• otherwise, verify that the instance is defeq to the instance provided by the new instance.