[Merged by Bors] - refactor(data/set/finite): reorganize and put emphasis on fintype instances #14136

kmill · 2022-05-14T02:22:36Z

I went through data/set/finite and reorganized it by rough topic (and moved some lemmas to their proper homes; closes #11177). Two important parts of this module are (1) fintype instances for various set constructions and (2) ways to create set.finite terms. This change puts the module closer to following a design where the set.finite terms are created in a formulaic way from the fintype instances. One tool for this is a set.finite_of_fintype constructor, which lets typeclass inference do most of the work.

Included in this commit is changing set.infinite to be protected so that it does not conflict with infinite.

archive/100-theorems-list/83_friendship_graphs.lean

kim-em · 2022-05-14T22:56:08Z

src/combinatorics/configuration.lean

  have h2 : ∀ l : {l : L // p ∈ l}, fintype.card {q // q ∈ l.1 ∧ q ≠ p} = order P L,
  { intro l,
    rw [←fintype.card_congr (equiv.subtype_subtype_equiv_subtype_inter _ _),
        fintype.card_subtype_compl, ←nat.card_eq_fintype_card],
+    any_goals { apply_instance },


Similarly what happened here?

This one is because I changed card_subtype_compl from

lemma fintype.card_subtype_compl [fintype α] {p : α → Prop} [decidable_pred p] : fintype.card {x // ¬ p x} = fintype.card α - fintype.card {x // p x} :=

to

lemma fintype.card_subtype_compl [fintype α] (p : α → Prop) [fintype {x // p x}] [fintype {x // ¬ p x}] : fintype.card {x // ¬ p x} = fintype.card α - fintype.card {x // p x}

and the rewrite is somehow not able to find the third fintype instance. If you give it the predicate directly, then it works fine. In the commit I pushed, I modified it to give the predicate directly.

I'm not sure what the best thing to do here is, and I don't really understand what's causing the instance lookup failure... (Maybe it's ne vs not-equals in whatever p it infers?)

into kmill_set_finite

src/data/set/basic.lean

into kmill_set_finite

b-mehta

I'll take it on trust that the lemmas in data/set/finite have moved and none have been lost, otherwise LGTM!

src/data/fintype/basic.lean

Co-authored-by: Bhavik Mehta <[email protected]>

kmill · 2022-05-22T00:11:17Z

@b-mehta Methodologically, I did copy/paste to put things into order, so nothing should be lost (and thankfully I haven't had to do a complicated merge so far). There's also a metaproof that nothing has gone missing: mathlib still compiles, and nobody adds anything to data/set/finite unless it's for something else!

kmill · 2022-05-22T01:07:52Z

I had been planning on making set.finite protected, but I guess that can't be done for inductive definitions. It seems like having set.infinite be protected is better than not (since Lean can't disambiguate between infinite and set.infinite on its own), but it's unfortunate that there's this inconsistency between set.finite and set.infinite.

src/data/fintype/basic.lean

b-mehta · 2022-05-22T23:12:48Z

src/data/fintype/basic.lean

+  [fintype s] [fintype t] : (s ∩ t).to_finset = s.to_finset ∩ t.to_finset :=
+by { ext, simp }
+
+lemma to_finset_union {α : Type*} [decidable_eq α] (s t : set α) [fintype (s ∪ t : set α)]


What's the reason for some of these to be simp and not others?

I'm not sure, this is how they were, and I didn't want to see if mathlib would compile with them as simp lemmas.

b-mehta · 2022-05-22T23:14:06Z

src/data/set/finite.lean

-      exact m }
-  end
-end
+/-- A `fintype` structure on `insert a s` when inserting a new element. -/


Can we reference fintype_insert in this docstring (and the next), and also vice-versa?

I'll do that in a followup PR

b-mehta · 2022-05-22T23:15:13Z

src/data/set/finite.lean

-fintype.card_of_subsingleton _
+/-- Normally, `insert a s` for `finset` requires `[decidable_eq α]`, but we can use this weaker
+assumption here. -/
+instance fintype_insert' (a : α) (s : set α) [decidable $ a ∈ s] [fintype s] :


Having this instance as well as the previous seems a bit odd to me, but can we reference the other?

This is from the original fintype_insert, which derives decidable membership from decidable equality and chooses one of the two fintype instances based on that decision. The new fintype_insert just uses the finset insert, which makes it more like instances for other set operations -- having looked at the history, it looks like the reason for this is that the original set.finite was a custom inductive type that made no use of finset. I let the original fintype_insert hang around in this form since it might still be useful.

eric-wieser · 2022-05-23T07:00:20Z

src/data/fintype/basic.lean

+  classical,
+  rw [fintype.card_of_subtype (set.to_finset pᶜ), set.to_finset_compl p, finset.card_compl,
+      fintype.card_of_subtype (set.to_finset p)];
+  intros; simp; refl


Are we missing a simp lemma?

This is code that had previously been through review, but I went ahead and fixed the non-terminal simp.

What's going on is that this proof is that p is not a set but the rewrites are using it as if it were one. In a quick test, set_of p doesn't fix it.

src/topology/metric_space/closeds.lean

eric-wieser · 2022-05-23T07:03:59Z

src/data/set/finite.lean

 inductive finite (s : set α) : Prop
 | intro : fintype s → finite

-lemma finite_def {s : set α} : finite s ↔ nonempty (fintype s) := ⟨λ ⟨h⟩, ⟨h⟩, λ ⟨h⟩, ⟨h⟩⟩
+/-- Constructor for `set.finite` with the `fintype` as an instance argument. -/


Can you make intro be this with something like

inductive finite (s : set α) : Prop | of_fintype [fintype s] : finite

Or is that annoying?

I'd found writing finite_def awkward that way, so I figured I'd leave it as Yury wrote it.

jcommelin · 2022-05-23T12:12:45Z

Thanks 🎉

bors merge

…tances (#14136) I went through `data/set/finite` and reorganized it by rough topic (and moved some lemmas to their proper homes; closes #11177). Two important parts of this module are (1) `fintype` instances for various set constructions and (2) ways to create `set.finite` terms. This change puts the module closer to following a design where the `set.finite` terms are created in a formulaic way from the `fintype` instances. One tool for this is a `set.finite_of_fintype` constructor, which lets typeclass inference do most of the work. Included in this commit is changing `set.infinite` to be protected so that it does not conflict with `infinite`.

bors · 2022-05-23T14:09:25Z

Pull request successfully merged into master.

Build succeeded:

This follows up with some review comments for #14136.

…14363) This follows up with some review comments for #14136.

…4468) This lemma was added in #11371 for the Lean version bump, since the more powerful congr lemmas revealed a bug in fintype instances that were finally corrected in #14136.

kmill added 4 commits May 13, 2022 18:18

reorganized data/set/finite

5835bcf

walk back some name changes

0c3ecf3

change import

a4693f5

walk back a couple more name changes

2e5e43a

kmill added the awaiting-author A reviewer has asked the author a question or requested changes label May 14, 2022

kmill added 16 commits May 13, 2022 19:24

walk back another name change

b76df6d

lint

eae560a

fix infinite

d8ffb5a

additional arg

41e6bd9

fixes

b572e0b

another fix

8774203

fix

ec15466

extract to_finset lemmas

feed464

dot notation

4b25d90

move more lemmas

84ba4e1

fix

ab44747

fix

b69ec3e

fix

ad7e533

fix

cdcf54b

revert change to finite.dependent_image

023cfa5

fix

5799e88

kmill added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels May 14, 2022

kim-em reviewed May 14, 2022

View reviewed changes

archive/100-theorems-list/83_friendship_graphs.lean Outdated Show resolved Hide resolved

kim-em reviewed May 14, 2022

View reviewed changes

kmill added 5 commits May 14, 2022 23:32

clean?

000351e

found old bug in fintype inter instances

494939c

Merge branch 'master' of https://github.com/leanprover-community/mathlib

5e3d59b

into kmill_set_finite

rename set.finite.intro' to set.to_finite

5409e54

rename to set.mk_finite

c2078a1

b-mehta reviewed May 20, 2022

View reviewed changes

src/data/set/basic.lean Outdated Show resolved Hide resolved

kmill added 4 commits May 20, 2022 16:23

b-mehta review

6c2898a

remove nonempty_congr

9c12a57

Merge branch 'master' of https://github.com/leanprover-community/mathlib

3854af7

into kmill_set_finite

Merge branch 'master' of https://github.com/leanprover-community/mathlib

aaeac4c

into kmill_set_finite

b-mehta approved these changes May 21, 2022

View reviewed changes

src/data/fintype/basic.lean Outdated Show resolved Hide resolved

formatting

1e3c1a8

Co-authored-by: Bhavik Mehta <[email protected]>

kmill commented May 22, 2022

View reviewed changes

src/data/fintype/basic.lean Outdated Show resolved Hide resolved

formatting

0497014

b-mehta approved these changes May 22, 2022

View reviewed changes

eric-wieser reviewed May 23, 2022

View reviewed changes

src/topology/metric_space/closeds.lean Outdated Show resolved Hide resolved

eric-wieser reviewed May 23, 2022

View reviewed changes

from eric-wieser review

a68b38d

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels May 23, 2022

bors bot changed the title ~~refactor(data/set/finite): reorganize and put emphasis on fintype instances~~ [Merged by Bors] - refactor(data/set/finite): reorganize and put emphasis on fintype instances May 23, 2022

bors bot closed this May 23, 2022

bors bot deleted the kmill_set_finite branch May 23, 2022 14:09

kmill mentioned this pull request May 23, 2022

[Merged by Bors] - refactor(data/set/finite): protect set.finite #14344

Closed

kmill added a commit that referenced this pull request May 24, 2022

feat(data/set/finite): set priority for fintype_insert' and document

0cb126c

This follows up with some review comments for #14136.

kmill mentioned this pull request May 24, 2022

[Merged by Bors] - feat(data/set/finite): set priority for fintype_insert' and document #14363

Closed

bors bot pushed a commit that referenced this pull request May 25, 2022

feat(data/set/finite): set priority for fintype_insert' and document (#…

c1e2121

…14363) This follows up with some review comments for #14136.

kmill mentioned this pull request May 30, 2022

[Merged by Bors] - chore(combinatorics/simple_graph/basic): remove unnecessary lemma #14468

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(data/set/finite): reorganize and put emphasis on fintype instances #14136

[Merged by Bors] - refactor(data/set/finite): reorganize and put emphasis on fintype instances #14136

kmill commented May 14, 2022 •

edited

Loading

kim-em May 14, 2022

kmill May 14, 2022 •

edited

Loading

b-mehta left a comment

kmill commented May 22, 2022

kmill commented May 22, 2022

b-mehta May 22, 2022

kmill May 22, 2022

b-mehta May 22, 2022

kmill May 22, 2022

b-mehta May 22, 2022

kmill May 22, 2022

eric-wieser May 23, 2022

kmill May 23, 2022

eric-wieser May 23, 2022

kmill May 23, 2022

jcommelin commented May 23, 2022

bors bot commented May 23, 2022

[Merged by Bors] - refactor(data/set/finite): reorganize and put emphasis on fintype instances #14136

[Merged by Bors] - refactor(data/set/finite): reorganize and put emphasis on fintype instances #14136

Conversation

kmill commented May 14, 2022 • edited Loading

Choose a reason for hiding this comment

kmill May 14, 2022 • edited Loading

Choose a reason for hiding this comment

b-mehta left a comment

Choose a reason for hiding this comment

kmill commented May 22, 2022

kmill commented May 22, 2022

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

jcommelin commented May 23, 2022

bors bot commented May 23, 2022

kmill commented May 14, 2022 •

edited

Loading

kmill May 14, 2022 •

edited

Loading