How to use SetLike?

Stream: new members

[Jakub Nowak]

I've tried to generalize some operation that was defined for Set, by using docs#SetLike.
But in other function I have Set, and when I try to use that generalized function, it doesn't work, because there's no instance for SetLike (Set α) α.

import Mathlib

def foo [SetLike Α α] (s : Α) (x : α) (hx : x ∈ s) : s := ⟨x, hx⟩

/--
error: failed to synthesize
  SetLike (Set α) α

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
---
error: Application type mismatch: The argument
  hx
has type
  @Membership.mem α (Set α) Set.instMembership s x
but is expected to have type
  @Membership.mem α (Set α) SetLike.instMembership s x
in the application
  foo s x hx
-/
#guard_msgs in
def foo' (s : Set α) (x : α) (hx : x ∈ s) : s := foo s x hx

I think my mistake was to use SetLike, I've tried using docs#Membership and docs#CoeSort instances, but then ⟨x, hx⟩ didn't work. I don't know what instance do I need to make it work.

[Jakub Nowak]

If I do

import Mathlib

def foo [SetLike Α α] (s : Α) (x : α) (hx : x ∈ s) : s := ⟨x, hx⟩

set_option pp.all true

/--
info: def foo.{u_1, u_2} : {Α : Type u_1} →
  {α : Type u_2} →
    [inst : SetLike.{u_1, u_2} Α α] →
      (s : Α) →
        (x : α) →
          (hx : @Membership.mem.{u_2, u_1} α Α (@SetLike.instMembership.{u_1, u_2} Α α inst) s x) →
            @Subtype.{u_2 + 1} α fun (x : α) =>
              @Membership.mem.{u_2, u_1} α Α (@SetLike.instMembership.{u_1, u_2} Α α inst) s x :=
fun {Α : Type u_1} {α : Type u_2} [inst : SetLike.{u_1, u_2} Α α] (s : Α) (x : α)
    (hx : @Membership.mem.{u_2, u_1} α Α (@SetLike.instMembership.{u_1, u_2} Α α inst) s x) =>
  @Subtype.mk.{u_2 + 1} α
    (fun (x : α) => @Membership.mem.{u_2, u_1} α Α (@SetLike.instMembership.{u_1, u_2} Α α inst) s x) x hx
-/
#guard_msgs in
#print foo

then it looks like s is just defeq to Subtype, but I don't know where this defeq comes from.

[Jakub Nowak]

Ah, wait, no, the return type is ↥s, which is defined to be a Subtype.

[Jakub Nowak]

So this works:

import Mathlib

def foo [Membership α Α] (s : Α) (x : α) (hx : x ∈ s) : { x : α // x ∈ s } := ⟨x, hx⟩

def foo' (s : Set α) (x : α) (hx : x ∈ s) : s := foo s x hx

But this doesn't

import Mathlib

def foo [CoeSort Α Type*] [Membership α Α] (s : Α) (x : α) (hx : x ∈ s) : s := ⟨x, hx⟩

def foo' (s : Set α) (x : α) (hx : x ∈ s) : s := foo s x hx

because coercion can be anything, not necessarily { x : α // x ∈ s } . Is it possible to be able to use coercion, or do I need to spell out { x : α // x ∈ s } explicitly when using Membership?

[Jakub Nowak]

Ah, I see, that works:

import Mathlib

local instance (priority := 100) [Membership α Α] : CoeSort Α (Type _) :=
  ⟨fun p => { x : α // x ∈ p }⟩

def foo [Membership α Α] (s : Α) (x : α) (hx : x ∈ s) : s := ⟨x, hx⟩

def foo' (s : Set α) (x : α) (hx : x ∈ s) : s := foo s x hx