Nat.unaryCast and one

Stream: general

[Sebastien Gouezel]

In current mathlib, we have:

example : (0 : Cardinal) = ((0 : ℕ) : Cardinal) := rfl -- works
example : (1 : Cardinal) = ((1 : ℕ) : Cardinal) := rfl -- fails
example : (2 : Cardinal) = ((2 : ℕ) : Cardinal) := rfl -- works
example : (3 : Cardinal) = ((3 : ℕ) : Cardinal) := rfl -- works
example : (4 : Cardinal) = ((4 : ℕ) : Cardinal) := rfl -- works
...

which is a little bit unpleasant -- I've been bitten by this in #6348.

This is due to the inductive definition of the cast, which is

protected def Nat.unaryCast {R : Type u} [One R] [Zero R] [Add R] : ℕ → R
  | 0 => 0
  | n + 1 => Nat.unaryCast n + 1

(so 1 is mapped to 0 + 1, not 1, which is why the rfl above breaks for n = 1).

We could fix this by changing the definition to

protected def Nat.unaryCast' {R : Type u} [One R] [Zero R] [Add R] : ℕ → R
  | 0 => 0
  | 1 => 1
  | n + 2 => (Nat.unaryCast' (n + 1)) + 1

but at the expense of the loss of the defeq

example (n : ℕ) : ((n + 1 : ℕ) : Cardinal) = (n : Cardinal) + 1 := rfl

(which works currently, but would be broken with the new definition).

For me, good defeqs for 1 are more important than coincidental defeqs in arithmetic equations, so I would be ready to refactor mathlib (not only in cardinals) by changing the definition of Nat.unaryCast to Nat.unaryCast'. But since it's a pretty fundamental change (and probably quite painful), I'd be happy to read your thoughts about that before I start.

[Eric Wieser]

Should we instead set Cardinal.natCast n := Quotient.mk (Fin n)?

[Eric Wieser]

That gives us nice defeqs for toNat

[Eric Wieser]

I think there might have been an abandoned Lean3 PR that did that

[Sebastien Gouezel]

It's not just for cardinals: in any type using the default Nat.unaryCast for natCast, defeqs for 1 are currently broken (while defeqs for all other natural numbers work just fine).

[Anne Baanen]

I assume the alternative would be to redefine the One instance to be 0 + 1?

[Sebastien Gouezel]

No, because then the cast of 1 would be 0 + (0 + 1)...

[Sebastien Gouezel]

It uses the One instance in the inductive definition.

[Eric Wieser]

My understanding is that unaryCast is just a compatibility shim for code that existing before natCast was introduced

[Eric Wieser]

Note that there are many other types where ($n : X) = (($n : ℕ) : X) is not defeq; two that come to mind are Fin k with n = 0 and Polynomial (due to irreducible_def)

[Sebastien Gouezel]

Eric Wieser said:

Should we instead set Cardinal.natCast n := Quotient.mk (Fin n)?

Done in #6384.