Viewing a List Nat as a List Rat

Stream: mathlib4

[Bhavik Mehta]

Here's my example:

import Mathlib.Data.Finsupp.Multiset

theorem coe_list {l : List ℕ} : l.map (id : ℚ → ℚ) = l.map (↑) := by
  sorry

Why does the theorem typecheck? It's taking a List Nat and coercing it to a List Rat, seemingly, even though the coercion doesn't seem to exist.

#synth CoeTC (List ℕ) (List ℚ)

fails, although maybe I should be looking for something else?

And the coercion has a weird form: when I'm doing maths and I put the rat/nat in the wrong place, seeing do notation with a pure isn't what I expect!

[Ruben Van de Velde]

It's because of List.instMonad, yeah. I thought we got rid of that, or maybe that was only for Set

[Bhavik Mehta]

I don't see how that could cause this. I also think it's definitely a good idea to keep the monad instance for lists!

[Edward van de Meent]

i think we did make that a non-instance... weird that it shows up

[Bhavik Mehta]

docs#List.instMonad it's an instance

[Edward van de Meent]

maybe it was removed from core or something?

[Edward van de Meent]

maybe we are getting confused because List.bind was renamed to List.flatMap

[Edward van de Meent]

(and List.join to List.flatten)

[Bhavik Mehta]

Losing do-notation for lists would be very unfortunate, in my opinion, so I sincerely hope that Monad List is not going anywhere

[Edward van de Meent]

it'd be ok if it were namespaced, imo

[Bhavik Mehta]

Why is it that this instance is showing up at all in this goal though?

[Ruben Van de Velde]

It's docs#Lean.Internal.coeM, no?

[Edward van de Meent]

because lean needs to coerce List N to List Q rather than N to Q

[Bhavik Mehta]

Ruben Van de Velde said:

It's docs#Lean.Internal.coeM, no?

I see, that was hard to find because it got inlined!

[Ruben Van de Velde]

Yeah, found it in the end by loogling for Bind.bind, "Coe" and then looking at the source of Mathlib.Data.Set.Functor

[Bhavik Mehta]

I'm also surprised that's defined using bind rather than fmap: I suppose they can be different for a non-lawful-monad, but it means that the coercion isn't even in simp normal form for specific monads like List

[Eric Wieser]

It's pretty much never going to be in simp-normal form because Functor.map is not as universe polymorphic as List.map

[Kyle Miller]

Bhavik Mehta said:

Why is it that this instance is showing up at all in this goal though?

The coercion system tries two things: finding a direct coercion, or recognizing that there's a monad lift available (here, the identity lift) and then coercing under the monad.

[Bhavik Mehta]

Kyle Miller said:

Bhavik Mehta said:

Why is it that this instance is showing up at all in this goal though?

The coercion system tries two things: finding a direct coercion, or recognizing that there's a monad lift available (here, the identity lift) and then coercing under the monad.

Makes sense, thanks.