-
Notifications
You must be signed in to change notification settings - Fork 331
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: more lemmas about List.dedup
and other lattice operations
#14282
Conversation
PR summary 179ad54926
|
File | Base Count | Head Count | Change |
---|---|---|---|
Mathlib.Data.List.Dedup | 324 | 325 | +1 (+0.31%) |
Import changes for all files
Files | Import difference |
---|---|
Mathlib.Data.List.Dedup |
1 |
Declarations diff
+ Disjoint.dedup_add
+ Disjoint.dedup_append
+ Disjoint.inter_eq_nil
+ Disjoint.ndinter_eq_zero
+ Disjoint.ndunion_eq
+ Disjoint.union_eq
+ Subset.dedup_add_left
+ Subset.dedup_add_right
+ Subset.dedup_append_right
+ Subset.inter_eq_left
+ Subset.ndinter_eq_left
+ Subset.ndunion_eq_right
+ Subset.union_eq_right
+ _root_.List.Subset.dedup_append_left
+ inter_nil'
++ _
++ dedup_map_of_injective
You can run this locally as follows
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>
## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>
@@ -132,6 +133,41 @@ theorem dedup_append (l₁ l₂ : List α) : dedup (l₁ ++ l₂) = l₁ ∪ ded | |||
· rw [dedup_cons_of_not_mem' h, insert_of_not_mem h] | |||
#align list.dedup_append List.dedup_append | |||
|
|||
theorem dedup_map_of_injective [DecidableEq β] {f : α → β} (hf : Function.Injective f) | |||
(xs : List α) : | |||
(xs.map f).dedup = xs.dedup.map f := by |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@Timeroot had this lemma somewhere. Did it ever land? What is the PR?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I assume we don't need to wait for an answer here? Of course, if @Timeroot comes along with a shorter proof after this is merged, we can always make a golf PR.
@@ -280,6 +289,12 @@ theorem ndinter_eq_zero_iff_disjoint {s t : Multiset α} : ndinter s t = 0 ↔ D | |||
rw [← subset_zero]; simp [subset_iff, Disjoint] | |||
#align multiset.ndinter_eq_zero_iff_disjoint Multiset.ndinter_eq_zero_iff_disjoint | |||
|
|||
alias ⟨_, Disjoint.ndinter_eq_zero⟩ := ndinter_eq_zero_iff_disjoint | |||
|
|||
theorem Subset.ndinter_eq_left {s t : Multiset α} (h : s ⊆ t) : s.ndinter t = s := by |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Same, can we have the right verSion?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't think the right version is meaningfully true? What statement do you want?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Ah indeed. But then this lemma is something like Multiset.filter_true_of_mem h
except that filter_true_of_mem
doesn't exist
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It exists for List
though; I golfed the proof there
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good now
maintainer merge
maintainer merge The conspiracy for bots to ignore Yael continues |
🚀 Pull request has been placed on the maintainer queue by eric-wieser. |
!bench |
I would guess the import change and the single simp are good but benched so I don't have to speculate. If it comes back reasonable, please merge. Thanks! bors delegate+ |
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
Here are the benchmark results for commit 179ad54. |
bors r+ |
…4282) Also the trivial `Multiset` wrappers.
Pull request successfully merged into master. Build succeeded: |
List.dedup
and other lattice operationsList.dedup
and other lattice operations
Also the trivial
Multiset
wrappers.