## Stream: new members

### Topic: list can't get longer by filter_map

#### Martin Dvořák (Jul 14 2022 at 21:24):

I need a proof that a list can't get longer by applying filter_map to it.

MWE:

example (l : list ℕ) (f : ℕ → option ℕ) :
(list.filter_map f l).length ≤ l.length :=
begin
sorry,
end


#### Eric Wieser (Jul 14 2022 at 22:00):

My guess would be docs#list.length_filter_map

#### Eric Wieser (Jul 14 2022 at 22:00):

But that doesn't exist!

#### Junyan Xu (Jul 14 2022 at 23:20):

I think this is the way to show it:

import data.list.basic

variables {α β : Type*} (f : α → option β) (l : list α)

theorem map_filter_map_some_eq_filter_map_is_some :
(l.filter_map f).map some = (l.map f).filter (λ b, b.is_some) :=
begin
rw [← list.filter_map_eq_filter, list.filter_map_map, list.map_filter_map],
congr, ext,
simp only [option.mem_def, option.guard_eq_some, option.map_eq_some'],
rw option.is_some_iff_exists,
split,
{ rintro ⟨a, h, rfl⟩, exact ⟨h, a, h⟩ },
{ rintro ⟨rfl, a, h⟩, exact ⟨a, h, h.symm⟩ },
end

theorem length_filter_map_le : (list.filter_map f l).length ≤ l.length :=
begin
rw [← list.length_map some, map_filter_map_some_eq_filter_map_is_some],
convert list.length_le_of_sublist (list.filter_sublist _),
rw list.length_map,
end


The first theorem could probably be golfed (it's possible that induction is faster).

#### Kyle Miller (Jul 15 2022 at 00:01):

Refactored and golfed:

import data.list.basic

variables {α β : Type*} (f : α → option β) (l : list α)

theorem list.map_filter_map_some_eq_filter_map_is_some :
(l.filter_map f).map some = (l.map f).filter (λ b, b.is_some) :=
begin
induction l with x xs ih,
{ simp },
{ cases h : f x; rw [list.filter_map_cons, h]; simp [h, ih] },
end

theorem list.length_filter_le (p : α → Prop) [decidable_pred p] :
(l.filter p).length ≤ l.length :=
list.length_le_of_sublist (list.filter_sublist _)

theorem list.length_filter_map_le : (list.filter_map f l).length ≤ l.length :=
begin
rw [← list.length_map some, list.map_filter_map_some_eq_filter_map_is_some, ← list.length_map f],
apply list.length_filter_le,
end

example (l : list ℕ) (f : ℕ → option ℕ) :
(list.filter_map f l).length ≤ l.length :=
list.length_filter_map_le _ _


#### Martin Dvořák (Jul 15 2022 at 00:04):

In the meanwhile, I wrote a simple proof by induction. Do you want me to commit my proof, or will you create a PR with your proof?

#### Notification Bot (Jul 15 2022 at 00:04):

Martin Dvořák has marked this topic as unresolved.

#### Junyan Xu (Jul 15 2022 at 00:06):

I like @Kyle Miller 's refactor and proofs!

#### Eric Wieser (Jul 15 2022 at 00:06):

Do we not have docs#list.length_filter_le?

#### Eric Wieser (Jul 15 2022 at 00:06):

I would expect it to appear next to docs#list.length_filter_lt_length_iff_exists

#### Eric Wieser (Jul 15 2022 at 00:06):

Oh, it follows from docs#list.countp_eq_length_filter

#### Kyle Miller (Jul 15 2022 at 00:09):

It also has the very direct proof list.length_le_of_sublist (list.filter_sublist _) that uses sublists rather than going through arithmetic and countp.

#### Kyle Miller (Jul 15 2022 at 00:09):

(I just fixed the naming in my code snippet.)

#### Martin Dvořák (Jul 15 2022 at 00:09):

OK, will you @Kyle Miller create the PR with your code please?

#### Kyle Miller (Jul 15 2022 at 00:11):

Would @Martin Dvořák or @Junyan Xu please do it? :smile: Feel free to add me as a reviewer.

#### Martin Dvořák (Jul 15 2022 at 00:14):

I can do it, but I don't know whether it is ethical to commit someone else's code under my name.

#### Junyan Xu (Jul 15 2022 at 00:23):

Free free to open a PR! You may add co-authored-by lines as appropriate.

OK.

#### Martin Dvořák (Jul 15 2022 at 00:56):

https://github.com/leanprover-community/mathlib/pull/15369

#### Martin Dvořák (Jul 29 2022 at 15:31):

Is anybody interested in having the lemma in mathlib? Or should I close the PR?

#### Alex J. Best (Jul 29 2022 at 15:39):

Seems like a useful enough lemma to me, not that I have a use for it in mind.

#### Alex J. Best (Jul 29 2022 at 15:40):

I just re-started the CI as it seems to have not completed for some reason

#### Martin Dvořák (Jul 29 2022 at 15:44):

Alex J. Best said:

I just re-started the CI as it seems to have not completed for some reason

Should I rebase the branch (currently more than 2 weeks behind) and try again?

#### Andrew Yang (Jul 29 2022 at 15:55):

When your PR is ready for review, you can mark the PR using the tag "awaiting-review". If not, the PR will not show up on the #queue and decrease the chance of your PR getting reviewed. For more such tips before PRing, checkout the page How to contribute to mathlib.

#### Martin Dvořák (Jul 29 2022 at 16:08):

Should I use "awaiting-review" even if my PR was already reviewed and I need a reply rather than another review?

#### Andrew Yang (Jul 29 2022 at 16:14):

Yes. See the Lifecycle of a PR section of that page. A typical PR will jump between the "awaiting-review" tag and the "awaiting-author" tag several times before it is merged.

#### Martin Dvořák (Aug 15 2022 at 19:15):

Is anybody interested in a finishing the PR? Or do you want me to close it?

Last updated: Dec 20 2023 at 11:08 UTC