Why does synthesizing Membership instance often fail?

Stream: new members

[aron]

I have a long piece of code with a lot of different Membership instances between a bunch of different types. I know this isn't recommended, but it fits my domain anyway. But either way I only have one instance between any two types and I always explicitly specify my types so it should never be ambiguous which types I'm referring to in a a ∈ b expression. But even then, I often get errors like

failed to synthesize
  Membership A B

even though I do have a Membership instance defined between A and B.

Things work when I specify the instance by name, like instMembershipAB.mem b a but if that works why can Lean often not find the membership instance on its own?

[Kevin Buzzard]

#mwe ?

[Kyle Miller]

It's not just not recommended, but incorrect to define multiple Membership instances.

The type α is an outParam, which means you must ensure that your instances satisfy the constraint that for any given γ there is at most α (in other words, among all the instances, γ determines α). Lean assumes you are satisfying this constraint.

class Membership (α : outParam (Type u)) (γ : Type v) where
  /-- The membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. -/
  mem : γ → α → Prop

[Kevin Buzzard]

(typo: at most one α)

[aron]

Kevin Buzzard said:

#mwe ?

I wasn't sure how complicated a #mwe I'd need to reproduce this issue but turns out not very complicated at all:

inductive A
inductive B

inductive Container
  | a (contents : A)
  | b (contents : B)

instance : Membership A Container where
  mem container item :=
    match container with
    | .a contents => item = contents
    | .b _contents => False

instance : Membership B Container where
  mem container item :=
    match container with
    | .a _contents => False
    | .b contents => item = contents

def testA (container : Container) (a : A) (_h : a ∈ container) := ()

/-- Doesn't work :( -/
def testB (container : Container) (b : B) (_h : b ∈ container) := ()

/-- Referencing instance explicitly does work -/
def testB' (container : Container) (b : B) (_h : instMembershipBContainer.mem container b) := ()

[aron]

Kyle Miller said:

The type α is an outParam, which means you must ensure that your instances satisfy the constraint that for any given γ there is at most α (in other words, among all the instances, γ determines α). Lean assumes you are satisfying this constraint.

hm I see what you're saying but this feels like a very limiting restriction. If your type can contain different things it feels only natural that you should be able to define membership for different things?

[aron]

I can understand that if you rely on type inference to tell you what the element type is that that would not always give you the type you want, because well, how could it know which of the different instances you want without telling it?

But if lean does know what the container and element types are because you've explicitly specified the types of the values used in your membership expression, why would that be an issue? surely lean could then unambiguously find the instance in question? and in fact in the example above it does know that it should be looking for an instance of Membership B Container – it doesn't get confused thinking that it should be looking for a Membership A Container. So I don't see why this is not a well supported use case

[Edward van de Meent]

this would all be fixed if the first argument to Membership was a semiOutParam...

[Edward van de Meent]

i.e. the following works:

class Membership' (α : semiOutParam (Type u)) (γ : Type v) where
  mem : γ → α → Prop

instance {α : semiOutParam (Type u)} {γ : Type v} [Membership' α γ] : Membership α γ where
  mem := Membership'.mem

infix:40 " ∈' " => fun x y => Membership'.mem y x

inductive A
inductive B

inductive Container
  | a (contents : A)
  | b (contents : B)

instance : Membership' A Container where
  mem container item :=
    match container with
    | .a contents => item = contents
    | .b _contents => False

instance : Membership' B Container where
  mem container item :=
    match container with
    | .a _contents => False
    | .b contents => item = contents

def testA (container : Container) (a : A) (_h : a ∈' container) := ()


/-- Doesn't work :( -/
def testB (container : Container) (b : B) (_h : b ∈' container) := ()

/-- Referencing instance explicitly does work -/
def testB' (container : Container) (b : B) (_h : instMembership'BContainer.mem container b) := ()

[Edward van de Meent]

(not sure i got the precedence right with the notation, but that's besides the point)

[Edward van de Meent]

also, a quick search suggests that this isn't the first time that this fact has caused (minor) inconvenience

[Kyle Miller]

aron said:

But if lean does know what the container and element types are because you've explicitly specified the types of the values used in your membership expression, why would that be an issue?

Lean takes outParam into account and assumes that you are writing your instances correctly — there's not much more to say. We could work out step-by-step what the consequences of it being an outParam are for why testB fails.

Edward's semiOutParam suggestion might work; it'd need to be thoroughly tested though.

Can you explain why you need more than one Membership instance in your concrete application?

In the linked thread, I'd suggested defining Membership instances for different syntaxes (projections for example). That doesn't work with your inductive Container example, and I think it's cleaner defining explicit Sets and using its membership. That opens up a lot of useful theory too.

import Mathlib.Data.Set.Basic

inductive A
inductive B

inductive Container
  | a (contents : A)
  | b (contents : B)

def Container.aSet (c : Container) : Set A :=
  { contents | c = .a contents }

def Container.bSet (c : Container) : Set B :=
  { contents | c = .b contents }

def testA (container : Container) (a : A) (_h : a ∈ container.aSet) := ()

def testB (container : Container) (b : B) (_h : b ∈ container.bSet) := ()

[Kyle Miller]

There's also something like this, where you define just one Membership instance:

import Mathlib.Data.Set.Basic

inductive A
inductive B

inductive Container
  | a (contents : A)
  | b (contents : B)

inductive ContainerObj
  | ofA (a : A)
  | ofB (b : B)

instance : CoeTail A ContainerObj := ⟨.ofA⟩
instance : CoeTail B ContainerObj := ⟨.ofB⟩

instance : Membership ContainerObj Container where
  mem s x :=
    match x, s with
    | .ofA x, .a contents => x = contents
    | .ofB x, .b contents => x = contents

def testA (container : Container) (a : A) (_h : ↑a ∈ container) := ()

def testB (container : Container) (b : B) (_h : ↑b ∈ container) := ()

Unfortunately you need an explicit coercion arrow...