monad question

Stream: Is there code for X?

[Floris van Doorn]

@[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]

@[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]

Thanks!

[Simon Hudon]

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

[Simon Hudon]

Actually norm_functor might be enough

[Floris van Doorn]

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]

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]

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]

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]

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]

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]

Actually, here's the answer:

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

[Floris van Doorn]

Ah ok

[Simon Hudon]

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