Problem extending classes

Stream: new members

[Marc Masdeu]

Hi,

I am trying to formalize Hilbert's axioms for the plane (again) using nice notation so that students can play with them. So I want undefined terms Point and Line (which I finally realized should be Types) and many axioms on them. In order to make the axioms (and subsequent theorems) easy to parse, I want to introduce concepts like Segment, Ray, Angle, Triangle,...
The place where I get stuck is when I try to use a structure that I created (namely Segment) inside the definition of the class. I guess that I need to add parameters to the definition, but I don't see how to do it. Maybe this MWE is illustrative:

import tactic

noncomputable theory
open_locale classical

class PreHilbertPlane :=
    (Point : Type)
    (Line : Type)

    (belongs : Point → Line → Prop)
    (between : Point → Point → Point → Prop)

    (notation A `∈` ℓ := belongs A ℓ)

    (I1 {A B : Point} (h : A ≠ B) : ∃! ℓ, ( A ∈ ℓ ) ∧ ( B ∈ ℓ ))
    (I2 (ℓ : Line) : ∃ A B : Point, A ≠ B ∧ A ∈ ℓ ∧ B ∈ ℓ)
    (I3 : ∃ A B C : Point, (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ (∀ ℓ : Line, (A ∈ ℓ ∧ B ∈ ℓ) → (¬ (C ∈ ℓ) ))))


variable {Ω : PreHilbertPlane}
variables {A B C : Ω.Point}
variables {ℓ : Ω.Line}

notation A `*` B `*` C := PreHilbertPlane.between A B C
notation A `∈` ℓ := PreHilbertPlane.belongs A ℓ

def line_to_set : Ω.Line → set Ω.Point := λ ℓ , { P : Ω.Point | P ∈ ℓ}

instance line_to_set_coe :
  has_coe (Ω.Line) (set Ω.Point) := ⟨line_to_set⟩

structure Segment :=
    (A : Ω.Point)
    (B : Ω.Point)

notation A `⬝`:100 B := Segment.mk A B

def segment_to_set {Ω : PreHilbertPlane} (S : Segment) : set Ω.Point :=
    {S.A} ∪ {S.B} ∪ {C | S.A * C * S.B}

instance segment_to_set_coe {Ω : PreHilbertPlane} :
  has_coe (Segment) (set Ω.Point) := ⟨segment_to_set⟩

class HilbertPlane extends PreHilbertPlane :=
    (seg_cong : Segment → Segment → Prop)
    (notation X `≅`:1 Y := seg_cong X Y)

    (C21 {S T U : Segment}: (S ≅ T) → (S ≅ U) → (T ≅ U))
    (C3 {A B C D E F : Point} : A⬝B ≅ D⬝E → B⬝C ≅ E⬝F → A⬝C ≅ D⬝F))

(Beware: the axioms are NOT correct, they need extra assumptions which I don't care about in this question)

After defining PreHilbertPlane with some axioms (and the notions of Point and Line, and belong), in order to introduce new axioms I need to have the (undefined) notion of "congruent segments". This can be thought foundationally as Point \imp Point \imp Point \imp Point \imp Prop, but I want to instead consider it as Segment \imp Segment \imp Prop. This will be more practical with later axioms, that would involve angles (and 6 points at least), and also with theorems that involve several segments and angles.

I want to define a structure called Segment that essentially remembers the two points that created it, and that can be thought of as a set when needed. In the HilbertPlane class I need to use this notion both to define "congruence" and to state axioms C21 and C3. But I can't make it to typecheck...

Any hints?

[Reid Barton]

It would be easier to guess if you mentioned which part doesn't type check, and with what error.

[Reid Barton]

But I'm suspicious that you write Ω.Point but not Ω.Segment; so I'm guessing that Lean has no way to work out what Ω you consider segments in.

[Marc Masdeu]

The first error is at C21. If I comment that line out, then C3 also errs.

[Marc Masdeu]

And yes, the problem is that I want the Omega in my segments appearing in C21 and C3 to be something like "this". That is, a term of type HilbertPlane, which I am just defining!

[Reid Barton]

This is a bit awkward and not necessarily the best way but something like (seg_cong : @Segment to_PreHilbertPlane → @Segment to_PreHilbertPlane → Prop) should be enough for Lean to get the right idea

[Marc Masdeu]

Thanks! What would be the Lean way to do it, then?

This works (I just added parentheses to avoid precedence fight):

class HilbertPlane extends PreHilbertPlane :=
    (seg_cong : @Segment to_PreHilbertPlane → @Segment to_PreHilbertPlane → Prop)
    (notation X `≅`:1 Y := seg_cong X Y)

    (C21 {S T U : Segment}: (S ≅ T) → (S ≅ U) → (T ≅ U))
    (C3 {A B C D E F : Point} : ((A⬝B) ≅ (D⬝E)) → ((B⬝C) ≅ (E⬝F)) → ((A⬝C) ≅ (D⬝F)))

[Marc Masdeu]

I encountered a new problem. When working with the Plane, it is convenient to being able to think of many objects (lines, segments, rays, ...) as sets, so that if S is a segment and L is a line, it should make sense to write S \subseteq L. The first example is (though stupid) that the underlying set of a line L is the set of points P such that belong P L to it, where belong is the undefined notion. When I write something like this:

import tactic

noncomputable theory
open_locale classical

namespace hilbertplane

class PreHilbertPlane :=
    (Point : Type)
    (Line : Type)
        (belongs : Point → Line → Prop)
    (I1 {A B : Point} (h : A ≠ B) : ∃! ℓ, ( belongs A ℓ ) ∧ ( belongs B ℓ ))

variable {Ω : PreHilbertPlane}
variables {A B : Ω.Point}
variables {ℓ : Ω.Line}

def line_to_set : Ω.Line → set Ω.Point := λ ℓ , { P : Ω.Point | PreHilbertPlane.belongs P ℓ}

@[priority 10] instance line_to_set_coe :
  has_coe (Ω.Line) (set Ω.Point) := ⟨line_to_set⟩

@[priority 10] instance line_to_set_coe_t :
  has_coe_t (Ω.Line) (set Ω.Point) := ⟨line_to_set⟩

@[priority 10] instance line_to_set_lift :
  has_lift (Ω.Line) (set Ω.Point) := ⟨line_to_set⟩

lemma I11 (h: A ≠ B) : ∃ (ℓ : Ω.Line), A ∈ ℓ ∧ B ∈ ℓ :=
begin
    exists_of_exists_unique (PreHilbertPlane.I1 h),
end
end hilbertplane

then lemma I11 doesn't typecheck because Lean doesn't understand A ∈ ℓ. I know that I could define notation in this case, or that A ∈ (ℓ : set Ω.Point) does work, but I'd like to avoid manual coercions. I'd hope that by opening set (or something similar) Lean would decide that the thing on the left has to be a set, and do the coercion automatically. Is this doable?

[Kevin Buzzard]

Why not just define a has_mem instance?

[Marc Masdeu]

Hi @Kevin Buzzard, has_mem would work in the same way that notation A `∈` r` := belongs A r would, but then for segments, rays,... I would need to write all the set-theory-like instances ( subset, intersect, union,...) as well, and that doesn't seem the right way. I want that statements like A#B \subseteq B#A work well (where A#B means the Segment A B). I want also that A#B \subseteq ray A B typechecks (the segment is contained in the ray originating at A through B) and so on.
I'd be willing to sacrifice the ∈ notation for the undefined concept of "belongs" so that everything except points is a set whenever needed.

[Kevin Buzzard]

I'm no expert at infrastructure but maybe you could put a simp lemma making it unfold to what you want it to unfold to?

[Marc Masdeu]

When I tried I couldn't make the statements of lemmas to typecheck. Simp lemmas help with the simp tactic, right? But do not work automatically, when writing statements, if I understand that correctly.

[Kevin Buzzard]

Maybe I don't understand the question properly, sorry

[Marc Masdeu]

I'll try to work out a more illustrative #mwe.

[Kevin Buzzard]

I'm sorry, I just rushed through your question -- I am in teaching hell for another week

[Kyle Miller]

@Marc Masdeu I don't think has_mem is able to automatically insert a coe for you -- part of it is that typeclass resolution is unable to infer that ℓ should be coerced to a set. I'll write some instances in just a moment for how to use has_mem and probably what @Kevin Buzzard is talking about with simp lemmas.

[Marc Masdeu]

Here is the #mwe I promised. I would like the four lemmas to typecheck, but only the first 2 do.

import tactic
import data.set

noncomputable theory
open_locale classical

class PreHilbertPlane :=
    (Point : Type)
    (Line : Type)

    (belongs : Point → Line → Prop)
    (between : Point → Point → Point → Prop)

    (notation A `∈` ℓ := belongs A ℓ)

    (I1 {A B : Point} (h : A ≠ B) : ∃! ℓ, ( A ∈ ℓ ) ∧ ( B ∈ ℓ ))
    (I2 (ℓ : Line) : ∃ A B : Point, A ≠ B ∧ A ∈ ℓ ∧ B ∈ ℓ)
    (I3 : ∃ A B C : Point, (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ (∀ ℓ : Line, (A ∈ ℓ ∧ B ∈ ℓ) → (¬ (C ∈ ℓ) ))))


variable {Ω : PreHilbertPlane}
variables {A B C : Ω.Point}
variables {ℓ : Ω.Line}

notation A `*` B `*` C := PreHilbertPlane.between A B C
notation A `∈` ℓ := PreHilbertPlane.belongs A ℓ

def line_to_set : Ω.Line → set Ω.Point := λ ℓ , { P : Ω.Point | P ∈ ℓ}

instance line_to_set_coe :
  has_coe (Ω.Line) (set Ω.Point) := ⟨line_to_set⟩

/-
    A segment is created by giving two points.
-/
structure Segment :=
    (A : Ω.Point)
    (B : Ω.Point)

notation A `⬝`:100 B := Segment.mk A B

/-
    When thought of as a set, it is the the set consisting of the endpoints
    and all the points between them
-/
def segment_to_set {Ω : PreHilbertPlane} (S : Segment) : set Ω.Point :=
    {S.A} ∪ {S.B} ∪ {C | S.A * C * S.B}

instance segment_to_set_coe {Ω : PreHilbertPlane} :
  has_coe (Segment) (set Ω.Point) := ⟨segment_to_set⟩

/-
    Here we write some axioms about an undefined notion of 'congruence of segments'
-/
class HilbertPlane extends PreHilbertPlane :=
    (seg_cong : @Segment to_PreHilbertPlane → @Segment to_PreHilbertPlane → Prop)
    (notation X `≅`:1 Y := seg_cong X Y)

    (C21 {S T U : Segment}: (S ≅ T) → (S ≅ U) → (T ≅ U))
    (C3 {A B C D E F : Point} : ((A⬝B) ≅ (D⬝E)) → ((B⬝C) ≅ (E⬝F)) → ((A⬝C) ≅ (D⬝F)))

lemma first_lemma (h: A ≠ B) : ∃ (ℓ : Ω.Line), A ∈ ℓ ∧ B ∈ ℓ := -- checks
begin
    sorry
end

lemma second_lemma : (A⬝B : set Ω.Point) ⊆ B⬝A := -- checks
begin
    sorry
end

lemma third_lemma : (A⬝B) ⊆ (B⬝A) := -- fails
begin
    sorry
end

lemma fourth_lemma : (ℓ ∩ (A⬝B)) = ∅ := -- fails
begin
    sorry
end

[Marc Masdeu]

At some point I was sold the idea that implementing the Hilbert Plane using types for both Point and Line was better than using sets. I saw the advantage, and I am trying to push it to the rest of objects. It is much nicer to have a lemma that says

nice_lemma (s t r: Segment) : s ≅ t → s ≅ r → t ≅ r

than one saying

not_so_nice_lemma (A B C D E F : Point) : A⬝B ≅ C⬝D → A⬝B ≅ E⬝F → C⬝D ≅ E⬝F

The nice_lemma has the advantage that I would easily impose that a segment requires two distinct points, and then the statement wouldn't have to change, whereas the not_so_nice_lemma would have to include a hypothesis for each pair of points. I regard the first solution as Lean's take on encapsulation, which is great.

[Kyle Miller]

@Marc Masdeu I have an idea for how to get subsets and such to work, but in the meantime here are some modifications to your code so far. One thing is that classes should have parameters so that they can actually play a role in the typeclass inference system. It seems reasonable to make Point a parameter, and then have variables {Plane : Type*} [PreHilbertPlane Plane] and speak of points X Y : Plane. Another is that custom notation should probably be different from built-in notation since Lean's disambiguation system doesn't always work out.

What I'm going to investigate is having Lines be sets outside the definition of the class. This would let you use subset notation.

import tactic
import data.set

noncomputable theory
open_locale classical

-- don't want this to be a class since it's not attached to any type, so there's nothing to infer.
-- Maybe if the points type were the type the plane is associated with then it would be a good class?
class PreHilbertPlane (Point : Type*) :=
(Line : Type*)
(belongs : Point → Line → Prop)
(between : Point → Point → Point → Prop)
(notation A `∈` ℓ := belongs A ℓ)
(I1' {A B : Point} (h : A ≠ B) : ∃! ℓ, ( A ∈ ℓ ) ∧ ( B ∈ ℓ ))
(I2' (ℓ : Line) : ∃ A B : Point, A ≠ B ∧ A ∈ ℓ ∧ B ∈ ℓ)
(I3' : ∃ A B C : Point, (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ (∀ ℓ : Line, (A ∈ ℓ ∧ B ∈ ℓ) → (¬ (C ∈ ℓ) ))))

namespace PreHilbertPlane
variables {Plane : Type*} [PreHilbertPlane Plane]

instance Line.has_mem : has_mem Plane (Line Plane) :=
⟨λ p ℓ, belongs p ℓ⟩

def line_to_set (ℓ : Line Plane) : set Plane := {P : Plane | P ∈ ℓ}

instance Line.has_coe : has_coe (Line Plane) (set Plane) := ⟨line_to_set⟩

def points_between (A B : Plane) : set Plane := {P : Plane | between A P B}

-- Put the axioms in terms of this has_mem
lemma I1 {A B : Plane} (h : A ≠ B) : ∃! ℓ : Line Plane, A ∈ ℓ ∧ B ∈ ℓ := I1' h
lemma I2 (ℓ : Line Plane) : ∃ A B : Plane, A ≠ B ∧ A ∈ ℓ ∧ B ∈ ℓ := I2' ℓ
lemma I3 : ∃ A B C : Plane, A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ ∀ ℓ : Line Plane, A ∈ ℓ ∧ B ∈ ℓ → ¬ C ∈ ℓ := I3'

end PreHilbertPlane

open PreHilbertPlane

-- it's best not to overload notation if you can help it.
--notation A `*` B `*` C := PreHilbertPlane.between A B C
--notation A `∈` ℓ := PreHilbertPlane.belongs A ℓ

/-- A segment is created by giving two points. -/
structure Segment (Point : Type*) :=
(A : Point)
(B : Point)

notation A `⬝`:100 B := Segment.mk A B

namespace Segment
variables {Plane : Type*} [PreHilbertPlane Plane]

/--
When thought of as a set, it is the the set consisting of the endpoints
and all the points between them
-/
def to_set (S : Segment Plane) : set Plane :=
{S.A} ∪ {S.B} ∪ points_between S.A S.B

instance has_coe_to_set : has_coe (Segment Plane) (set Plane) := ⟨to_set⟩

end Segment

/-
Here we write some axioms about an undefined notion of 'congruence of segments'
-/
class HilbertPlane (Plane : Type*) extends PreHilbertPlane Plane :=
(seg_cong : Segment Plane → Segment Plane → Prop)
(notation X `≅`:50 Y := seg_cong X Y)
(C21 {S T U : Segment Plane}: (S ≅ T) → (S ≅ U) → (T ≅ U))
(C3 {A B C D E F : Plane} : ((A⬝B) ≅ (D⬝E)) → ((B⬝C) ≅ (E⬝F)) → ((A⬝C) ≅ (D⬝F)))

notation X `≅`:50 Y := HilbertPlane.seg_cong X Y

variables {Plane : Type*} [HilbertPlane Plane] (A B C : Plane)

lemma first_lemma (h: A ≠ B) : ∃ (ℓ : Line Plane), A ∈ ℓ ∧ B ∈ ℓ := -- checks
begin
    sorry
end

lemma second_lemma : (A⬝B : set Plane) ⊆ B⬝A := -- checks
begin
    sorry
end

lemma third_lemma : (A⬝B) ⊆ (B⬝A) := -- fails
begin
    sorry
end

lemma fourth_lemma : (ℓ ∩ (A⬝B)) = ∅ := -- fails
begin
    sorry
end

[Kyle Miller]

Some example simp lemmas you might have in the PreHilbertSpace namespace are

@[simp] lemma coe_to_mem (p : Plane) (ℓ : Line Plane) : p ∈ (ℓ : set Plane) ↔ p ∈ ℓ := by refl
@[simp] lemma to_set_to_mem (p : Plane) (ℓ : Line Plane) : p ∈ line_to_set ℓ ↔ p ∈ ℓ := by refl

These normalize things to be in terms of between, which is how the has_mem instance is defined.

[Yury G. Kudryashov]

I wonder if we can redefine subset using something like

def subset {α β γ : Type*} [has_mem α β] [has_mem α γ] (s : β) (t : γ) := ∀ {{x : α}}, x ∈s → x ∈ t

[Yury G. Kudryashov]

I'm not sure if Lean is good enough at finding α based on has_mem instances to make it work.

[Yury G. Kudryashov]

@Gabriel Ebner What do you think?

[Yury G. Kudryashov]

This would solve, e.g., some duplication of lemmas between sets and finsets.

[Yury G. Kudryashov]

And we'll be able to say s ⊆ t for (s : set α) and (t : finset α) without any coercions.

[Marc Masdeu]

Kyle Miller said:

Some example simp lemmas you might have in the PreHilbertSpace namespace are

@[simp] lemma coe_to_mem (p : Plane) (ℓ : Line Plane) : p ∈ (ℓ : set Plane) ↔ p ∈ ℓ := by refl
@[simp] lemma to_set_to_mem (p : Plane) (ℓ : Line Plane) : p ∈ line_to_set ℓ ↔ p ∈ ℓ := by refl

These normalize things to be in terms of between, which is how the has_mem instance is defined.

Thanks! I assume you mean belongs and not between :-). I'll try to see how this plays with the other definitions...

[Marc Masdeu]

@Yury G. Kudryashov I think I don't need to work with finset at this time... I just want the set notation to work with all my objects. Ideally, without defining each of subset, intersect,...

[Kyle Miller]

Indeed :smile:. These sorts of simp lemmas exist pretty much whenever a has_coe_to_fun instance or a has_coe instance with a has_mem instance exist. In the latter case, you can see it with submonoid. (and @Yury G. Kudryashov is just thinking about the design of Lean/mathlib in general)

[Yury G. Kudryashov]

You'll have to define intersect anyway because you want it to act on bundled objects, not their coercions to set α.

[Yury G. Kudryashov]

And yes, I'm thinking how can we refactor mathlib to make it easier to add more "bundled sets"

[Yury G. Kudryashov]

And finset is just a example.

[Yury G. Kudryashov]

Bringing in submonoids raises more questions (e.g., set notation vs lattice notation).

[Kyle Miller]

@Marc Masdeu I can't see a way to get set-like notation to work without having a coercion function. Maybe you'll be ok with the one below, which is a function pts that can take things to their set of points. It's like has_coe, but the thing being turned into the set of points gets to decide the points type. (I also added extension of segments to lines.)

import tactic
import data.set

noncomputable theory
open_locale classical

class PreHilbertPlane (Plane : Type*) :=
(Line : Type*)
(belongs : Plane → Line → Prop)
(between : Plane → Plane → Plane → Prop)
(notation A `∈` ℓ := belongs A ℓ)
(I1' {A B : Plane} (h : A ≠ B) : ∃! ℓ, ( A ∈ ℓ ) ∧ ( B ∈ ℓ ))
(I2' (ℓ : Line) : ∃ A B : Plane, A ≠ B ∧ A ∈ ℓ ∧ B ∈ ℓ)
(I3' : ∃ A B C : Plane, (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ (∀ ℓ : Line, (A ∈ ℓ ∧ B ∈ ℓ) → (¬ (C ∈ ℓ) ))))

class has_points (point_type : out_param $ Type*) (α : Type*) :=
(pts : α → set point_type)

open has_points (pts)

namespace PreHilbertPlane
variables {Plane : Type*} [PreHilbertPlane Plane]

instance : has_points Plane (Line Plane) :=
{ pts := λ ℓ, {P : Plane | belongs P ℓ} }

instance Line.has_coe : has_coe (Line Plane) (set Plane) := ⟨pts⟩

def points_between (A B : Plane) : set Plane := {P : Plane | between A P B}

-- Put the axioms in terms of this has_mem
lemma I1 {A B : Plane} (h : A ≠ B) : ∃! ℓ : Line Plane, A ∈ pts ℓ ∧ B ∈ pts ℓ := I1' h
lemma I2 (ℓ : Line Plane) : ∃ A B : Plane, A ≠ B ∧ A ∈ pts ℓ ∧ B ∈ pts ℓ := I2' ℓ
lemma I3 : ∃ A B C : Plane, A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ ∀ ℓ : Line Plane, A ∈ pts ℓ ∧ B ∈ pts ℓ → ¬ C ∈ pts ℓ := I3'

@[simp] lemma mem_coe_to_mem_pts (p : Plane) (ℓ : Line Plane) : p ∈ (ℓ : set Plane) ↔ p ∈ pts ℓ := by refl

end PreHilbertPlane

open PreHilbertPlane

/-- A segment is created by giving two points. -/
structure Segment (Point : Type*) :=
(A : Point)
(B : Point)

notation A `⬝`:100 B := Segment.mk A B

namespace Segment
variables {Plane : Type*} [PreHilbertPlane Plane]

/--
When thought of as a set, it is the the set consisting of the endpoints
and all the points between them
-/
instance : has_points Plane (Segment Plane) :=
{ pts := λ S, {S.A} ∪ {S.B} ∪ points_between S.A S.B }

instance has_coe_to_set : has_coe (Segment Plane) (set Plane) := ⟨pts⟩

@[simp] lemma mem_coe_to_mem_pts (p : Plane) (S : Segment Plane) : p ∈ (S : set Plane) ↔ p ∈ pts S := by refl
@[simp] lemma mem_pts (p : Plane) (S : Segment Plane) : p ∈ pts S ↔ (p = S.A ∨ p = S.B ∨ p ∈ points_between S.A S.B) :=
begin
  dunfold pts, simp, conv_lhs { congr, rw or.comm, }, rw or.assoc,
end

end Segment


/-
Here we write some axioms about an undefined notion of 'congruence of segments'
-/
class HilbertPlane (Plane : Type*) extends PreHilbertPlane Plane :=
(seg_cong : Segment Plane → Segment Plane → Prop)
(notation X `≅`:50 Y := seg_cong X Y)
(C21 {S T U : Segment Plane}: (S ≅ T) → (S ≅ U) → (T ≅ U))
(C3 {A B C D E F : Plane} : ((A⬝B) ≅ (D⬝E)) → ((B⬝C) ≅ (E⬝F)) → ((A⬝C) ≅ (D⬝F)))

notation X `≅`:50 Y := HilbertPlane.seg_cong X Y

variables {Plane : Type*} [HilbertPlane Plane] (A B C : Plane) (ℓ : Line Plane)

/-- first_lemma, which is just `PreHilbertPlane.I1` but for a `HilbertPlane`, so not really necessary. -/
lemma I1 (h: A ≠ B) : ∃! (ℓ : Line Plane), A ∈ pts ℓ ∧ B ∈ pts ℓ := I1 h

def Segment.extend (S : Segment Plane) (h : S.A ≠ S.B) : Line Plane := classical.some (I1 _ _ h)

lemma Segment.extend_spec (S : Segment Plane) (h : S.A ≠ S.B) : S.A ∈ pts (S.extend h) ∧ S.B ∈ pts (S.extend h) :=
(classical.some_spec (I1 _ _ h)).1

lemma Segment.extend_unique (S : Segment Plane) (h : S.A ≠ S.B) (S' : Segment Plane) (h' : S'.A ≠ S'.B)
  (h'' : S.A ∈ pts (S'.extend h') ∧ S.B ∈ pts (S'.extend h')) : S'.extend h' = S.extend h :=
(classical.some_spec (I1 _ _ h)).2 (S'.extend h') h''

lemma second_lemma : (A⬝B : set Plane) ⊆ B⬝A :=
begin
  intro x, simp,
  intro h, rw ←or.assoc, conv { congr, rw or.comm }, rw or.assoc,
  sorry, -- needs commutativity of `between`
end

lemma third_lemma : pts (A⬝B) ⊆ pts (B⬝A) :=
begin
  intros x, simp,
  sorry
end

lemma fourth_lemma : (pts ℓ ∩ pts (A⬝B)) = ∅ :=
begin
    sorry
end

[Kyle Miller]

I removed the has_mem instances because pts suffices. You could also remove the has_coe instances unless you find you need them for some reason.

[Kyle Miller]

Actually, it seems like has_mem is the way to go along with an extra definition

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

This is a coercion to sets such that β determines α. You mostly don't need to use pts below unless you deal with, for example, subsets or intersections.

import tactic
import data.set

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

@[simp] lemma mem_pts {α β : Type*} [has_mem α β] (x : α) (S : β) : x ∈ pts S ↔ x ∈ S := by refl

noncomputable theory
open_locale classical

class PreHilbertPlane (Plane : Type*) :=
(Line : Type*)
(belongs : Plane → Line → Prop)
(between : Plane → Plane → Plane → Prop)
(notation A `∈` ℓ := belongs A ℓ)
(I1' {A B : Plane} (h : A ≠ B) : ∃! ℓ, ( A ∈ ℓ ) ∧ ( B ∈ ℓ ))
(I2' (ℓ : Line) : ∃ A B : Plane, A ≠ B ∧ A ∈ ℓ ∧ B ∈ ℓ)
(I3' : ∃ A B C : Plane, (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ (∀ ℓ : Line, (A ∈ ℓ ∧ B ∈ ℓ) → (¬ (C ∈ ℓ) ))))

namespace PreHilbertPlane
variables {Plane : Type*} [PreHilbertPlane Plane]

instance : has_mem Plane (Line Plane) := ⟨belongs⟩

instance Line.has_coe : has_coe (Line Plane) (set Plane) := ⟨pts⟩
@[simp] lemma mem_coe_to_mem (p : Plane) (ℓ : Line Plane) : p ∈ (ℓ : set Plane) ↔ p ∈ ℓ := by refl

def points_between (A B : Plane) : set Plane := {P : Plane | between A P B}

-- Put the axioms in terms of this has_mem
lemma I1 {A B : Plane} (h : A ≠ B) : ∃! ℓ : Line Plane, A ∈ ℓ ∧ B ∈ ℓ := I1' h
lemma I2 (ℓ : Line Plane) : ∃ A B : Plane, A ≠ B ∧ A ∈ ℓ ∧ B ∈ ℓ := I2' ℓ
lemma I3 : ∃ A B C : Plane, A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ ∀ ℓ : Line Plane, A ∈ ℓ ∧ B ∈ ℓ → ¬ C ∈ ℓ := I3'

end PreHilbertPlane

open PreHilbertPlane

/-- A segment is created by giving two points. -/
structure Segment (Point : Type*) :=
(A : Point)
(B : Point)

notation A `⬝`:100 B := Segment.mk A B

namespace Segment
variables {Plane : Type*} [PreHilbertPlane Plane]

/--
When thought of as a set, it is the the set consisting of the endpoints
and all the points between them
-/
instance : has_mem Plane (Segment Plane) :=
⟨λ P S, P = S.A ∨ P = S.B ∨ P ∈ points_between S.A S.B⟩

instance has_coe_to_set : has_coe (Segment Plane) (set Plane) := ⟨pts⟩
@[simp] lemma mem_coe_to_mem_pts (p : Plane) (S : Segment Plane) : p ∈ (S : set Plane) ↔ p ∈ pts S := by refl

@[simp] lemma mem_pts (P : Plane) (S : Segment Plane) : P ∈ S ↔ (P = S.A ∨ P = S.B ∨ P ∈ points_between S.A S.B) :=
by refl

end Segment


/-
Here we write some axioms about an undefined notion of 'congruence of segments'
-/
class HilbertPlane (Plane : Type*) extends PreHilbertPlane Plane :=
(seg_cong : Segment Plane → Segment Plane → Prop)
(notation X `≅`:50 Y := seg_cong X Y)
(C21 {S T U : Segment Plane}: (S ≅ T) → (S ≅ U) → (T ≅ U))
(C3 {A B C D E F : Plane} : ((A⬝B) ≅ (D⬝E)) → ((B⬝C) ≅ (E⬝F)) → ((A⬝C) ≅ (D⬝F)))

notation X `≅`:50 Y := HilbertPlane.seg_cong X Y

variables {Plane : Type*} [HilbertPlane Plane] (A B C : Plane) (ℓ : Line Plane)

/-- first_lemma, which is just `PreHilbertPlane.I1` but for a `HilbertPlane`, so not really necessary. -/
lemma I1 (h: A ≠ B) : ∃! (ℓ : Line Plane), A ∈ ℓ ∧ B ∈ ℓ := I1 h

def Segment.extend (S : Segment Plane) (h : S.A ≠ S.B) : Line Plane := classical.some (I1 _ _ h)

lemma Segment.extend_spec (S : Segment Plane) (h : S.A ≠ S.B) : S.A ∈ S.extend h ∧ S.B ∈ S.extend h :=
(classical.some_spec (I1 _ _ h)).1

lemma Segment.extend_unique (S : Segment Plane) (h : S.A ≠ S.B) (S' : Segment Plane) (h' : S'.A ≠ S'.B)
  (h'' : S.A ∈ pts (S'.extend h') ∧ S.B ∈ pts (S'.extend h')) : S'.extend h' = S.extend h :=
(classical.some_spec (I1 _ _ h)).2 (S'.extend h') h''

lemma second_lemma : (A⬝B : set Plane) ⊆ B⬝A :=
begin
  intro x, simp,
  intro h, rw ←or.assoc, conv { congr, rw or.comm }, rw or.assoc,
  sorry, -- needs commutativity of `between`
end

lemma third_lemma : pts (A⬝B) ⊆ pts (B⬝A) :=
begin
  intros x, simp,
  sorry
end

lemma fourth_lemma : (pts ℓ ∩ pts (A⬝B)) = ∅ :=
begin
    sorry
end

[Marc Masdeu]

Thanks @Kyle Miller ! I had hoped that this pts function was unnecessary, but maybe it's not so bad after all. I'll see if I can adapt all the code to it.