simplifying composition in map

Stream: general

[Bernd Losert]

I have the following context:

h'' : r.converges (map g (map f ℱ)) (g (f x))
⊢ r.converges (map (g ∘ f) ℱ) ((g ∘ f) x)

I'm not sure how to turn h'' into the goal. I tried rw is_lawful_functor.comp_map, but that didn't help since comp_map uses <$> and not map.

[Adam Topaz]

Try dsimp?

[Adam Topaz]

Or convert h''

[Eric Wieser]

docs#filter.map_map?

[Eric Wieser]

Which map are you looking at? There is no docs#map

[Kevin Buzzard]

#mwe ?

[Bernd Losert]

Eric Wieser said:

docs#filter.map_map?

Ah, filter.map_map worked. Thanks a lot.

[Bernd Losert]

convert h''

This also magically works.

[Johan Commelin]

"Lean doesn't do magic" -- Kenny Lau

[Bernd Losert]

"Any sufficiently advanced technology is indistinguishable from magic." -- Arthur C. Clarke

[Bernd Losert]

I've noticed that filter has certain theorems have are basically specializations of more general theorems (e.g. filter.map_map vs. is_lawful_functor.comp_map). I suppose the reason for this is because Lean can't figure out how to instantiate very general theorems in certain cases, so having a specific one is better.

[Eric Wieser]

docs#is_lawful_functor.comp_map isn't universe polymorphic

[Eric Wieser]

It requires α β γ : Type u

[Eric Wieser]

filter.map_map is, it requires {α : Type u} {β : Type v} {γ : Type w}

[Bernd Losert]

I thought the ? in Type ? means any universe. I didn't realize it was a name for a universe variable.

[Eric Wieser]

Have a look at src#is_lawful_functor

[Yaël Dillies]

Is there any reason why functors aren't universe-polymorphic btw? I can't find the source of the restriction.

[Eric Wieser]

Try writing the class to be polymorphic, it doesn't work

[Yaël Dillies]

Hmm... So that's a technical restriction, not a mathematical one?

[Eric Wieser]

The problem is that (f : Type u → Type v) is a quantification over types, and means that in the rest of the typeclass you can only talk about f α where α : Type u

[Yaël Dillies]

Yeah but this problem would go away if we did the refactor we talked about, right?

[Eric Wieser]

If you deal with f in the way I do in my thread about redesigning the functor typeclasses to use out_param, that problem goes away

[Eric Wieser]

If you deal with f in the way I do in my thread about redesigning the functor typeclasses to use out_param, that problem goes away

[Eric Wieser]

Yes

[Yaël Dillies]

Ah yes!

[Yaël Dillies]

How's this refactor going? Do you need a helping hand?

[Eric Wieser]

But the functor typeclasses are hard-coded in the lean3 do notation parser

[Yaël Dillies]

Can Leo or Gabriel do anything about that?

[Bernd Losert]

What is that out_param thing? I see it every once-in-a-while in type classes.

[Yaël Dillies]

It's a way to stop Lean from trying to infer metavariables.

[Bernd Losert]

Is that similar/analogous to the {| |} stuff?

[Eric Wieser]

Leo could try this refactor in lean 4, if we could convince him that a) it works, and b) it's worthwhile.

[Bernd Losert]

Any documentation about it I can read?

[Eric Wieser]

docs#out_param has one line of docs I think

[Yaël Dillies]

The point is when you have an instance instance foo.to_bar [foo a b c] : bar a b where one variable that appears in the hypotheses does not appear in the goal. Because of the way TC inference works, when Lean looks for bar a b, it will find foo.to_bar and then look for foo a b ?c, and it will timeout trying to unify that metavariable.

[Eric Wieser]

Do you need a helping hand

Feel free to adopt my branch in the other thread. My goal there was simply to check that it's possible to state all the monad typeclasses in that style, not to actually replace all the old classes for new.

[Yaël Dillies]

So instead we make c an out_param to prevent Lean from trying to figure out what it is.

[Bernd Losert]

I get it. Interesting.

[Mario Carneiro]

Eric Wieser said:

But the functor typeclasses are hard-coded in the lean3 do notation parser

Actually I don't think this is true. It is hard-coded to make use of whatever bind resolves to, but not monads / functors specifically

[Mario Carneiro]

namespace foo
def bind (x : ℕ) (y : ℕ → ℕ) := y (2 * x)
def bar : ℕ := do a ← 1, 2 + a
end foo
#print foo.bar
-- def foo.bar : ℕ :=
-- foo.bind 1 (λ (a : ℕ), 2 + a)

[Eric Wieser]

I thought tactic mode begin end used more than just bind, but perhaps I'm mistaken