Zulip Chat Archive

Stream: general

Topic: filter map

Patrick Massot (May 10 2018 at 18:38):

Is this already somewhere in core or mathlib?

lemma filter_map_comm {I : Type*} {J : Type*} (f : I → J) (P : J → Prop) (r: list I) [decidable_pred P] :
  filter P (map f r) = map f (filter (P ∘ f) r) :=
begin
  induction r with h _ IH,
  { simp },
  { by_cases H : P (f h) ; simp [filter_cons_of_pos, filter_cons_of_neg, H, IH] }
end

Simon Hudon (May 10 2018 at 19:08):

try:

theorem filter_map_eq_map (f : α → β) : filter_map (some ∘ f) = map f :=
theorem filter_map_eq_filter (p : α → Prop) [decidable_pred p] :
  filter_map (option.guard p) = filter p :=
theorem filter_map_filter_map (f : α → option β) (g : β → option γ) (l : list α) :
  filter_map g (filter_map f l) = filter_map (λ x, (f x).bind g) l :=

from data.list.basic

Patrick Massot (May 10 2018 at 19:10):

What do you mean? The lemma is not there but there may be a shorter proof using those results?

Simon Hudon (May 10 2018 at 19:11):

Yes exactly. Sorry, I was overly concise

Patrick Massot (May 10 2018 at 19:12):

It looks at least as complicated as what I already have

Patrick Massot (May 10 2018 at 19:13):

And I don't want to frustrate Kenny by stealing a golfing challenge from him

Simon Hudon (May 10 2018 at 19:14):

That's very considerate :)

Patrick Massot (May 10 2018 at 19:15):

Actually I'd rather use Kenny (or anyone else) to help me fighting nat substraction

Patrick Massot (May 10 2018 at 19:15):

For instance:

Simon Hudon (May 10 2018 at 19:15):

I like the resulting proof because it avoids induction

Patrick Massot (May 10 2018 at 19:15):

example (a b k : ℕ) : b + k - (a + k) = b - a

Patrick Massot (May 10 2018 at 19:16):

What do you mean avoid induction? map and filter are defined inductively

Patrick Massot (May 10 2018 at 19:16):

You can at best hide induction

Patrick Massot (May 10 2018 at 19:16):

Note that both sides are zero is b is larger than a

Patrick Massot (May 10 2018 at 19:17):

So it looks like a "false" result but this one is actually true

Patrick Massot (May 10 2018 at 19:17):

I think

Patrick Massot (May 10 2018 at 19:18):

Do you have a solution with filter_map? Actually it could be useful to learn what filter_map is good for

Simon Hudon (May 10 2018 at 19:20):

What do you mean avoid induction? map and filter are defined inductively

They're recursively defined. But yeah, you can never get around using induction / recursion directly or indirectly but I feel hiding induction produces nicer interfaces. The laws about filter_map seem like you can prove a lot about filter and map without induction.

Simon Hudon (May 10 2018 at 19:21):

It's a generalization of both map and filter.

Patrick Massot (May 10 2018 at 19:22):

I still don't see how it could help me here

Reid Barton (May 10 2018 at 19:29):

example (a b k : ℕ) : b + k - (a + k) = b - a

example (a b k : ℕ) : b + k - (a + k) = b - a :=
nat.add_sub_add_right b k a

Patrick Massot (May 10 2018 at 19:30):

:astonished:

Simon Hudon (May 10 2018 at 19:30):

I think I overlooked a detail. I thought just doing a rw would work but here is what I get:

  rw [← filter_map_eq_map
     ,← filter_map_eq_filter
     ,← filter_map_eq_filter
     ,filter_map_filter_map
     ,filter_map_filter_map],
  congr, funext,
-- ⊢ option.bind ((some ∘ f) x) (option.guard P) = option.bind (option.guard (P ∘ f) x) (some ∘ f)

That should be hard either, but it makes the proof longer than expected

Patrick Massot (May 10 2018 at 19:30):

That's crazy

Patrick Massot (May 10 2018 at 19:30):

That's also crazy

Patrick Massot (May 10 2018 at 19:31):

Thanks Reid

Patrick Massot (May 10 2018 at 19:31):

I wasn't hoping for this to be in Lean core...

Patrick Massot (May 10 2018 at 19:43):

I'm becoming better and better at proof obfuscation. If I ever need to read those proofs, I'll hate myself.

Reid Barton (May 10 2018 at 19:44):

it's too hard to resist the golf

Patrick Massot (May 10 2018 at 19:46):

Right now I'm staring at line saying congr_n 1 ; funext ; simp only [nat.add_sub_cancel, nat.add_sub_add_right]

Patrick Massot (May 10 2018 at 19:46):

I wrote two minutes ago

Patrick Massot (May 10 2018 at 19:46):

And I already have no clue what it does

Patrick Massot (May 10 2018 at 19:46):

Mario and Johannes will be so proud

Patrick Massot (May 10 2018 at 19:48):

Because it's half the proof of some trivial statement, and trivial statement must have obfuscated proof according to mathlib style guide

Patrick Massot (May 10 2018 at 19:48):

lemma big.shift (P : ℕ → Prop) [decidable_pred P] (F : ℕ → R) (a b k : ℕ) :
  (big[(◆)/nil]_(i=a..b | (P i)) (F i)) = (big[(◆)/nil]_(i=(a+k)..(b+k) | (P (i-k))) (F (i-k))) :=
begin
  rw [range'_add_map, big.map],
  congr_n 1 ; funext ; simp only [nat.add_sub_cancel, nat.add_sub_add_right]
end