has_mem and has_coe to set

Stream: general

[Marc Masdeu]

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]

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]

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]

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]

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]

I don't really know what set_like is, but maybe it helps?

[Eric Rodriguez]

docs#set_like

[Kevin Buzzard]

Maybe this is the relevant part of the documentation?

[Kevin Buzzard]

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]

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]

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]

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]

I think your original problem would go away if you used has_coe_t instead of has_coe

[Eric Wieser]

Regarding your ray comment; do you really want Ray A B ≠ Ray A C when morally the rays are the same?

[Marc Masdeu]

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]

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