Zulip Chat Archive

Stream: new members

Topic: MohanadAhmed

MohanadAhmed (May 14 2022 at 14:06):

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)


Thanks and looking forward to learning.

Patrick Johnson (May 14 2022 at 14:17):

See #backticks to learn how to post code directly.

MohanadAhmed (May 14 2022 at 14:34):

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 :=
  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}},

MohanadAhmed (May 14 2022 at 14:35):

Thanks a lot @Patrick Johnson

Julian Berman (May 14 2022 at 14:59):

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

Patrick Johnson (May 14 2022 at 15:38):

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

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


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 :=
  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 ],

Last updated: Dec 20 2023 at 11:08 UTC