Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(data/finset/basic): insert and erase lemmas#18729

Closed
YaelDillies wants to merge 6 commits intomasterfrom
disjoint_erase_comm
Closed

[Merged by Bors] - feat(data/finset/basic): insert and erase lemmas#18729
YaelDillies wants to merge 6 commits intomasterfrom
disjoint_erase_comm

Conversation

@YaelDillies
Copy link
Copy Markdown
Collaborator

@YaelDillies YaelDillies commented Apr 4, 2023

Interaction of insert and erase with inter, union and disjoint.

Open in Gitpod

@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. labels Apr 4, 2023
@YaelDillies YaelDillies mentioned this pull request Apr 4, 2023
Closed
1 task
@alexjbest
Copy link
Copy Markdown
Member

alexjbest commented Apr 5, 2023

Are the corresponding lemmas already there for set? (do we try to keep the APIs there in sync or not?)

@YaelDillies
Copy link
Copy Markdown
Collaborator Author

YaelDillies commented Apr 5, 2023

There's no set.erase, so the erase lemmas are usually covered by either a more general set lemma about diff or even by the boolean algebra API. The other ones I've done my best to align, but it's really hard because the two files are very much not aligned overall. In doing so, I found I was introducing some duplicates, so you might want to be on the lookout.

@alexjbest
Copy link
Copy Markdown
Member

alexjbest commented Apr 5, 2023

If only someone had a linter for that...
I will try and find my duplicate linter branch, it might be high time for a run of it.

eric-wieser
eric-wieser reviewed Apr 18, 2023
View reviewed changes
src/data/finset/basic.lean
Comment on lines +1475 to +1479
lemma erase_sdiff_comm (s t : finset α) (a : α) : s.erase a \ t = (s \ t).erase a :=
by simp_rw [erase_eq, sdiff_right_comm]

lemma insert_union_comm (s t : finset α) (a : α) : insert a s ∪ t = s ∪ insert a t :=
by rw [insert_union, union_insert]
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser Apr 18, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

comm seems to mean bin (unary x) y = unary (bin x y) in the first name but bin (unary x) y = bin x (unary y) in the second one, Calling the first one erase_sdiff would ease this a little.

Copy link
Copy Markdown
Collaborator Author

@YaelDillies YaelDillies Apr 18, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If you consider both insert and erase to be binary, they're respectively

  • bin1 (bin2 s a) t = bin2 (bin1 s t) a
  • bin1 (bin2 a s) t = bin1 s (bin2 a t)

so the first one is clearly right commutativity, but the second one isn't clearly anything.

@ericrbg
Copy link
Copy Markdown
Collaborator

ericrbg commented Apr 18, 2023

(I merged master to try fix the bibtool error)

@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Apr 19, 2023

@alexjbest, did you want to take a final look?

@alexjbest
Copy link
Copy Markdown
Member

alexjbest commented Apr 19, 2023

@eric-wieser nothing more from me I think

@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Apr 19, 2023

bors d+

Thanks!

@bors
Copy link
Copy Markdown

bors bot commented Apr 19, 2023

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Apr 19, 2023
@YaelDillies
Copy link
Copy Markdown
Collaborator Author

YaelDillies commented Apr 19, 2023

Looks like building is alright, so

bors merge

bors bot pushed a commit that referenced this pull request Apr 19, 2023
@YaelDillies @ericrbg
feat(data/finset/basic): insert and erase lemmas (#18729)
9ac7c0c 
Interaction of `insert` and `erase` with `inter`, `union` and `disjoint`.



Co-authored-by: Eric Rodriguez <ericrboidi@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Apr 20, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/finset/basic): insert and erase lemmas [Merged by Bors] - feat(data/finset/basic): insert and erase lemmas Apr 20, 2023
@bors bors bot closed this Apr 20, 2023
@bors bors bot deleted the disjoint_erase_comm branch April 20, 2023 02:32
@YaelDillies YaelDillies mentioned this pull request Apr 21, 2023
Closed
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Apr 24, 2023
@YaelDillies
feat: insert and erase lemmas (#3569)
0437079 
Match leanprover-community/mathlib3#18729

* [`order.heyting.basic`@`4e42a9d0a79d151ee359c270e498b1a00cc6fa4e`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/order/heyting/basic?range=4e42a9d0a79d151ee359c270e498b1a00cc6fa4e..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`order.boolean_algebra`@`bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/order/boolean_algebra?range=bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`data.set.basic`@`29cb56a7b35f72758b05a30490e1f10bd62c35c1`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/data/set/basic?range=29cb56a7b35f72758b05a30490e1f10bd62c35c1..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`data.finset.basic`@`68cc421841f2ebb8ad2b5a35a853895feb4b850a`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/data/finset/basic?range=68cc421841f2ebb8ad2b5a35a853895feb4b850a..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
kim-em pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 10, 2023
@YaelDillies
feat: insert and erase lemmas (#3569)
fe76a1b 
Match leanprover-community/mathlib3#18729

* [`order.heyting.basic`@`4e42a9d0a79d151ee359c270e498b1a00cc6fa4e`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/order/heyting/basic?range=4e42a9d0a79d151ee359c270e498b1a00cc6fa4e..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`order.boolean_algebra`@`bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/order/boolean_algebra?range=bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`data.set.basic`@`29cb56a7b35f72758b05a30490e1f10bd62c35c1`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/data/set/basic?range=29cb56a7b35f72758b05a30490e1f10bd62c35c1..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`data.finset.basic`@`68cc421841f2ebb8ad2b5a35a853895feb4b850a`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/data/finset/basic?range=68cc421841f2ebb8ad2b5a35a853895feb4b850a..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
hrmacbeth pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 10, 2023
@YaelDillies @hrmacbeth
feat: insert and erase lemmas (#3569)
4cf99fa 
Match leanprover-community/mathlib3#18729

* [`order.heyting.basic`@`4e42a9d0a79d151ee359c270e498b1a00cc6fa4e`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/order/heyting/basic?range=4e42a9d0a79d151ee359c270e498b1a00cc6fa4e..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`order.boolean_algebra`@`bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/order/boolean_algebra?range=bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`data.set.basic`@`29cb56a7b35f72758b05a30490e1f10bd62c35c1`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/data/set/basic?range=29cb56a7b35f72758b05a30490e1f10bd62c35c1..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`data.finset.basic`@`68cc421841f2ebb8ad2b5a35a853895feb4b850a`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/data/finset/basic?range=68cc421841f2ebb8ad2b5a35a853895feb4b850a..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
hrmacbeth pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 11, 2023
@YaelDillies @hrmacbeth
feat: insert and erase lemmas (#3569)
fc7620f 
Match leanprover-community/mathlib3#18729

* [`order.heyting.basic`@`4e42a9d0a79d151ee359c270e498b1a00cc6fa4e`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/order/heyting/basic?range=4e42a9d0a79d151ee359c270e498b1a00cc6fa4e..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`order.boolean_algebra`@`bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/order/boolean_algebra?range=bc7d81beddb3d6c66f71449c5bc76c38cb77cf9e..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`data.set.basic`@`29cb56a7b35f72758b05a30490e1f10bd62c35c1`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/data/set/basic?range=29cb56a7b35f72758b05a30490e1f10bd62c35c1..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
* [`data.finset.basic`@`68cc421841f2ebb8ad2b5a35a853895feb4b850a`..`9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4`](https://leanprover-community.github.io/mathlib-port-status/file/data/finset/basic?range=68cc421841f2ebb8ad2b5a35a853895feb4b850a..9ac7c0c8c4d7a535ec3e5b34b8859aab9233b2f4)
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

1 more reviewer

@eric-wieser eric-wieser eric-wieser left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

delegated The PR author may merge after reviewing final suggestions. modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@YaelDillies @alexjbest @ericrbg @eric-wieser