# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: monad question

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

#### Floris van Doorn (Sep 20 2020 at 05:06):

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) := ...
instance [monad m] : monad (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):

Actually, here's the answer:

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

#### Floris van Doorn (Sep 20 2020 at 05:33):

Ah ok

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