Pythagorean Theorem With Trig

Stream: maths

[Taylor Belcher]

Hello!
Because of the recent news story on high schoolers proving the pythagorean theorem I found myself looking at Zimba's proof using trig. I am attempting to formalize part of the argument. I made a lot of progress but I have become very stuck today.

--Formalization of Part 4 of Zimba's Proof at this URL: https://forumgeom.fau.edu/FG2009volume9/FG200925.pdf
--Discovered because of the link from Cut The Knot here: https://www.cut-the-knot.org/pythagoras/TrigProof.shtml#Zimba


import data.complex.exponential
import analysis.special_functions.trigonometric.basic
import data.real.basic

-- Define local notation for pi
local notation `π` := real.pi
local notation `cos` := real.cos
local notation `sin` := real.sin

--establish that if x,y are in the domain of cosine with y less than x then so is x minus y
lemma trig_bounds (x y : ℝ) (h₁: 0 < x ∧ x < π/2 ) (h₂ : 0 < y ∧ y < x) : 0 < (x-y) ∧ (x-y) < π /2 :=
begin
split,
repeat {linarith,},
end

--apply the subtraction formulas for cosine and sine repeatedly, which are already in Lean
lemma subtraction_to_pythag (x y : ℝ) : cos y = ((sin x)^2 + (cos x)^2) * cos y :=
begin

  have h : cos y = cos (x - (x-y)) :=
    begin
      rw sub_eq_add_neg x (x-y),
      rw neg_eq_neg_one_mul,
      rw mul_sub,
      simp,
    end,
rw h,
rw real.cos_sub x (x-y),
rw real.cos_sub x y,
rw real.sin_sub x y,
--simp "works" here to close the goal but it ends up using the pythagorean theorem to do it
sorry,

end


--just need to do some algebra to imply Pythagoras
lemma pythag_with_trig (x y : ℝ) (h: cos y = ((sin x)^2 + (cos x)^2) * cos y) :  (sin x)^2 + (cos x)^2 = 1 :=
begin
rw mul_comm at h,
apply self_eq_mul_right.1,
end

--connect the above lemma to triangles

Here is the feedback from lean:

invalid apply tactic, failed to unify
sin x ^ 2 + cos x ^ 2 = 1
with
?m_2 = 1

Can anyone help? Thanks!

[Yakov Pechersky]

self_eq_mul_right is only valid for groups, while you're in a field. For example, consider your h, what if cos y is always 0? Then h is true.

[Taylor Belcher]

@Yakov Pechersky
Thank you, this is helpful.

It looks like somewhere in the proof I need to confirm that cos y will be in the interval (0,1) because that is what I want for this proof.

And also I will look for an equivalent version of self_eq_mul_right in a field.

[David Michael Roberts]

I've heard mutterings about this, but seen no link to an actual paper. Can someone supply?

[Felix Weilacher]

This video attempts to reconstruct the proof from an image of the presentation. It's the best I've been able to find.
https://www.youtube.com/watch?v=nQD6lDwFmCc

[Taylor Belcher]

The Zimba proof I have in the comments in the code is the older one. The recent proof from the two high schoolers I have not seen.

[Taylor Belcher]

I found an issue in my code by the way. Lean was using the pythagorean theorem in simp. But I have fixed it. Still working on that issue and the issues from before.

[Kevin Buzzard]

I find these "prove true thing X without assuming a proof of true thing Y" questions very difficult to formalise. I wonder if this is somehow an informal notion, like the Langlands correspondence being canonical

[Felix Weilacher]

I guess it's not exactly what is meant in this Pythagorean theorem example, but reverse math is one way to formalize such questions.

[Taylor Belcher]

I fixed some issues, but there are still others.

--Formalization of Part 4 of Zimba's Proof at this URL: https://forumgeom.fau.edu/FG2009volume9/FG200925.pdf
--Discovered because of the link from Cut The Knot here: https://www.cut-the-knot.org/pythagoras/TrigProof.shtml#Zimba


import data.complex.exponential
import analysis.special_functions.trigonometric.basic
import data.real.basic

variables (x y : ℝ )

-- Define local notation for pi
local notation `π` := real.pi
local notation `cos` := real.cos
local notation `sin` := real.sin

#check cos y
#check sin x



--establish that if x,y are in the domain of cosine with y less than x then so is x minus y
lemma input_bounds (x y : ℝ) (h₁: 0 < x ∧ x < π/2 ) (h₂ : 0 < y ∧ y < x) : 0 < (x-y) ∧ (x-y) < π /2 :=
begin
split,
repeat {linarith,},
end

--establish domain and range of real cos without using the pythagorean theorem
lemma cos_range (x:ℝ) (h: 0 < x ∧ x < π/2 ) : 0 < cos x ∧ cos x < 1  :=
--lean does not appear to be recognizing cos x as a real number
begin
sorry,
end

--establish domain and range of sin without using the pythagorean theorem
lemma sin_range (x:ℝ) (h: 0 < x ∧ x < π/2 ) : 0 < sin x ∧ sin x < 1  :=
--lean does not appear to be recognizing sin x as a real number
begin
sorry,
end

--apply the subtraction formulas for cosine and sine repeatedly, which are already in Lean
lemma subtraction_to_pythag : ∀ x y : ℝ, cos y = ((sin x)^2 + (cos x)^2) * cos y :=
begin

--I think I need to add an intros here but I am still having issues with pattern matching later.
intros x y,


  have h : cos y = cos (x - (x-y)) :=
    begin
      rw sub_eq_add_neg x (x-y),
      rw neg_eq_neg_one_mul,
      rw mul_sub,
      simp only [neg_mul, one_mul, neg_sub_neg, add_sub_cancel'_right],
    end,
conv
  begin
    to_lhs,
    rw h,
  end,
rw real.cos_sub x (x-y),
rw real.cos_sub x y,
rw real.sin_sub x y,
rw mul_add,
rw mul_sub,
rw add_comm,
rw ← mul_assoc (sin x),
rw ← mul_assoc (sin x),
rw ← mul_assoc (cos x),
rw ← mul_assoc (cos x),
rw mul_comm (cos x) (sin x),
conv
  begin
    to_lhs,
    simp,
  end,
rw add_mul,
rw pow_two,
rw pow_two,
end


--just need to do some algebra to imply Pythagoras
lemma pythag_with_trig (x y : ℝ) :  (sin x)^2 + (cos x)^2 = 1 :=
begin

have h : cos y = cos y * ((sin x)^2 + (cos x)^2) :=
  begin
  --exact subtraction_to_pythag,
  sorry,
  end,
sorry,
end

--connect the above lemma to triangles