feat(data/[fin]set): add some more basic properties of (finite) sets by fpvandoorn · Pull Request #905 · leanprover-community/mathlib3

fpvandoorn · 2019-04-08T19:07:35Z

Part 2: (fin)sets

TO CONTRIBUTORS:

Make sure you have:

reviewed and applied the coding style: coding, naming
make sure definitions and lemmas are put in the right files
make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

jcommelin · 2019-04-08T19:28:06Z

src/data/finset.lean

 @[simp] lemma coe_sdiff (s₁ s₂ : finset α) : ↑(s₁ \ s₂) = (↑s₁ \ ↑s₂ : set α) :=
 set.ext $ λ _, mem_sdiff

+lemma to_set_sdiff (s t : finset α) : (s \ t).to_set = s.to_set \ t.to_set :=


Is this a simp-lemma?

About finset-simp lemmas: I don't see a simp lemma rewriting s.to_set to (↑s : set _) or the other way around, so I'm not sure what the "canonical form" of this function is. If it's ↑s, then this simp lemma is superfluous (I don't know if that is a problem at all).

@digama0 Is there a general mathlib preference here?

I've never heard of s.to_set before this (and I wrote it). It's definitely written ↑s everywhere.

jcommelin · 2019-04-08T19:29:14Z

src/data/set/basic.lean

+lemma compl_empty_iff {s : set α} : -s = ∅ ↔ s = univ :=
+by { split, intro h, rw [←compl_compl s, h, compl_empty], intro h, rw [h, compl_univ] }
+
+lemma compl_univ_iff {s : set α} : -s = ∅ ↔ s = univ :=


This one is identical to the previous one. Which is not what you intended... I guess

He probably meant -s = empty iff s = univ. I think both of these should be @[simp]

The name suggests: -s = univ ↔ s = ∅

oops, copy-paste without actually changing the statement. Yes, Johannes wrote the statement I had in mind.

jcommelin · 2019-04-08T19:30:08Z

src/data/set/basic.lean

+lemma compl_univ_iff {s : set α} : -s = ∅ ↔ s = univ :=
+by { split, intro h, rw [←compl_compl s, h, compl_empty], intro h, rw [h, compl_univ] }
+
+lemma nonempty_compl {s : set α} : s ≠ univ ↔ nonempty (-s : set α) :=


Given the name, I would expect the sides of the iff to be swapped.

jcommelin · 2019-04-08T19:31:38Z

src/data/set/basic.lean

  set.range (@subtype.val _ p) = {x | p x} :=
 by rw ← set.image_univ; simp [-set.image_univ, val_image]
+
+lemma range_val (s : set α) : range (subtype.val : s → α) = s :=


simp-lemma?

avigad

The PR looks good, but I'd like a bit of discussion on the nonempty question, because it will come up a lot in proofs.

avigad · 2019-04-10T15:17:47Z

src/data/finset.lean


 @[simp] lemma coe_empty : ↑(∅ : finset α) = (∅ : set α) := rfl

+lemma coe_nonempty_iff_ne_empty (s : finset α) : nonempty (↑s : set α) ↔ s ≠ ∅  :=


Here is a general question: should the library favor nonempty (↑s : set α) or s ≠ ∅? The library should be consistent about using one or the other to state theorems. The second seems more natural and useful to me. If we go with that, then this should be a simplifier rule. If we go the other way, we should probably simplify the second to the first.

Either way, this lemma should be named nonempty_iff_ne_empty or nonempty_coe_iff_ne_empty. With the current name, it will be very hard to find using tab completion.

@ChrisHughes24 @jcommelin @johoelzl I am curious to hear your thoughts on this.

I think the second looks nicer. Otoh, nonempty is a class, which might allow the type class system to take care of some proof obligations.

The second looks more natural, but is less useful in practice. I noticed that in my proofs I preferred the nonempty, because I can immediately extract an element from that with cases. But I'm ok with using s ≠ ∅ as default since that is mathematically more accepted.

I used this name to be consistent with set.coe_nonempty_iff_ne_empty in set.basic. I would personally also name it nonempty_iff_ne_empty.

The ability to uses cases with nonempty is compelling to me, so I am happy to make that the canonical idiom if nobody objects. In that case, we should try (at least over time) to state theorems that way, and also in set.

But I really do think it is better to have the name start with nonempty, also for the one in set.

The general mathlib preference is for the s ≠ ∅ idiom, although I can see the advantage of an inductive predicate so that you can use cases directly. It's still not that much better since you have to case twice; the additional coercion in the middle makes it less desirable since that makes it internally more complicated. I agree that we should use ne_empty and nonempty consistently to mean s ≠ ∅ and nonempty s respectively, though.

Also, I think nonempty s reads quite naturally. I can't imagine many mathematicians stumbling over that... (-;

avigad · 2019-04-10T15:21:31Z

src/data/set/basic.lean


 @[simp] lemma diff_self {s : set α} : s \ s = ∅ := ext $ by simp

+lemma mem_diff_singleton_empty {s : set α} {t : set (set α)} :


Do we really need this? This is essentially just a combination of mem_diff and mem_singleton_iff.

I don't know. I definitely wanted it for my specific use-case, since I needed it multiple (10?) times. But maybe mathlib is not the place for "combined" facts like this. I will remove it.

If you needed it 10 times, I think it's legit to keep it. In my eyes >80% of formalisation libraries consist of little lemmas that are "essentially just a combination"... (not being sarcastic).

I would suggest generalizing to s \in t \ {a} <-> s \in t /\ s != a, assuming the situation with ne_zero vs nonempty is resolved.

digama0 · 2019-04-11T06:01:09Z

src/data/set/finite.lean

+lemma finite.coe_to_finset {α} {s : set α} (h : finite s) : ↑h.to_finset = s :=
+by { ext, apply mem_to_finset }
+
+lemma exists_finset_of_finite {s : set α} (h : finite s) : ∃(s' : finset α), s'.to_set = s :=


this should use coercion instead of to_set

digama0 · 2019-04-11T06:05:48Z

src/data/set/basic.lean

 λ x xs y ys h, H _ _ (hp x xs y ys h)

+/- Disjoint sets and pairwise disjoint collections of sets -/
+lemma disjoint_of_subset {s t s' t' : set α} (hst : s ∩ t = ∅) (hs : s' ⊆ s) (ht : t' ⊆ t) :


There is already a definition of disjoint (and pairwise disjoint) in data.set.lattice, which is preferred over this one. Could you move / merge these lemmas?

fpvandoorn · 2019-04-18T21:30:52Z

Superseded by #948

feat(data/[fin]set): add some more basic properties of (finite) sets

81f8a7b

fpvandoorn requested a review from a team as a code owner April 8, 2019 19:07

jcommelin reviewed Apr 8, 2019

View reviewed changes

avigad reviewed Apr 10, 2019

View reviewed changes

digama0 reviewed Apr 11, 2019

View reviewed changes

cipher1024 assigned digama0 Apr 12, 2019

fpvandoorn mentioned this pull request Apr 18, 2019

feat(data/[fin]set): add some more basic properties of (finite) sets #948

Merged

fpvandoorn closed this Apr 18, 2019


		@[simp] lemma coe_empty : ↑(∅ : finset α) = (∅ : set α) := rfl

		lemma coe_nonempty_iff_ne_empty (s : finset α) : nonempty (↑s : set α) ↔ s ≠ ∅ :=


		@[simp] lemma diff_self {s : set α} : s \ s = ∅ := ext $ by simp

		lemma mem_diff_singleton_empty {s : set α} {t : set (set α)} :

Conversation

fpvandoorn commented Apr 8, 2019

Uh oh!

Choose a reason for hiding this comment

Uh oh!

fpvandoorn Apr 10, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

avigad left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

digama0 Apr 11, 2019 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

fpvandoorn commented Apr 18, 2019

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

fpvandoorn Apr 10, 2019 •

edited

Loading

digama0 Apr 11, 2019 •

edited

Loading