Avoiding boilerplate with subclasses

Stream: general

[Marc Masdeu]

Hi,

I am trying to prepare for some geometry introduction to Lean, where students will need to prove facts about synthetic geometry, using concepts like lines, segments, rays, angles, circles, triangles,... All these have in common that they are subsets of the plane, which are "distinguished" in some way, so I decided that there would be structures corresponding to each of them, which would remember how they were created. Ideally I would redefine then the equality sign (a ray is defined by two points -it's the half-line starting at the first and containing the second point-, but the second point is not uniquely determined given a ray). If I'm not mistaken, the equality cannot be changed, so instead I go for has_equiv. Here is a mwe of what I have:

import tactic

noncomputable theory
open_locale classical

def pts {α β : Type*} [has_mem α β] (S : β) : set α := {x : α | x ∈ S}

class IncidencePlane (Point : Type*) :=
    (Line : Type*)
  (belongs : Point → Line → Prop)
  (between : Point → Point → Point → Prop)

namespace IncidencePlane

variables (Ω : Type*) [IncidencePlane Ω]
variables (A B : Ω)

-- Stuff about Line
instance : has_mem Ω (Line Ω) := ⟨belongs⟩
instance : has_coe (Line Ω) (set Ω) := ⟨pts⟩

-- Stuff about Segment
structure Segment :=
(A : Ω) (B : Ω)
infix `⬝`:100 := Segment.mk

namespace Segment
instance : has_mem Ω (Segment Ω) := ⟨λ P S, between S.A P S.B⟩
instance : has_equiv (Segment Ω) := ⟨λ S T, (S.A = T.A ∧ S.B = T.B) ∨ (S.A = T.B ∧ S.B = T.A)⟩
instance Segment.has_coe_to_set : has_coe (Segment Ω) (set Ω) := ⟨pts⟩
end Segment

-- Stuff about Ray
structure Ray (Point : Type*):=
    (origin : Point) (target : Point)
notation A `=>` B := Ray.mk A B

namespace Ray
instance : has_mem Ω (Ray Ω) := ⟨λ P r, (between r.origin P r.target) ∨ (between r.origin  r.target  P)⟩
instance : has_equiv (Ray Ω) := ⟨λ S T, S.origin = T.origin ∧ ((between S.origin S.target T.target) ∨ between S.origin T.target S.target)⟩
instance has_coe_to_set : has_coe (Ray Ω) (set Ω) := ⟨pts⟩
end Ray


#check (A⬝B : set Ω) -- works
#check (A=>B : set Ω) -- works

end IncidencePlane

As you can see, both Segment and Rayare instances of has_mem (they are subsets of points) and have a defined notion of equivalence has_equiv. When defining a new such object, I need to write a bunch of code that deals with this. I would like to instead have them be instances of a class, say Subset Ω, so that something like this would make the last checks pass:

structure Segment (A B :Ω) extends Subset Ω :=
{
(mem : ...)
(equiv : ...)
}

and then I would be able to, given S : Segment Ω, consider S.A, S.B, and also S : set Ω. I'm sure that this is possible, I tried something like

structure Subset (Ω : Type*) :=
(mem : Ω → Prop)
instance has_mem_subset (Ω : Type*) : has_mem Ω (subset Ω) := ⟨λ P S, S.mem P⟩
instance coe_subset_to_set (Ω : Type*) : has_coe (subset Ω) (set Ω) := ⟨pts⟩

but I am a bit lost. Any pointers?

Thank you.

[Yaël Dillies]

Do you know about docs#sym2?

[Marc Masdeu]

That would probably help with segments, but not with the rest of distinguished subsets, right?

[Marc Masdeu]

Here's a more concise question. I'd like to avoid the line instance : has_coe (Segment Ω) (Subset Ω) := ⟨λ S, S.to_Subset⟩ in the code below, at the cost of adding as many lines as necessary in the Segment part.

import tactic

class IncidencePlane (Point : Type*) :=
    (Line : Type*)
  (between : Point → Point → Point → Prop)

namespace IncidencePlane

variables {Ω : Type*} [IncidencePlane Ω]
variables (A B : Ω)

class Subset (Ω : Type*) :=
(mem : Ω → Prop)
instance has_mem_subset (Ω : Type*) : has_mem Ω (Subset Ω) := ⟨λ P S, @Subset.mem Ω S P⟩
instance coe_subset_to_set (Ω : Type*) : has_coe (Subset Ω) (set Ω) := ⟨λ S, {x : Ω | x ∈ S}⟩

structure Segment (Ω : Type*) extends Subset Ω :=
(A : Ω) (B : Ω)
instance : has_coe (Segment Ω) (Subset Ω) := ⟨λ S, S.to_Subset⟩

def Segment_mk (A B : Ω) : Segment Ω := { mem := λ P, between A P B,
  A := A,
  B := B }
infix `⬝`:100 := Segment_mk

#check A⬝B -- works
#check (A⬝B : set Ω) -- WANT THIS TO WORK

end IncidencePlane

[Kevin Buzzard]

It works for me in the sense that there are no errors. What do you want to happen? Output is ↑(A⬝B) : set Ω.

[Marc Masdeu]

@Kevin Buzzard it works as is, but I want to reduce the boilerplate needed to declare the Segment stuff. I have half a more structures like Segment (Ray, Angle, Circle, Triangle) and for each of them now I need about 6 lines of code. It seems to me that it should be doable in one line (plus one more to define notation)...