feat(Data/Finset & List): Add Lemmas for Sorting and Filtering #9605

davikrehalt · 2024-01-10T03:55:03Z

This PR includes several useful lemmas to the Data/Finset and Data/List modules in Lean's mathlib:

toFinset_filter (List): Shows that filtering commutes with toFinset.
toFinset_is_singleton_implies_replicate (List): Shows a list with a singleton toFinset is a List.replicate.
filter_sort_commute (Finset): Sorting and filtering can be interchanged in Finsets.
Sorted.filter (List): A sorted list stays sorted after filtering.
Sorted.append_largest (List): Appending the largest element keeps a list sorted.
sort_monotone_map (Finset): Relates sorting of a Finset after mapping to sorting of a list.
sort_insert_largest (Finset): Sorting a Finset with an inserted largest element.
sort_range (Finset): Sorting a range in a Finset equals the corresponding range list.
~~filter_eval_true (List): Filtering a list with a predicate always true keeps the list unchanged.~~
~~filter_eval_false (List): Filtering with an always-false predicate gives an empty list.~~
~~pairwise_concat (List): Iff condition for Pairwise relation in concatenated lists (similar to pairwise_join).~~
list_map_toFinset (Finset): toFinset commutes with map under injection

depends on: [Merged by Bors] - feat: interactions between List.map and sorting lists #15952

This is my first PR to mathlib, so I'm not too familiar with etiquette's and more specifically there are two proofs in the PR which uses aesop, and I am not sure if it's frowned upon. I kept the aesop in there for now as I couldn't construct very short proofs otherwise. The sort_range function proof was suggested in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Computing.20Finset.20sort.20of.20Finset.20range/near/410346731 by Ruben Van de Velde. Thanks for your time for improving this PR.

…re idiomatically, probably should be rewritten somehow)

…lists, not sure if it's necessary

…Sort which addresses how sorted list changes upon adding an element larger than all

…_replicate

Mathlib/Data/List/Basic.lean

remove space Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

…o list_lemma_davik merge to current state

…thlib4 into list_lemma_davik update to current state

…o list_lemma_davik current state

Mathlib/Data/Finset/Image.lean

urkud · 2024-01-22T17:15:40Z

Please remove extra indentation inside the list in the PR description and use backticks for identifiers.

urkud · 2024-01-22T17:18:02Z

Mathlib/Data/Finset/Basic.lean

+    rw [toFinset_filter f]
+
+theorem toFinset_is_singleton_implies_replicate {l : List α} {a : α}
+    (h : l.toFinset ⊆ {a}) : l = List.replicate l.length a := by


This lemma follows immediately from List.eq_replicate_of_mem.

(and therefore should be removed?)

Please remove this lemma

urkud · 2024-01-22T17:21:29Z

Mathlib/Data/List/Sort.lean

@@ -157,6 +157,27 @@ theorem Sorted.rel_of_mem_take_of_mem_drop {l : List α} (h : List.Sorted r l) {
  exact h.rel_nthLe_of_lt _ _ (Nat.lt_add_right _ (lt_min_iff.mp hix).left)
 #align list.sorted.rel_of_mem_take_of_mem_drop List.Sorted.rel_of_mem_take_of_mem_drop

+theorem Sorted.filter {l : List α} (f : α → Bool) (h : Sorted r l) :
+    Sorted r (filter f l) := by


This follows from more general facts:

(~~not yet in Mathlib~~ defeq to List.Pairwise.sublist) a sublist of a sorted list is sorted;

filter f l is a sublist of l, see List.filter_sublist.

Please ~~add the first fact and~~ use it to get your lemma. Also, this lemma should be protected.

I've moved this to #18466

urkud · 2024-01-22T17:28:23Z

Mathlib/Data/List/Sort.lean

+    exact Sorted.filter f (Sorted.of_cons h)
+
+theorem Sorted.append_largest {a : α} {l : List α} :
+    Sorted r (l ++ [a]) ↔ (∀ b ∈ l, r b a) ∧ Sorted r l := by


We have List.concat in Lean core. Should it be protected theorem Sorted.concat?

Please apply this

Mathlib/Data/List/Pairwise.lean

github-actions · 2024-06-30T23:20:33Z

PR summary 9f72d47cba

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Sorted.append_largest
+ Sorted.filter
+ filter_sort_commute
+ list_map_toFinset
+ sort_insert_largest
+ sort_monotone_map
+ sort_range
+ toFinset_is_singleton_implies_replicate

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

eric-wieser · 2024-06-30T23:21:04Z

Mathlib/Data/List/Basic.lean

+theorem filter_eval_false (l : List α)
+    (h : ∀ a ∈ l, p a = false) : List.filter p l = []:= by


This is subsumed by List.filter_eq_nil

Mathlib/Data/List/Basic.lean

eric-wieser · 2024-06-30T23:23:03Z

Mathlib/Data/Finset/Basic.lean

+    rw [toFinset_filter f]
+
+theorem toFinset_is_singleton_implies_replicate {l : List α} {a : α}
+    (h : l.toFinset ⊆ {a}) : l = List.replicate l.length a := by


(and therefore should be removed?)

jcommelin · 2024-07-23T14:09:04Z

@davikrehalt Are you planning to continue working on this PR? Would you like some help from others, or do you want to hand over completely? (In the latter case, please label it with please-adopt.)

YaelDillies · 2024-07-25T13:16:10Z

Mathlib/Data/Finset/Sort.lean

@@ -81,6 +81,76 @@ theorem sort_perm_toList (s : Finset α) : sort r s ~ s.toList := by
  simp only [coe_toList, sort_eq]
 #align finset.sort_perm_to_list Finset.sort_perm_toList

+theorem filter_sort_commute [DecidableEq α](f : α → Prop) [DecidablePred f] (s : Finset α) :


Suggested change

theorem filter_sort_commute [DecidableEq α](f : α → Prop) [DecidablePred f] (s : Finset α) :

theorem filter_sort_comm [DecidableEq α](f : α → Prop) [DecidablePred f] (s : Finset α) :

YaelDillies · 2024-07-25T13:16:30Z

Mathlib/Data/Finset/Sort.lean

+  rw [List.toFinset_filter]
+  simp
+
+theorem sort_monotone_map [DecidableEq α] [DecidableEq β]


Suggested change

theorem sort_monotone_map [DecidableEq α] [DecidableEq β]

theorem sort_map_of_monotone [DecidableEq α] [DecidableEq β]

YaelDillies · 2024-07-25T13:16:45Z

Mathlib/Data/Finset/Sort.lean

+  simp
+
+theorem sort_monotone_map [DecidableEq α] [DecidableEq β]
+    (r' : β → β → Prop) [DecidableRel r'] [IsTrans β r'] [IsAntisymm β r'] [IsTotal β r']


Why are you taking an unbundled relation here?

Please answer this

Mathlib/Data/Finset/Sort.lean

Mathlib/Data/List/Pairwise.lean

davikrehalt · 2024-08-06T02:06:05Z

@davikrehalt Are you planning to continue working on this PR? Would you like some help from others, or do you want to hand over completely? (In the latter case, please label it with please-adopt.)

Sorry! I got busy since January--will label accordingly because I don't trust myself to be on top of this. again sorry!

Mathlib/Data/Finset/Sort.lean

leanprover-community-mathlib4-bot · 2024-08-20T23:05:05Z

This PR/issue depends on:

~~[Merged by Bors] - feat: interactions between List.map and sorting lists #15952~~
By Dependent Issues (🤖). Happy coding!

eric-wieser · 2024-08-20T23:53:15Z

I pushed a bunch of proof cleanups, and deleted the three lemmas that were exact duplicates of ones already in Mathlib.

I haven't attempted to tidy the statements of the remaining lemmas.

davikrehalt · 2024-09-04T04:55:05Z

Hi I have some time to work on polishing this now. But since it's been a while it's unclear to me what the remaining issues are. If someone could help tell me this I can try to make it suitable to be merged. Thanks!

YaelDillies

Here is a list of everything you should fix. You should also look at CI and perform the changes it's asking you to do.

YaelDillies · 2024-09-04T05:09:41Z

Mathlib/Data/Finset/Basic.lean

+    rw [toFinset_filter f]
+
+theorem toFinset_is_singleton_implies_replicate {l : List α} {a : α}
+    (h : l.toFinset ⊆ {a}) : l = List.replicate l.length a := by


Please remove this lemma

YaelDillies · 2024-09-04T07:11:41Z

Mathlib/Data/Finset/Image.lean

@@ -277,6 +277,12 @@ theorem disjiUnion_map {s : Finset α} {t : α → Finset β} {f : β ↪ γ} {h
      s.disjiUnion (fun a => (t a).map f) (h.mono' fun _ _ ↦ (disjoint_map _).2) :=
  eq_of_veq <| Multiset.map_bind _ _ _

+theorem list_map_toFinset [DecidableEq α] [DecidableEq β] (l : List α) :


Suggested change

theorem list_map_toFinset [DecidableEq α] [DecidableEq β] (l : List α) :

theorem map_listToFinset [DecidableEq α] [DecidableEq β] (l : List α) :

YaelDillies · 2024-09-04T07:12:27Z

Mathlib/Data/Finset/Sort.lean

+theorem filter_sort_commute [DecidableEq α] (f : α → Prop) [DecidablePred f] (s : Finset α) :
+    sort r (filter (f ·) s) = List.filter f (sort r s) := by


It's not really a commutativity lemma as it talks about two different filters here

Suggested change

theorem filter_sort_commute [DecidableEq α] (f : α → Prop) [DecidablePred f] (s : Finset α) :

sort r (filter (f ·) s) = List.filter f (sort r s) := by

theorem sort_filter [DecidableEq α] (f : α → Prop) [DecidablePred f] (s : Finset α) :

sort r (filter (f ·) s) = List.filter f (sort r s) := by

YaelDillies · 2024-09-04T07:14:47Z

Mathlib/Data/Finset/Sort.lean

+  simp
+
+theorem sort_monotone_map [DecidableEq α] [DecidableEq β]
+    (r' : β → β → Prop) [DecidableRel r'] [IsTrans β r'] [IsAntisymm β r'] [IsTotal β r']


Please answer this

YaelDillies · 2024-09-04T07:21:47Z

Mathlib/Data/List/Sort.lean

+    exact Sorted.filter f (Sorted.of_cons h)
+
+theorem Sorted.append_largest {a : α} {l : List α} :
+    Sorted r (l ++ [a]) ↔ (∀ b ∈ l, r b a) ∧ Sorted r l := by


Please apply this

vihdzp · 2024-10-30T21:04:40Z

Mathlib/Data/Finset/Sort.lean

+  rw [List.perm_cons]
+  apply (sort_perm_toList _ _).symm
+
+theorem sort_range (k : ℕ) : sort (· ≤ ·) (range k) = List.range k := by


I've reproved this theorem in #18465

davikrehalt added 12 commits January 9, 2024 13:42

added Sorted.filter

6801059

added toFinset.filter

b9a00a7

added filter_sort_commute

5d836d8

added filter_eval_true/false (I'm not sure how to write the proofs mo…

591772e

…re idiomatically, probably should be rewritten somehow)

added sort_monotone_map

417c6e5

added Pairwise_concat which is the same as Pairwise.join but for two …

621bd1b

…lists, not sure if it's necessary

added Sorted.append_largest and simplified scope of Sorted.filter

99bedbd

refactored sort_monotone_map and added sort_insert_largest in Finset.…

ee9d239

…Sort which addresses how sorted list changes upon adding an element larger than all

added the sort of Finset.range is List.range

000b939

added toFinset is singleton implies List.replicate

5e43740

changed name to be more descriptive for toFinset_is_singleton_implies…

b64ab90

…_replicate

add/remove spaces

a8bb565

github-actions bot reviewed Jan 10, 2024

View reviewed changes

Mathlib/Data/List/Basic.lean Outdated Show resolved Hide resolved

Update Mathlib/Data/List/Basic.lean

5192e3c

remove space Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

davikrehalt added the awaiting-review label Jan 10, 2024

davikrehalt added 4 commits January 9, 2024 23:08

Merge branch 'master' of github.com:leanprover-community/mathlib4 int…

0a882d7

…o list_lemma_davik merge to current state

forgot to include a lemma on List.toFinset commuting with map

0105ec0

Merge branch 'list_lemma_davik' of github.com:leanprover-community/ma…

ce92752

…thlib4 into list_lemma_davik update to current state

Merge branch 'master' of github.com:leanprover-community/mathlib4 int…

a371569

…o list_lemma_davik current state

github-actions bot reviewed Jan 10, 2024

View reviewed changes

Mathlib/Data/Finset/Image.lean Outdated Show resolved Hide resolved

wrong indent

1d21b5a

urkud reviewed Jan 22, 2024

View reviewed changes

Mathlib/Data/List/Pairwise.lean Outdated Show resolved Hide resolved

urkud added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Jan 22, 2024

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 12, 2024

grunweg added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Mar 25, 2024

Merge remote-tracking branch 'origin/master' into list_lemma_davik

a33aff4

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 30, 2024

eric-wieser reviewed Jun 30, 2024

View reviewed changes

YaelDillies self-assigned this Jul 23, 2024

YaelDillies reviewed Jul 25, 2024

View reviewed changes

davikrehalt added the please-adopt Inactive PR (would be valuable to adopt) label Aug 6, 2024

grunweg added the t-data Data (lists, quotients, numbers, etc) label Aug 15, 2024

eric-wieser reviewed Aug 19, 2024

View reviewed changes

Mathlib/Data/Finset/Sort.lean Show resolved Hide resolved

leanprover-community-mathlib4-bot added blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) labels Aug 19, 2024

eric-wieser added 6 commits August 20, 2024 23:10

Merge remote-tracking branch 'origin/master' into list_lemma_davik

3507eac

remove some duplicate theorems

25008ae

some cleanup

d885396

golf another proof

76d05ae

some cleanup

dd61713

reduce diff

9f72d47

YaelDillies reviewed Sep 4, 2024

View reviewed changes

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Oct 4, 2024

vihdzp reviewed Oct 30, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(Data/Finset & List): Add Lemmas for Sorting and Filtering #9605

feat(Data/Finset & List): Add Lemmas for Sorting and Filtering #9605

davikrehalt commented Jan 10, 2024 •

edited by Parcly-Taxel

Loading

urkud commented Jan 22, 2024

urkud Jan 22, 2024

eric-wieser Jun 30, 2024

YaelDillies Sep 4, 2024

urkud Jan 22, 2024 •

edited

Loading

vihdzp Oct 30, 2024

urkud Jan 22, 2024

YaelDillies Sep 4, 2024

github-actions bot commented Jun 30, 2024 •

edited

Loading

Declarations diff

eric-wieser Jun 30, 2024

eric-wieser Jun 30, 2024

jcommelin commented Jul 23, 2024

YaelDillies Jul 25, 2024

YaelDillies Jul 25, 2024

YaelDillies Jul 25, 2024

YaelDillies Sep 4, 2024

davikrehalt commented Aug 6, 2024

leanprover-community-mathlib4-bot commented Aug 20, 2024

eric-wieser commented Aug 20, 2024

davikrehalt commented Sep 4, 2024

YaelDillies left a comment

YaelDillies Sep 4, 2024

YaelDillies Sep 4, 2024

YaelDillies Sep 4, 2024

YaelDillies Sep 4, 2024

YaelDillies Sep 4, 2024

vihdzp Oct 30, 2024

		theorem filter_eval_false (l : List α)
		(h : ∀ a ∈ l, p a = false) : List.filter p l = []:= by

	theorem filter_sort_commute [DecidableEq α](f : α → Prop) [DecidablePred f] (s : Finset α) :
	theorem filter_sort_comm [DecidableEq α](f : α → Prop) [DecidablePred f] (s : Finset α) :

	theorem sort_monotone_map [DecidableEq α] [DecidableEq β]
	theorem sort_map_of_monotone [DecidableEq α] [DecidableEq β]

	theorem list_map_toFinset [DecidableEq α] [DecidableEq β] (l : List α) :
	theorem map_listToFinset [DecidableEq α] [DecidableEq β] (l : List α) :

		theorem filter_sort_commute [DecidableEq α] (f : α → Prop) [DecidablePred f] (s : Finset α) :
		sort r (filter (f ·) s) = List.filter f (sort r s) := by

feat(Data/Finset & List): Add Lemmas for Sorting and Filtering #9605

Are you sure you want to change the base?

feat(Data/Finset & List): Add Lemmas for Sorting and Filtering #9605

Conversation

davikrehalt commented Jan 10, 2024 • edited by Parcly-Taxel Loading

urkud commented Jan 22, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

urkud Jan 22, 2024 • edited Loading

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

github-actions bot commented Jun 30, 2024 • edited Loading

PR summary 9f72d47cba

Import changes for modified files

Declarations diff

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jcommelin commented Jul 23, 2024

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

davikrehalt commented Aug 6, 2024

leanprover-community-mathlib4-bot commented Aug 20, 2024

eric-wieser commented Aug 20, 2024

davikrehalt commented Sep 4, 2024

YaelDillies left a 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

davikrehalt commented Jan 10, 2024 •

edited by Parcly-Taxel

Loading

urkud Jan 22, 2024 •

edited

Loading

github-actions bot commented Jun 30, 2024 •

edited

Loading