Trying to state Morley’s Theorem

Stream: new members

[Anders Larsson]

I'm working on learning Lean 4 and tried to state Morley’s Theorem from the Coq
proof. And borrowing from https://leanprover-community.github.io/mathlib4_docs/Archive/Wiedijk100Theorems/HeronsFormula.html .

import Mathlib.Geometry.Euclidean.Triangle

def equilateral {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P]
  (p1 p2 p3 : P ) : Prop :=
    p1 ≠ p2 ∧
    p2 ≠ p3 ∧
    dist p1 p2 = dist p1 p3 ∧
    dist p1 p2 = dist p2 p3

theorem morley {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P]
  {a b c : ℝ } {A B C R Q T : P} :
  0 < a →
  0 < b →
  0 < c →
  (a + b + c) * 3 = Real.pi →
  A ≠ B →
  A ≠ C →
  B ≠ C →
  B ≠ R →
  B ≠ Q →
  A ≠ T →
  C ≠ T →
  b = (EuclideanGeometry.angle B C R) →
  b = (EuclideanGeometry.angle B R Q) →
  b = (EuclideanGeometry.angle B Q A) →
  c = (EuclideanGeometry.angle C R B) →
  c = (EuclideanGeometry.angle C T R) →
  a = (EuclideanGeometry.angle A B Q) →
  a = (EuclideanGeometry.angle A Q T) →
  a = (EuclideanGeometry.angle A T C) →
  equilateral R Q T := by
  admit

/-
The Coq Freek 100 theorem statement:

Theorem Morley:
  forall (a b c : R) (A B C P Q T : PO),
  0 < a ->
  0 < b ->
  0 < c ->
  (a + b) + c = pisurtrois ->
  A <> B ->
  A <> C ->
  B <> C ->
  B <> P ->
  B <> Q ->
  A <> T ->
  C <> T ->
  image_angle b = cons_AV (vec B C) (vec B P) ->
  image_angle b = cons_AV (vec B P) (vec B Q) ->
  image_angle b = cons_AV (vec B Q) (vec B A) ->
  image_angle c = cons_AV (vec C P) (vec C B) ->
  image_angle c = cons_AV (vec C T) (vec C P) ->
  image_angle a = cons_AV (vec A B) (vec A Q) ->
  image_angle a = cons_AV (vec A Q) (vec A T) ->
  image_angle a = cons_AV (vec A T) (vec A C) -> equilateral P Q T.
-/

[Johan Commelin]

I guess you need to assume that all those points lie in a 2-dim subspace?

[Johan Commelin]

Also, if you open EuclideanGeometry, then you can simply write angle

[Anders Larsson]

open EuclideanGeometry really improved readability!

import Mathlib.Geometry.Euclidean.Triangle

def equilateral {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P]
  (p1 p2 p3 : P ) : Prop :=
    p1 ≠ p2 ∧
    p2 ≠ p3 ∧
    dist p1 p2 = dist p1 p3 ∧
    dist p1 p2 = dist p2 p3


open EuclideanGeometry

theorem morley {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P]
  {a b c : ℝ } {A B C R Q T : P} :
  0 < a →
  0 < b →
  0 < c →
  (a + b + c) * 3 = Real.pi →
  A ≠ B →
  A ≠ C →
  B ≠ C →
  B ≠ R →
  B ≠ Q →
  A ≠ T →
  C ≠ T →
  b = ∠ B C R →
  b = ∠ B R Q →
  b = ∠ B Q A →
  c = ∠ C R B →
  c = ∠ C T R →
  a = ∠ A B Q →
  a = ∠ A Q T →
  a = ∠ A T C →
  equilateral R Q T := sorry

I guess you need to assume that all those points lie in a 2-dim subspace?

You are right. The Heron's formula statement was just about 3 points in a triangle and the exact middle point between them. So it works in any dimension.

[Eric Wieser]

(note that the playground link is auto-inserted by code blocks, so there is no need to paste unreadable links to it)

[Anders Larsson]

That's nice. The Lean has come a long way since I started looking at Lean 3 during the pandemic.

[Eric Wieser]

You can also write ∠ A B C instead of angle A B C

[Anders Larsson]

Nifty (I updated the the post above).

I haven't read up on all the spaces but I would like to know that I'm really in a flat space where the angles of triangles actually sums to 180 degrees.

[Yaël Dillies]

Anders Larsson said:

I would like to know that I'm really in a flat space where the angles of triangles actually sums to 180 degrees.

What you should do then is finding the lemma "Angles of triangles sum to 180 degrees" in mathlib and see what it assumes.

[Eric Wieser]

docs#EuclideanGeometry.angle_add_angle_add_angle_eq_pi tells you what those assumptions are

[Yaël Dillies]

Note that it doesn't hold only in two dimensions so maybe you should find a better property that you want to be true but might only be in 2D

[Anders Larsson]

I think this:

(a + b + c) * 3 = Real.pi →

forces the inner points R, Q, T into the same plane as the outher points A, B and C, regardless of if we formally are in something like R^2 or not.
But that's maybe too unhelpful for a reader.

[Johan Commelin]

I think you are right.

[Johan Commelin]

Just add a half-line comment. Should be enough.

[Joseph Myers]

Anders Larsson said:

def equilateral {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V]
  [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P]
  (p1 p2 p3 : P ) : Prop :=
    p1 ≠ p2 ∧
    p2 ≠ p3 ∧
    dist p1 p2 = dist p1 p3 ∧
    dist p1 p2 = dist p2 p3

I think equilateral might better be defined as a property of an arbitrary indexed family of points in a PseudoEMetricSpace rather than just for three points in a Euclidean context.

  {a b c : ℝ } {A B C R Q T : P} :
  0 < a →
  0 < b →
  0 < c →
  (a + b + c) * 3 = Real.pi →
  A ≠ B →
  A ≠ C →
  B ≠ C →

And then state the result for a Triangle (referring to its vertices as t.points 0 etc.), so avoiding needing to give various nondegeneracy conditions here.

  b = ∠ B C R →
  b = ∠ B R Q →
  b = ∠ B Q A →

And then state that various angles are ∠ (t.points 0) (t.points 1) (t.points 2) / 3, so eliminating a, b, c (note: the angles at B should have B as the second argument to ∠, not the first).

The fact that if ∠ a b c + ∠ c b d = ∠ a b d then (possibly with some nondegeneracy conditions required) you have coplanarity would be an early lemma to add to mathlib - probably first proving a corresponding statement for vectors (see the existing proof_wanted angle_triangle for a corresponding inequality).