Zulip Chat Archive

Stream: general

Topic: filter map


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Simon Hudon (May 10 2018 at 19:11):

Yes exactly. Sorry, I was overly concise

view this post on Zulip Patrick Massot (May 10 2018 at 19:12):

It looks at least as complicated as what I already have

view this post on Zulip Patrick Massot (May 10 2018 at 19:13):

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

view this post on Zulip Simon Hudon (May 10 2018 at 19:14):

That's very considerate :)

view this post on Zulip Patrick Massot (May 10 2018 at 19:15):

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

view this post on Zulip Patrick Massot (May 10 2018 at 19:15):

For instance:

view this post on Zulip Simon Hudon (May 10 2018 at 19:15):

I like the resulting proof because it avoids induction

view this post on Zulip Patrick Massot (May 10 2018 at 19:15):

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

view this post on Zulip Patrick Massot (May 10 2018 at 19:16):

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

view this post on Zulip Patrick Massot (May 10 2018 at 19:16):

You can at best hide induction

view this post on Zulip Patrick Massot (May 10 2018 at 19:16):

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

view this post on Zulip Patrick Massot (May 10 2018 at 19:17):

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

view this post on Zulip Patrick Massot (May 10 2018 at 19:17):

I think

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Simon Hudon (May 10 2018 at 19:21):

It's a generalization of both map and filter.

view this post on Zulip Patrick Massot (May 10 2018 at 19:22):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 10 2018 at 19:30):

:astonished:

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 10 2018 at 19:30):

That's crazy

view this post on Zulip Patrick Massot (May 10 2018 at 19:30):

That's also crazy

view this post on Zulip Patrick Massot (May 10 2018 at 19:31):

Thanks Reid

view this post on Zulip Patrick Massot (May 10 2018 at 19:31):

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

view this post on Zulip 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.

view this post on Zulip Reid Barton (May 10 2018 at 19:44):

it's too hard to resist the golf

view this post on Zulip 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]

view this post on Zulip Patrick Massot (May 10 2018 at 19:46):

I wrote two minutes ago

view this post on Zulip Patrick Massot (May 10 2018 at 19:46):

And I already have no clue what it does

view this post on Zulip Patrick Massot (May 10 2018 at 19:46):

Mario and Johannes will be so proud

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 10 2018 at 19:49):

(for instance big[(◆)/nil] could be a \Sum operator

view this post on Zulip Kevin Buzzard (May 10 2018 at 19:51):

This is just the sort of stuff which I really needed last November and wasn't there

view this post on Zulip Kevin Buzzard (May 10 2018 at 19:51):

I remember having to give up on a 1st year problem sheet question because I couldn't prove that sum from 1 to n was equal to sum from n to 1 :-)

view this post on Zulip Kevin Buzzard (May 10 2018 at 19:51):

[at the time]

view this post on Zulip Reid Barton (May 10 2018 at 19:52):

imagine where we'd be if Gauss had had a computer

view this post on Zulip Kevin Buzzard (May 10 2018 at 19:52):

I don't even want to think about that

view this post on Zulip Kevin Buzzard (May 10 2018 at 19:52):

how much time did Gauss and Euler waste working out examples etc

view this post on Zulip Patrick Massot (May 10 2018 at 19:52):

They would have had computer aided waste of time instead

view this post on Zulip Kevin Buzzard (May 10 2018 at 19:53):

Maybe they would have just played minecraft all day

view this post on Zulip Kevin Buzzard (May 10 2018 at 19:53):

and we'd be worse off

view this post on Zulip Patrick Massot (May 10 2018 at 19:53):

yep

view this post on Zulip Patrick Massot (May 10 2018 at 19:53):

or watched lol cats on youtube

view this post on Zulip Sean Leather (May 11 2018 at 07:07):

If they were functional programmers (esp. in Haskell), I think they would have enjoyed Lambdacats.

view this post on Zulip Moses Schönfinkel (May 11 2018 at 08:00):

Hehe, we're slowly eroding formality of this forum :).

view this post on Zulip Patrick Massot (May 11 2018 at 08:05):

I think it was already pretty badly eroded

view this post on Zulip Moses Schönfinkel (May 11 2018 at 08:06):

I believe cat pictures are new tho.

view this post on Zulip Moses Schönfinkel (May 11 2018 at 08:06):

Dank memes next.

view this post on Zulip Sean Leather (May 11 2018 at 08:33):

Hehe, we're slowly eroding formality of this forum :smiley:.

Given that theorem proving is a formal method, what does an eroded formal method look like? :thinking_face:

Ah ha! :light_bulb: This must be why the name “lean” was chosen: the methodological mountain was so eroded, it couldn't stand up straight.


Last updated: May 14 2021 at 07:19 UTC