Set.toFinset without Fintype or Set.Finite

Stream: Is there code for X?

[Terence Tao]

Is the following variant of Set.toFinset already somewhere in Mathlib?

noncomputable def Set.toFinset' {α: Type*} (s: Set α) : Finset α :=
  dite (h := Classical.dec (Set.Finite s)) Set.Finite.toFinset (fun _ ↦ ∅)

lemma Set.toFinset'_of_set_finite {α: Type*} {s: Set α} (h:Set.Finite s) : s.toFinset' = h.toFinset := by
  simp [h, Set.toFinset']

lemma Set.toFinset'_of_finite {α: Type*} {s: Set α} [Finite s] : s.toFinset' = s.toFinite.toFinset := by
  simp [toFinite s, Set.toFinset']

lemma Set.toFinset'_of_set_infinite {α: Type*} {s: Set α} (h: Set.Infinite s) : s.toFinset' = ∅ := by
  simp [mt Set.Finite.not_infinite (not_not_intro h), Set.toFinset']

lemma Set.toFinset'_of_infinite {α: Type*} {s: Set α} [h: Infinite s] : s.toFinset' = ∅ := by
  simp [mt Set.Finite.not_infinite (not_not_intro (infinite_coe_iff.mp h)), Set.toFinset']

@[simp]
lemma Set.toFinset'_of_fintype {α: Type*} (s: Set α) [Fintype s] : s.toFinset' = s.toFinset := by
  simp [Set.toFinite s, Set.toFinset']

That is to say, the same operation as Set.toFinset or Set.Finite.toFinset, but without the requirement of Set.Finite s or [Fintype s], instead assigning a junk value of ∅ in the case of infinite sets. I found it useful to have this broader version of Set.toFinset in order to make certain definitions shorter (e.g., summing over a set that one eventually will prove is finite, but for which one doesn't want to embed the proof of finiteness into the definition that involves the sum).

[Also, a tangential question: why does one need to suppress the argument Set.Finite s in the invocation of dite? From docs#dite I would have thought I needed to write dite (Set.Finite s) (h := Classical.dec (Set.Finite s)) Set.Finite.toFinset (fun _ ↦ ∅), but Lean doesn't like that spelling.]

[Kyle Miller]

I like the idea of this variant. I'd considered it before, but I didn't have a project to motivate it.

Here's some more development on the idea:

import Mathlib.Data.Set.Finite
import Mathlib.Data.Set.Card

variable {α : Type*}

/--
Given a set `s`, `s.toFinset'` is a `Finset` that has the same elements as `s`
if `s` is a finite set.
This is similar to `s.toFinset` but it does not require a `Set.Finite` proof.

In case `s` is not finite, then it is defined to use `s.toFinset' = ∅`.

The specification for this function is given by the lemmas
`Set.Finite.toFinset'` and `Set.Infinite.toFinset'`.

This definition satisfies `s.toFinset'.card = s.ncard` (see `Set.card_toFinite'_eq_ncard`).
-/
protected noncomputable def Set.toFinset' (s : Set α) : Finset α :=
  haveI := Classical.dec
  if h : s.Finite then h.toFinset else ∅

variable {s : Set α}

/-- Defining lemma specifying `s.toFinset'` if `s` is finite. -/
protected lemma Set.Finite.toFinset' (h : s.Finite) : s.toFinset' = h.toFinset := by
  simp [Set.toFinset', h]

-- missing set API
protected lemma Set.Infinite.not_finite (h : s.Infinite) : ¬ s.Finite := by
  rwa [← not_infinite, not_not]

/-- Defining lemma specifying `s.toFinset'` if `s` is infinite. -/
protected lemma Set.Infinite.toFinset' (h : s.Infinite) : s.toFinset' = ∅ := by
  simp [Set.toFinset', h.not_finite]

lemma Set.toFinset'_eq_of_finite [Finite s] : s.toFinset' = s.toFinite.toFinset := by
  simp [Set.toFinset', s.toFinite]

-- missing set API
lemma Set.infinite_of_subtype (s : Set α) [Infinite s] : s.Infinite :=
  Set.infinite_coe_iff.mp ‹_›

lemma Set.toFinset'_eq_of_infinite [Infinite s] : s.toFinset' = ∅ :=
  s.infinite_of_subtype.toFinset'

-- Not sure this should be a simp lemma, since it leads to switching from Set to Finset worlds.
-- An issue is that the result of the simplification depends on exactly what Fintype instances
-- are around, and how they are defined.
-- Maybe we should have a custom simp set for trying to convert to Finset?
lemma Set.toFinset'_of_fintype [Fintype s] : s.toFinset' = s.toFinset := by
  simp only [toFinset'_eq_of_finite, toFinite_toFinset]

lemma Set.card_toFinite'_eq_ncard : s.toFinset'.card = s.ncard := by
  cases Set.finite_or_infinite s with
  | inl h => simp [h.toFinset', ncard_eq_toFinset_card s h]
  | inr h => simp [h.toFinset', h.ncard]

[Kyle Miller]

In the realm of finiteness, before the port started I was thinking about developing

structure FiniteSet (α : Type*) where
  toSet : Set α
  finite : toSet.Finite

The idea is that this would be for purely classical finite sets; it lets you completely avoid Decidable. I like how it also has the property that creating a FiniteSet and then coercing back to the Set is defeq to the original Set. If there are places where you do want computational content, then the idea would be that you could register Fintype instances and use Set.toFinset on the coerced FiniteSet.

If we had this, then there could be a Set.toFiniteSet : Set α -> FiniteSet α analogue of your function, that gives the empty set for infinite sets.

[Kyle Miller]

Terence Tao said:

[Also, a tangential question: why does one need to suppress the argument Set.Finite s in the invocation of dite? From docs#dite I would have thought I needed to write dite (Set.Finite s) (h := Classical.dec (Set.Finite s)) Set.Finite.toFinset (fun _ ↦ ∅), but Lean doesn't like that spelling.]

That's odd. It looks like it might be an elaboration bug.

[Yaël Dillies]

Kyle Miller said:

I like how it also has the property that creating a FiniteSet and then coercing back to the Set is defeq to the original Set.

My idea of adding a carrier field to Finset would also give you this

[Terence Tao]

Kyle Miller said:

Here's some more development on the idea:

Thanks! That may be close to the full API available for Set.toFinset', which is otherwise a pretty lousy operation. (It behaves well with respect to embeddings and equivalences, and also erase, but actually it may be better not to put in the few lemmas that it does satisfy, because I view this operation as a placeholder whose primary purpose is to allow certain Finset-based definitions (such as anything involving Finset.sum) to be made easily, with the intent to pass from Set.toFinset' to Set.toFinset (or ∅) as quickly as possible to take advantage of the much better API there. That's why I thought Set.toFinset'_of_fintype (and also Set.toFinset'_eq_of_infinite) should be simp lemmas - anything that gets you out of Set.toFinset' is progress.

As for a yet another structure to capture finiteness beyond the four we already have (Fintype, Finite, Set.Finite, and Finset), I feel that this could be too much complexity (cf. https://xkcd.com/927/). Finset seems quite deeply embedded in the current Mathlib library and I don't see a realistic way to dethrone it; at best one could create a niche variant of the concept (something like ClassicalFinset perhaps?) with a much smaller API (ideally with easy ways to transfer a large fraction of Finset lemmas over to ClassicalFinset without having to duplicate everything).

[Kevin Buzzard]

The xkcd reference is very pertinent. I was part of the problem here: I found finsets very hard to work with in 2019, partly because the community had not understood all the tricks yet (so we would end up with problems when dealing with finite sets of naturals because some lemmas would use decidability in Nat and others would use classical decidability, and there would be subsingleton diamonds which stopped rw from working and it was very frustrating; since then we discovered the rules of thumb such as asking for decidability rather than working classically if the theorem statment wouldn't compile otherwise). I pushed for Set.Finite and with an undergraduate at Imperial wrote a bunch of API for it, with a typical proof being "this is proved for finsets, so use the finset version and deduce the finite version", and the ridiculous irony was that by the end of developing the API I had worked so much with finsets that I had now really got the hang of them, so afterwards I just went back to using finsets instead :-/

[Oliver Nash]

Terence Tao said:

Finset seems quite deeply embedded in the current Mathlib library and I don't see a realistic way to dethrone it.

IMHO we could and should dethrone docs#Fintype and docs#Finset. It would be a significant refactor but certainly not impossible. As noted above, the thing we currently lack is bundled, classical finiteness for subsets and so we constantly use docs#Finset instead, which forces us to care about how things are finite when most of the time we only care that they are finite.

[Yury G. Kudryashov]

OTOH, we will no longer have computability this way.

[Yury G. Kudryashov]

So, it will be no longer possible to decide away simple properties.

[Yury G. Kudryashov]

Though we may have a tactic that moves things from noncomputable world to computable world finding necessary Decidable* or whatever on its way.

[Terence Tao]

For me as an analyst, the main reason why I have to work with Finset is that the default summation notation ∑ is tied to Finset.sum. (There is of course also ∑' that is tied to infinite summation tsum, but often one really wants to work with finite summation.) For most other usecases it doesn't seem to matter much which flavor of finiteness one works with - one just changes the methods and does some appropriate coercions - but for summation it would be rather annoying to use a class other than the one that ∑ is defaulted to using.

[Yury G. Kudryashov]

We also have docs#finsum

[Yury G. Kudryashov]

It moves proofs of finiteness from statements of theorems to their proofs.

[Yury G. Kudryashov]

It came to Mathlib much later and has less API at the moment.

[Terence Tao]

Ah, didn't know about that alternative. Actually, that's a pretty reasonable solution. Also fits well with the toFinset' method I proposed above.

[Yury G. Kudryashov]

The xkcd reference is very appropriate for anything "finite"-related in Mathlib.

[Terence Tao]

For instance, one can now add to the previous proposed API:

lemma toFinset'_subset : (s.toFinset' : Set α) ⊆ s := by
  cases Set.finite_or_infinite s with
  | inl h => simp [h.toFinset', Eq.subset rfl]
  | inr h => simp [h.toFinset']

open BigOperators

lemma finsum_eq_sum' {M : Type*} {α : Type*} [AddCommMonoid M] (f : α → M)
  : ∑ᶠ x, f x = ∑ x in (Function.support f).toFinset', f x := by
  cases Set.finite_or_infinite (Function.support f) with
  | inl h => rw [finsum_eq_sum f h, Set.Finite.toFinset' h]
  | inr h => rw [finsum_of_infinite_support h, Set.Infinite.toFinset' h, Finset.sum_empty]

lemma finsum_on_set_eq_sum' {M : Type*} {α : Type*} [AddCommMonoid M] (f : α → M) (s: Set α)
  : ∑ᶠ x ∈ s, f x = ∑ x in (s ∩ Function.support f).toFinset', f x := by
  simp_rw [finsum_eq_sum', finsum_eq_indicator_apply]
  apply Finset.sum_congr
  . rw [Set.support_indicator]
  intro x hx
  replace hx := toFinset'_subset hx
  simp [Set.mem_of_mem_diff hx]

[Edited to add the version restricted to sets.]

[Terence Tao]

In that case, Finsets are actually quite avoidable in most of the type of math I've been dealing with then.

[Terence Tao]

(though finsum definitely needs a bit more API, in particular for restricted sums ∑ᶠ x in s, f x, which doesn't seem to exist yet.)

[Yury G. Kudryashov]

We have ∑ᶠ x ∈ s, f x

[Yury G. Kudryashov]

The PLift trick allows us to use ∑ᶠ k < 10, f k

[Yury G. Kudryashov]

But a lot of API is missing.

[Terence Tao]

Yury G. Kudryashov said:

We have ∑ᶠ x ∈ s, f x

Is there a systematic naming convention on when to use ∈ and when to use in? Right now, ∑and ∫ use in, while ∑ᶠ, ⋃, and ⋂ use ∈.

[Mario Carneiro]

They mean different things. The in variant, when it exists, represents a single composite operation, like a finset sum which requires the finset for its definition. The other binary operators are piggybacking on general support for extended binders, and generally mean some kind of iterated binder

[Kyle Miller]

Terence Tao said:

Also, a tangential question: why does one need to suppress the argument Set.Finite s in the invocation of dite? [...]

(It appears that lean4#1867 is the relevant issue, and I added this dite example.)