Cardinal.mk

Stream: mathlib4

[Yaël Dillies]

#α in the Cardinal scope is notation for Cardinal.mk α. People in the past have found it confusing that this is the constructor for Cardinal, hence don't usually reach for the name mk. What do people think of renaming mk to card or something similar?

[Yaël Dillies]

This is wanting I've wanted to do for a while, but @Yury G. Kudryashov is blocking my smaller scope PR #18808 on it

[Yaël Dillies]

@Violeta Hernández says

The fact that #α is precisely the constructor of Cardinal applied to α is not really intuitive unless you're aware of it. I'd also prefer that we simply rename these theorems to use card.

To clarify, cardinal_mk in lemma names would have to be changed to cardinalCard, not merely card because it is ambiguous with docs#Fintype.card, docs#Finset.card, docs#FinEnum.card

[Johan Commelin]

So Cardinal.card or _root_.card?

[Yaël Dillies]

As explained just above, _root_.card would be disastrous for ambiguity. _root_.ccard/_root_.cCard/_root_.cardC would be nice but I'm not sure we can name a constructor of a structure outside its namespace?

[Johan Commelin]

It would have to be an alias

[Johan Commelin]

I find cardinalCard quite duplicaty

[Johan Commelin]

But that's my only objection

[Eric Wieser]

Another option would be a HasCard typeclass providing a global card, instantiated as HasCard (Type u) Cardinal.{u} and HasCard (Finset X) Nat etc; though perhaps this makes it too easy to accidentally truncate with Nat.card...

[Yaël Dillies]

I've already thought of this typeclass and the issue is that it would make #{x | p x} not elaborate asFinset.filter Finset.univ fun x => p x anymore, which I would find very sad.

[Daniel Weber]

Following docs#Nat.card this should be Cardinal.card, but there is a duplication there

[Daniel Weber]

I don't think using card is ambiguous with docs#Fintype.card, docs#Finset.card, docs#FinEnum.card if it's in the Cardinal namespace

[Yury G. Kudryashov]

About blocking #18808: I assumed (possibly, incorrectly) that @Eric Wieser 's comment blocks it. If Eric is OK with merging #18808 now and deciding about another rename later, then I'm OK too.

[Violeta Hernández]

Eric Wieser said:

Another option would be a HasCard typeclass providing a global card, instantiated as HasCard (Type u) Cardinal.{u} and HasCard (Finset X) Nat etc; though perhaps this makes it too easy to accidentally truncate with Nat.card...

This feels like the cleanest solution to me, and then # can be notation for card in both cases. Note that instances HasCard (Multiset X) Nat and maybe HasCard (List X) Nat could also make sense, though perhaps that's getting ahead of ourselves.

Yaël Dillies said:

I've already thought of this typeclass and the issue is that it would make #{x | p x} not elaborate asFinset.filter Finset.univ fun x => p x anymore, which I would find very sad.

What would it elaborate as instead?

[Yury G. Kudryashov]

What about Cardinal.mk vs Nat.card vs ENat.card for a Type?

[Violeta Hernández]

That's the current status quo, isn't it?

[Yury G. Kudryashov]

How do you suggest to make it work with HasCard?

[Violeta Hernández]

Oh, I misunderstood your question.

[Yury G. Kudryashov]

Sorry, I should've formulated it better.

[Violeta Hernández]

Yeah, I don't think we could have notation for all three at once

[Violeta Hernández]

Unless we want to do stuff like #ₙ and #ₑ

[Yury G. Kudryashov]

We can have # with different indices for different "types" of cardinalities.

[Eric Wieser]

Yaël Dillies said:

I've already thought of this typeclass and the issue is that it would make #{x | p x} not elaborate asFinset.filter Finset.univ fun x => p x anymore, which I would find very sad.

It already doesn't?

import Mathlib

open scoped Finset Cardinal

#check #{x | Nat.Prime x} -- Cardinal

[Eric Wieser]

Though interestingly #check #{x | Nat.Prime (x : Fin 6)} hits the ambiguity between the notations

[Violeta Hernández]

Yury G. Kudryashov said:

We can have # with different indices for different "types" of cardinalities.

Actually that's not a bad idea at all, and it's compatible with the HasCard idea, I think.

[Yury G. Kudryashov]

What should be the index for "Finset/Fintype"?

[Eric Wieser]

So you mean #ₙ?

[Yury G. Kudryashov]

I think that #ₙ should mean Nat.card or Set.ncard.

[Eric Wieser]

I'd propose #ₙx means @HasCard.card _ Nat x and #x means @HasCard.card _ Cardinal x

[Yury G. Kudryashov]

How do you tell Fintype.card from Nat.card?

[Eric Wieser]

Ugh, I forgot Nat.card acted on types

[Eric Wieser]

Maybe #!, since it's like the get! of the array world?

[Damiano Testa]

Or an index f for Finite, like the n could be Nat?

[Yury G. Kudryashov]

Note that you can have HasCard on Finsets but not on Types.

[Violeta Hernández]

My perhaps controversial suggestion is that Fintype.card should be explicitly specified, as a way to signal that you do in fact have a Fintype instance.

[Yury G. Kudryashov]

Because the signature is Fintype.card (α) [Fintype α] : Nat, not Type* → Nat.

[Eric Wieser]

Yury G. Kudryashov said:

About blocking #18808: I assumed (possibly, incorrectly) that Eric Wieser 's comment blocks it. If Eric is OK with merging #18808 now and deciding about another rename later, then I'm OK too.

My intent was not to block, only to make sure we were aware of the possibility of having to pay the cost of two sequential renames. Just renaming the constructor would have been easy enough, if we want to do it.

[Violeta Hernández]

Nat.card seems more useful in general

[Eric Wieser]

Yury G. Kudryashov said:

Because the signature is Fintype.card (α) [Fintype α] : Nat, not Type* → Nat.

I think this means I retract my proposal

[Yury G. Kudryashov]

I think that we can introduce notation like #ₙ, #, #ₑ for different cardinalities without introducing typeclasses.

[Eric Wieser]

That doesn't help with the naming question that started this thread though

[Yury G. Kudryashov]

Anyway, different cardinalities have different assumptions for the same lemmas.

[Yury G. Kudryashov]

/me is away for ~40min

[Violeta Hernández]

What's the way we currently handle Nat.card and Fintype.card in theorem names?

[Yury G. Kudryashov]

AFAICT, there is no system. Many lemmas are formulated for 1 of them only. We have ncard and encard for Set.ncard and Set.encard though.

[Violeta Hernández]

I think it makes sense not to be redundant with Fintype.card and Nat.card, but clearly Cardinal.mk is a different situation.

[Violeta Hernández]

I fear cardinalMk might actually be our best choice

[Violeta Hernández]

Unless we want to use something like ccard (cardinal cardinality)

[Daniel Weber]

Would the following behavior make sense? It could be implemented as a custom elaborator. For #s:

• If s can elaborate as a Finset, use Finset.card
• Otherwise, if it can elaborate as a Set, if the excepted type is ENat use Set.encard, otherwise use Set.ncard
• Otherwise, elaborate it as a Type _ (fail if this fails). Now try to synthesize a Fintype instance for it. If that succeeds, use Fintype.card.
• Otherwise, if the excepted type is Cardinal use Cardinal.mk
• Otherwise use Nat.card

[Yury G. Kudryashov]

I think that this will make the code less readable.

[Yury G. Kudryashov]

I would prefer to have different notation for different functions.