Set.toNonempty

Stream: Is there code for X?

[Terence Tao]

This is a somewhat trivial thing, but would it make sense to have an analogue of docs#Set.toFinite for non-emptiness, i.e.,

import Mathlib

theorem Set.toNonempty {α : Type u} (s : Set α) [hs: Nonempty s] : Set.Nonempty s := nonempty_coe_sort.mp hs

so that one can use s.toNonempty instead of nonempty_coe_sort.mp (s := s) (by infer_instance)? With the current API it seems unnecessarily clunky to be able to actually establish a Set.Nonempty proposition.

[Johan Commelin]

Sounds good. What do you think of calling it Set.of_nonempty_coe?

[Terence Tao]

Would that mean that Set.toFinite should be similarly aliased to Set.of_finite_coe? I'm fine with either (or both), but I suppose we should try to be consistent with naming conventions if there is no pressing reason to deviate from them.

[Yaël Dillies]

I think of Set.toFinite as a pretty poor name. Certainly, I can't guess it every time I need it! I think Set.Finite.of_subtype or Set.Finite.of_coe or Set.Finite.of_coe_sort would be better.

[Terence Tao]

Similarly one could have

theorem Set.of_infinite_coe {α : Type u} (s : Set α) [hs: Infinite s] : Set.Infinite s := infinite_coe_iff.mp hs

theorem Set.of_subsingleton_coe {α : Type u} (s : Set α) [hs: Subsingleton s] : Set.Subsingleton s := (subsingleton_coe s).mp hs

On the other hand, we already have docs#Set.to_countable. It seems that the naming conventions here are not uniform.

[Yaël Dillies]

Yeah, I am happy to open a PR to clean this up. I've been annoyed by it.

[Terence Tao]

Would you still keep Set.toFinite and Set.to_countable as aliases for (I presume) Set.of_finite_coe and Set.of_countable_coe? Certainly Set.toFinite is used extensively in PFR for instance.

[Yaël Dillies]

As deprecated aliases, likely.

[Yaël Dillies]

The point of a name like Set.Finite.of_coe is that you can write .of_coe wherever Lean expects a term of type Set.Finite _.

[Terence Tao]

But then conversely if one only has a name for the set s and not the Finite instance, how do you use dot notation to prove Set.Finite s using the name Set.Finite.of_coe? I find s.toFinite a convenient notation.

[Yaël Dillies]

What would s.toFinite do if you didn't have the Finite s instance around? I would expect that to error.

[Terence Tao]

"failed to synthesize instance Finite ↑s".

[Terence Tao]

I use s.toFinite.toFinset a lot to create Finset versions of a Finite set. Not sure how else to do it actually.

[Yaël Dillies]

Oh you can just use docs#Set.toFinset

[Yaël Dillies]

A neat alternative is the lift tactic. If s : Set α and hs : s.Finite, then lift s to Finset α using hs will replace s : Set α by s : Finset α everywhere. It's magic.

[Kyle Miller]

Yaël Dillies said:

The point of a name like Set.Finite.of_coe is that you can write .of_coe wherever Lean expects a term of type Set.Finite _.

I feel like dot notation is frequently used for this where expected types aren't available

[Kyle Miller]

There's no harm having multiple aliases though (or maybe there are simp lemmas where this matters...)

[Kyle Miller]

I'm not sure I agree that Set.toFinite should be fundamentally renamed, but it should be Set.to_finite per the convention, right?

[Terence Tao]

Yaël Dillies said:

Oh you can just use docs#Set.toFinset

Set.toFinset requires a Fintype instance, which is not automatically generated from a Finite instance (a decidability issue perhaps?).

[Yaël Dillies]

You can use classical to fix this.

[Yury G. Kudryashov]

We don't have Finite α → Fintype α as an instance in classic to avoid diamonds.

[Yaël Dillies]

Yes but Fintype α → Fintype s becomes an instance.

[Kyle Miller]

One trick is have := Fintype.ofFinite to force the classical instances that s.toFinite.toFinset gives. I'm sure this causes issues places, but you can always be more precise with the have by giving an argument

[Terence Tao]

Currently we have the following converters regarding finite sets:

• Set.toFinite : converts Finite instance to Set.Finite proposition
• Finset.finite_toSet: converts a Finset type to a Set.Finite proposition
• Fintype.finite: converts a Fintype instance to a Finite instance
• Set.Finite.to_subtype: converts Set.Finite proposition to a Finite instance
• Finite.of_fintype: Instance inference from Fintype to Finite
• Set.Finite.fintype: converts Set.Finite proposition to a Fintype instance
• Fintype.ofFinite: converts a Finite instance to a Fintype instance
• Fintype.ofFinset: converts a Finset type to a Fintype instance
• Set.Finite.toFinset: converts a Set.Finite proposition to a Finset type

I could imagine that there might be a more logical naming system here (in particular we might also want to have a wrapper for Set.finite_coe_iff.mpr).

[Yury G. Kudryashov]

Isn't docs#Set.Finite.to_subtype a wrapper for docs#Set.finite_coe_iff ?