instance subtypeCoe on Vector

Stream: new members

[Mark Fischer]

So vector is defined as a subtype of List. Subtypes have CoeOut instance that coerces to the subtype's .val. My intuition is that these two below should be the same, but bar doesn't typecheck

def foo (l : Vector ℕ 5) : Prop := (42:ℕ) ∈ l.val
def bar (l : Vector ℕ 5) : Prop := (42:ℕ) ∈ ↑l

Even more confusingly, vscode will display this in the proof state with ↑ even though the type checker doesn't like it. What is/isn't happening?

[Eric Rodriguez]

There could be multiple coercions out of Vector, and the docs#Membership.mem operator does not give Lean an expected type for what ↑l should be; so Lean just gives up.

[Mark Fischer]

Yeah, looking at the error that makes sense. It's not failing on an instance of membership List, but of Vector. Though I was expecting something telling me the coersion failed rather than that the instance lookup failed. I supposed it just coerced into itself under the hood?

I'm surprised Vector doesn't have an instance for membership defined. Not that this is hard to work around.

[Kyle Miller]

Coercions are allowed to be identity coercions, and it looks like this is a case where it chooses that.

Generally, to get coercions to work there needs to be an expected type, like Eric said. One way is to add a type ascription, which has the added feature that Lean inserts a coercion at this point if there's a type mismatch. For example, you might want

def bar (l : Vector ℕ 5) : Prop := (42:ℕ) ∈ (l : List ℕ)

However, it looks like Vector doesn't have a coercion to List, so there's an error at the type ascription.

[Mark Fischer]

Shouldn't this:
https://leanprover-community.github.io/mathlib4_docs/Init/Coe.html#subtypeCoe

mean that Vector gets a coercion to List? Am I reading it wrong?

[Yaël Dillies]

docs#Vector is semireducible. So the answer is "No, unless someone made an explict Coe instance about Vector"

[Kyle Miller]

In other words, the definition of Vector is a def rather than an abbrev, so the typeclass mechanism isn't aware Vector is a Subtype.

[Mark Fischer]

Yup. That makes sense. So the following works:

abbrev Vector (α : Type u) (n : ℕ) := { l : List α // l.length = n }
def bar (l : Vector ℕ 5) : Prop := 42 ∈ (l : List ℕ)

[Matt Diamond]

just curious, is there a difference between abbrev and a def with @[reducible]?

[Yaël Dillies]

Yes, abbrev is @[reducible, inline] def if I'm not wrong