Cardinal NatCast

Stream: mathlib4

[Violeta Hernández]

Currently, the cast ℕ → Cardinal is defined as #(Fin n). I get this is really nice from a mathematical perspective, but is it really useful?

[Yury G. Kudryashov]

What do you suggest?

[Violeta Hernández]

Well, I'm wondering why not just use the default natCast implementation

[Violeta Hernández]

That way ↑0 = 0, ↑1 = 1, and ↑(n + 1) = ↑n + 1 are all def-eq

[Violeta Hernández]

#(Fin n) = n can be a simp lemma rather than a definitional equality

[Violeta Hernández]

This is what Ordinal does btw, even though we very well could have had ↑n = @type (Fin n) (· < ·)

[Yury G. Kudryashov]

See #6384

[Yury G. Kudryashov]

Authored by @Sébastien Gouëzel

[Violeta Hernández]

Hm yeah, I'm not sure I agree with that rationale

[Violeta Hernández]

I'd argue the main reason to choose one implementation of something like NatCast over another is the def-eqs. After all, all implementations are supposed to be prop-eq anyways.

[Violeta Hernández]

#(Fin n) gives us nothing of the sort. The fact Zero and One had to be redefined from what I'd argue are pretty clear canonical definitions #PEmpty and #PUnit just illustrates that further

[Yury G. Kudryashov]

Let's wait for Sébastien.

[Sébastien Gouëzel]

I don't really remember the details, but for me the main point is that it's a good mathematical definition. The defeq ↑(n + 1) = ↑n + 1 that you would get from the other definition is in my opinion not something important, for computations you have lemmas, while having a definition that makes sense is much more enlightening. I think it would be a good idea to do the same for ordinals, by the way, I just didn't have time to do it then!

[Violeta Hernández]

I'd oppose this on ordinals even more. Def-eqs work even nicer on them, since we can define succ x as x + 1. So for instance, succ 2 = 3 is currently def-eq.

[Violeta Hernández]

I don't think either definition is any more illuminating than the other, they both satisfy the same theorems. But one is slightly more annoying to work with.

[Violeta Hernández]

Here's the example that prompted me to create this thread. Consider the statement #{a, b, c, d} ≤ 4. By using Cardinal.mk_insert_le repeatedly, you can show #{a, b, c, d} ≤ 1 + 1 + 1 + 1. But because of the nonstandard NatCast, to get from 1 + 1 + 1 + 1 to 4 you need to either use Nat.cast_add_one a couple of times or insert norm_cast somewhere.

[Violeta Hernández]

Hypothetically with 4 def-eq to #(Fin n) you could call Cardinal.mk_le and establish an injection between your set and Fin 4, or something of the sort, but all that seems strictly more convoluted.

[Sébastien Gouëzel]

Having #(Fin n) = n in a defeq way seems to me much more important that defeqs for cardinal arithmetic (which should be handled by norm_num or suitable simp lemmas, definitely not rely on defeq coincidence): Fin n is used in Mathlib as the reference set of cardinality n, so we should make sure that this is reflected in the design choices.

[Violeta Hernández]

I wouldn't call it "defeq coincidence", the default NatCast implementation is pretty deliberate in what def-eqs you get. 0 = ↑0, 1 = ↑1, and ↑(n + 1) = ↑n + 1.

[Violeta Hernández]

If the reasoning is ultimately that "#(Fin n) is the standard mathematical definition and we got to stick to it", so be it, but I'll still disagree.

[Sébastien Gouëzel]

I think your feeling is guided by the fact that you're doing a lot of operations on cardinals and ordinals currently, and for this the defeq you're advocating for would be most convenient. But in mathematics, 95% of the time, cardinals are used to compare the size of things, not to do operations on them, so it seems natural to have a definition fitting these 95% of uses.

[Violeta Hernández]

Alright, I agree with that logic.

[Violeta Hernández]

I've thought about this for a while and I think I do agree that using the default natcast isn't always the best idea. I'll look into redefining the cast for ordinals as type (Fin n)

[Violeta Hernández]

And on that note, another weird NatCast instance we have is docs#SetTheory.PGame.instNatCast, which doesn't even agree with the usual definition of natural numbers as pre-games (it yields an equivalent but not an identical game)

[Violeta Hernández]

I'll try and fix that

[Violeta Hernández]

...actually, I'd like to discuss that instance separately

[Violeta Hernández]

Heh, looks like I already had a thread here for it, but I can't edit it anymore