# Zulip Chat Archive

## Stream: general

### Topic: has_mem and has_coe to set

#### Marc Masdeu (Jun 08 2022 at 16:35):

I am struggling with type class resolution. I would like to know why my code fails, and how could I make it work. Here is a #mwe:

```
import tactic
class IncidencePlane (Point : Type*) :=
(Line : Type*)
(between : Point → Point → Point → Prop)
namespace IncidencePlane
variables {Ω : Type*} [IncidencePlane Ω]
variables (A B : Ω)
instance (X Y : Type*) [has_mem X Y] : has_coe Y (set X) := ⟨λ L P , P ∈ L⟩
structure Segment (Ω : Type*) [IncidencePlane Ω] :=
(A : Ω) (B : Ω)
infix `⬝`:100 := λ A B, Segment.mk A B
instance (Ω : Type*) [IncidencePlane Ω] : has_mem Ω (Segment Ω) := ⟨λ P L, between L.A P L.B⟩
#check A⬝B -- works
#check {P : Ω | P ∈ A⬝B} -- works
#check (A⬝B : set Ω) -- doesn't work
end IncidencePlane
```

#### Oliver Nash (Jun 08 2022 at 16:37):

I don't have time to look at this properly but I'll just note that the following works:

```
#check (↑(A⬝B : Segment Ω) : set Ω)
```

#### Kevin Buzzard (Jun 08 2022 at 16:40):

```
set_option trace.class_instances true
```

at least shows you what the problem is: after a while Lean is trying to solve `has_coe_to_fun (set Ω) ?x_8 `

and after a while it realises it will be done if it can solve `has_coe_to_fun (set Ω) ?x_21`

and then after some further time it realises it will be done if it can solve `has_coe_to_fun (set Ω) ?x_48`

and etc etc. My guess is that `instance (X Y : Type*) [has_mem X Y] : has_coe Y (set X) := ⟨λ L P , P ∈ L⟩`

is a bad idea; why not make something more specific to your situation?

#### Kevin Buzzard (Jun 08 2022 at 16:43):

Yeah, this doesn't look good: `has_mem ?x_27 (set Ω)`

-> `has_mem ?x_54 (set Ω)`

-> `has_mem ?x_81 (set Ω)`

-> `has_mem ?x_108 (set Ω)`

-> ...

#### Marc Masdeu (Jun 08 2022 at 16:44):

Thanks for looking into this. I tried to make something more specific to my situation but I didn't get answers then... I want to consider Lean to know that A.B *is* a segment (so in a Lemma that talks about three segments doesn't need to take six points, but instead three variables s1, s2, s3). But at the same time a lot of statements need that segments are thought of as sets ( for instance). I'd like this to be as seamless as possible.

#### Kevin Buzzard (Jun 08 2022 at 16:45):

I don't really know what `set_like`

is, but maybe it helps?

#### Eric Rodriguez (Jun 08 2022 at 16:45):

#### Kevin Buzzard (Jun 08 2022 at 16:47):

Maybe this is the relevant part of the documentation?

#### Kevin Buzzard (Jun 08 2022 at 16:47):

But I'm not saying it will solve your problem -- I don't really understand this stuff properly, I'm just flagging that it's there.

#### Marc Masdeu (Jun 08 2022 at 16:49):

I was just reading about this (thanks @Eric Rodriguez and @Kevin Buzzard !). It's similar to what I want, although maybe I'd reimplement it myself to avoid having to prove injectivity (my objects are set_like, but maybe I don't want to prove it right away when defining them). This would not allow me to have some of the lemmas, I know...

#### Marc Masdeu (Jun 08 2022 at 16:56):

In fact, I don't think my objects are `set_like`

. If I define a `Ray A B`

as a half-line, then there are many other `Ray A C`

that are equal to it. I had opted for thinking of those as *different* (and having a `has_equiv`

for them), but for set_like objects that wouldn't work. Do you see a good solution to this?

#### Marc Masdeu (Jun 08 2022 at 17:01):

OK, I don't really know what I'm doing, but copying the code for `set_like`

and removing everything related to injectivity made my mwe work:

```
import tactic
@[protect_proj]
class subset (A : Type*) (B : out_param $ Type*) :=
(coe : A → set B)
namespace subset
variables {A : Type*} {B : Type*} [i : subset A B]
include i
instance : has_coe_t A (set B) := ⟨subset.coe⟩
@[priority 100]
instance : has_mem B A := ⟨λ x p, x ∈ (p : set B)⟩
-- `dangerous_instance` does not know that `B` is used only as an `out_param`
@[nolint dangerous_instance, priority 100]
instance : has_coe_to_sort A Type* := ⟨λ p, {x : B // x ∈ p}⟩
variables (p q : A)
@[simp, norm_cast] theorem coe_sort_coe : ((p : set B) : Type*) = p := rfl
variables {p q}
protected theorem «exists» {q : p → Prop} :
(∃ x, q x) ↔ (∃ x ∈ p, q ⟨x, ‹_›⟩) := set_coe.exists
protected theorem «forall» {q : p → Prop} :
(∀ x, q x) ↔ (∀ x ∈ p, q ⟨x, ‹_›⟩) := set_coe.forall
@[simp] theorem mem_coe {x : B} : x ∈ (p : set B) ↔ x ∈ p := iff.rfl
@[simp, norm_cast] lemma coe_eq_coe {x y : p} : (x : B) = y ↔ x = y := subtype.ext_iff_val.symm
@[simp, norm_cast] lemma coe_mk (x : B) (hx : x ∈ p) : ((⟨x, hx⟩ : p) : B) = x := rfl
@[simp] lemma coe_mem (x : p) : (x : B) ∈ p := x.2
@[simp] protected lemma eta (x : p) (hx : (x : B) ∈ p) : (⟨x, hx⟩ : p) = x := subtype.eta x hx
end subset
class IncidencePlane (Point : Type*) :=
(Line : Type*)
(between : Point → Point → Point → Prop)
namespace IncidencePlane
variables {Ω : Type*} [IncidencePlane Ω]
variables (A B : Ω)
structure Segment (Ω : Type*) [IncidencePlane Ω] :=
(A : Ω) (B : Ω)
infix `⬝`:100 := λ A B, Segment.mk A B
instance : subset (Segment Ω) Ω := ⟨λ L P, between L.A P L.B⟩
#check A⬝B -- works
#check {P : Ω | P ∈ A⬝B} -- works
#check (A⬝B : set Ω) -- works
end IncidencePlane
```

#### Eric Wieser (Jun 08 2022 at 19:02):

I think your original problem would go away if you used `has_coe_t`

instead of `has_coe`

#### Eric Wieser (Jun 08 2022 at 19:04):

Regarding your ray comment; do you really want `Ray A B ≠ Ray A C`

when morally the rays are the same?

#### Marc Masdeu (Jun 09 2022 at 06:15):

I'd love to have Ray A B = Ray A C, but I thought that equality for structures was the same as equality for all their constructors. If it's not the case, then how would I do it? This is why I was implementing separately a `has_equiv`

. @Eric Wieser is there a way to have a `has_eq`

?

#### Eric Wieser (Jun 09 2022 at 06:36):

You might be looking for docs#quotient by `setoid.ker`

Last updated: Dec 20 2023 at 11:08 UTC