Highschool Euclidean geometry?

Stream: new members

[Ilmārs Cīrulis]

(While Mathlib is building...)

1) Let's suppose I want to prove the Pythagorean theorem from the axioms of Euclidean geometry... Which set of notions and axioms about them should I choose for the use with Lean/Mathlib? :sweat_smile: Of course, if this question even makes sense.
2) Highschool/synthetic geometry (starting from simple exercises and, probably, ending with olympiad geometry) - how much does Mathlib support it?

[Chase Norman]

Mathlib should probably not be building. Run “lake update Mathlib” to download the cached version.

[Ilmārs Cīrulis]

I'm working on one tiny PR to Mathlib, that's the reason I had to build it.

[Chase Norman]

Ah, sorry. It always tripped me up early on

[(deleted)]

2) there is no support. I don't even see code for triangle similarity

[Aaron Liu]

We have angles I think

[Ilmārs Cīrulis]

#Is there code for X? > Euclidean Geometry - found this topic, reading it currently.

[Weiyi Wang]

I don't even see code for triangle similarity

At least we got triangle congruence not long ago https://leanprover-community.github.io/mathlib4_docs/Mathlib/Geometry/Euclidean/Congruence.html

[Alex Kontorovich]

Have a look at #7300, which proves the Pythagorean theorem from synthetic Euclidean-style axioms (due to Avigad)

[Ilmārs Cīrulis]

For anyone interested, the axiomatic system used at #7300 should be from https://www.andrew.cmu.edu/user/avigad/Papers/formal_system_for_euclids_elements.pdf, it seems

(I didn't find any reference to it in the development)

[Ilmārs Cīrulis]

I will put this here, as I don't want to make a new conversation.

I was in mood for some tinkering and tried to formalize part of the BIrkhoff's axioms for Euclidean geometry - about points and lines.
It's kinda a variation of the theme, with inspiration from "Birkhoff's Axioms for Space Geometry" by Roland Brossard.

import Mathlib

structure ruler {point line : Type} (point_belongs_to_line : point → line → Prop) where
  get_coordinate : line → point → ℝ
  get_point : line → ℝ → point
  get_point_property : ∀ (L : line) (x : ℝ), point_belongs_to_line (get_point L x) L
  coordinate_function_bijective_1 : ∀ {p : point} {L : line},
    point_belongs_to_line p L → get_point L (get_coordinate L p) = p
  coordinate_function_bijective_2 : ∀ (x : ℝ) (L : line), get_coordinate L (get_point L x) = x

def ruler.distance {point line point_belongs_to_line}
    (R : @ruler point line point_belongs_to_line) : line → point → point → ℝ :=
  fun L p1 p2 => abs (R.get_coordinate L p1 - R.get_coordinate L p2)

-- just the beginning part of the axioms for now
structure Birkhoff_geometry_axioms_kinda'' where
  point : Type
  point_A : point
  point_B : point

  line : Type
  line_through_two_points : point → point → line
  point_belongs_to_line : point → line → Prop
  point_not_on_line : line → point

  all_rulers : Set (ruler point_belongs_to_line)
  given_ruler : ruler point_belongs_to_line

  two_distinct_points : point_A ≠ point_B
  two_points_belong_to_line_through_them : ∀ (p1 p2 : point),
    point_belongs_to_line p1 (line_through_two_points p1 p2) ∧
    point_belongs_to_line p2 (line_through_two_points p1 p2)
  unique_line_through_two_distinct_points : ∀ {p1 p2 : point} {L : line},
    p1 ≠ p2 → point_belongs_to_line p1 L → point_belongs_to_line p2 L →
    L = line_through_two_points p1 p2
  point_not_on_line_property : ∀ (L : line), ¬ point_belongs_to_line (point_not_on_line L) L

  rulers_nonempty : given_ruler ∈ all_rulers
  same_distances : ∀ {R: ruler point_belongs_to_line}, R ∈ all_rulers →
    ∀ {L : line} {p1 p2 : point},
    point_belongs_to_line p1 L → point_belongs_to_line p2 L →
    R.distance L p1 p2 = given_ruler.distance L p1 p2

1) Is this style okay?
2) Does it make mathematical sense?

EDIT: defined structure for ruler, the notion of distance for it etc., more closely following idea of Birkhoff.

[Ilmārs Cīrulis]

Is there a way to automatize/golf this proof?

import Mathlib

theorem aux (x y z : ℝ) :
    (x ≤ y ∧ y ≤ z ∨ z ≤ y ∧ y ≤ x) ↔ abs (x - y) + abs (y - z) = abs (x - z) := by
  constructor <;> intro H
  · obtain ⟨H, H0⟩ | ⟨H, H0⟩ := H
    · have H1 := ge_trans H0 H
      rw [← sub_nonpos] at H H0 H1
      rw [abs_of_nonpos H, abs_of_nonpos H0, abs_of_nonpos H1]
      simp only [neg_sub, sub_add_sub_cancel']
    · have H1 := le_trans H H0
      rw [← sub_nonneg] at H H0 H1
      rw [abs_of_nonneg H, abs_of_nonneg H0, abs_of_nonneg H1]
      simp only [sub_add_sub_cancel]
  · obtain H0 | H0 := lt_or_ge (x - y) 0 <;>
    obtain H1 | H1 := lt_or_ge (y - z) 0 <;>
    obtain H2 | H2 := lt_or_ge (x - z) 0
    · simp at *
      left; constructor
      · exact le_of_lt H0
      · exact le_of_lt H1
    · linarith
    · rw [abs_of_neg H0, abs_of_nonneg H1, abs_of_neg H2] at H
      simp at *
      have H3 : y = z := by linarith
      simp_all
      exact LinearOrder.le_total x z
    · rw [abs_of_neg H0, abs_of_nonneg H1, abs_of_nonneg H2] at H
      linarith
    · rw [abs_of_nonneg H0, abs_of_neg H1, abs_of_neg H2] at H
      simp at *
      have H3 : y = x := by linarith
      simp_all
      exact LinearOrder.le_total x z
    · rw [abs_of_nonneg H0, abs_of_neg H1, abs_of_nonneg H2] at H
      linarith
    · linarith
    · simp_all

[Ilmārs Cīrulis]

Woop! There it is! :partying_face:

import Mathlib

theorem abs_as_ite (x : ℝ) : abs x = if 0 ≤ x then x else - x := by
  split_ifs <;> rename_i H
  · exact abs_of_nonneg H
  · simp only [not_le, abs_eq_neg_self] at *
    exact le_of_lt H

theorem aux (x y z : ℝ) :
    (x ≤ y ∧ y ≤ z ∨ z ≤ y ∧ y ≤ x) ↔ abs (x - y) + abs (y - z) = abs (x - z) := by
  rw [abs_as_ite, abs_as_ite, abs_as_ite]
  split_ifs <;> grind

[Ruben Van de Velde]

docs#abs_cases?

[Ilmārs Cīrulis]

That works too, thank you!

import Mathlib

theorem aux' (x y z : ℝ) :
    (x ≤ y ∧ y ≤ z ∨ z ≤ y ∧ y ≤ x) ↔ abs (x - y) + abs (y - z) = abs (x - z) := by
  obtain H1 | H1 := abs_cases (x - y) <;>
  obtain H2 | H2 := abs_cases (y - z) <;>
  obtain H3 | H3 := abs_cases (x - z) <;> grind

[Ilmārs Cīrulis]

(deleted)

[Ilmārs Cīrulis]

(deleted)

[Ilmārs Cīrulis]

(deleted)

[Ilmārs Cīrulis]

(deleted)