[Merged by Bors] - feat port: Data.Set.Lattice #1121

ChrisHughes24 · 2022-12-20T09:55:22Z

Mostly name changes. The proof of subset_bunionᵢ_of_mem needed a bunch of explicit arguments for some reason. I also moved the definition of set.sUnion from Init.Set into this file and changed its name. I also protected the definition of Set.compl

Mathlib/Data/Set/Lattice.lean

kbuzzard

A monumental effort! I approve modulo the things I flagged.

Mathlib/Data/Set/Lattice.lean

kbuzzard · 2022-12-20T15:08:25Z

Mathlib/Data/Set/Lattice.lean

+#align set.sInter Set.interₛ
+
+/-- Notation for `Set.interₛ` Intersection of a set of sets. -/
+prefix:110 "⋂₀ " => interₛ


Talking point: how about we change this to ⋂ₛ?

Makes sense, but maybe we do it after the port?

Part of me agrees, and part of me wants to say "well we just changed ten other things to use this little s and little i notation and I think it's really cool".

Mathlib/Data/Set/Lattice.lean

kbuzzard · 2022-12-20T16:54:50Z

Mathlib/Data/Set/Lattice.lean

+  hf.infᵢ_nat_add k
+#align antitone.Inter_nat_add Antitone.interᵢ_nat_add
+
+--Porting note: removing `simp`. LHS does not simplify


I'm confused about this one.

example (f : ℕ → Set α) (k : ℕ) : (⋃ n, ⋂ i ≥ n, f (i + k)) = ⋃ n, ⋂ i ≥ n, f i := by simp

works fine if unionᵢ_interᵢ_ge_nat_add is tagged @[simp] and doesn't work otherwise. Is this a bug in the linter? Are we sure this shouldn't be tagged @[simp]?

I added a link to the Zulip discussion https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/complete_lattice.20and.20has_sup/near/316497982

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

changes made

eric-wieser · 2022-12-21T16:38:14Z

This will conflict with @negiizhao's #1109, for which leanprover-community/mathlib#17882 is on the queue

negiizhao · 2022-12-21T17:16:03Z

I believe this just needs to remove some lemmas in Data.Set.Lattice.

eric-wieser · 2022-12-21T17:20:24Z

That sounds like an argument in favor of merging #1109 first?

negiizhao · 2022-12-21T17:41:59Z

Both are easy to deal with. To ensure that no more lemmas are removed by mistake, it might be better to merge #1121 first (then we can compare the diffs).

jcommelin · 2022-12-22T16:46:52Z

Let's merge this. Then we can move forward with #1109.
If @kbuzzard's question needs to be addressed, then that can be done in a future PR.

bors merge

Mostly name changes. The proof of `subset_bunionᵢ_of_mem` needed a bunch of explicit arguments for some reason. I also moved the definition of `set.sUnion` from `Init.Set` into this file and changed its name. I also `protected` the definition of `Set.compl` Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

bors · 2022-12-22T17:18:02Z

Pull request successfully merged into master.

Build succeeded:

Fixes some doc comment typos added added in #1121. Note that the `sUnion` comment is correct is mathlib3: https://github.com/leanprover-community/mathlib/blob/b76e9f654df09f8a832aeee712511fe5f3e57869/src/data/set/lattice.lean#L72-L74

initial commit

10b8724

ChrisHughes24 added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Dec 20, 2022

ChrisHughes24 added 12 commits December 20, 2022 10:08

start fixing

ecfb5d1

more fixes

9d4ef61

some search and replace

78912e8

more find and replace

2918bcc

more search and replace

72aa99f

more search and replace

dd706cb

more fixing

17c07be

nearly fixed build

4eb386e

protect compl

c94ab53

more fixes

b852961

no more red or yellow

c3afef8

linting

3f690ca

ChrisHughes24 added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Dec 20, 2022

ChrisHughes24 added 3 commits December 20, 2022 13:58

line length

cef1c87

comments

33b13e9

very minor tidy up

f84b34b

Ruben-VandeVelde previously requested changes Dec 20, 2022

View reviewed changes

kbuzzard approved these changes Dec 20, 2022

View reviewed changes

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

ChrisHughes24 and others added 6 commits December 21, 2022 09:53

Apply suggestions from code review

3bc6510

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

Apply suggestions from code review

089351a

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

Apply suggestions from code review

c879321

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

Apply suggestions from code review

7ba8cea

Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

Apply suggestions from code review

9754a84

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

maps_to -> mapsTo

5d7bb31

ChrisHughes24 added 3 commits December 21, 2022 10:05

minor changes

c73bc81

Remove old TODOs

f073c03

add link to Zulip

15920c5

ChrisHughes24 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 Dec 21, 2022

ChrisHughes24 added 2 commits December 21, 2022 10:45

newline

c7e9dba

restore docstrings

d138111

eric-wieser mentioned this pull request Dec 21, 2022

[Merged by Bors] - chore(data/set/lattice): move basic lemmas to basic files leanprover-community/mathlib#17882

Closed

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Dec 22, 2022

bors bot changed the title ~~feat port: Data.Set.Lattice~~ [Merged by Bors] - feat port: Data.Set.Lattice Dec 22, 2022

bors bot closed this Dec 22, 2022

bors bot deleted the Data.Set.Lattice branch December 22, 2022 17:18

github-actions bot mentioned this pull request Dec 23, 2022

[Merged by Bors] - chore(*): add mathlib4 synchronization comments leanprover-community/mathlib#17979

Closed

dwrensha mentioned this pull request May 16, 2023

[Merged by Bors] - fix: sUnion doc comment typos #4039

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat port: Data.Set.Lattice #1121

[Merged by Bors] - feat port: Data.Set.Lattice #1121

ChrisHughes24 commented Dec 20, 2022 •

edited

kbuzzard left a comment

kbuzzard Dec 20, 2022

jcommelin Dec 21, 2022

kbuzzard Dec 21, 2022

kbuzzard Dec 20, 2022

ChrisHughes24 Dec 21, 2022

eric-wieser commented Dec 21, 2022 •

edited

negiizhao commented Dec 21, 2022

eric-wieser commented Dec 21, 2022

negiizhao commented Dec 21, 2022

jcommelin commented Dec 22, 2022

bors bot commented Dec 22, 2022

[Merged by Bors] - feat port: Data.Set.Lattice #1121

[Merged by Bors] - feat port: Data.Set.Lattice #1121

Conversation

ChrisHughes24 commented Dec 20, 2022 • edited

kbuzzard left a comment

Choose a reason for hiding this comment

kbuzzard Dec 20, 2022

Choose a reason for hiding this comment

jcommelin Dec 21, 2022

Choose a reason for hiding this comment

kbuzzard Dec 21, 2022

Choose a reason for hiding this comment

kbuzzard Dec 20, 2022

Choose a reason for hiding this comment

ChrisHughes24 Dec 21, 2022

Choose a reason for hiding this comment

eric-wieser commented Dec 21, 2022 • edited

negiizhao commented Dec 21, 2022

eric-wieser commented Dec 21, 2022

negiizhao commented Dec 21, 2022

jcommelin commented Dec 22, 2022

bors bot commented Dec 22, 2022

ChrisHughes24 commented Dec 20, 2022 •

edited

eric-wieser commented Dec 21, 2022 •

edited