Zulip Chat Archive

Stream: Is there code for X?

Topic: monad question


view this post on Zulip Floris van Doorn (Sep 20 2020 at 04:34):

@[simp] lemma map_map_seq {α β γ δ} (m : Type*  Type*) [monad m] [is_lawful_monad m]
  (f : α  β  γ) (g : γ  δ) (u : m α) (v : m β) :
  g <$> (f <$> u <*> v) = (λ x y, g (f x y)) <$> u <*> v :=
sorry

Is this true? I want it for filters.

view this post on Zulip Mario Carneiro (Sep 20 2020 at 04:39):

@[simp] lemma map_map_seq {α β γ δ} (m : Type*  Type*) [monad m] [is_lawful_monad m]
  (f : α  β  γ) (g : γ  δ) (u : m α) (v : m β) :
  g <$> (f <$> u <*> v) = (λ x y, g (f x y)) <$> u <*> v :=
by simp [ bind_map_eq_seq, bind_assoc,  bind_pure_comp_eq_map]

view this post on Zulip Floris van Doorn (Sep 20 2020 at 05:06):

Thanks!

view this post on Zulip Simon Hudon (Sep 20 2020 at 05:07):

Have you tried using simp with norm_monad. That might do it completely automatically

view this post on Zulip Simon Hudon (Sep 20 2020 at 05:07):

Actually norm_functor might be enough

view this post on Zulip Floris van Doorn (Sep 20 2020 at 05:18):

Oh nice, that also works:

@[simp] lemma map_map_seq {α β γ δ} (m : Type*  Type*) [monad m] [is_lawful_monad m]
  (f : α  β  γ) (g : γ  δ) (u : m α) (v : m β) :
  g <$> (f <$> u <*> v) = (λ x y, g (f x y)) <$> u <*> v :=
by simp with functor_norm

However, instantiating to filters doesn't work:

@[simp] lemma {u} filter.map_map_seq {α β γ δ : Type u} (f : α  β  γ) (g : γ  δ) (u : filter α)
  (v : filter β) : map g (map f u <*> v) = map (λ x y, g (f x y)) u <*> v :=
by { convert @map_map_seq _ _ _ _ filter filter.monad filter.is_lawful_monad f g u v,
 -- Goal: ⊢ filter.has_seq = applicative.to_has_seq
}

So clearly I'm doing something I'm not supposed to do...

I might be multiple levels deep into #xy. My previous goal was the following lemma, where after the following partial proof I wanted to rewrite with the aforementioned lemma.

import topology.list topology.algebra.monoid

open filter

@[simp] lemma tendsto_pure_left {α β} (f : α  β) (x : α) (u : filter β) :
  tendsto f (pure x) u   s  u, f x  s :=
by { simp [tendsto, pure_le_iff] }

lemma continuous_prod {α} [topological_space α] [monoid α] [has_continuous_mul α] :
  continuous (list.prod : list α  α) :=
begin
  rw [continuous_iff_continuous_at], intros l, simp [continuous_at],
  cases l, { simp [nhds_nil, mem_of_nhds] {contextual := tt} },
  simp [nhds_cons, tendsto],
end

view this post on Zulip Simon Hudon (Sep 20 2020 at 05:22):

Your lemma only needs applicative m and is_lawful_applicative m as an assumption. When you change that, your monad will no longer be converted into an applicative in the general lemma

view this post on Zulip Floris van Doorn (Sep 20 2020 at 05:26):

I see, that works. Thanks!
It still seems to be a design flaw that filter has multiple transitive has_seq instances. Or is that inevitable?

view this post on Zulip Simon Hudon (Sep 20 2020 at 05:29):

No, that seems like a mistake. In filter/basic.lean, line 1452:

instance : applicative filter := { map := @filter.map, seq := @filter.seq }

What happens if you delete that line?

view this post on Zulip Simon Hudon (Sep 20 2020 at 05:30):

Having a separate monad and applicative instance is useful for monad transformers because you have different assumptions for each:

instance [applicative m] : applicative (foo_t m) := ...
instance [monad m] : monad (foo_t m) := ...

But that does not apply for filter

view this post on Zulip Floris van Doorn (Sep 20 2020 at 05:32):

A couple of things break later on (not too many). It seems to be done intentionally, since line 1438 says:

-- this section needs to be before applicative, otherwise the wrong instance will be chosen

view this post on Zulip Simon Hudon (Sep 20 2020 at 05:32):

Actually, here's the answer:

https://github.com/leanprover-community/mathlib/blob/master/src/order/filter/basic.lean#L1387-L1393

view this post on Zulip Floris van Doorn (Sep 20 2020 at 05:33):

Ah ok

view this post on Zulip Simon Hudon (Sep 20 2020 at 05:34):

The applicative and monad definitions are distinct, that's why you have to pick the right one in the lemma that you were proving in this thread


Last updated: May 16 2021 at 05:21 UTC