cardinalities

Stream: mathlib4

[Antoine Chambert-Loir]

There are various ways to access the cardinality of a (finite) set, docs#Nat.card, docs#Set.ncard and docs#Set.encard, docs#Finset.card, docs#Fintype.card, or docs#PartENat.card…
For basic combinatorial manipulations, which one is recommended?

(All APIs are not complete, for example, there is no Nat.card_union_add_card_inter corresponding to docs#Set.ncard_union_add_ncard_inter)

[Jireh Loreaux]

I would say it depends on the situation. If your sets are structurally finite (i.e., they are Finsets or lie in a Fintype), then you probably want Finset.card (perhaps accessed with Set.toFinset in the case of a fintype). However, if they are just provably finite, then likely Set.ncard is the way to go. If they are finite in some situations, but not others, then you'll want Set.encard. Note that Nat.card and Fintype.card should be used for types not sets (in general).

[Jireh Loreaux]

I would avoid using PartENat.card for now. There was recent talk of removing PartENat and developing an ENat.card API.

[Antoine Chambert-Loir]

Thanks. (I had not realized that Nat.card should only be used for types, that should explain some of my troubles…)

Additional question : should we use [Finite] whenever we don't make use of an explicit enumeration given by [Fintype]?

[Jireh Loreaux]

Yes. In fact, as long as the statement doesn't need Fintype, you should use Finite, even if in the proof you need the Fintype. You can get a Fintype instance from a Finite instance locally within the proof using docs#Fintype.ofFinite

[Thomas Browning]

You can use Nat.card for sets, since sets are automatically coerced into types, but this is exactly how Set.ncard is defined, so you should just use Set.ncard since it gives you access to more relevant API

[Kyle Miller]

Jireh Loreaux said:

Note that Nat.card and Fintype.card should be used for types not sets (in general).

There's a good amount of API for Fintype.card of sets, probably because it's more convenient than s.to_finset.card. I think you're right in principle though, since I remember having troubles with simp lemmas turning Fintype.card expressions for sets into inconvenient forms (but perhaps it doesn't affect Lean 4 now that coercions work differently... Still, it's nice having Set.ncard to keep things in Set language.)

[Yaël Dillies]

Antoine Chambert-Loir said:

I had not realized that Nat.card should only be used for types

I don't actually think that's true? At any rate, the best choice is Finset.card in most scenarii.

[Junyan Xu]

Thomas Browning said:

You can use Nat.card for sets, since sets are automatically coerced into types, but this is exactly how Set.ncard is defined

Nope?

Set.ncard s = ↑ENat.toNat (Set.encard s)
Set.encard s = ↑PartENat.withTopEquiv (PartENat.card ↑s)
PartENat.card α = ↑Cardinal.toPartENat (Cardinal.mk α)
Nat.card α = ↑Cardinal.toNat (Cardinal.mk α)

so Set.ncard goes from Cardinal -> PartENat -> ENat -> Nat while Nat.card does it in one step. (This might have recently changed in #5908. I didn't know the first three defs exist before this thread!)

Jireh Loreaux said:

I would avoid using PartENat.card for now. There was recent talk of removing PartENat and developing an ENat.card API.

How would the hypothetic ENat.card API be different from the Set.encard API?

[Eric Wieser]

One would operate on types, the other sets

[Junyan Xu]

While Finset.card necessarily take a (Fin)set since its computability doesn't work for a general type, I think for the other cardinalities that are defined in terms of Cardinal.mk and noncomputable anyways, we don't lose anything by restricting the definition to types and centering the API around types, and using coercion when applying it to sets. It's actually less convenient the other way, as we'd need to use type annotations like ⊤ : Set α when applying it to a type α. I think this is also the design we adopted for properties of Submodules, etc.

[Jireh Loreaux]

Junyan, the problem is you want statements about the cardinality of a union of two sets and the like. And then it gets a bit messy if you don't have a set version. Ask @Peter Nelson.

[Antoine Chambert-Loir]

Also: when acting (probably carelessly) with types, I easily ended ups with finiteness instances that Lean had created but couldn't manage to identify, so that apparently obvious equalities of the form Nat.card ↑s = Nat.card ↑s wre not proved by rfl…

[Junyan Xu]

docs#Nat.card doesn't take any finite instances. Do you mean Fintype.card?

[Junyan Xu]

the problem is you want statements about the cardinality of a union of two sets and the like

We'd have docs#Cardinal.mk_union_le and docs#Cardinal.mk_union_of_disjoint but the main definition still applies to a type.

[Jireh Loreaux]

Probably he meant that he needed finiteness assumptions for Nat.card to avoid the junk value.

Yes, I realize you can do it that way, but I think ultimately it's going to be more painful than just having a dedicated def for sets. I could be wrong though.

[Antoine Chambert-Loir]

Having rewritten many lemmas using Set.ncard systematically, I can confirm that the proofs are simpler.

[Peter Nelson]

Junyan Xu said:

While Finset.card necessarily take a (Fin)set since its computability doesn't work for a general type, I think for the other cardinalities that are defined in terms of Cardinal.mk and noncomputable anyways, we don't lose anything by restricting the definition to types and centering the API around types, and using coercion when applying it to sets. It's actually less convenient the other way, as we'd need to use type annotations like ⊤ : Set α when applying it to a type α. I think this is also the design we adopted for properties of Submodules, etc.

One thing that is lost is dot notation for sets. And having coercion symbols everywhere. What kind of lemmas about Nat.card for types (that aren't more naturally phrased as statements about sets) do you have in mind?

[Peter Nelson]

Junyan Xu said:

so Set.ncard goes from Cardinal -> PartENat -> ENat -> Nat while Nat.card does it in one step. (This might have recently changed in #5908. I didn't know the first three defs exist before this thread!)

Originally Set.ncard was defined in terms of Nat.card. The change was made to defining it via Set.encard at @Jireh Loreaux 's suggestion. But it's still propositionally equal; see Set.Nat.card_coe_set_eq. I don't have a strong view on which defeq is preferable.