## Stream: Is there code for X?

#### 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. #### 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]


Thanks!

#### Simon Hudon (Sep 20 2020 at 05:07):

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

#### Simon Hudon (Sep 20 2020 at 05:07):

Actually norm_functor might be enough

#### 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


#### 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

#### 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?

#### 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?

#### 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) := ...


But that does not apply for filter

#### 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


#### Simon Hudon (Sep 20 2020 at 05:32):

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