MohanadAhmed

Stream: new members

[MohanadAhmed]

Hello everyone
New one here.
Just started learning lean. Hoping this would be fun.
Went through tutorials at https://github.com/leanprover-community/tutorials
And then though I would start with school geometry like showing that angles of equilateral triangle are all pi/3
Any comments are welcome.

(Not sure how to post code directly so attaching it)

equi_traingle.lean

Thanks and looking forward to learning.

[Patrick Johnson]

See #backticks to learn how to post code directly.

[MohanadAhmed]

lemma equi_triangle_pi_3 {p1 p2 p3 : P}
  (h1 : dist p1 p2 = dist p1 p3) (h2: dist p2 p1 = dist p2 p3)
  (ha : p2 ≠ p1) (hb : p3 ≠ p1) :
    ∠ p1 p2 p3 = (π / 3) ∧ ∠ p1 p3 p2 = π / 3 ∧ ∠ p2 p1 p3 = π / 3 :=
begin
  have eq12 : ∠ p1 p2 p3 = ∠ p1 p3 p2 ∧ ∠ p2 p1 p3 = ∠ p2 p3 p1,
    {apply equi_triangle h1 h2},
  cases eq12 with eq1 eq2,
  have eqx : ∠ p1 p3 p2 = ∠ p2 p3 p1,
        {apply euclidean_geometry.angle_comm},
  have eqy : ∠ p3 p1 p2 = ∠ p2 p1 p3,
        {apply euclidean_geometry.angle_comm},
  have eqπ : ∠ p1 p2 p3 + ∠ p2 p3 p1 + ∠ p3 p1 p2 = π,
        {apply euclidean_geometry.angle_add_angle_add_angle_eq_pi ha hb},
  rw eq1 at eqπ,
  rw eqx at eqπ,
  rw eqy at eqπ,
  rw eq2 at eqπ,
  have xp3: ∠ p2 p3 p1 = π / 3, {by linarith},
  rw xp3 at eq2,
  rw ← eqx at xp3,
  rw xp3 at eq1,
  split, {linarith}, {split, {linarith}, {linarith}},
end

[MohanadAhmed]

Thanks a lot @Patrick Johnson

[Julian Berman]

Welcome! I'm sure one can do even better, but angle brackets are cool, and the tactic#rintro and tactic#rcases tactics are nice.

lemma equi_triangle {p1 p2 p3 : P}
    (h1 : dist p1 p2 = dist p1 p3) (h2: dist p2 p1 = dist p2 p3) :
    ∠ p1 p2 p3 = ∠ p1 p3 p2 ∧ ∠ p2 p1 p3 = ∠ p2 p3 p1:=
    ⟨euclidean_geometry.angle_eq_angle_of_dist_eq h1, euclidean_geometry.angle_eq_angle_

  lemma equi_triangle_pi_3 {p1 p2 p3 : P}
    (h1 : dist p1 p2 = dist p1 p3) (h2: dist p2 p1 = dist p2 p3)
    (ha : p2 ≠ p1) (hb : p3 ≠ p1) :
      ∠ p1 p2 p3 = (π / 3) ∧ ∠ p1 p3 p2 = π / 3 ∧ ∠ p2 p1 p3 = π / 3 :=                   begin
    rcases equi_triangle h1 h2 with ⟨eq1, eq2⟩,
    have eqπ := euclidean_geometry.angle_add_angle_add_angle_eq_pi ha hb,
    have eqx : ∠ p2 p3 p1 = ∠ p1 p3 p2 := euclidean_geometry.angle_comm _ _ _,
    have eqy : ∠ p3 p1 p2 = ∠ p2 p1 p3 := euclidean_geometry.angle_comm _ _ _,
    have xp3 : ∠ p2 p3 p1 = π / 3 := by linarith,
    exact ⟨by linarith, by linarith, by linarith⟩
  end

[Patrick Johnson]

You can use semicolons to reduce duplication. Semicolon applies the tactic on the right to all goals produces by the tactic on the left. For example

split,
{ apply euclidean_geometry.angle_eq_angle_of_dist_eq h1 },
{ apply euclidean_geometry.angle_eq_angle_of_dist_eq h2 },

becomes:

split; apply euclidean_geometry.angle_eq_angle_of_dist_eq; assumption,

tactic#assumption closes the goal using an appropriate assumption. Also note that

split, {linarith}, {split, {linarith}, {linarith}},

can be simplified to

refine ⟨_, _, _⟩; linarith,

Tactic linarith takes an optional list of assumptions as argument, so you don't need so much have statements and you don't even need equi_triangle lemma. Here is a simplified proof:

import geometry.euclidean.triangle
open euclidean_geometry
open_locale euclidean_geometry
open_locale real

lemma equi_triangle_pi_3 {V P : Type*}
  [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P]
  {p1 p2 p3 : P}
  (h1 : dist p1 p2 = dist p1 p3) (h2: dist p2 p1 = dist p2 p3)
  (ha : p2 ≠ p1) (hb : p3 ≠ p1) :
  ∠ p1 p2 p3 = π / 3 ∧ ∠ p1 p3 p2 = π / 3 ∧ ∠ p2 p1 p3 = π / 3 :=
begin
  refine ⟨_, _, _⟩; linarith
  [ angle_comm p1 p3 p2,
    angle_comm p3 p1 p2,
    angle_eq_angle_of_dist_eq h1,
    angle_eq_angle_of_dist_eq h2,
    angle_add_angle_add_angle_eq_pi ha hb ],
end