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

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

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 :=


: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

That's crazy

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

That's also crazy

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
end


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

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

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

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 :-)

[at the time]

Kevin Buzzard (May 10 2018 at 19:52):

I don't even want to think about that

Kevin Buzzard (May 10 2018 at 19:52):

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

Kevin Buzzard (May 10 2018 at 19:53):

Maybe they would have just played minecraft all day

Kevin Buzzard (May 10 2018 at 19:53):

and we'd be worse off

yep

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

or watched lol cats on youtube

Sean Leather (May 11 2018 at 07:07):

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

Moses Schönfinkel (May 11 2018 at 08:00):

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

Moses Schönfinkel (May 11 2018 at 08:06):

I believe cat pictures are new tho.

Dank memes next.

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: Dec 20 2023 at 11:08 UTC