Right implementation of Hilbert Plane?

Stream: maths

[Marc Masdeu]

With lots of help from @Kevin Buzzard , @Kyle Miller , @Alex J. Best , @Yury G. Kudryashov , @Johan Commelin and many others that I am regretfuly forgetting, here is a Lean formalization of the Hilbert Plane, essentially following Hartshorne's account on Hilbert. The only difference (up to errors that I am probably missing) is that I made two of the axioms (line through points and transport of angle) constructive.
I'd like to get some (constructive) criticism about how things are implemented (i.e. what should one change to make this mathlib-ready). I think that if the basics are laid out properly, then proving many of Euclid's results should be "easy". I haven't gone very far yet (much less than @Ali Sever, by the way): so far, I have proofs of basic facts using only the I and B axioms...

import tactic

noncomputable theory
open_locale classical

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

notation p `xor` q := (p ∧ ¬ q) ∨ (q ∧ ¬ p)

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

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

    (line_through' {A B : Point} (h: A ≠ B) : Line ) -- existence of line
    (I1spec' {A B : Point} (h: A ≠ B) : A ∈ line_through' h ∧ B ∈ line_through' h)
    (I1uniq' {A B : Point} {ℓ : Line} (h: A ≠ B) : A ∈ ℓ → B ∈ ℓ → ℓ = line_through' h) -- uniqueness of line
    (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 {Ω : Type*} [PreHilbertPlane Ω]

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

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

def points_between (A B : Ω) : set Ω := {P : Ω | between A P B}
notation A `*` B `*` C := PreHilbertPlane.between A B C

-- Put the axioms in terms of this has_mem
def line_through {A B : Ω} (h: A ≠ B) : Line Ω := line_through' h
lemma I1specl {A B : Ω} (h: A ≠ B) : A ∈ line_through h := (I1spec' h).1
lemma I1specr {A B : Ω} (h: A ≠ B) : B ∈ line_through h := (I1spec' h).2
lemma I1uniq {A B : Ω} {ℓ : Line Ω} (h: A ≠ B) : A ∈ ℓ → B ∈ ℓ → ℓ = line_through h := I1uniq' h

lemma I1 {A B : Ω} (h : A ≠ B) : ∃! (ℓ : Line Ω), ( A ∈ ℓ ) ∧ ( B ∈ ℓ ) :=
begin
    use line_through h,
    exact ⟨ ⟨I1specl h, I1specr h⟩, λ r hr, I1uniq h hr.1 hr.2⟩,
end
lemma I2 (ℓ : Line Ω) : ∃ A B : Ω, A ≠ B ∧ A ∈ ℓ ∧ B ∈ ℓ := I2' ℓ
lemma I3 : ∃ A B C : Ω, A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ ∀ ℓ : Line Ω, A ∈ ℓ ∧ B ∈ ℓ → ¬ C ∈ ℓ := I3'


def collinear (A B C : Ω) := ∃ (ℓ : Line Ω), A ∈ ℓ ∧ B ∈ ℓ ∧ C ∈ ℓ
@[simp] lemma collinear_iff {A B C : Ω} :
    collinear A B C ↔ ∃ ℓ : Line Ω, A ∈ ℓ ∧ B ∈ ℓ ∧ C ∈ ℓ :=
begin
    rw collinear,
end

def intersect (r s : Line Ω) := ∃ A, A ∈ r ∧ A ∈ s

def parallel (r s : Line Ω) := (r = s) ∨ (¬ intersect r s)
notation r `||` s := parallel r s

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 {Ω : Type*} [PreHilbertPlane Ω]

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

instance has_coe_to_set : has_coe (Segment Ω) (set Ω) := ⟨pts⟩
@[simp] lemma mem_coe_to_mem_pts (P : Ω) (S : Segment Ω) :
    P ∈ (S : set Ω) ↔ (P = S.A ∨ P = S.B ∨ S.A * P * S.B) := by refl

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

end Segment


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

namespace Ray
variables {Ω : Type*} [PreHilbertPlane Ω]

instance : has_mem Ω (Ray Ω) :=
⟨λ P r, P = r.origin ∨ (collinear r.origin P r.target ∧ ¬ r.origin ∈ pts (P⬝r.target))⟩

instance has_coe_to_set : has_coe (Ray Ω) (set Ω) := ⟨pts⟩
@[simp] lemma mem_coe_to_mem_pts (P : Ω) (r : Ray Ω) :
    P ∈ (r : set Ω) ↔
    P = r.origin ∨ (collinear r.origin P r.target ∧ ¬ r.origin ∈ pts (P⬝r.target)) := by refl
@[simp] lemma mem_pts (P : Ω) (r : Ray Ω) :
    P ∈ pts r ↔ P = r.origin ∨ (collinear r.origin P r.target ∧ ¬ r.origin ∈ pts (P⬝r.target)) := by refl

end Ray

structure Angle (Point : Type*) :=
    (A : Point) (x : Point) (B : Point)
notation `∟`:100 := Angle.mk

namespace Angle
variables {Ω : Type*} [PreHilbertPlane Ω]

def nondegenerate (a : Angle Ω) := ¬ collinear a.A a.x a.B

instance : has_mem Ω (Angle Ω) :=
⟨λ P a, P ∈ pts (a.x=>a.A) ∨ P ∈ pts (a.x=>a.B)⟩

instance has_coe_to_set : has_coe (Angle Ω) (set Ω) := ⟨pts⟩
@[simp] lemma mem_coe_to_mem_pts (P : Ω) (a : Angle Ω) :
    P ∈ (a : set Ω) ↔
    P ∈ pts (a.x=>a.A) ∨ P ∈ pts (a.x=>a.B) := by refl

@[simp] lemma mem_pts (P : Ω) (a : Angle Ω) :
    P ∈ a ↔
    P ∈ pts (a.x=>a.A) ∨ P ∈ pts (a.x=>a.B) := by refl

end Angle

class HilbertPlane (Point : Type*) extends PreHilbertPlane Point :=
    (B11 {A B C : Point} : (A * B * C) → (C * B * A))
    (B12 {A B C : Point} : (A * B * C) → (A ≠ B ∧ A ≠ C ∧ B ≠ C ∧ collinear A B C))
    (B2 {A B : Point} : ∃ C, A * B * C)
    (B3 {A B C : Point} {ℓ : Line}
        (hAB : A ≠ B) (hAC : A ≠ C) (hBC : B ≠ C)
        (hAl : A ∈ ℓ) (hBl : B ∈ ℓ) (hCl : C ∈ ℓ) :
        ((A * B * C) ∧ ¬( B * A * C ) ∧ ¬ (A * C * B)) ∨
        (¬ (A * B * C) ∧ ( B * A * C ) ∧ ¬ (A * C * B)) ∨
        (¬ (A * B * C) ∧ ¬( B * A * C ) ∧ (A * C * B)))

    (B4 {A B C D : Point} {ℓ : Line} -- Pasch
        (hnc: ¬ collinear A B C)
        (hnAl: ¬ (A ∈ ℓ)) (hnBl: ¬ B ∈ ℓ) (hnCl: ¬ C ∈ ℓ)
        (hDl: D ∈ ℓ) (hADB: A * D * B) :
            (∃ E ,  E ∈ ℓ ∧ (A * E * C)) xor (∃ E, E ∈ ℓ ∧ (B * E * C)))

    --(parallel_postulate {ℓ r s : Line} : (intersect r s) ∧ (r || ℓ) ∧ (s || ℓ) → (r = s))

    (seg_cong : Segment Point → Segment Point → Prop)
    (notation X `≅`:50 Y := seg_cong X Y)
    (ang_cong : Angle Point → Angle Point → Prop)
    (notation X `≃`:50 Y := ang_cong X Y)

    (C1 {S : Segment Point} {r : Ray Point} :
        ∃! D, (D ∈ pts r) ∧ ((S.A⬝S.B) ≅ (r.origin⬝D)))
    (C21 {S T U}: (S ≅ T) → (S ≅ U) → (T ≅ U))
    (C22 {A B} : (A⬝B) ≅ (A⬝B))
    (C3 {A B C D E F} : (A * B * C) → (D * E * F) →
        ((A⬝B) ≅ (D⬝E)) → ((B⬝C) ≅ (E⬝F)) → ((A⬝C) ≅ (D⬝F)))

    (C4 {α : Angle Point} {S : Segment Point} {s : Point}
        (hBAC : α.nondegenerate) (hs : ¬ collinear s S.A S.B ) (hr : S.A ≠ S.B) :  Point)
    (C4spec {α : Angle Point} {S : Segment Point} {s : Point}
        (hBAC : α.nondegenerate) (hs : ¬ collinear s S.A S.B) (hr : S.A ≠ S.B) :
        (∟ (C4 hBAC hs hr) S.A S.B ≃ α) ∧
        (∀ (x : Point), ((C4 hBAC hs hr) * x * s) → ¬ x ∈ line_through hr))
    (C4uniq {α : Angle Point} {S : Segment Point} {s : Point} {Z : Point}
        (hBAC : α.nondegenerate) (hs : ¬ collinear s S.A S.B) (hr : S.A ≠ S.B) :
         (∟ Z S.A S.B ≃ α) →
         ((∀ (x : Point), (Z * x * s) → ¬ x ∈ line_through hr)) →
         pts (S.A=>Z) = pts (S.A=>(C4 hBAC hs hr)))
    (C5 {α β γ : Angle Point} : α ≃ β → α ≃ γ → β ≃ γ)
    (C6 {A B C D E F} : (A⬝B ≅ D⬝E) → (A⬝C ≅ D⬝F) → (∟ B A C ≃ ∟ E D F) →
        (B⬝C ≅ E⬝F) ∧ (∟ A B C ≃ ∟ D E F) ∧ (∟ A C B ≃ ∟ D F E))


namespace HilbertPlane

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

end HilbertPlane

[Bryan Gin-ge Chen]

@Joseph Myers might be interested too as he's been doing a lot of Euclidean geometry in mathlib.

[Joseph Myers]

I guess a natural thing to do with a definition of Hilbert plane once you have it is to show that two-dimensional Euclidean spaces (i.e. {V : Type*} {P : Type*} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [finite_dimensional ℝ V] (h : findim ℝ V = 2)) are instances of it, as are hyperbolic spaces (which arguably gives item 12 from Freek's list) and conversely classify models of Hilbert planes with / without the parallel postulate (so construct the inner_product_space etc. structures given a Hilbert plane with the parallel postulate). But that doesn't answer the best way to structure the code.

[Joseph Myers]

Is there a version of Hilbert's axioms for n-dimensional geometry, like there is for Tarski's? The geometry in mathlib is in any (not necessarily finite) dimension, working where possible for affine subspaces of any dimension not just lines and planes, etc. (and results that do rely on a plane are expressed in terms of coplanar points, where the ambient Euclidean space might have a higher dimension, possibly with a separate version where the space is two-dimensional if having that version is useful as well).