list can't get longer by filter_map

Stream: new members

[Martin Dvořák]

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]

My guess would be docs#list.length_filter_map

[Eric Wieser]

But that doesn't exist!

[Junyan Xu]

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]

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]

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]

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

[Junyan Xu]

I like @Kyle Miller 's refactor and proofs!

[Eric Wieser]

Do we not have docs#list.length_filter_le?

[Eric Wieser]

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

[Eric Wieser]

Oh, it follows from docs#list.countp_eq_length_filter

[Kyle Miller]

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]

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

[Martin Dvořák]

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

[Kyle Miller]

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

[Martin Dvořák]

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

[Junyan Xu]

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

[Martin Dvořák]

OK.

[Martin Dvořák]

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

[Martin Dvořák]

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

[Alex J. Best]

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

[Alex J. Best]

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

[Martin Dvořák]

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]

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]

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

[Andrew Yang]

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]

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