Sebastian Zivota

Stream: new members

[Sebastian Zivota]

Hi, I'm interested in formalizing some (synthetic) projective geometry in Lean for my own enjoyment. To be honest I'm already struggling with how to formulate the definition of a projective plane, to wit: A projective plane comprises a set P of Points and a set L of Lines, with an incidence relation ε between them, satisfying the following axioms:

1. For every p, q ∈ P with p ≠ q, there is a unique ℓ ∈ L such that p ε ℓ and q ε ℓ.
2. For every ℓ, m ∈ L with ℓ ≠ m, there is a p ∈ P such that p ε ℓ and p ε m.
3. There are four points such that no three among them lie on a line.

My first approach was to model this as a structure:

structure projective_plane (P : Type) (L : Type) :=
  (is_on : P → L → Prop)
  (connecting_line : …)
  (intersection_point : …)
  (exists_quadrangle : …)

But if I do this, I don't see how I can e.g. define ε as notation for is_on (because it's relative to the plane). Is this the right approach or should I be doing something differently?

[Adam Topaz]

Here is a rough estimate for what could be done...

class projective_plane (P : Type) (L : Type) :=
  (is_on : P → L → Prop)
  (connecting_line : sorry)
  (intersection_point : sorry)
  (exists_quadrangle : sorry)

notation a `ε` b := projective_plane.is_on a b

example {P L : Type} [projective_plane P L] (p : P) (l : L) : Prop := p ε l

[Sebastian Zivota]

Excellent, thank you very much.

[Huỳnh Trần Khanh]

yeah, creating a typeclass is a nice idea. alternatively, you can also use a variables declaration to introduce an instance of the plane structure, and then define notations to your heart's content!

[Huỳnh Trần Khanh]

I prefer variables because that's what the IMO Grand Challenge does

[Huỳnh Trần Khanh]

mathlib is a treasure trove of quality lean code. you should clone and read the code to learn lean https://github.com/leanprover-community/mathlib/tree/master/archive/imo

[Yaël Dillies]

Making projective_plane a class sounds like the way to go, because then you can instantiate it for concrete projective planes instead of always having to pass around the same 3 hypotheses.

[Eric Wieser]

Why not a structure?

[Sebastian Zivota]

Does it make sense to create an auxiliary class has_incidence so that I can use the ε notation in the definition of a projective plane? And can I set this up so that I don't have to put both [has_incidence] and [projective_plane] bounds on functions?

[Patrick Massot]

Do you really insist on not using the usual $\in$ symbol?

[Sebastian Zivota]

No, not at all. I'd be fine with using ∈.

[Heather Macbeth]

To use the standard symbol, you can extend the has_mem class:

class projective_plane (P : Type) (L : Type) extends has_mem P L :=
  (connecting_line : sorry)
  (intersection_point : sorry)
  (exists_quadrangle : sorry)

example {P L : Type} [projective_plane P L] (p : P) (l : L) : Prop := p ∈ l

[Sebastian Zivota]

Is there an equivalent of has_mem in Lean 4?

[David Renshaw]

yes, in mathlib4: https://github.com/leanprover-community/mathlib4/blob/ceae8916f072cb3cb7fc67a88e01828d42bd924f/Mathlib/Init/SetNotation.lean#L1-L2

[Kyle Miller]

There's also a little-used feature where you can define notation for use inside a definition. I don't recommend it here because it conflicts with has_mem, but anyway here's how that works:

class projective_plane (P : Type) (L : Type) :=
(is_on : P → L → Prop)
(infix ` ∈ ` := is_on)
(connecting_line : ∀ (p q : P), p ≠ q → ∃! (ℓ : L), p ∈ ℓ)
(intersection_point : ∀ (ℓ ℓ' : L), ℓ ≠ ℓ' → ∃! (p : P), p ∈ ℓ ∧ p ∈ ℓ')
(exists_quadrangle : sorry)

infix ` ∈ ` := projective_plane.is_on

[Sebastian Zivota]

How can I use/import mathlib4?

[Kevin Buzzard]

mathlib4 right now is just some playground for experimenting with mathematics in Lean 4. Are you sure you want to use/import it? If so then just clone it and open it in VS Code, making sure you have the lean 4 extension enabled. Note however that all the code above was written in Lean 3, and there is no compatibility between the two versions.

[Sebastian Zivota]

Right, I'm gonna switch to Lean 3 then :)

[Sebastian Zivota]

Can I define a function for the connecting line of two distinct points? The problem is that it wouldn't be well-defined for all pairs of points.

[Yaël Dillies]

In the context of affine geometry?

[Heather Macbeth]

You can use if ... then ... else ... and just have it take a junk value if the two points are the same (you might need to assume [nonempty L], then the junk value can be default L). This is an approach taken fairly often in similar situations in mathlib.

Here's a discussion of the "junk value" technique from Kevin Buzzard's blog:
https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/

[Adam Topaz]

Sebastian Zivota said:

Can I define a function for the connecting line of two distinct points? The problem is that it wouldn't be well-defined for all pairs of points.

How do you define "line"? In the context of affine geometry, you could take two points and return the affine span of the two points, so if the two points are the same you just get the point back.

[Yaël Dillies]

AH of course this is for your projective geometry above :sweat_smile:

[Adam Topaz]

Ah ok, so if you have already defined projective spaces, you could (first define, then.....) take the projective span ;)

[Adam Topaz]

Ah I see, you want to use projective_planefrom the code above. Yes, I would follow Heather's advice.

[Adam Topaz]

(sorry, my connection seems to be lagging a bit today)

[Kyle Miller]

Sebastian Zivota said:

Can I define a function for the connecting line of two distinct points? The problem is that it wouldn't be well-defined for all pairs of points.

If your axiom is connecting_line : ∀ (p q : P), p ≠ q → ∃! (ℓ : L), p ∈ ℓ, then you can use docs#exists.some

For example if h is a proof that p and q are not equal, you can do (connecting_line p q h).some (though you might need to specify the intended type L for the typeclass resolution to work).

[Sebastian Zivota]

Kyle Miller said:

Sebastian Zivota said:

Can I define a function for the connecting line of two distinct points? The problem is that it wouldn't be well-defined for all pairs of points.

If your axiom is connecting_line : ∀ (p q : P), p ≠ q → ∃! (ℓ : L), p ∈ ℓ, then you can use docs#exists.some

For example if h is a proof that p and q are not equal, you can do (connecting_line p q h).some (though you might need to specify the intended type L for the typeclass resolution to work).

Assuming you mean Exists.some: this doesn't appear to use the uniqueness at all.
Should I define

connecting_line : ∀ p q : P, ∃ ℓ : L, p ∈ ℓ ∧ q ∈ ℓ
line p q := Exists.some (connecting_line p q)
line_connects₁ := p ∈ line p q
line_connects₂ := q ∈ line p q
line_unique : ∀ (p q : P) (ℓ : L), p ≠ q → p ∈ l → q ∈ l → l = line p q

i.e. have line p q defined even for p = q and prove the interesting property (uniqueness) only for distinct points? Or is there another way to do it?

[Adam Topaz]

@Sebastian Zivota do you have a #mwe with your projective_plane class?

[Kyle Miller]

That's true that docs#Exists.some doesn't need uniqueness. You can make use of the uniqueness property (to characterize this function) using docs#Exists.some_spec

Splitting the axiom like that seems like a reasonable idea, though, since we do know that there's a line running through every point.

[Kyle Miller]

That then makes docs#Exists.some responsible for choosing the "junk data" for line p p

[Sebastian Zivota]

Adam Topaz said:

Sebastian Zivota do you have a #mwe with your projective_plane class?

Working, if not exactly pretty.

import logic.basic

variables {P L : Type}

def is_triangle [has_mem P L] (p q r : P) : Prop :=
    p ≠ q
  ∧ p ≠ r
  ∧ q ≠ r
  ∧ ¬ ∃ l : L, p ∈ l ∧ q ∈ l ∧ r ∈ l

def is_quadrangle [has_mem P L] (p q r s : P) : Prop :=
    @is_triangle _ L _ p q r
  ∧ @is_triangle _ L _ p q s
  ∧ @is_triangle _ L _ p r s
  ∧ @is_triangle _ L _ q r s

class projective_plane (P L : Type) extends has_mem P L :=
  (exists_connecting_line : ∀ p q : P, ∃ l : L, p ∈ l ∧ q ∈ l)
  (exists_intersection_point : ∀ l m : L, ∃ p : P, p ∈ l ∧ p ∈ m)
  (point_line_uniq : ∀ {p q : P} {l m : L}, p ∈ l → q ∈ l → p ∈ m → q ∈ m → p = q ∨ l = m)
  (exists_quadrangle : ∃ (p q r s : P), @is_quadrangle _ L _ p q r s)

namespace projective_plane

variables {p q : P}

noncomputable
def connecting_line [projective_plane P L] (p q : P) : L := Exists.some (exists_connecting_line p q)

notation p ` ⊔ ` q := connecting_line p q

theorem connecting_line_left [projective_plane P L] : ∀ p q : P,  p ∈ (@connecting_line P L _ p q ) :=
begin
    intros p q,
    exact (Exists.some_spec (exists_connecting_line p q)).left,
end

theorem connecting_line_right [projective_plane P L] : ∀ p q : P,  q ∈ (@connecting_line P L _ p q) :=
begin
    intros p q,
    exact (Exists.some_spec (exists_connecting_line p q)).right,
end

theorem connecting_line_uniq [projective_plane P L] : ∀ (p q : P) (l : L), p ≠ q → p ∈ l → q ∈ l → l = p ⊔ q :=
begin
    intros p q l hpq hpl hql,
    have hpm : p ∈ p ⊔ q := connecting_line_left p q,
    have hqm : q ∈ p ⊔ q := connecting_line_right p q,
    have h : p = q ∨ l = p ⊔ q := (point_line_uniq hpl hql hpm hqm),
    exact or_iff_not_imp_left.mp h hpq
end

noncomputable
def intersection_point (l m : L) [projective_plane P L] : P := Exists.some $ exists_intersection_point l m

notation l ` ⊓ ` m := intersection_point l m

end projective_plane
-- insert dual theorems here

I find myself having to fully spell out an uncomfortable number of types that I would rather keep implicit, like @is_triangle _ L _ p q r in the definition of is_quadrangle. I'm also not happy with the end of the proof of connecting_line_uniq; I wonder if there is a more elegant way to derive B from A ∨ B and ¬A than using or_iff_not_imp_left.mp.

[Reid Barton]

Sebastian Zivota said:

I'm also not happy with the end of the proof of connecting_line_uniq; I wonder if there is a more elegant way to derive B from A ∨ B and ¬A than using or_iff_not_imp_left.mp.

docs#or.resolve_left

[Huỳnh Trần Khanh]

ah, and tauto is also pretty useful for closing simple 1st order logic goals!

[Huỳnh Trần Khanh]

https://leanprover-community.github.io/mathlib_docs/tactics.html#tautology