refactor(data/set/finite): use `finite` #15034

urkud · 2022-06-28T17:30:44Z

redefine set.finite in terms of finite;
move contents of data.finite.set to data.set.finite, use these instances to prove properties of set.finite;
use finite instead of fintype in some lemmas outside of these files.

kmill · 2022-07-01T16:58:59Z

This is a surprising change to see appear in the queue -- it would be nice to have some design discussion about this somewhere, for example at the Zulip threads where I've explained how I'd been thinking about redesigning finiteness.

I'd like to get a chance to review this before it's merged.

urkud · 2022-07-01T18:17:14Z

I'm sorry for not discussing it with you first. Could you please tag me in a thread about this? I'm on a phone, and it's less convenient to search from phone.

kmill · 2022-07-01T18:31:51Z

Sure, I'll do so once I have a chance to think through these changes. In principle, I think it's good to make set.finite use finite, but with everything moving around it's hard to tell immediately whether different considerations I had are carrying through.

urkud · 2022-07-01T18:33:14Z

I have Prop- valued countable almost done on top of this branch.

urkud · 2022-07-02T12:45:08Z

@kmill Will you have time to look at it soon? I'm afraid that it'll rot.

kmill

I'm on board with the changes now -- thanks for doing this reorganizational work!

The one thing I feel strongly about is getting a good name for set.finite_of_subtype. I previously had set.finite_of_finite for this, which admittedly sounds silly, but here are some other options:

set.mk_finite
set.finite_of
set.to_finite

I think set.finite_of is the strongest of these.

kmill · 2022-07-06T15:10:52Z

src/data/set/finite.lean

@@ -17,7 +18,7 @@ about finite sets and gives ways to manipulate `set.finite` expressions.

 * `set.finite : set α → Prop`
 * `set.infinite : set α → Prop`
-* `set.finite_of_fintype` to prove `set.finite` for a `set` from a `fintype` instance.
+* `set.finite_of_subtype` to prove `set.finite` for a `set` from a `fintype` instance.


Suggested change

* `set.finite_of_subtype` to prove `set.finite` for a `set` from a `fintype` instance.

* `set.finite_of_subtype` to prove `set.finite` for a `set` from a `finite` instance.

kmill · 2022-07-06T15:17:57Z

src/data/set/finite.lean

-/-- Constructor for `set.finite` with the `fintype` as an instance argument. -/
-theorem finite_of_fintype (s : set α) [h : fintype s] : s.finite := ⟨h⟩
+/-- Constructor for `set.finite` with the `finite` as an instance argument. -/
+theorem finite_of_subtype (s : set α) [h : finite s] : s.finite := ⟨h⟩


This name is passable, but I feel like set.finite_of_subtype isn't self-explanatory enough for such an important function. I had used set.finite_of_finite for this in the deleted src/data/finite/set.lean, but maybe set.mk_finite or set.to_finite instead?

src/data/finite/set.lean

kmill · 2022-07-06T15:38:30Z

src/data/finite/set.lean

-
-example {s : set α} [finite α] : finite s := infer_instance
-example : finite (∅ : set α) := infer_instance
-example (a : α) : finite ({a} : set α) := infer_instance


Could you please move these examples too? They're partly a sanity check and partly documentation to let mathlib users know what to expect should work.

Should they go to test/?

I'm more interested in the documentation part than the test part, which is why I had included them in this file in the first place. One thing they help with is that when you're refactoring they quickly answer the question of whether these instances exist. There are plenty of examples within mathlib that check instances like this, too.

kmill · 2022-07-06T15:44:36Z

src/data/set/finite.lean

+  finite (s \ t : set α) := finite.set.subset s (diff_subset s t)
+
+instance finite_range (f : ι → α) [finite ι] : finite (range f) :=
+by { haveI := fintype.of_finite (plift ι), apply_instance }


(I see why this moved up, but it'd make reviewing easier if proof simplifications, large-scale code motion, and file deletions weren't all happening all at the same time.)

AFAIR, when I started, this was still in data.finite.set. I'll try to split this PR tonight.

Right, it used to be in data.finite.set, but then the move got composed with a permutation.

I think splitting this PR into two will just cause more work for everyone with little benefit by this point. I was just complaining 😉

kmill · 2022-07-06T15:46:23Z

src/data/finite/set.lean

-begin
-  refine finite.of_injective (set.range_factorization f) (λ x y h, hf _),
-  simpa only [range_factorization_coe] using congr_arg (coe : range f → β) h,
-end


All four of these lemmas seem to have disappeared.

They were added after I created my branch. I'm not sure that we should duplicate lots of API about finite sets with [finite s] assumptions. I'm adding set.finite versions of these lemmas. In particular, function.injective.finite_range_iff works for a function from a Sort*.

The first three had been there since the beginning, but finite.of_injective_finite_range is new. The finite.set.finite_of_finite_image lemma has simpler hypotheses than the fintype version since it doesn't need to try to be computable.

I haven't thought too much about whether finite.of_injective_finite_range should exist, but I'm not comfortable deleting a lemma that had just been merged four days ago... At least we can delete it in a simpler PR.

I think that it should exist but it should take a set.finite argument, not a [finite _] argument.

kmill · 2022-07-06T15:55:17Z

src/data/set/finite.lean

-  by simpa [← @exists_finite_iff_finset α (λ t, t ⊆ a ∧ t = s), subset_to_finset_iff,
-    ← and.assoc] using h.subset⟩
+begin
+  convert (h.to_finset.powerset.map finset.coe_emb.1).finite_to_set using 1,


This is meant to be the application of the deleted set.finite.of_finset (from src/data/finite/set.lean)

urkud · 2022-07-06T18:16:03Z

I don't care about the name. Should we run a zulip poll? Or just let you choose one of these options?

kmill · 2022-07-06T18:27:36Z

Thinking about it more, set.to_finite reads well both as set.to_finite s and as s.to_finite. I'd be happy if we went with this, but if you want we can ask Zulip.

…ib into YK-set-finite-new

urkud added 4 commits June 26, 2022 19:58

Snapshot

fd3d480

Snapshot

74e9617

Merge branch 'master' into YK-set-finite-new

d7e82eb

Add Kyle Miller to authors

98f4927

urkud added the awaiting-review The author would like community review of the PR label Jun 28, 2022

Fix

3e42e24

kmill self-requested a review July 1, 2022 16:59

urkud added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jul 2, 2022

Merge branch 'master' into YK-set-finite-new

21adfea

urkud removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jul 2, 2022

urkud added 3 commits July 2, 2022 12:23

Fix aliases

52c5f17

Fix

ba10757

Fix

4f7026c

kmill approved these changes Jul 6, 2022

View reviewed changes

urkud added 2 commits July 6, 2022 22:29

Merge branch 'master' into YK-set-finite-new

936ce03

Follow some suggestions in the code review

d539784

urkud mentioned this pull request Jul 7, 2022

[Merged by Bors] - refactor(data/finite/set,data/set/finite): move most contents of one file to another #15166

Closed

Merge branch 'staging' of ssh://github.com/leanprover-community/mathl…

dbac582

…ib into YK-set-finite-new

urkud added WIP Work in progress and removed awaiting-review The author would like community review of the PR labels Jul 7, 2022

urkud closed this Nov 24, 2022

urkud deleted the YK-set-finite-new branch November 24, 2022 21:46

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

refactor(data/set/finite): use `finite` #15034

refactor(data/set/finite): use `finite` #15034

urkud commented Jun 28, 2022

kmill commented Jul 1, 2022

urkud commented Jul 1, 2022

kmill commented Jul 1, 2022

urkud commented Jul 1, 2022

urkud commented Jul 2, 2022

kmill left a comment

kmill Jul 6, 2022

kmill Jul 6, 2022

kmill Jul 6, 2022

urkud Jul 7, 2022

kmill Jul 7, 2022

kmill Jul 6, 2022

urkud Jul 7, 2022

kmill Jul 7, 2022

kmill Jul 6, 2022

urkud Jul 7, 2022

kmill Jul 7, 2022

urkud Jul 7, 2022

kmill Jul 6, 2022

urkud commented Jul 6, 2022

kmill commented Jul 6, 2022

	* `set.finite_of_subtype` to prove `set.finite` for a `set` from a `fintype` instance.
	* `set.finite_of_subtype` to prove `set.finite` for a `set` from a `finite` instance.

refactor(data/set/finite): use finite #15034

refactor(data/set/finite): use finite #15034

Conversation

urkud commented Jun 28, 2022

kmill commented Jul 1, 2022

urkud commented Jul 1, 2022

kmill commented Jul 1, 2022

urkud commented Jul 1, 2022

urkud commented Jul 2, 2022

kmill left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

urkud commented Jul 6, 2022

kmill commented Jul 6, 2022

refactor(data/set/finite): use `finite` #15034

refactor(data/set/finite): use `finite` #15034