diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.5.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.5.lean index 35fb5a6a..a34486c5 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.5.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.5.lean @@ -95,13 +95,13 @@ As a consequence, we know that $PQRS$ is a parallelogram. -- Since $P$ lies on $AB$, we have $AP, AB$ are of the same direction, _= (SEG_nd e.A e.B B_ne_A).toDir := by symm; - exact eq_todir_of_lies_int_seg_nd e.A e.B e.P B_ne_A e.P_int_AB + exact SegND.toDir_eq_of_lies_int e.A e.B e.P B_ne_A e.P_int_AB -- in parallelogram $ABCD$, we have $AB, DC$ are of the same direction, _= (SEG_nd e.D e.C C_ne_D).toDir := todir_eq_of_is_prg_nd e.A e.B e.C e.D e.hprgnd B_ne_A C_ne_D -- $CD, DC$ are of the opposite direction because of symmetry, _= - (SEG_nd e.C e.D C_ne_D.symm).toDir := by apply SegND.toDir_of_rev_eq_neg_toDir (seg_nd := (SEG_nd e.C e.D C_ne_D.symm)) -- since $R$ lies on $CD$, we have $CR, CD$ are of the same direction, - _= - (SEG_nd e.C e.R R_ne_C).toDir := by simp only [eq_todir_of_lies_int_seg_nd e.C e.D e.R C_ne_D.symm e.R_int_CD] + _= - (SEG_nd e.C e.R R_ne_C).toDir := by simp only [SegND.toDir_eq_of_lies_int e.C e.D e.R C_ne_D.symm e.R_int_CD] -- $CR, RC$ are of the opposite direction because of symmetry. _= (SEG_nd e.R e.C R_ne_C.symm).toDir := by symm; apply SegND.toDir_of_rev_eq_neg_toDir (seg_nd := (SEG_nd e.C e.R R_ne_C)) -- We have $AP = RC$. @@ -125,13 +125,13 @@ As a consequence, we know that $PQRS$ is a parallelogram. -- Since $S$ lies on $AD$, we have $AS, AD$ are of the same direction, _= (SEG_nd e.A e.D D_ne_A).toDir := by symm; - exact eq_todir_of_lies_int_seg_nd e.A e.D e.S D_ne_A S_int_AD + exact SegND.toDir_eq_of_lies_int e.A e.D e.S D_ne_A S_int_AD -- in parallelogram $ABCD$, we have $AD, BC$ are of the same direction, _= (SEG_nd e.B e.C C_ne_B).toDir := todir_eq_of_is_prg_nd_variant e.A e.B e.C e.D e.hprgnd D_ne_A C_ne_B -- $BC, CB$ are of the opposite direction because of symmetry, _= - (SEG_nd e.C e.B C_ne_B.symm).toDir := by apply SegND.toDir_of_rev_eq_neg_toDir (seg_nd := (SEG_nd e.C e.B C_ne_B.symm)) -- since $Q$ lies on $CB$, we have $CQ, CB$ are of the same direction, - _= - (SEG_nd e.C e.Q Q_ne_C).toDir := by simp only [eq_todir_of_lies_int_seg_nd e.C e.B e.Q C_ne_B.symm Q_int_CB] + _= - (SEG_nd e.C e.Q Q_ne_C).toDir := by simp only [SegND.toDir_eq_of_lies_int e.C e.B e.Q C_ne_B.symm Q_int_CB] -- $CQ, QC$ are of the opposite direction because of symmetry. _= (SEG_nd e.Q e.C Q_ne_C.symm).toDir := by symm; apply SegND.toDir_of_rev_eq_neg_toDir (seg_nd := (SEG_nd e.C e.Q Q_ne_C)) -- We have $AS = QC$. @@ -169,7 +169,7 @@ As a consequence, we know that $PQRS$ is a parallelogram. _= (SEG e.S e.Q).midpoint := by exact eq_midpt_of_diag_inx_of_is_prg_nd'_variant isprgnd_ASCQ -- the midpoint of $SQ$ is the same as the midpoint of $QS$ by symmetry. - _= (SEG e.Q e.S).midpoint := midpt_of_rev_eq_midpt e.S e.Q + _= (SEG e.Q e.S).midpoint := (SEG e.Q e.S).reverse_midpt_eq_midpt -- We have that $ABCD$ is convex, since it's a nondegenerate parallelogram. have hprgnd' : (QDR e.A e.B e.C e.D) IsPRG_nd := e.hprgnd have cvx_ABCD : (QDR e.A e.B e.C e.D).IsConvex := by diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.7.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.7.lean index a0245cec..c120b55b 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.7.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.7.lean @@ -82,7 +82,6 @@ Therefore, $DX = EY$. have E_int_ray_CB : e.E LiesInt (RAY e.C e.B C_ne_B.symm) := by -- It suffices to prove that $E$ lies on segment $CB$. apply SegND.lies_int_toRay_of_lies_int (seg_nd := (SEG_nd e.C e.B C_ne_B.symm)) - apply lies_int_seg_nd_of_lies_int_seg e.C e.B e.E C_ne_B.symm _ -- By symmetry, we only need to show that $E$ lies on segment $BC$, apply (Seg.lies_int_rev_iff_lies_int (seg := (SEG e.B e.C))).mpr -- which is what we already know. @@ -115,7 +114,7 @@ Therefore, $DX = EY$. -- It suffices to prove that $D$ lies on segment $BC$. apply SegND.lies_int_toRay_of_lies_int (seg_nd := (SEG_nd e.B e.C C_ne_B)) -- which is what we already know. - exact lies_int_seg_nd_of_lies_int_seg e.B e.C e.D C_ne_B e.D_int_BC + exact e.D_int_BC -- We have that $X$ lies on ray $BA$. have X_int_ray_BA : e.X LiesInt (RAY e.B e.A A_ne_B) := by simp only [e.hd, Line.line_of_pt_pt_eq_rev A_ne_B.symm] diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.8.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.8.lean index c0141835..8db1964a 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.8.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.8.lean @@ -89,8 +89,8 @@ Therefore, $BD = CE$. -- Since $D$ lies on the extension of $BC$, we know that $\angle DBA$ is the same as $\angle CBA$. _= ∠ e.C e.B e.A B_ne_C.symm e.A_ne_B := by symm; - apply Angle.value_eq_of_lies_on_ray_pt_pt (e.B_ne_C.symm) e.A_ne_B D_ne_B e.A_ne_B - · exact lies_int_toray_of_lies_int_ext_of_seg_nd e.B e.C e.D e.B_ne_C.symm e.D_int_BC_ext + apply Angle.value_eq_of_lies_on_ray_pt_pt e.A_ne_B D_ne_B e.A_ne_B + · exact lies_int_toRay_of_lies_int_extn e.B e.C e.D e.B_ne_C.symm e.D_int_BC_ext · exact Ray.snd_pt_lies_int_mk_pt_pt e.B e.A e.A_ne_B -- In regular triangle $ABC$, $\angle CBA = \angle ACB$. _= ∠ e.A e.C e.B A_ne_C e.B_ne_C := by @@ -99,7 +99,7 @@ Therefore, $BD = CE$. -- Since $E$ lies on the extension of $CA$, we know that $\angle BCA$ is the same as $\angle ECB$. _= ∠ e.E e.C e.B E_ne_C e.B_ne_C := by apply Angle.value_eq_of_lies_on_ray_pt_pt A_ne_C e.B_ne_C E_ne_C e.B_ne_C - · exact lies_int_toray_of_lies_int_ext_of_seg_nd e.C e.A e.E A_ne_C e.E_int_CA_ext + · exact lies_int_toRay_of_lies_int_extn e.C e.A e.E A_ne_C e.E_int_CA_ext · exact Ray.snd_pt_lies_int_mk_pt_pt e.C e.B e.B_ne_C -- We have $BD = CE$. have BD_eq_CE : (SEG e.B e.D).length = (SEG e.C e.E).length := by diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.9.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.9.lean index 98c646b8..bd0b6cc4 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.9.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.9.lean @@ -9,6 +9,8 @@ namespace Schaum namespace Problem1_9 +open Angle + /- Let $\triangle ABC$ be an isoceles triangle in which $AB = AC$. Let $E$ be a point on the extension of $BA$.Let X be a point on the ray through $A$ with the same direction to $\vec{BC}$. @@ -113,7 +115,7 @@ Therefore, $\angle EAX = \angle ABC = - \angle ACB = \angle XAC$. calc ∠ e.E e.A e.X e.E_ne_A e.X_ne_A -- As $AE$ has the same direction as $BA$ and that $AX$ has the same direction as $BC$, we know that $\angle EAX = \angle ABC$, - _= ∠ e.A e.B e.C e.B_ne_A.symm e.C_ne_B := ang_eq_ang_of_toDir_eq_toDir dir_AE_eq_dir_BA dir_AX_eq_dir_BC + _= ∠ e.A e.B e.C e.B_ne_A.symm e.C_ne_B := value_eq_of_dir_eq dir_AE_eq_dir_BA dir_AX_eq_dir_BC -- $\angle ABC = - \angle CBA$ by symmetry, _= - ∠ e.C e.B e.A e.C_ne_B e.B_ne_A.symm := by exact neg_value_of_rev_ang e.B_ne_A.symm e.C_ne_B -- $ - \angle CBA = - \angle ACB$ because $\angle CBA = \angle ACB$ in the isoceles triangle $ABC$, diff --git a/EuclideanGeometry/Example/ShanZun/Ex1a.lean b/EuclideanGeometry/Example/ShanZun/Ex1a.lean index 162575ac..97dc9a0b 100644 --- a/EuclideanGeometry/Example/ShanZun/Ex1a.lean +++ b/EuclideanGeometry/Example/ShanZun/Ex1a.lean @@ -30,10 +30,8 @@ variable {E : P} {he : E = (SEG A B).midpoint} theorem Shan_Problem_1_3 : (SEG C D).length = 2 * (SEG C E).length := by -- Extend $AC$ to $F$ such that $CF = AC$ let F := Ray.extpoint (SEG_nd A C c_ne_a).extension (SEG A C).length - have cf_eq_ac : (SEG C F).length = (SEG A C).length := by - apply seg_length_eq_dist_of_extpoint (SEG_nd A C c_ne_a).extension - simp - exact length_nonneg + have cf_eq_ac : (SEG C F).length = (SEG A C).length := + (SEG_nd A C c_ne_a).extension.dist_of_extpoint (SEG A C).length_nonneg -- $\triangle A B F$ is congruent to $\triangle A C D$, so $BF = CD$ have iso : (▵ A B F) ≅ₐ (▵ A C D) := sorry have bf_eq_cd : (SEG B F).length = (SEG C D).length := iso.edge₁ @@ -63,10 +61,8 @@ variable {D : P} {hd : D = perp_foot A (LIN B C B_ne_C.symm)} theorem Shan_Problem_1_4 : (SEG B D).length = (SEG A C).length + (SEG C D).length := by -- Extend $BC$ to $E$ such that $CE = CA$ let E := Ray.extpoint (SEG_nd B C B_ne_C.symm).extension (SEG C A).length - have ce_eq_ca : (SEG C E).length = (SEG C A).length := by - apply seg_length_eq_dist_of_extpoint (SEG_nd B C B_ne_C.symm).extension - simp - exact length_nonneg + have ce_eq_ca : (SEG C E).length = (SEG C A).length := + (SEG_nd B C B_ne_C.symm).extension.dist_of_extpoint (SEG C A).length_nonneg -- $DE = AC + CD$ have de_eq_ac_plus_cd : (SEG D E).length = (SEG A C).length + (SEG C D).length := sorry -- $C A E$ is not colinear diff --git a/EuclideanGeometry/Example/ShanZun/Ex1d.lean b/EuclideanGeometry/Example/ShanZun/Ex1d.lean index 2ecf7265..0dc080db 100644 --- a/EuclideanGeometry/Example/ShanZun/Ex1d.lean +++ b/EuclideanGeometry/Example/ShanZun/Ex1d.lean @@ -86,10 +86,8 @@ theorem Shan_Problem_1_10 : (SEG A D).length = (SEG D C).length := by have a_ne_e : A ≠ E := sorry -- Extend $EA$ to $M$ such that $AM = EC$ let M := Ray.extpoint (SEG_nd E A a_ne_e).extension (SEG E C).length - have am_eq_ec : (SEG A M).length = (SEG E C).length := by - apply seg_length_eq_dist_of_extpoint (SEG_nd E A a_ne_e).extension - simp - exact length_nonneg + have am_eq_ec : (SEG A M).length = (SEG E C).length := + (SEG_nd E A a_ne_e).extension.dist_of_extpoint (SEG E C).length_nonneg -- Claim: $M \ne C$, $B \ne M$ have m_ne_c : M ≠ C := sorry have b_ne_m : B ≠ M := sorry diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Angle.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Angle.lean index a25b517a..b5519818 100644 --- a/EuclideanGeometry/Foundation/Axiom/Basic/Angle.lean +++ b/EuclideanGeometry/Foundation/Axiom/Basic/Angle.lean @@ -418,11 +418,15 @@ theorem isND_iff : θ.IsND ↔ θ ≠ 0 ∧ θ ≠ π := theorem not_isND_iff : ¬ θ.IsND ↔ (θ = 0 ∨ θ = π) := (not_iff_not.mpr θ.isND_iff).trans or_iff_not_and_not.symm -theorem isND_iff_two_nsmul_ne_zero : θ.IsND ↔ 2 • θ ≠ 0 := - (θ.isND_iff).trans (θ.two_nsmul_ne_zero_iff).symm +theorem two_nsmul_ne_zero_iff_isND : 2 • θ ≠ 0 ↔ θ.IsND := + (θ.two_nsmul_ne_zero_iff).trans (θ.isND_iff).symm -theorem not_isND_iff_two_nsmul_eq_zero : ¬ θ.IsND ↔ 2 • θ = 0 := - (θ.not_isND_iff).trans (θ.two_nsmul_eq_zero_iff).symm +theorem two_nsmul_eq_zero_iff_not_isND : 2 • θ = 0 ↔ ¬ θ.IsND := + (θ.two_nsmul_eq_zero_iff).trans (θ.not_isND_iff).symm + +theorem ne_neg_self_iff_isND : θ ≠ - θ ↔ θ.IsND := sorry + +theorem eq_neg_self_iff_not_isND : θ = - θ ↔ ¬ θ.IsND := sorry theorem not_isND_iff_coe : ¬ θ.IsND ↔ θ = (0 : AngDValue) := not_isND_iff.trans (θ.coe_eq_zero_iff).symm @@ -865,7 +869,7 @@ section cos theorem isAcu_iff_zero_lt_cos : θ.IsAcu ↔ 0 < cos θ := (θ.isAcu_iff).trans (θ.zero_lt_cos_iff).symm -theorem isObt_iff_zero_lt_cos : θ.IsObt ↔ cos θ < 0 := +theorem isObt_iff_cos_lt_zero : θ.IsObt ↔ cos θ < 0 := (θ.isObt_iff).trans (θ.cos_lt_zero_iff).symm theorem isRight_iff_cos_eq_zero : θ.IsRight ↔ cos θ = 0 := @@ -898,7 +902,7 @@ theorem not_isRight_of_eq_zero (h : θ = 0) : ¬ θ.IsRight := by exact zero_not_isRight theorem pi_isObt : ∠[π].IsObt := by - simp only [isObt_iff_zero_lt_cos, cos_coe, cos_pi, Left.neg_neg_iff, zero_lt_one] + simp only [isObt_iff_cos_lt_zero, cos_coe, cos_pi, Left.neg_neg_iff, zero_lt_one] theorem pi_not_isAcu : ¬ ∠[π].IsAcu := not_isAcu_of_isObt pi_isObt @@ -926,7 +930,7 @@ theorem neg_isAcu_iff_isAcu : (- θ).IsAcu ↔ θ.IsAcu := by @[simp] theorem neg_isObt_iff_isObt : (- θ).IsObt ↔ θ.IsObt := by - simp only [isObt_iff_zero_lt_cos, cos_neg] + simp only [isObt_iff_cos_lt_zero, cos_neg] @[simp] theorem neg_isRight_iff_isRight : (- θ).IsRight ↔ θ.IsRight := by @@ -938,11 +942,11 @@ section add_pi @[simp] theorem add_pi_isAcu_iff_isObt : (θ + π).IsAcu ↔ θ.IsObt := by - rw [isAcu_iff_zero_lt_cos, cos_add_pi, Left.neg_pos_iff, isObt_iff_zero_lt_cos] + rw [isAcu_iff_zero_lt_cos, cos_add_pi, Left.neg_pos_iff, isObt_iff_cos_lt_zero] @[simp] theorem add_pi_isObt_iff_isAcu : (θ + π).IsObt ↔ θ.IsAcu := by - rw [isAcu_iff_zero_lt_cos, isObt_iff_zero_lt_cos, cos_add_pi, Left.neg_neg_iff] + rw [isAcu_iff_zero_lt_cos, isObt_iff_cos_lt_zero, cos_add_pi, Left.neg_neg_iff] @[simp] theorem add_pi_isRight_iff_isRight : (θ + π).IsRight ↔ θ.IsRight := by @@ -972,11 +976,11 @@ section pi_sub @[simp] theorem pi_sub_isAcu_iff_isObt : (π - θ).IsAcu ↔ θ.IsObt := by - rw [isAcu_iff_zero_lt_cos, cos_pi_sub, Left.neg_pos_iff, isObt_iff_zero_lt_cos] + rw [isAcu_iff_zero_lt_cos, cos_pi_sub, Left.neg_pos_iff, isObt_iff_cos_lt_zero] @[simp] theorem pi_sub_isObt_iff_isAcu : (π - θ).IsObt ↔ θ.IsAcu := by - rw [isAcu_iff_zero_lt_cos, isObt_iff_zero_lt_cos, cos_pi_sub, Left.neg_neg_iff] + rw [isAcu_iff_zero_lt_cos, isObt_iff_cos_lt_zero, cos_pi_sub, Left.neg_neg_iff] @[simp] theorem pi_sub_isRight_iff_isRight : (π - θ).IsRight ↔ θ.IsRight := by @@ -996,7 +1000,7 @@ theorem add_pi_div_two_isPos_iff_isAcu : (θ + ∠[π / 2]).IsPos ↔ θ.IsAcu : rw [isPos_iff_zero_lt_sin, isAcu_iff_zero_lt_cos, sin_add_pi_div_two] theorem add_pi_div_two_isNeg_iff_isObt : (θ + ∠[π / 2]).IsNeg ↔ θ.IsObt := by - rw [isNeg_iff_sin_lt_zero, isObt_iff_zero_lt_cos, sin_add_pi_div_two] + rw [isNeg_iff_sin_lt_zero, isObt_iff_cos_lt_zero, sin_add_pi_div_two] theorem add_pi_div_two_not_isND_iff_isRight : ¬ (θ + ∠[π / 2]).IsND ↔ θ.IsRight := by rw [not_isND_iff_sin_eq_zero, isRight_iff_cos_eq_zero, sin_add_pi_div_two] @@ -1008,7 +1012,7 @@ theorem add_pi_div_two_isAcu_iff_isNeg : (θ + ∠[π / 2]).IsAcu ↔ θ.IsNeg : rw [isNeg_iff_sin_lt_zero, isAcu_iff_zero_lt_cos, cos_add_pi_div_two, Left.neg_pos_iff] theorem add_pi_div_two_isObt_iff_isPos : (θ + ∠[π / 2]).IsObt ↔ θ.IsPos := by - rw [isPos_iff_zero_lt_sin, isObt_iff_zero_lt_cos, cos_add_pi_div_two, Left.neg_neg_iff] + rw [isPos_iff_zero_lt_sin, isObt_iff_cos_lt_zero, cos_add_pi_div_two, Left.neg_neg_iff] theorem add_pi_div_two_isRight_iff_not_isND : (θ + ∠[π / 2]).IsRight ↔ ¬ θ.IsND := by rw [not_isND_iff_sin_eq_zero, isRight_iff_cos_eq_zero, cos_add_pi_div_two, neg_eq_zero] @@ -1017,7 +1021,7 @@ theorem add_pi_div_two_not_isRight_iff_isND : ¬ (θ + ∠[π / 2]).IsRight ↔ rw [isND_iff_sin_ne_zero, isRight_iff_cos_eq_zero, cos_add_pi_div_two, neg_eq_zero] theorem sub_pi_div_two_isPos_iff_isObt : (θ - ∠[π / 2]).IsPos ↔ θ.IsObt := by - rw [isPos_iff_zero_lt_sin, isObt_iff_zero_lt_cos, sin_sub_pi_div_two, Left.neg_pos_iff] + rw [isPos_iff_zero_lt_sin, isObt_iff_cos_lt_zero, sin_sub_pi_div_two, Left.neg_pos_iff] theorem sub_pi_div_two_isNeg_iff_isAcu : (θ - ∠[π / 2]).IsNeg ↔ θ.IsAcu := by rw [isNeg_iff_sin_lt_zero, isAcu_iff_zero_lt_cos, sin_sub_pi_div_two, Left.neg_neg_iff] @@ -1032,7 +1036,7 @@ theorem sub_pi_div_two_isAcu_iff_isPos : (θ - ∠[π / 2]).IsAcu ↔ θ.IsPos : rw [isPos_iff_zero_lt_sin, isAcu_iff_zero_lt_cos, cos_sub_pi_div_two] theorem sub_pi_div_two_isObt_iff_isNeg : (θ - ∠[π / 2]).IsObt ↔ θ.IsNeg := by - rw [isNeg_iff_sin_lt_zero, isObt_iff_zero_lt_cos, cos_sub_pi_div_two] + rw [isNeg_iff_sin_lt_zero, isObt_iff_cos_lt_zero, cos_sub_pi_div_two] theorem sub_pi_div_two_isRight_iff_not_isND : (θ - ∠[π / 2]).IsRight ↔ ¬ θ.IsND := by rw [not_isND_iff_sin_eq_zero, isRight_iff_cos_eq_zero, cos_sub_pi_div_two] @@ -1044,7 +1048,7 @@ theorem pi_div_two_sub_isPos_iff_isAcu : (∠[π / 2] - θ).IsPos ↔ θ.IsAcu : rw [isPos_iff_zero_lt_sin, isAcu_iff_zero_lt_cos, sin_pi_div_two_sub] theorem pi_div_two_sub_isNeg_iff_isAcu : (∠[π / 2] - θ).IsNeg ↔ θ.IsObt := by - rw [isNeg_iff_sin_lt_zero, isObt_iff_zero_lt_cos, sin_pi_div_two_sub] + rw [isNeg_iff_sin_lt_zero, isObt_iff_cos_lt_zero, sin_pi_div_two_sub] theorem pi_div_two_sub_not_isND_iff_isRight : ¬ (∠[π / 2] - θ).IsND ↔ θ.IsRight := by rw [not_isND_iff_sin_eq_zero, isRight_iff_cos_eq_zero, sin_pi_div_two_sub] @@ -1056,7 +1060,7 @@ theorem pi_div_two_sub_isAcu_iff_isPos : (∠[π / 2] - θ).IsAcu ↔ θ.IsPos : rw [isPos_iff_zero_lt_sin, isAcu_iff_zero_lt_cos, cos_pi_div_two_sub] theorem pi_div_two_sub_isObt_iff_isNeg : (∠[π / 2] - θ).IsObt ↔ θ.IsNeg := by - rw [isNeg_iff_sin_lt_zero, isObt_iff_zero_lt_cos, cos_pi_div_two_sub] + rw [isNeg_iff_sin_lt_zero, isObt_iff_cos_lt_zero, cos_pi_div_two_sub] theorem pi_div_two_sub_isRight_iff_not_isND : (∠[π / 2] - θ).IsRight ↔ ¬ θ.IsND := by rw [not_isND_iff_sin_eq_zero, isRight_iff_cos_eq_zero, cos_pi_div_two_sub] diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean index 8fbb6255..ac25c480 100644 --- a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean +++ b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean @@ -1634,6 +1634,9 @@ instance : AddTorsor AngDValue Proj where induction p using Proj.ind simp +instance instCircularOrderedAddTorsor : CircularOrderedAddTorsor AngDValue Proj := + AddTorsor.CircularOrderedAddTorsor_of_CircularOrderedAddCommGroup AngDValue Proj + @[pp_dot] def perp (p : Proj) : Proj := ∡[π / 2] +ᵥ p diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean index de656675..e1844e51 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean @@ -133,7 +133,7 @@ theorem mk_pt_pt_lieson {O A : P} [PtNe O A] : A LiesOn (CIR O A) := rfl theorem mk_pt_pt_diam_fst_lieson {A B : P} [_h : PtNe A B] : A LiesOn (mk_pt_pt_diam A B) := by show dist (SEG A B).midpoint A = dist (SEG A B).midpoint B rw [dist_comm, ← Seg.length_eq_dist, ← Seg.length_eq_dist] - exact dist_target_eq_dist_source_of_midpt (seg := (SEG A B)) + exact (SEG A B).dist_target_eq_dist_source_of_midpt theorem mk_pt_pt_diam_snd_lieson {A B : P} [_h : PtNe A B] : B LiesOn (mk_pt_pt_diam A B) := rfl diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean b/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean index 0e7d28a7..5b56d46c 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean @@ -8,7 +8,7 @@ namespace EuclidGeom variable {P : Type _} [EuclideanPlane P] -open DirLC CC +open DirLC CC Angle namespace Circle @@ -123,7 +123,7 @@ lemma tangents_perp₁ {ω : Circle P} {p : P} (h : p LiesOut ω) : (DLIN p (pt_ calc _ = (RAY p (pt_tangent_circle_pts h).left).toProj := rfl _ = (RAY (pt_tangent_circle_pts h).left p).toProj := by apply Ray.toProj_eq_toProj_of_mk_pt_pt - _ = (RAY (pt_tangent_circle_pts h).left ω.center).toProj.perp := dvalue_eq_ang_rays_perp heq₁ + _ = (RAY (pt_tangent_circle_pts h).left ω.center).toProj.perp := dir_perp_iff_dvalue_eq_pi_div_two.mpr heq₁ _ = (RAY ω.center (pt_tangent_circle_pts h).left).toProj.perp := by rw [Ray.toProj_eq_toProj_of_mk_pt_pt] _ = (DLIN ω.center (pt_tangent_circle_pts h).left).toProj.perp := rfl @@ -139,7 +139,7 @@ lemma tangents_perp₂ {ω : Circle P} {p : P} (h : p LiesOut ω) : (DLIN p (pt_ calc _ = (RAY p (pt_tangent_circle_pts h).right).toProj := rfl _ = (RAY (pt_tangent_circle_pts h).right p).toProj := by apply Ray.toProj_eq_toProj_of_mk_pt_pt - _ = (RAY (pt_tangent_circle_pts h).right ω.center).toProj.perp := dvalue_eq_ang_rays_perp heq₂ + _ = (RAY (pt_tangent_circle_pts h).right ω.center).toProj.perp := dir_perp_iff_dvalue_eq_pi_div_two.mpr heq₂ _ = (RAY ω.center (pt_tangent_circle_pts h).right).toProj.perp := by rw [Ray.toProj_eq_toProj_of_mk_pt_pt] _ = (DLIN ω.center (pt_tangent_circle_pts h).right).toProj.perp := rfl diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean b/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean index 74ddaf18..86d44455 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean @@ -9,7 +9,7 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.Basic_ex noncomputable section namespace EuclidGeom -open AngValue +open AngValue Angle @[ext] structure Arc (P : Type _) [EuclideanPlane P] where @@ -133,14 +133,11 @@ theorem cangle_of_complementary_arc_are_opposite (β : Arc P) : β.cangle.value apply neg_value_of_rev_ang theorem antipode_iff_colinear (A B : P) {ω : Circle P} [h : PtNe B A] (h₁ : A LiesOn ω) (h₂ : B LiesOn ω) : Arc.IsAntipode A B h₁ h₂ ↔ colinear ω.center A B := by - constructor - · intro hh - unfold Arc.IsAntipode Arc.cangle Arc.mk_pt_pt_circle Arc.angle_mk_pt_arc at hh - simp at hh - apply colinear_of_angle_eq_pi hh - intro hh haveI : PtNe A ω.center := Circle.pt_lieson_ne_center h₁ haveI : PtNe B ω.center := Circle.pt_lieson_ne_center h₂ + constructor + · exact colinear_of_angle_eq_pi + intro hh show ∠ A ω.center B = π have hl : B LiesOn LIN ω.center A := Line.pt_pt_maximal hh have heq₁ : VEC A ω.center = VEC ω.center B := by @@ -160,7 +157,7 @@ theorem antipode_iff_colinear (A B : P) {ω : Circle P} [h : PtNe B A] (h₁ : A show VEC A ω.center = 2⁻¹ • (VEC A B) rw [heq₂] simp - apply liesint_segnd_value_eq_pi _ hli + exact value_eq_pi_of_lies_int_seg_nd hli theorem mk_pt_pt_diam_isantipode {A B : P} [h : PtNe A B] : Arc.IsAntipode A B (Circle.mk_pt_pt_diam_fst_lieson) (Circle.mk_pt_pt_diam_snd_lieson) := by have hc : colinear (SEG A B).midpoint A B := by diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean index 8b8a7ec8..96e7c93b 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean @@ -69,7 +69,7 @@ lemma dist_pt_line_ineq {l : DirLine P} {ω : Circle P} (h : DirLine.IsIntersect rw [abs_of_nonneg, abs_of_pos] exact this exact ω.rad_pos - exact length_nonneg + exact Seg.length_nonneg linarith def Inxpts {l : DirLine P} {ω : Circle P} (_h : DirLine.IsIntersected l ω) : DirLCInxpts P where @@ -165,8 +165,7 @@ theorem inx_pts_same_iff_tangent {l : DirLine P} {ω : Circle P} (h : DirLine.Is apply dist_pt_line_ineq h apply (sq_eq_sq _ _).mp linarith - unfold dist_pt_line - exact length_nonneg + exact Seg.length_nonneg apply le_iff_lt_or_eq.mpr left; exact ω.rad_pos exfalso diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Colinear.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Colinear.lean index 3ef598b8..20d6d57b 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Colinear.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Colinear.lean @@ -25,12 +25,6 @@ def colinear (A B C : P) : Prop := -- The definition of colinear now includes two cases: the degenerate case and the nondegenerate case. We use to_dir' to avoid problems involving using conditions of an "if" in its "then" and "else". And we only use VEC to define colinear. -theorem toProj_eq_of_colinear {A B C : P} [hba : PtNe B A] [hca : PtNe C A] (h : colinear A B C) : (SEG_nd A B).toProj = (SEG_nd A C).toProj := - if hbc : B = C then by congr - else ((dite_prop_iff_and _).mp h).2 <| by - push_neg - exact ⟨Ne.symm hbc, Fact.out, Fact.out⟩ - /-- Given three points $A$, $B$, $C$ and a real number $t$, if the vector $\overrightarrow{AC}$ is $t$ times the vector $\overrightarrow{AB}$, then $A$, $B$, and $C$ are colinear. -/ theorem colinear_of_vec_eq_smul_vec {A B C : P} {t : ℝ} (e : VEC A C = t • VEC A B) : colinear A B C := by have : colinear A B C = True := by @@ -159,6 +153,15 @@ theorem ne_of_not_colinear {A B C : P} (h : ¬ colinear A B C) : (C ≠ B) ∧ ( rcases h with ⟨g, _⟩ tauto +theorem colinear_iff_toProj_eq_of_ptNe {A B C : P} [hba : PtNe B A] [hca : PtNe C A] : colinear A B C ↔ (VEC_nd A B).toProj = (VEC_nd A C).toProj := by + if hbc : B = C then simp only [hbc, colinear_of_trd_eq_snd A rfl] + else + refine' ⟨fun h ↦ _, fun h ↦ _⟩ + exact ((dite_prop_iff_and _).mp h).2 <| by + push_neg + exact ⟨Ne.symm hbc, hca.1.symm, hba.1⟩ + exact (dite_prop_iff_and _).mpr ⟨fun _ ↦ trivial, fun _ ↦ h⟩ + end colinear section compatibility diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean index e87945bf..bf4b9a47 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean @@ -785,7 +785,7 @@ theorem pt_pt_maximal {A B C : P} [_h : PtNe B A] (Co : colinear A B C) : C Lies exact snd_pt_lies_on_mk_pt_pt else haveI : PtNe C B := ⟨hcb⟩ (lies_on_iff_eq_toProj_of_lies_on snd_pt_lies_on_mk_pt_pt).mpr <| - (toProj_eq_of_colinear (perm_colinear_snd_trd_fst Co)).trans <| + (colinear_iff_toProj_eq_of_ptNe.mp (perm_colinear_snd_trd_fst Co)).trans <| congrArg Line.toProj (line_of_pt_pt_eq_rev (_h := _h)).symm theorem maximal {l : Line P} {A B C : P} (h₁ : A LiesOn l) (h₂ : B LiesOn l) [_h : PtNe B A] (Co : colinear A B C) : C LiesOn l := by diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean index a40cc1a0..3c413835 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean @@ -5,22 +5,12 @@ namespace EuclidGeom variable {P : Type _} [EuclideanPlane P] -theorem ne_source_of_lies_int_seg_nd (A B C : P) [hne : PtNe B A] (h : C LiesInt (SEG_nd A B)) : C ≠ A := by sorry - -theorem ne_source_of_lies_int_seg (A B C : P) (h2 : C LiesInt (SEG A B)) : C ≠ A := by sorry - -theorem eq_todir_of_lies_int_seg_nd (A B C : P) [hne : PtNe B A] (h : C LiesInt (SEG A B)) : (SEG_nd A B).toDir = (SEG_nd A C (ne_source_of_lies_int_seg_nd A B C h)).toDir := by sorry - -theorem lies_int_seg_nd_of_lies_int_seg (A B C : P) [hne : PtNe B A] (h : C LiesInt (SEG A B)) : C LiesInt (SEG_nd A B) := by sorry - -theorem lies_on_seg_nd_of_lies_on_seg (A B C : P) [hne : PtNe B A] (h : C LiesOn (SEG A B)) : C LiesOn (SEG_nd A B) := by sorry - theorem same_dist_eq_or_eq_neg {A B C : P} [hne : PtNe B A] (h : C LiesOn (LIN A B)) (heq : dist A C = dist A B) : (C = B) ∨ (VEC A C = VEC B A) := by have : LIN A B = (RAY A B).toLine := rfl rw [this] at h rcases Ray.lies_on_toLine_iff_lies_on_or_lies_on_rev.mp h with h | h · left; apply (eq_iff_vec_eq_zero _ _).mpr - have : VEC A C = (dist A C) • (RAY A B).2.unitVec := Ray.lieson_eq_dist h + have : VEC A C = (dist A C) • (RAY A B).2.unitVec := Ray.vec_eq_dist_smul_toDir_of_lies_on h calc _ = VEC A C - VEC A B := by rw [vec_sub_vec] _ = (dist A B) • (RAY A B).2.unitVec - VEC A B := by rw [this, heq] @@ -33,7 +23,7 @@ theorem same_dist_eq_or_eq_neg {A B C : P} [hne : PtNe B A] (h : C LiesOn (LIN A rfl right calc - _ = (dist A C) • (RAY A B).reverse.2.unitVec := Ray.lieson_eq_dist h + _ = (dist A C) • (RAY A B).reverse.2.unitVec := Ray.vec_eq_dist_smul_toDir_of_lies_on h _ = (dist A C) • (- (VEC_nd A B).toDir.unitVec) := by simp _ = (dist A B) • (- (VEC_nd A B).toDir.unitVec) := by rw [heq] _ = - (‖VEC_nd A B‖ • (VEC_nd A B).toDir.unitVec) := by @@ -70,8 +60,7 @@ theorem midpoint_dist_eq_iff_eq_endpts {A B C : P} [hne : PtNe B C] (h : A LiesO rcases hh with hh | hh · rw [hh] rw [hh, dist_comm, ← Seg.length_eq_dist, ← Seg.length_eq_dist] - symm - apply dist_target_eq_dist_source_of_midpt (seg := (SEG B C)) + exact ((SEG B C).dist_target_eq_dist_source_of_midpt).symm theorem midpoint_dist_gt_iff_liesout {A B C : P} [hne : PtNe B C] (h : A LiesOn (LIN B C)) : dist A (SEG B C).midpoint > dist B (SEG B C).midpoint ↔ ¬ (A LiesOn (SEG B C)) := by apply Iff.not_right @@ -101,11 +90,13 @@ theorem liesint_segnd_iff_lieson_ray_reverse {A B C : P} [hne₁ : PtNe B C] [hn theorem not_lies_on_segnd_iff_lieson_ray {A B C : P} [hne₁ : PtNe B C] [hne₂ : PtNe A B] (h : A LiesOn (LIN B C)) : ¬ (A LiesOn (SEG B C)) ↔ C LiesOn (RAY A B) := sorry --Guan Nailin -theorem ne_vertex_of_lies_int_seg_nd {seg_nd : SegND P} {A : P} (h : A LiesInt seg_nd) : (A ≠ seg_nd.source) ∧ (A ≠ seg_nd.target) := by sorry -theorem eq_toDir_of_source_to_pt_lies_int {seg_nd : SegND P} {A : P} (h : A LiesInt seg_nd) : (SEG_nd seg_nd.source A (ne_vertex_of_lies_int_seg_nd h).1).toDir = seg_nd.toDir := by sorry -theorem eq_toDirLine_of_source_to_pt_lies_int {seg_nd : SegND P} {A : P} (h : A LiesInt seg_nd) : (SEG_nd seg_nd.source A (ne_vertex_of_lies_int_seg_nd h).1).toDirLine = seg_nd.toDirLine := by sorry -theorem eq_toDir_of_pt_lies_int_to_target {seg_nd : SegND P} {A : P} (h : A LiesInt seg_nd) : (SEG_nd A seg_nd.target (ne_vertex_of_lies_int_seg_nd h).2.symm).toDir = seg_nd.toDir := by sorry -theorem eq_toDirLine_of_pt_lies_int_to_target {seg_nd : SegND P} {A : P} (h : A LiesInt seg_nd) : (SEG_nd A seg_nd.target (ne_vertex_of_lies_int_seg_nd h).2.symm).toDirLine = seg_nd.toDirLine := by sorry +theorem eq_toDir_of_source_to_pt_lies_int {seg_nd : SegND P} {A : P} (h : A LiesInt seg_nd) : (SEG_nd seg_nd.source A h.ne_source).toDir = seg_nd.toDir := by sorry + +theorem eq_toDirLine_of_source_to_pt_lies_int {seg_nd : SegND P} {A : P} (h : A LiesInt seg_nd) : (SEG_nd seg_nd.source A h.ne_source).toDirLine = seg_nd.toDirLine := by sorry + +theorem eq_toDir_of_pt_lies_int_to_target {seg_nd : SegND P} {A : P} (h : A LiesInt seg_nd) : (SEG_nd A seg_nd.target h.ne_target.symm).toDir = seg_nd.toDir := by sorry + +theorem eq_toDirLine_of_pt_lies_int_to_target {seg_nd : SegND P} {A : P} (h : A LiesInt seg_nd) : (SEG_nd A seg_nd.target h.ne_target.symm).toDirLine = seg_nd.toDirLine := by sorry end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean index f626aa51..530f7a0d 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean @@ -321,7 +321,7 @@ theorem Vec.linear_combination_of_not_colinear_dir {u v : Dir} (w : Vec) (h' : u exact @linear_combination_of_not_colinear' u.unitVec v.unitVec w (VecND.ne_zero _) (h₁ h') /-- Given two unparallel rays, this function gives the intersection of their extension lines. -/ -def inx_of_extn_line (r₁ r₂ : Ray P) (h : ¬ r₁ ∥ r₂) : P := (cu r₁.toDir.unitVecND r₂.toDir.unitVecND (VEC r₁.source r₂.source) • r₁.toDir.unitVec +ᵥ r₁.source) +def inx_of_extn_line (r₁ r₂ : Ray P) (_h : ¬ r₁ ∥ r₂) : P := (cu r₁.toDir.unitVecND r₂.toDir.unitVecND (VEC r₁.source r₂.source) • r₁.toDir.unitVec +ᵥ r₁.source) /-- Given two unparallel rays, we define the intersection of their extension lines. -/ theorem inx_of_extn_line_symm (r₁ r₂ : Ray P) (h : ¬ r₁ ∥ r₂) : diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean index 1d44836a..391f7ae9 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean @@ -83,10 +83,14 @@ theorem perp_foot_eq_self_iff_lies_on (A : P) (l : Line P) : perp_foot A l = A theorem perp_foot_ne_self_iff_not_lies_on (A : P) (l : Line P) : perp_foot A l ≠ A ↔ ¬ A LiesOn l := (perp_foot_eq_self_iff_lies_on A l).not +theorem pt_ne_iff_not_lies_on_of_eq_perp_foot {A B : P} {l : Line P} (h : B = perp_foot A l) : B ≠ A ↔ ¬ A LiesOn l := by + rw [h] + exact (perp_foot_ne_self_iff_not_lies_on A l) + theorem line_of_self_perp_foot_eq_perp_line_of_not_lies_on {A : P} {l : Line P} (h : ¬ A LiesOn l) : LIN A (perp_foot A l) ((perp_foot_ne_self_iff_not_lies_on A l).2 h) = perp_line A l := eq_line_of_pt_pt_of_ne (_h := ⟨(perp_foot_ne_self_iff_not_lies_on A l).2 h⟩) (pt_lies_on_of_mk_pt_proj A l.toProj.perp) (Line.inx_is_inx (toProj_ne_perp_toProj A l)).2 -theorem line_of_self_perp_foot_perp_line_of_not_lies_on {A : P} {l : Line P} (h : ¬ (A LiesOn l)) : LIN A (perp_foot A l) ((perp_foot_ne_self_iff_not_lies_on A l).2 h) ⟂ l := +theorem line_of_self_perp_foot_perp_line_of_not_lies_on {A : P} {l : Line P} (h : ¬ A LiesOn l) : LIN A (perp_foot A l) ((perp_foot_ne_self_iff_not_lies_on A l).2 h) ⟂ l := (congrArg toProj (line_of_self_perp_foot_eq_perp_line_of_not_lies_on h)).trans (perp_line_perp A l) theorem dist_eq_zero_iff_lies_on (A : P) (l : Line P) : dist_pt_line A l = 0 ↔ A LiesOn l := diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular_trash.lean index 70a33257..96609a48 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular_trash.lean @@ -10,15 +10,9 @@ variable {P : Type _} [EuclideanPlane P] theorem segnd_perp_line_of_line_perp_line {A B : P} (B_ne_A : B ≠ A) {l : Line P} (h : (SEG_nd A B B_ne_A) ⟂ l) : (LIN A B B_ne_A) ⟂ l := by sorry theorem perp_foot_unique' {A B : P} {l : DirLine P} (h : A LiesOn l) (hne : B ≠ A) (hp : (DLIN B A hne.symm) ⟂ l) : perp_foot B l = A := sorry -lemma perp_foot_ne_self_iff_not_lies_on' (A B : P) (l : Line P) (B_is_perp_foot : B = (perp_foot A l)) : B ≠ A ↔ ¬ A LiesOn l := by - simp only [B_is_perp_foot] - exact (perp_foot_ne_self_iff_not_lies_on A l) -theorem not_colinear_with_perp_foot_of_ne_perp_foot (A B C : P) (l : Line P) (B_on_l : B LiesOn l) (A_not_on_l : ¬ A LiesOn l) (C_is_perp_foot : C = (perp_foot A l)) (B_ne_C : B ≠ C): ¬ colinear C B A := sorry - -theorem angle_eq_pi_div_two_or_neg_pi_div_two_at_perp_foot (A B C : P) (l : Line P) (B_on_l : B LiesOn l) (A_not_on_l : ¬ A LiesOn l) (C_is_perp_foot : C = (perp_foot A l)) (B_ne_C : B ≠ C) : (∠ A C B ((perp_foot_ne_self_iff_not_lies_on' A C l C_is_perp_foot).mpr A_not_on_l).symm B_ne_C = ↑ (π / 2)) ∨ (∠ A C B ((perp_foot_ne_self_iff_not_lies_on' A C l C_is_perp_foot).mpr A_not_on_l).symm B_ne_C = ↑(-(π / 2))) := by sorry -theorem angle_dval_eq_pi_div_two_at_perp_foot (A B C : P) (l : Line P) (B_on_l : B LiesOn l) (A_not_on_l : ¬ A LiesOn l) (C_is_perp_foot : C = (perp_foot A l)) (B_ne_C : B ≠ C) : (ANG A C B ((perp_foot_ne_self_iff_not_lies_on' A C l C_is_perp_foot).mpr A_not_on_l).symm B_ne_C).dvalue = ↑ (π / 2) := by sorry +theorem not_colinear_with_perp_foot_of_ne_perp_foot (A B C : P) (l : Line P) (B_on_l : B LiesOn l) (A_not_on_l : ¬ A LiesOn l) (C_is_perp_foot : C = (perp_foot A l)) (B_ne_C : B ≠ C): ¬ colinear C B A := sorry theorem perp_foot_unique {A B : P} {l : DirLine P} (h : A LiesOn l) [_hne : PtNe A B] (hp : (DLIN B A) ⟂ l) : perp_foot B l = A := sorry diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean index 930146ba..f2aa651b 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean @@ -170,7 +170,11 @@ protected def IsOn (X : P) (ray : Ray P) : Prop := ∃ (t : ℝ), 0 ≤ t ∧ VEC ray.source X = t • ray.toDir.unitVec /-- Given a point $X$ and a ray, this function returns whether the point lies in the interior of the ray; here saying that a point lies in the interior of a ray means that it lies on the ray and is not equal to the source of the ray. -/ -protected def IsInt (X : P) (ray : Ray P) : Prop := Ray.IsOn X ray ∧ X ≠ ray.source +protected structure IsInt (X : P) (ray : Ray P) : Prop where + isOn : Ray.IsOn X ray + ne_source : X ≠ ray.source + +alias ne_source_of_lies_int := IsInt.ne_source /-- Given a ray, its carrier is the set of points that lie on the ray. -/ protected def carrier (ray : Ray P) : Set P := { X : P | Ray.IsOn X ray } @@ -182,7 +186,7 @@ protected def interior (ray : Ray P) : Set P := { X : P | Ray.IsInt X ray } instance : IntFig (Ray P) P where carrier := Ray.carrier interior := Ray.interior - interior_subset_carrier _ _ := And.left + interior_subset_carrier _ _ := IsInt.isOn end Ray @@ -205,6 +209,10 @@ protected structure IsInt (X : P) (seg : Seg P) : Prop where ne_source : X ≠ seg.source ne_target : X ≠ seg.target +alias ne_source_of_lies_int := IsInt.ne_source + +alias ne_target_of_lies_int := IsInt.ne_target + /-- Given a segment, this function returns the set of points that lie on the segment. -/ protected def carrier (seg : Seg P) : Set P := { X : P | Seg.IsOn X seg } @@ -324,7 +332,7 @@ theorem pt_pt_seg_toRay_eq_pt_pt_ray {A B : P} [_h : PtNe B A] : (SEG_nd A B).to theorem Seg.IsND_iff_toVec_ne_zero {l : Seg P} : l.IsND ↔ l.toVec ≠ 0 := toVec_eq_zero_of_deg.not /-- If $ray_1$ and $ray_2$ are two rays with the same projective direction, then the direction vector of $ray_2$ is a real multiple of the direction vector of $ray_1$. -/ -theorem dir_parallel_of_same_proj {ray₁ ray₂ : Ray P} (h : ray₁.toProj = ray₂.toProj) : ∃t : ℝ, ray₂.toDir.unitVec = t • ray₁.toDir.unitVec := by +theorem dir_parallel_of_same_proj {ray₁ ray₂ : Ray P} (h : ray₁.toProj = ray₂.toProj) : ∃ t : ℝ, ray₂.toDir.unitVec = t • ray₁.toDir.unitVec := by rcases Dir.toProj_eq_toProj_iff.mp h with xy | xy · use 1 rw [one_smul, xy] @@ -405,6 +413,14 @@ theorem SegND.lies_int_iff {X : P} {seg_nd : SegND P}: X LiesInt seg_nd ↔ ∃ rw [h1, smul_ne_zero_iff] exact ⟨by linarith, seg_nd.toVecND.2⟩ +/-- For a nondegenerate segment $AB$, if a point $X$ lies on $AB$ the $X$ not equal to $A$. -/ +theorem SegND.ne_source_of_lies_int {X : P} {s : SegND P} (h : X LiesInt s) : X ≠ s.source := + h.ne_source + +/-- For a nondegenerate segment $AB$, if a point $X$ lies on $AB$ the $X$ not equal to $B$. -/ +theorem SegND.ne_target_of_lies_int {X : P} {s : SegND P} (h : X LiesInt s) : X ≠ s.target := + h.ne_target + /-- For a segment $AB$, if there exists an interior point $X$, then it is nondegenerate. -/ theorem Seg.isND_of_pt_liesint {seg : Seg P} {X : P} (h : X LiesInt seg) : seg.IsND := by sorry @@ -418,7 +434,6 @@ theorem Seg.lies_int_iff {X : P} {seg : Seg P}: X LiesInt seg ↔ seg.IsND ∧ ( let segnd : SegND P := ⟨ seg, h2.1 ⟩ exact (segnd.lies_int_iff).mpr h2.2 - /-- Given a segment $AB$, the source $A$ of the segment lies on the segment. -/ @[simp] theorem Seg.source_lies_on {seg : Seg P} : seg.source LiesOn seg := @@ -426,7 +441,7 @@ theorem Seg.source_lies_on {seg : Seg P} : seg.source LiesOn seg := /-- Given a segment $AB$, the target $B$ lies on the segment $AB$. -/ @[simp] -theorem Seg.target_lies_on {seg : Seg P} : seg.target LiesOn seg := ⟨1, zero_le_one, by rfl, by rw [one_smul]⟩ +theorem Seg.target_lies_on {seg : Seg P} : seg.target LiesOn seg := ⟨1, zero_le_one, Eq.le rfl, by rw [one_smul]⟩ /-- Given a segment $AB$, the source $A$ does not belong to the interior of $AB$. -/ @[simp] @@ -472,10 +487,9 @@ theorem Ray.source_not_lies_int {ray : Ray P} : ¬ ray.source LiesInt ray := fun @[simp] theorem Ray.lies_on_of_lies_int {X : P} {ray : Ray P} (h : X LiesInt ray) : X LiesOn ray := h.1 - /-- Given a ray, a point lies in the interior of the ray if and only if it lies on the ray and is different from the source of ray. -/ -theorem Ray.lies_int_def {X : P} {ray : Ray P} : X LiesInt ray ↔ X LiesOn ray ∧ X ≠ ray.source := Iff.rfl - +theorem Ray.lies_int_def {X : P} {ray : Ray P} : X LiesInt ray ↔ X LiesOn ray ∧ X ≠ ray.source := + ⟨fun h ↦ ⟨h.1, h.2⟩, fun h ↦ ⟨h.1, h.2⟩⟩ /-- For a nondegenerate segment $AB$, every point of the segment $AB$ lies on the ray associated to $AB$. -/ theorem SegND.lies_on_toRay_of_lies_on {X : P} {seg_nd : SegND P} (h : X LiesOn seg_nd) : X LiesOn seg_nd.toRay := by @@ -511,18 +525,31 @@ theorem Ray.pt_pt_toDir_eq_ray_toDir {ray : Ray P} {A : P} (h : A LiesInt ray) : theorem Ray.pt_pt_eq_ray {ray : Ray P} {A : P} (h : A LiesInt ray) : RAY ray.1 A h.2 = ray := (Ray.ext _ ray) rfl (pt_pt_toDir_eq_ray_toDir h) - /-- Given a point $A$ on a ray, the ray associated to the segment from the source of the ray to $A$ is the same as the original ray. -/ theorem Ray.source_int_toRay_eq_ray {ray : Ray P} {A : P} (h : A LiesInt ray) : (SEG_nd ray.source A h.2).toRay = ray := Ray.pt_pt_eq_ray h +theorem Ray.vec_eq_dist_smul_toDir_of_lies_on {A : P} {r : Ray P} (h : A LiesOn r) : VEC r.1 A = (dist r.1 A) • r.toDir.unitVec := by + by_cases heq : A = r.1 + · rw [← heq, vec_same_eq_zero, dist_self, zero_smul] + push_neg at heq + have h : A LiesInt r := ⟨h, heq⟩ + have h₁ : RAY r.1 A h.2 = r := Ray.pt_pt_eq_ray h + calc + _ = (VEC_nd r.1 A h.2).1 := rfl + _ = ‖VEC_nd r.1 A h.2‖ • (VEC_nd r.1 A h.2).toDir.unitVec := by simp + _ = (dist r.1 A) • (VEC_nd r.1 A h.2).toDir.unitVec := by + rw [dist_comm, NormedAddTorsor.dist_eq_norm'] + rfl + _ = (dist r.1 A) • (RAY r.1 A h.2).2.unitVec := rfl + _ = (dist r.1 A) • r.2.unitVec := by rw [h₁] /-- Given two segments $seg_1$ and $seg_2$, if the source and the target of the $seg_1$ both lie on $seg_2$, then every point of $seg_1$ lies on $seg_2$. -/ theorem every_pt_lies_on_seg_of_source_and_target_lies_on_seg {seg₁ seg₂ : Seg P} (h₁ : seg₁.source LiesOn seg₂) (h₂ : seg₁.target LiesOn seg₂) {A : P} (ha : A LiesOn seg₁) : (A LiesOn seg₂) := by rcases h₁ with ⟨x,xnonneg,xle1,hx⟩ rcases h₂ with ⟨y,ynonneg,yle1,hy⟩ rcases ha with ⟨t,tnonneg,tleone,ht⟩ - rw[←vec_add_vec seg₁.source seg₂.source,←vec_add_vec seg₁.source seg₂.source seg₁.target,←neg_vec,hx,hy,neg_add_eq_iff_eq_add,←neg_smul,smul_add,smul_smul,smul_smul,←add_smul,←add_smul,←add_assoc,mul_neg,←sub_eq_add_neg,←one_mul x,←mul_assoc,←sub_mul,mul_one] at ht + rw [←vec_add_vec seg₁.source seg₂.source,←vec_add_vec seg₁.source seg₂.source seg₁.target,←neg_vec,hx,hy,neg_add_eq_iff_eq_add,←neg_smul,smul_add,smul_smul,smul_smul,←add_smul,←add_smul,←add_assoc,mul_neg,←sub_eq_add_neg,←one_mul x,←mul_assoc,←sub_mul,mul_one] at ht use ( (1- t) * x + t * y) constructor apply add_nonneg @@ -543,10 +570,10 @@ theorem every_pt_lies_on_seg_of_source_and_target_lies_on_seg {seg₁ seg₂ : S /-- Given two segments $seg_1$ and $seg_2$, if the source and the target of $seg_1$ both lie in the interior of $seg_2$, and if $A$ is a point on $seg_1$, then $A$ lies in the interior of $seg_2$. -/ theorem every_pt_lies_int_seg_of_source_and_target_lies_int_seg {seg₁ seg₂ : Seg P} (h₁ : seg₁.source LiesInt seg₂) (h₂ : seg₁.target LiesInt seg₂) {A : P} (ha : A LiesOn seg₁) : A LiesInt seg₂ := by - rw[Seg.lies_int_iff] + rw [Seg.lies_int_iff] constructor apply ((Seg.lies_int_iff).mp h₁).1 - rw[Seg.lies_int_iff] at h₁ h₂ + rw [Seg.lies_int_iff] at h₁ h₂ rcases h₁ with ⟨ _ ,x,xpos,xlt1,hx⟩ rcases h₂ with ⟨ _ ,y,ypos,ylt1,hy⟩ rcases ha with ⟨t,tnonneg,tle1,ht⟩ @@ -558,7 +585,7 @@ theorem every_pt_lies_int_seg_of_source_and_target_lies_int_seg {seg₁ seg₂ : constructor simp only [←h, sub_zero, one_mul, zero_mul, add_zero] exact xlt1 - rw[←h,zero_smul,←eq_iff_vec_eq_zero] at ht + rw [←h,zero_smul,←eq_iff_vec_eq_zero] at ht simp only [← h, sub_zero, one_mul, zero_mul, add_zero,ht,hx] constructor apply lt_of_lt_of_le (mul_pos (lt_of_le_of_ne tnonneg h) ypos) @@ -582,7 +609,7 @@ theorem every_pt_lies_int_seg_of_source_and_target_lies_int_seg {seg₁ seg₂ : linarith linarith linarith - rw[←vec_add_vec seg₂.1 seg₁.1 A,ht,←vec_sub_vec seg₂.1 seg₁.1 seg₁.2,hy,hx,←sub_smul,smul_smul,←add_smul,←sub_eq_zero,←sub_smul,smul_eq_zero] + rw [←vec_add_vec seg₂.1 seg₁.1 A,ht,←vec_sub_vec seg₂.1 seg₁.1 seg₁.2,hy,hx,←sub_smul,smul_smul,←add_smul,←sub_eq_zero,←sub_smul,smul_eq_zero] left ring @@ -593,23 +620,23 @@ theorem every_int_pt_lies_int_seg_of_source_and_target_lies_on_seg {seg₁ seg rcases h₂ with ⟨y,ynonneg,yle1,hy⟩ rcases (Seg.lies_int_iff).mp ha with ⟨nd,t,tpos,tlt1,ht⟩ constructor - rw[Seg.IsND,ne_iff_vec_ne_zero] + rw [Seg.IsND,ne_iff_vec_ne_zero] contrapose! nd - rw[nd,smul_zero,←eq_iff_vec_eq_zero] at hx hy - rw[Seg.IsND,not_not,eq_iff_vec_eq_zero,hx,hy,vec_same_eq_zero] - rw[Seg.toVec,←vec_sub_vec seg₂.1,← vec_sub_vec seg₂.1 seg₁.1 seg₁.2,sub_eq_iff_eq_add,hx,hy,←sub_smul,smul_smul,←add_smul] at ht + rw [nd,smul_zero,←eq_iff_vec_eq_zero] at hx hy + rw [Seg.IsND,not_not,eq_iff_vec_eq_zero,hx,hy,vec_same_eq_zero] + rw [Seg.toVec,←vec_sub_vec seg₂.1,← vec_sub_vec seg₂.1 seg₁.1 seg₁.2,sub_eq_iff_eq_add,hx,hy,←sub_smul,smul_smul,←add_smul] at ht use ( (1- t) * x + t * y) have ynex:y≠x:= by contrapose! nd - rw[Seg.IsND,not_not,eq_iff_vec_eq_zero,←vec_sub_vec seg₂.1,hx,hy,←sub_smul,nd,sub_self,zero_smul] + rw [Seg.IsND,not_not,eq_iff_vec_eq_zero,←vec_sub_vec seg₂.1,hx,hy,←sub_smul,nd,sub_self,zero_smul] constructor by_cases h : 0=x - rw[←h,mul_zero,zero_add] + rw [←h,mul_zero,zero_add] apply mul_pos exact tpos apply lt_of_le_of_ne exact ynonneg - rw[h] + rw [h] symm exact ynex have :0<(1-t)*x:=by @@ -628,7 +655,7 @@ theorem every_int_pt_lies_int_seg_of_source_and_target_lies_on_seg {seg₁ seg apply mul_lt_mul_of_pos_left apply lt_of_le_of_ne exact yle1 - rw[h] + rw [h] exact ynex exact tpos have :(1-t)*x+t*y<(1-t)+t*y:=by @@ -640,11 +667,11 @@ theorem every_int_pt_lies_int_seg_of_source_and_target_lies_on_seg {seg₁ seg exact h linarith apply lt_of_lt_of_le this - rw[sub_add,tsub_le_iff_right, le_add_iff_nonneg_right, sub_nonneg,←mul_one t,mul_assoc,one_mul] + rw [sub_add,tsub_le_iff_right, le_add_iff_nonneg_right, sub_nonneg,←mul_one t,mul_assoc,one_mul] apply mul_le_mul _ yle1 ynonneg linarith linarith - rw[ht,←sub_eq_zero,Seg.toVec,←sub_smul,smul_eq_zero] + rw [ht,←sub_eq_zero,Seg.toVec,←sub_smul,smul_eq_zero] left ring @@ -653,7 +680,7 @@ theorem every_pt_lies_on_ray_of_source_and_target_lies_on_ray {seg : Seg P} {ray rcases h₁ with ⟨x,xnonneg,hx⟩ rcases h₂ with ⟨y,ynonneg,hy⟩ rcases ha with ⟨t,tnonneg,tleone,ht⟩ - rw[←vec_add_vec seg.source ray.source,←vec_add_vec seg.source ray.source seg.target,←neg_vec,hx,hy,neg_add_eq_iff_eq_add,←neg_smul,smul_add,smul_smul,smul_smul,←add_smul,←add_smul,←add_assoc,mul_neg,←sub_eq_add_neg,←one_mul x,←mul_assoc,←sub_mul,mul_one] at ht + rw [←vec_add_vec seg.source ray.source,←vec_add_vec seg.source ray.source seg.target,←neg_vec,hx,hy,neg_add_eq_iff_eq_add,←neg_smul,smul_add,smul_smul,smul_smul,←add_smul,←add_smul,←add_assoc,mul_neg,←sub_eq_add_neg,←one_mul x,←mul_assoc,←sub_mul,mul_one] at ht use ( (1- t) * x + t * y) constructor apply add_nonneg @@ -663,7 +690,7 @@ theorem every_pt_lies_on_ray_of_source_and_target_lies_on_ray {seg : Seg P} {ray apply mul_nonneg linarith linarith - rw[ht] + rw [ht] /-- Given a segment and a ray, if the source and the target of the segment both lie in the interior of the ray, and if $A$ is a point on the segment, then $A$ lies in the interior of the ray.-/ theorem every_pt_lies_int_ray_of_source_and_target_lies_int_ray {seg : Seg P} {ray : Ray P} (h₁ : seg.source LiesInt ray) (h₂ : seg.target LiesInt ray) {A : P} (ha : A LiesOn seg) : A LiesInt ray := by @@ -671,18 +698,18 @@ theorem every_pt_lies_int_ray_of_source_and_target_lies_int_ray {seg : Seg P} {r rcases (Ray.lies_int_iff.mp h₂) with ⟨y,ypos,hy⟩ apply Ray.lies_int_iff.mpr rcases ha with ⟨t,tnonneg,tle1,ht⟩ - rw[←vec_sub_vec ray.source,←vec_sub_vec ray.source seg.source seg.target,hx,hy,sub_eq_iff_eq_add,←sub_smul,smul_smul,←add_smul,mul_sub] at ht + rw [←vec_sub_vec ray.source,←vec_sub_vec ray.source seg.source seg.target,hx,hy,sub_eq_iff_eq_add,←sub_smul,smul_smul,←add_smul,mul_sub] at ht use (t*y+(1-t)*x) constructor by_cases h : 0=t - rw[←h] + rw [←h] linarith apply lt_of_lt_of_le (mul_pos (lt_of_le_of_ne tnonneg h) ypos) simp only [le_add_iff_nonneg_right, gt_iff_lt, sub_pos] apply mul_nonneg linarith linarith - rw[ht,←sub_eq_zero,←sub_smul,smul_eq_zero] + rw [ht,←sub_eq_zero,←sub_smul,smul_eq_zero] left ring @@ -696,15 +723,15 @@ theorem every_int_pt_lies_int_ray_of_source_and_target_lies_on_ray {seg : Seg P} use (1-t)*x+t*y have ynex:y≠x:= by contrapose! nd - rw[Seg.IsND,not_not,eq_iff_vec_eq_zero,←vec_sub_vec ray.1,hx,hy,←sub_smul,nd,sub_self,zero_smul] + rw [Seg.IsND,not_not,eq_iff_vec_eq_zero,←vec_sub_vec ray.1,hx,hy,←sub_smul,nd,sub_self,zero_smul] constructor by_cases h : 0=x - rw[←h,mul_zero,zero_add] + rw [←h,mul_zero,zero_add] apply mul_pos exact tpos apply lt_of_le_of_ne exact ynonneg - rw[h] + rw [h] symm exact ynex have :0<(1-t)*x:=by @@ -716,7 +743,7 @@ theorem every_int_pt_lies_int_ray_of_source_and_target_lies_on_ray {seg : Seg P} apply mul_nonneg linarith linarith - rw[ht,←sub_eq_zero,←sub_smul,smul_eq_zero] + rw [ht,←sub_eq_zero,←sub_smul,smul_eq_zero] left ring @@ -727,18 +754,22 @@ theorem every_pt_lies_on_ray_of_source_lies_on_ray_and_same_dir {ray₁ ray₂ : use x+t constructor linarith - rw[←vec_add_vec ray₂.source ray₁.source A,hx,ht,e,add_smul] + rw [←vec_add_vec ray₂.source ray₁.source A,hx,ht,e,add_smul] /-- Given two rays $ray_1$ and $ray_2$ with same direction, if the source of $ray_1$ lies in the interior of $ray_2$, and if $A$ is a point on $ray_1$, then $A$ lies in the interior of $ray_2$. -/ theorem every_pt_lies_int_ray_of_source_lies_int_ray_and_same_dir {ray₁ ray₂ : Ray P} (e : ray₁.toDir = ray₂.toDir) (h : ray₁.source LiesInt ray₂) {A : P} (ha : A LiesOn ray₁) : A LiesInt ray₂ := by apply Ray.lies_int_iff.mpr rcases ha with ⟨t,tnonneg,ht⟩ rcases Ray.lies_int_iff.mp h with ⟨x, xpos, hx⟩ - rw[e] at ht + rw [e] at ht use x+t constructor linarith - rw[←vec_add_vec ray₂.1 ray₁.1,hx,ht,add_smul] + rw [←vec_add_vec ray₂.1 ray₁.1,hx,ht,add_smul] + +theorem SegND.toDir_eq_of_lies_int {seg_nd : SegND P} {A : P} (h : A LiesInt seg_nd) : (SEG_nd seg_nd.source A h.ne_source).toDir = seg_nd.toDir := sorry + +theorem SegND.toDir_eq_neg_toDir_of_lies_int {A : P} {s : SegND P} (h : A LiesInt s) : (VEC_nd A s.source h.2.symm).toDir = - (VEC_nd A s.target h.3.symm).toDir := sorry end lieson_compatibility @@ -927,15 +958,15 @@ theorem Ray.eq_source_iff_lies_on_and_lies_on_rev {A : P} {ray : Ray P} : A = ra constructor use 0 simp only [le_refl, zero_smul, true_and] - rw[h,vec_same_eq_zero] + rw [h,vec_same_eq_zero] use 0 simp only [le_refl, smul_neg, zero_smul, neg_zero, true_and,Ray.reverse] - rw[h,vec_same_eq_zero] + rw [h,vec_same_eq_zero] simp only [and_imp] rintro ⟨a,⟨anneg,h⟩⟩ ⟨b,⟨bnneg,h'⟩⟩ replace h' : a + b = 0 · simp only [Ray.reverse, smul_neg,h] at h' - rw[←add_zero a,← sub_self b,add_sub,sub_smul] at h' + rw [←add_zero a,← sub_self b,add_sub,sub_smul] at h' simpa using h' have : a = 0 := by linarith subst this @@ -950,7 +981,7 @@ theorem Ray.not_lies_on_of_lies_int_rev {A : P} {ray : Ray P} (liesint : A LiesI rcases liesint with ⟨h',nsource⟩ have: A LiesOn ray.reverse:=by apply h' - have :A=ray.source:=by + have : A=ray.source:=by rw [Ray.eq_source_iff_lies_on_and_lies_on_rev] constructor exact h @@ -1143,13 +1174,13 @@ theorem target_lies_int_seg_source_pt_of_pt_lies_int_extn {X : P} {seg_nd : SegN have raysourcesegtarget:seg_nd.1.target=seg_nd.extension.1:=by rfl have sourcetargetA:VEC seg_nd.1.source seg_nd.1.target+VEC seg_nd.1.target X=VEC seg_nd.1.source X:=by - rw[vec_add_vec] + rw [vec_add_vec] have vec_ndtoVec:VEC seg_nd.1.source seg_nd.1.target=seg_nd.toVecND.1:=by rfl have apos:0 < a:=by contrapose! nonsource - have:a=0:=by linarith - rw[this] at ha + have: A=0:=by linarith + rw [this] at ha simp only [Dir.toVec_neg_eq_neg_toVec, smul_neg, zero_smul, neg_zero] at ha apply (eq_iff_vec_eq_zero _ _).mpr exact ha @@ -1164,38 +1195,37 @@ theorem target_lies_int_seg_source_pt_of_pt_lies_int_extn {X : P} {seg_nd : SegN have aseg_nonzero:VecND.norm (SegND.toVecND seg_nd)+a≠ 0:=by linarith have raydir:seg_nd.extension.toDir.toVec=seg_nd.toVecND.toDir.toVec:=by - rw[Ray.toDir_of_rev_eq_neg_toDir] - rw[Ray.toDir_of_rev_eq_neg_toDir,←SegND.toDir_eq_toRay_toDir,SegND.toDir_of_rev_eq_neg_toDir,neg_neg] + rw [Ray.toDir_of_rev_eq_neg_toDir] + rw [Ray.toDir_of_rev_eq_neg_toDir,←SegND.toDir_eq_toRay_toDir,SegND.toDir_of_rev_eq_neg_toDir,neg_neg] constructor use (seg_nd.toVecND.norm)*(seg_nd.toVecND.norm+a)⁻¹ constructor apply mul_nonneg linarith[seg_pos] norm_num - rw[←norm_of_VecND_eq_norm_of_VecND_fst] + rw [←norm_of_VecND_eq_norm_of_VecND_fst] linarith constructor - rw[←mul_inv_cancel aseg_nonzero] + rw [←mul_inv_cancel aseg_nonzero] apply mul_le_mul linarith linarith norm_num - rw[← norm_of_VecND_eq_norm_of_VecND_fst] + rw [← norm_of_VecND_eq_norm_of_VecND_fst] linarith linarith simp only [Seg.target] - rw[←raysourcesegtarget] at ha - rw[←sourcetargetA,ha,vec_ndtoVec,←VecND.norm_smul_toDir_eq_self (seg_nd.toVecND),←norm_of_VecND_eq_norm_of_VecND_fst,raydir] - rw[←add_smul,← mul_smul,mul_assoc,inv_mul_cancel,mul_one] + rw [←raysourcesegtarget] at ha + rw [←sourcetargetA,ha,vec_ndtoVec,←VecND.norm_smul_toDir_eq_self (seg_nd.toVecND),←norm_of_VecND_eq_norm_of_VecND_fst,raydir] + rw [←add_smul,← mul_smul,mul_assoc,inv_mul_cancel,mul_one] linarith constructor exact seg_nd.2 - rw[←raysourcesegtarget] at nonsource + rw [←raysourcesegtarget] at nonsource symm exact nonsource -/ - /-- If a point lies on the ray associated to a segment, then either it lies on the segment or it lies on the extension ray of the segment. -/ theorem lies_on_seg_nd_or_extension_of_lies_on_toRay {seg_nd : SegND P} {A : P} (h : A LiesOn seg_nd.toRay) : A LiesOn seg_nd ∨ A LiesOn seg_nd.extension := by rcases h with ⟨t, tpos, eq⟩ @@ -1213,6 +1243,8 @@ theorem lies_on_seg_nd_or_extension_of_lies_on_toRay {seg_nd : SegND P} {A : P} simp [eq, mul_smul] rfl⟩ +theorem lies_int_toRay_of_lies_on_extn {seg_nd : SegND P} (A : P) (h : A LiesOn seg_nd.extension) : A LiesInt seg_nd.toRay := by sorry + theorem not_lies_int_rev_extn_of_lies_on {A : P} {seg_nd : SegND P} (lieson : A LiesOn seg_nd.1) : ¬ A LiesInt seg_nd.reverse.extension := by apply Ray.not_lies_int_of_lies_on_rev rw [rev_extn_eq_toRay_rev, Ray.rev_rev_eq_self] @@ -1224,6 +1256,27 @@ theorem not_lies_int_extn_of_lies_on {A : P} {seg_nd : SegND P} (lieson : A Lies end SegND +namespace Ray + +-- Define the extpoint of a ray to be a point lies on the ray.toLine which has given distence to the ray.source +def extpoint (l : Ray P) (t : ℝ) : P := t • l.toDir.unitVec +ᵥ l.source + +theorem extpoint_lies_on_of_nonneg {r : Ray P} {t : ℝ} (ht : 0 ≤ t) : r.extpoint t LiesOn r := sorry + +theorem lies_on_of_eq_nonneg_extpoint {r : Ray P} {A : P} {t : ℝ} (ht : 0 ≤ t) (h : A = Ray.extpoint r t) : A LiesOn r := by + rw [h] + exact extpoint_lies_on_of_nonneg ht + +theorem extpoint_lies_int_of_pos {r : Ray P} {t : ℝ} (ht : 0 < t) : r.extpoint t LiesInt r := sorry + +theorem lies_int_of_eq_pos_extpoint {r : Ray P} {A : P} {t : ℝ} (ht : 0 < t) (h : A = Ray.extpoint r t) : A LiesInt r := sorry + +theorem dist_of_extpoint {r : Ray P} {t : ℝ} (ht : 0 ≤ t) : dist r.source (r.extpoint t) = t := sorry + +theorem dist_eq_of_eq_extpoint {r : Ray P} {A : P} {t : ℝ} (ht : 0 ≤ t) (h : A = Ray.extpoint r t) : dist r.source A = t := sorry + +end Ray + end extension section length @@ -1247,7 +1300,7 @@ theorem Seg.length_eq_norm_toVec {seg : Seg P} : seg.length = norm seg.toVec := abbrev SegND.length (seg_nd : SegND P) : ℝ := seg_nd.1.length /-- Every segment has nonnegative length. -/ -theorem length_nonneg {seg : Seg P} : 0 ≤ seg.length := dist_nonneg +theorem Seg.length_nonneg {seg : Seg P} : 0 ≤ seg.length := dist_nonneg /-- A segment has positive length if and only if it is nondegenerate. -/ theorem length_pos_iff_nd {seg : Seg P} : 0 < seg.length ↔ seg.IsND := @@ -1271,7 +1324,6 @@ theorem length_eq_zero_iff_deg {seg : Seg P} : seg.length = 0 ↔ (seg.target = rw [Seg.length_eq_norm_toVec] exact ((toVec_eq_zero_of_deg).trans norm_eq_zero.symm).symm - /-- Reversing a segment does not change its length. -/ @[simp] theorem Seg.length_of_rev_eq_length {seg : Seg P} : seg.reverse.length = seg.length := by @@ -1304,6 +1356,8 @@ theorem length_eq_length_add_length {seg : Seg P} {A : P} (lieson : A LiesOn seg norm_smul, norm_smul, ← add_mul, Real.norm_of_nonneg a, Real.norm_of_nonneg (sub_nonneg.mpr b)] linarith +theorem SegND.length_eq_length_add_length_of_lies_on_extn {seg_nd : SegND P} {A : P} (h : A LiesOn seg_nd.extension) : (SEG seg_nd.source A).length = seg_nd.1.length + (SEG seg_nd.target A).length := sorry + end length section midpoint @@ -1329,7 +1383,6 @@ theorem SegND.vec_source_midpt {seg_nd : SegND P} : VEC seg_nd.source seg_nd.mid simp only [SegND.midpoint] exact seg_nd.1.vec_source_midpt - theorem Seg.vec_midpt_target {seg : Seg P} : VEC seg.midpoint seg.2 = (1 / 2 : ℝ) • VEC seg.1 seg.2 := by rw [midpoint, ← vec_add_vec _ seg.1 _, ← neg_vec, vec_of_pt_vadd_pt_eq_vec] apply smul_right_injective _ (two_ne_zero' ℝ) @@ -1339,7 +1392,6 @@ theorem SegND.vec_midpt_target {seg_nd : SegND P} : VEC seg_nd.midpoint seg_nd.t simp only [SegND.midpoint] exact seg_nd.1.vec_midpt_target - /-- Given a segment $AB$, the vector from $A$ to the midpoint of $AB$ is same as the vector from the midpoint of $AB$ to $B$ -/ theorem Seg.vec_midpt_eq {seg : Seg P} : VEC seg.1 seg.midpoint = VEC seg.midpoint seg.2 := by rw [seg.vec_source_midpt, seg.vec_midpt_target] @@ -1356,25 +1408,25 @@ theorem SegND.vec_eq_of_eq_midpt {seg_nd : SegND P} (h : A = seg_nd.midpoint) : exact seg_nd.1.vec_eq_of_eq_midpt h /-- Given a segment $AB$ and a point P, if vector $\overrightarrow{AP}$ is half of vector $\overrightarrow{AB}$, P is the midpoint of $AB$. -/ -theorem midpt_of_vector_from_source {seg : Seg P} (h : VEC seg.1 A = (1 / 2 : ℝ) • VEC seg.1 seg.2) :A = seg.midpoint := by +theorem Seg.midpt_of_vector_from_source {seg : Seg P} (h : VEC seg.1 A = (1 / 2 : ℝ) • VEC seg.1 seg.2) : A = seg.midpoint := by rw [← start_vadd_vec_eq_end seg.1 A, h, Seg.midpoint] norm_num -theorem nd_midpt_of_vector_from_source {seg_nd : SegND P} (h : VEC seg_nd.source A = (1 / 2 : ℝ) • VEC seg_nd.source seg_nd.target) :A = seg_nd.midpoint := by - exact midpt_of_vector_from_source h +theorem SegND.midpt_of_vector_from_source {seg_nd : SegND P} (h : VEC seg_nd.source A = (1 / 2 : ℝ) • VEC seg_nd.source seg_nd.target) : A = seg_nd.midpoint := + Seg.midpt_of_vector_from_source h /-- Given a segment $AB$ and a point P, if vector $\overrightarrow{PB}$ is half of vector $\overrightarrow{AB}$, P is the midpoint of $AB$. -/ -theorem midpt_of_vector_to_target {seg : Seg P} (h : VEC A seg.2 = (1 / 2 : ℝ) • VEC seg.1 seg.2) :A = seg.midpoint := by +theorem Seg.midpt_of_vector_to_target {seg : Seg P} (h : VEC A seg.2 = (1 / 2 : ℝ) • VEC seg.1 seg.2) : A = seg.midpoint := by refine' midpt_of_vector_from_source _ rw [← add_left_inj (VEC A seg.target), vec_add_vec, h, ← add_smul] norm_num -theorem nd_midpt_of_vector_to_target {seg_nd : SegND P} (h : VEC A seg_nd.target = (1 / 2 : ℝ) • VEC seg_nd.source seg_nd.target) :A = seg_nd.midpoint := by - exact midpt_of_vector_to_target h +theorem SegND.midpt_of_vector_to_target {seg_nd : SegND P} (h : VEC A seg_nd.target = (1 / 2 : ℝ) • VEC seg_nd.source seg_nd.target) : A = seg_nd.midpoint := + Seg.midpt_of_vector_to_target h /-- Given a segment $AB$ and a point P, if vector $\overrightarrow{AP}$ is same as vector $\overrightarrow{PB}$, P is the midpoint of $AB$. -/ -theorem midpt_of_same_vector_to_source_and_target {seg : Seg P} (h : VEC seg.1 A = VEC A seg.2) :A = seg.midpoint := by - refine' midpt_of_vector_from_source _ +theorem Seg.midpt_of_same_vector_to_source_and_target {seg : Seg P} (h : VEC seg.1 A = VEC A seg.2) : A = seg.midpoint := by + refine' Seg.midpt_of_vector_from_source _ apply smul_right_injective _ (two_ne_zero' ℝ) dsimp rw [two_smul] @@ -1382,11 +1434,12 @@ theorem midpt_of_same_vector_to_source_and_target {seg : Seg P} (h : VEC seg.1 A rw [two_smul, vec_add_vec, ← add_smul] norm_num -theorem midpt_of_same_vector_to_source_and_target_nd {seg_nd : SegND P} (h : VEC seg_nd.source A = VEC A seg_nd.target) :A = seg_nd.midpoint := by - exact midpt_of_same_vector_to_source_and_target h +theorem SegND.midpt_of_same_vector_to_source_and_target {seg_nd : SegND P} (h : VEC seg_nd.source A = VEC A seg_nd.target) : A = seg_nd.midpoint := + Seg.midpt_of_same_vector_to_source_and_target h /-- The midpoint of a segment lies on the segment. -/ -theorem Seg.midpt_lies_on {seg : Seg P} : seg.midpoint LiesOn seg := ⟨1 / 2, by norm_num; exact seg.vec_source_midpt⟩ +theorem Seg.midpt_lies_on {seg : Seg P} : seg.midpoint LiesOn seg := + ⟨1 / 2, by norm_num; exact seg.vec_source_midpt⟩ /-- The midpoint of a segment lies on the segment. -/ theorem Seg.lies_on_of_eq_midpt {seg : Seg P} (h : A = seg.midpoint) : A LiesOn seg := by @@ -1411,24 +1464,24 @@ theorem SegND.lies_int_of_eq_midpt {seg_nd : SegND P} (h : A = seg_nd.midpoint) exact seg_nd.midpt_lies_int /-- A point $X$ on a given segment $AB$ is the midpoint if and only if the vector $\overrightarrow{AX}$ is the same as the vector $\overrightarrow{XB}$. -/ -theorem midpt_iff_same_vector_to_source_and_target {X : P} {seg : Seg P} : X = seg.midpoint ↔ (SEG seg.source X).toVec = (SEG X seg.target).toVec := - ⟨fun h ↦ Seg.vec_eq_of_eq_midpt h, fun h ↦ midpt_of_same_vector_to_source_and_target h⟩ +theorem Seg.midpt_iff_same_vector_to_source_and_target {X : P} {seg : Seg P} : X = seg.midpoint ↔ (SEG seg.source X).toVec = (SEG X seg.target).toVec := + ⟨fun h ↦ vec_eq_of_eq_midpt h, fun h ↦ midpt_of_same_vector_to_source_and_target h⟩ theorem SegND.midpt_iff_same_vector_to_source_and_target {X : P} {seg_nd : SegND P} : X = seg_nd.midpoint ↔ (SEG seg_nd.source X).toVec = (SEG X seg_nd.target).toVec := - ⟨fun h ↦ Seg.vec_eq_of_eq_midpt h, fun h ↦ midpt_of_same_vector_to_source_and_target h⟩ + ⟨fun h ↦ vec_eq_of_eq_midpt h, fun h ↦ midpt_of_same_vector_to_source_and_target h⟩ /-- The midpoint of a segment has same distance to the source and to the target of the segment. -/ -theorem dist_target_eq_dist_source_of_midpt {seg : Seg P} : (SEG seg.source seg.midpoint).length = (SEG seg.midpoint seg.target).length := by +theorem Seg.dist_target_eq_dist_source_of_midpt {seg : Seg P} : (SEG seg.source seg.midpoint).length = (SEG seg.midpoint seg.target).length := by rw [Seg.length_eq_norm_toVec, Seg.length_eq_norm_toVec] exact congrArg norm seg.vec_midpt_eq /-- The midpoint of a segment has same distance to the source and to the target of the segment. -/ -theorem dist_target_eq_dist_source_of_eq_midpt {X : P} {seg : Seg P} (h : X = seg.midpoint) : (SEG seg.1 X).length = (SEG X seg.2).length := by +theorem Seg.dist_target_eq_dist_source_of_eq_midpt {X : P} {seg : Seg P} (h : X = seg.midpoint) : (SEG seg.1 X).length = (SEG X seg.2).length := by rw [h] exact dist_target_eq_dist_source_of_midpt /-- A point $X$ is the midpoint of a segment $AB$ if and only if $X$ lies on $AB$ and $X$ has equal distance to $A$ and $B$. -/ -theorem eq_midpoint_iff_in_seg_and_dist_target_eq_dist_source {X : P} {seg : Seg P} : X = seg.midpoint ↔ (X LiesOn seg) ∧ (SEG seg.source X).length = (SEG X seg.target).length := by +theorem Seg.eq_midpt_iff_in_seg_and_dist_target_eq_dist_source {X : P} {seg : Seg P} : X = seg.midpoint ↔ (X LiesOn seg) ∧ (SEG seg.source X).length = (SEG X seg.target).length := by refine' ⟨fun h ↦ ⟨Seg.lies_on_of_eq_midpt h, dist_target_eq_dist_source_of_eq_midpt h⟩, _⟩ intro ⟨⟨t, ht0, ht1, ht⟩, hv⟩ rw [Seg.length_eq_norm_toVec, Seg.length_eq_norm_toVec] at hv @@ -1449,8 +1502,13 @@ theorem eq_midpoint_iff_in_seg_and_dist_target_eq_dist_source {X : P} {seg : Seg exact (eq_add_of_sub_eq (mul_right_cancel₀ h0 h)).symm exact midpt_of_vector_from_source (by rw [ht, h]) -theorem SegND_eq_midpoint_iff_in_seg_and_dist_target_eq_dist_source {X : P} {seg_nd : SegND P} : X = seg_nd.midpoint ↔ (X LiesOn seg_nd) ∧ (SEG seg_nd.source X).length = (SEG X seg_nd.target).length := - eq_midpoint_iff_in_seg_and_dist_target_eq_dist_source +theorem SegND.eq_midpt_iff_in_seg_and_dist_target_eq_dist_source {X : P} {seg_nd : SegND P} : X = seg_nd.midpoint ↔ (X LiesOn seg_nd) ∧ (SEG seg_nd.source X).length = (SEG X seg_nd.target).length := + seg_nd.1.eq_midpt_iff_in_seg_and_dist_target_eq_dist_source + +theorem Seg.reverse_midpt_eq_midpt {seg : Seg P} : seg.reverse.midpoint = seg.midpoint := sorry + +theorem SegND.reverse_midpt_eq_midpt {seg_nd : SegND P} : seg_nd.reverse.midpoint = seg_nd.midpoint := + seg_nd.1.reverse_midpt_eq_midpt end midpoint @@ -1460,11 +1518,11 @@ section existence_theorem -/ /-- Given a segment $AB$, the midpoint of $A$ and $B + \overrightarrow{AB}$ is B. -/ -theorem target_eq_vec_vadd_target_midpt {seg : Seg P} : seg.2 = (SEG seg.1 (seg.toVec +ᵥ seg.2)).midpoint := +theorem Seg.target_eq_vec_vadd_target_midpt {seg : Seg P} : seg.2 = (SEG seg.1 (seg.toVec +ᵥ seg.2)).midpoint := midpt_of_same_vector_to_source_and_target (vadd_vsub seg.toVec seg.2).symm theorem SegND.target_eq_vec_vadd_target_midpt {seg_nd : SegND P} : seg_nd.target = (SEG seg_nd.source (seg_nd.toVecND.1 +ᵥ seg_nd.target)).midpoint := - midpt_of_same_vector_to_source_and_target (vadd_vsub seg_nd.toVecND.1 seg_nd.target).symm + Seg.midpt_of_same_vector_to_source_and_target (vadd_vsub seg_nd.toVecND.1 seg_nd.target).symm /-- `This theorem should be replaced! B is midpt of A and B + VEC A B, midpt liesint a seg_nd` Given a nondegenerate segment $AB$, B lies in the interior of the segment of $A(B + \overrightarrow{AB})$. -/ theorem SegND.target_lies_int_seg_source_vec_vadd_target {seg_nd : SegND P} : seg_nd.target LiesInt (SEG seg_nd.source (seg_nd.toVecND.1 +ᵥ seg_nd.target)) := sorry diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean index 72ed5b99..0613a3f8 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean @@ -8,31 +8,6 @@ variable {P : Type _} [EuclideanPlane P] (seg_nd : SegND P) -- theorem same_extn_of_source_lies_int {seg_nd : SegND P} {A : P} (h : A LiesInt seg_nd) : (SEG_nd A seg_nd.target ) = seg_nd.extension --- Define the extpoint of a ray to be a point lies on the ray.toLine which has given distence to the ray.source -def Ray.extpoint (l : Ray P) (r : ℝ) : P := sorry -- r * l.toDir.toVec +ᵥ l.source - -theorem lies_on_of_nonneg_extpoint (l : Ray P) {A : P} {r : ℝ} {hnonneg : 0 ≤ r} (h : A = Ray.extpoint l r) : A LiesOn l := sorry -theorem lies_int_of_pos_extpoint (l : Ray P) {A : P} {r : ℝ} {hpos : 0 < r} (h : A = Ray.extpoint l r) : A LiesInt l := sorry -theorem seg_length_eq_dist_of_extpoint (l : Ray P) {A : P} {r : ℝ} {hnonneg : 0 ≤ r} (h : A = Ray.extpoint l r): (SEG l.source A).length = r := sorry --- 暂时只是想实现这一功能，能够写“延长AB到C使得AB=BC”这种话，内容可能还不是很好 - -theorem length_eq_length_add_length_of_lies_on_extension (seg_nd : SegND P) {A : P} (h : A LiesOn seg_nd.extension) : (SEG seg_nd.source A).length = seg_nd.1.length + (SEG seg_nd.target A).length := sorry - -theorem Ray.lieson_eq_dist {A : P} {r : Ray P} (h : A LiesOn r) : VEC r.1 A = (dist r.1 A) • r.2.unitVec := by - by_cases heq : A = r.1 - · rw [← heq, vec_same_eq_zero, dist_self, zero_smul] - push_neg at heq - have h : A LiesInt r := ⟨h, heq⟩ - have h₁ : RAY r.1 A h.2 = r := Ray.pt_pt_eq_ray h - calc - _ = (VEC_nd r.1 A h.2).1 := rfl - _ = ‖VEC_nd r.1 A h.2‖ • (VEC_nd r.1 A h.2).toDir.unitVec := by simp - _ = (dist r.1 A) • (VEC_nd r.1 A h.2).toDir.unitVec := by - rw [dist_comm, NormedAddTorsor.dist_eq_norm'] - rfl - _ = (dist r.1 A) • (RAY r.1 A h.2).2.unitVec := rfl - _ = (dist r.1 A) • r.2.unitVec := by rw [h₁] - /-SegND_eq_midpoint_iff_in_seg_and_dist_target_eq_dist_source should be replaced by the following three midpoint → liesint seg_nd midpoint → dist source = dist target @@ -41,14 +16,4 @@ theorem Ray.lieson_eq_dist {A : P} {r : Ray P} (h : A LiesOn r) : VEC r.1 A = (d by the way in_seg shoud be renamed by current naming system -/ - -theorem lies_int_of_midpoint_of_seg_nd {seg_nd : SegND P} : seg_nd.midpoint LiesInt seg_nd := by sorry - -theorem dist_source_eq_dist_target_of_midpoint {seg : Seg P} : (SEG seg.midpoint seg.source).length = (SEG seg.midpoint seg.target).length := by sorry - -theorem eq_midpoint_of_lies_on_and_dist_source_eq_dist_target {seg : Seg P} {M : P} {h : M LiesOn seg} {heq : (SEG M seg.source).length = (SEG M seg.target).length} : M = seg.midpoint := by sorry -theorem midpt_of_rev_eq_midpt (A B : P) : (SEG A B).midpoint = (SEG B A).midpoint := by sorry - -theorem lies_int_toray_of_lies_int_ext_of_seg_nd (A B C : P) (h1 : B ≠ A) (h : C LiesInt ((SEG_nd A B h1).extension)) : C LiesInt (SEG_nd A B h1).toRay := by sorry - end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean index 903275a1..f7d9f558 100644 --- a/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean +++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean @@ -1,4 +1,4 @@ -import EuclideanGeometry.Foundation.Axiom.Linear.Parallel +import EuclideanGeometry.Foundation.Axiom.Linear.Perpendicular import EuclideanGeometry.Foundation.Axiom.Basic.Angle /-! @@ -8,13 +8,20 @@ import EuclideanGeometry.Foundation.Axiom.Basic.Angle noncomputable section -open Classical - namespace EuclidGeom +open Classical Dir + /-- The angle value between two directed figures. -/ def DirObj.AngDiff {α β} [DirObj α] [DirObj β] (F : α) (G : β) : AngValue := toDir G -ᵥ toDir F +/-- The `AngDValue` between two figures with projective directions. -/ +def ProjObj.DAngDiff {α β} [ProjObj α] [ProjObj β] (F : α) (G : β) : AngDValue := toProj G -ᵥ toProj F + +export ProjObj (DAngDiff) + +export DirObj (AngDiff) + /- Define values of oriented angles, in (-π, π], modulo 2 π. -/ /- Define oriented angles, ONLY taking in two rays starting at one point! And define ways to construct oriented angles, by given three points on the plane, and etc. -/ @@ -28,8 +35,6 @@ structure Angle (P : Type*) [EuclideanPlane P] where attribute [pp_dot] Angle.source Angle.dir₁ Angle.dir₂ --- Do we need the angle between two lines, which is determined by a vertex and two `proj`s, and take values in `AngDValue`? - variable {P : Type _} [EuclideanPlane P] namespace Angle @@ -46,17 +51,17 @@ def mk_two_ray_of_eq_source (r : Ray P) (r' : Ray P) (_h : r.source = r'.source) formed by rays $OA$ and $OB$. We use $\verb|ANG|$ to abbreviate $\verb|Angle.mk_pt_pt_pt|$. -/ def mk_pt_pt_pt (A O B : P) (h₁ : A ≠ O) (h₂ : B ≠ O) : Angle P where source := O - dir₁ := (RAY O A h₁).toDir - dir₂ := (RAY O B h₂).toDir + dir₁ := (VEC_nd O A h₁).toDir + dir₂ := (VEC_nd O B h₂).toDir def mk_ray_pt (r : Ray P) (A : P) (h : A ≠ r.source) : Angle P where source := r.source dir₁ := r.toDir - dir₂ := (RAY r.source A h).toDir + dir₂ := (VEC_nd r.source A h).toDir def mk_pt_ray (A : P) (r : Ray P) (h : A ≠ r.source) : Angle P where source := r.source - dir₁ := (RAY r.source A h).toDir + dir₁ := (VEC_nd r.source A h).toDir dir₂ := r.toDir def mk_dirline_dirline (l₁ l₂ : DirLine P) (h : ¬ l₁ ∥ l₂) : Angle P where @@ -72,6 +77,12 @@ def value : AngValue := ang.dir₂ -ᵥ ang.dir₁ @[pp_dot] abbrev dvalue : AngDValue := (ang.value : AngDValue) +@[pp_dot] +abbrev proj₁ : Proj := ang.dir₁.toProj + +@[pp_dot] +abbrev proj₂ : Proj := ang.dir₂.toProj + @[pp_dot] abbrev IsPos : Prop := ang.value.IsPos @@ -93,7 +104,7 @@ abbrev IsRight : Prop := ang.value.IsRight end Angle /-- The value of $\verb|Angle.mk_pt_pt_pt| A O B$. We use `∠` to abbreviate -$\verb|Angle.value_of_angle_of_three_point_nd|$.-/ +$\verb|Angle.value_of_angle_of_three_point_nd|$. -/ abbrev value_of_angle_of_three_point_nd (A O B : P) (h₁ : A ≠ O) (h₂ : B ≠ O) : AngValue := (Angle.mk_pt_pt_pt A O B h₁ h₂).value @@ -191,9 +202,12 @@ theorem source_lies_on_end_ray : ang.source LiesOn ang.end_ray := theorem start_ray_not_para_end_ray_of_isND (h : ang.IsND) : ¬ ang.start_ray ∥ ang.end_ray := Dir.toProj_ne_toProj_iff_neg_vsub_isND.mpr h -theorem start_ray_eq_end_ray_of_value_eq_zero (h : ang.value = 0) : ang.start_ray = ang.end_ray := sorry +theorem start_ray_eq_end_ray_of_value_eq_zero (h : ang.value = 0) : ang.start_ray = ang.end_ray := + Ray.ext ang.start_ray ang.end_ray rfl (eq_of_vsub_eq_zero h).symm -theorem start_ray_eq_end_ray_reverse_of_value_eq_pi (h : ang.value = π) : ang.start_ray = ang.end_ray.reverse := sorry +theorem start_ray_eq_end_ray_reverse_of_value_eq_pi (h : ang.value = π) : ang.start_ray = ang.end_ray.reverse := + Ray.ext ang.start_ray ang.end_ray.reverse rfl + (neg_eq_iff_eq_neg.mp ((eq_neg_of_vsub_eq_pi ang.dir₂ ang.dir₁).mpr h).symm) @[pp_dot] def start_dirLine (ang : Angle P) : DirLine P := DirLine.mk_pt_dir ang.source ang.dir₁ @@ -231,6 +245,27 @@ theorem start_dirLine_eq_end_dirLine_reverse_of_value_eq_pi (h : ang.value = π) end start_end_ray section carrier +/- +def dir_min (ang : Angle P) : Dir := if ang.IsNeg then ang.dir₂ else ang.dir₁ + +def dir_max (ang : Angle P) : Dir := if ang.IsNeg then ang.dir₁ else ang.dir₂ + +def abs (ang : Angle P) : Angle P where + source := ang.source + dir₁ := ang.dir_min + dir₂ := ang.dir_max + +variable {ang : Angle P} + +theorem abs_value_eq_value_abs : ang.abs.value = ang.value.abs := sorry + +theorem abs_not_isNeg : ¬ ang.abs.IsNeg := sorry + +protected structure IsInt (p : P) (ang : Angle P) : Prop where + ne_source : p ≠ ang.source + isInt : sbtw ang.dir_min (VEC_nd ang.source p ne_source).toDir ang.dir_max +-/ + /- -- `should discuss this later, is there a better definition?` ite, dite is bitter to deal with /- `What does it mean to be LiesIn a angle? when the angle < 0`, for now it is defined as the smaller side. and when angle = π, it is defined as the left side -/ @@ -239,13 +274,13 @@ section carrier protected def IsOn (p : P) (ang : Angle P) : Prop := if h : p = ang.source then True - else btw ang.dir₁ (RAY ang.source p h).toDir ang.dir₂ + else btw ang.dir₁ (VEC_nd ang.source p h).toDir ang.dir₂ /- There may be problems when `ang.value = 0`. See the example below. Maybe change it to `ang.IsInt p ∨ p LiesOn ang.strat_ray ∨ p LiesOn ang.end_ray`. -/ protected structure IsInt (p : P) (ang : Angle P) : Prop where ne_source : p ≠ ang.source - isInt : sbtw ang.dir₁ (RAY ang.source p ne_source).toDir ang.dir₂ + isInt : sbtw ang.dir₁ (VEC_nd ang.source p ne_source).toDir ang.dir₂ variable {p : P} {ang : Angle P} {d : Dir} {r : Ray P} @@ -268,13 +303,13 @@ instance : IntFig (Angle P) P where interior_subset_carrier _ _ := Angle.ison_of_isint theorem source_lies_on (ang : Angle P) : ang.source LiesOn ang := by - show if h : ang.1 = ang.1 then True else btw ang.dir₁ (RAY ang.1 ang.1 h).toDir ang.dir₂ + show if h : ang.1 = ang.1 then True else btw ang.dir₁ (VEC_nd ang.1 ang.1 h).toDir ang.dir₂ simp only [dite_true] theorem lies_on_of_eq (h : p = ang.source) : p LiesOn ang := by simp only [h, source_lies_on] -theorem lies_on_iff_btw_of_ptNe [_h : PtNe p ang.source] : p LiesOn ang ↔ btw ang.dir₁ (RAY ang.source p).toDir ang.dir₂ := +theorem lies_on_iff_btw_of_ptNe [_h : PtNe p ang.source] : p LiesOn ang ↔ btw ang.dir₁ (VEC_nd ang.source p).toDir ang.dir₂ := (dite_prop_iff_and _).trans ((and_iff_right (fun _ ↦ trivial)).trans (forall_prop_of_true _h.1)) example (p : P) {ang : Angle P} [PtNe p ang.source] (h : ang.dir₁ = ang.dir₂) : p LiesOn ang := by @@ -319,7 +354,10 @@ theorem mk_two_ray_of_eq_source_start_ray : (mk_two_ray_of_eq_source r r' h).sta theorem mk_two_ray_of_eq_source_end_ray : (mk_two_ray_of_eq_source r r' h).end_ray = r' := Ray.ext (mk_two_ray_of_eq_source r r' h).end_ray r' h rfl -theorem mk_two_ray_of_eq_source_value : (Angle.mk_two_ray_of_eq_source r r' h).value = r'.toDir -ᵥ r.toDir := rfl +theorem mk_two_ray_of_eq_source_value : (mk_two_ray_of_eq_source r r' h).value = r'.toDir -ᵥ r.toDir := rfl + +theorem same_ray_value_eq_zero (r : Ray P) : (mk_two_ray_of_eq_source r r rfl).value = 0 := + vsub_self r.2 end mk_two_ray @@ -331,10 +369,10 @@ variable {A O B : P} (ha : A ≠ O) (hb : B ≠ O) theorem mk_pt_pt_pt_source : (ANG A O B ha hb).source = O := rfl @[simp] -theorem mk_pt_pt_pt_dir₁ : (ANG A O B ha hb).dir₁ = (RAY O A ha).toDir := rfl +theorem mk_pt_pt_pt_dir₁ : (ANG A O B ha hb).dir₁ = (VEC_nd O A ha).toDir := rfl @[simp] -theorem mk_pt_pt_pt_dir₂ : (ANG A O B ha hb).dir₂ = (RAY O B hb).toDir := rfl +theorem mk_pt_pt_pt_dir₂ : (ANG A O B ha hb).dir₂ = (VEC_nd O B hb).toDir := rfl @[simp] theorem mk_pt_pt_pt_start_ray : (ANG A O B ha hb).start_ray = RAY O A ha := rfl @@ -342,8 +380,60 @@ theorem mk_pt_pt_pt_start_ray : (ANG A O B ha hb).start_ray = RAY O A ha := rfl @[simp] theorem mk_pt_pt_pt_end_ray : (ANG A O B ha hb).end_ray = RAY O B hb := rfl +@[simp] +theorem neg_value_eq_rev_ang : - ∠ A O B ha hb = ∠ B O A hb ha := + neg_vsub_eq_vsub_rev (VEC_nd O B hb).toDir (VEC_nd O A ha).toDir + +theorem neg_value_of_rev_ang {A B O : P} [h₁ : PtNe A O] [h₂ : PtNe B O] : ∠ A O B = -∠ B O A := + (neg_value_eq_rev_ang h₂.1 h₁.1).symm + +theorem pt_pt_pt_value_eq_zero_of_same_pt (A O : P) [PtNe A O] : ∠ A O A = 0 := + vsub_self (VEC_nd O A).toDir + end pt_pt_pt +section mk_ray_pt + +variable (r : Ray P) (A : P) (h : A ≠ r.source) + +@[simp] +theorem mk_ray_pt_source : (mk_ray_pt r A h).source = r.source := rfl + +@[simp] +theorem mk_ray_pt_dir₁ : (mk_ray_pt r A h).dir₁ = r.toDir := rfl + +@[simp] +theorem mk_ray_pt_dir₂ : (mk_ray_pt r A h).dir₂ = (VEC_nd r.source A h).toDir := rfl + +@[simp] +theorem mk_ray_pt_start_ray : (mk_ray_pt r A h).start_ray = r := rfl + +@[simp] +theorem mk_ray_pt_end_ray : (mk_ray_pt r A h).end_ray = RAY r.source A h := rfl + +end mk_ray_pt + +section mk_pt_ray + +variable (A : P) (r : Ray P) (h : A ≠ r.source) + +@[simp] +theorem mk_pt_ray_source : (mk_pt_ray A r h).source = r.source := rfl + +@[simp] +theorem mk_pt_ray_dir₁ : (mk_pt_ray A r h).dir₁ = (VEC_nd r.source A h).toDir := rfl + +@[simp] +theorem mk_pt_ray_dir₂ : (mk_pt_ray A r h).dir₂ = r.toDir := rfl + +@[simp] +theorem mk_pt_ray_start_ray : (mk_pt_ray A r h).start_ray = RAY r.source A h := rfl + +@[simp] +theorem mk_pt_ray_end_ray : (mk_pt_ray A r h).end_ray = r := rfl + +end mk_pt_ray + section change_dir def mk_dir₁ (ang : Angle P) (d : Dir) : Angle P where @@ -356,9 +446,20 @@ def mk_dir₂ (ang : Angle P) (d : Dir) : Angle P where dir₁ := d dir₂ := ang.dir₂ -theorem value_mk_dir₁ (ang : Angle P) (d : Dir) : (mk_dir₁ ang d).value = d -ᵥ ang.dir₁ := rfl +@[simp] +theorem mk_dir₁_source {ang : Angle P} (d : Dir) : (mk_dir₁ ang d).source = ang.source := rfl + +@[simp] +theorem mk_dir₂_source {ang : Angle P} (d : Dir) : (mk_dir₂ ang d).source = ang.source := rfl + +theorem mk_dir₁_value {ang : Angle P} (d : Dir) : (mk_dir₁ ang d).value = d -ᵥ ang.dir₁ := rfl + +theorem mk_dir₂_value {ang : Angle P} (d : Dir) : (mk_dir₂ ang d).value = ang.dir₂ -ᵥ d := rfl + +theorem mk_dir₁_dir₂_eq_self {ang : Angle P} : mk_dir₁ ang ang.dir₂ = ang := rfl + +theorem mk_dir₂_dir₁_eq_self {ang : Angle P} : mk_dir₂ ang ang.dir₁ = ang := rfl -theorem value_mk_dir₂ (ang : Angle P) (d : Dir) : (mk_dir₂ ang d).value = ang.dir₂ -ᵥ d := rfl /- variable {p : P} {ang : Angle P} {d : Dir} @@ -392,27 +493,45 @@ variable {ang : Angle P} @[simp] theorem mk_start_ray_end_ray_eq_self : mk_two_ray_of_eq_source ang.start_ray ang.end_ray rfl = ang := rfl -theorem eq_of_lies_on_ray {A B : P} [PtNe A ang.source] [PtNe B ang.source] (ha : A LiesOn ang.start_ray) (hb : B LiesOn ang.end_ray) : ANG A ang.source B = ang := sorry +theorem eq_of_lies_int_ray {A B : P} (ha : A LiesInt ang.start_ray) (hb : B LiesInt ang.end_ray) : ANG A ang.source B ha.2 hb.2 = ang := + Angle.ext (ANG A ang.source B ha.2 hb.2) ang rfl + (Ray.pt_pt_toDir_eq_ray_toDir ha) (Ray.pt_pt_toDir_eq_ray_toDir hb) + +theorem value_eq_of_lies_int_ray {A B : P} (ha : A LiesInt ang.start_ray) (hb : B LiesInt ang.end_ray) : ∠ A ang.source B ha.2 hb.2 = ang.value := + congrArg value (eq_of_lies_int_ray ha hb) + +theorem eq_of_lies_on_ray {A B : P} [_ha : PtNe A ang.source] [_hb : PtNe B ang.source] (ha : A LiesOn ang.start_ray) (hb : B LiesOn ang.end_ray) : ANG A ang.source B = ang := + eq_of_lies_int_ray ⟨ha, _ha.1⟩ ⟨hb, _hb.1⟩ theorem value_eq_of_lies_on_ray {A B : P} [PtNe A ang.source] [PtNe B ang.source] (ha : A LiesOn ang.start_ray) (hb : B LiesOn ang.end_ray) : ∠ A ang.source B = ang.value := congrArg value (eq_of_lies_on_ray ha hb) -theorem eq_of_lies_int_ray {A B : P} (ha : A LiesInt ang.start_ray) (hb : B LiesInt ang.end_ray) : ANG A ang.source B ha.2 hb.2 = ang := sorry +theorem eq_of_lies_on_ray_pt_pt {A B C D O : P} [PtNe A O] [PtNe B O] [_hc : PtNe C O] [_hd : PtNe D O] (hc : C LiesOn (RAY O A)) (hd : D LiesOn (RAY O B) ) : ANG C O D = ANG A O B := + have hc : C LiesOn (ANG A O B).start_ray := hc + have hd : D LiesOn (ANG A O B).end_ray := hd + haveI : PtNe C (ANG A O B).source := _hc + haveI : PtNe D (ANG A O B).source := _hd + eq_of_lies_on_ray hc hd -theorem value_eq_of_lies_int_ray {A B : P} (ha : A LiesInt ang.start_ray) (hb : B LiesInt ang.end_ray) : ∠ A ang.source B ha.2 hb.2 = ang.value := - congrArg value (eq_of_lies_int_ray ha hb) +theorem value_eq_of_lies_on_ray_pt_pt {A B C D O : P} [PtNe A O] [PtNe B O] [PtNe C O] [PtNe D O] (hc : C LiesOn (RAY O A)) (hd : D LiesOn (RAY O B) ) : ∠ C O D = ∠ A O B := + congrArg value (eq_of_lies_on_ray_pt_pt hc hd) -theorem eq_of_lies_on_ray_pt_pt {A B C D O : P} [PtNe A O] [PtNe B O] [PtNe C O] [PtNe D O] (hc : C LiesOn (RAY O A) ) (hd : D LiesOn (RAY O B) ) : ANG C O D = ANG A O B := sorry +theorem mk_ray_pt_eq_of_lies_int {A : P} (h : A LiesInt ang.end_ray) : mk_ray_pt ang.start_ray A h.2 = ang := + Angle.ext (mk_ray_pt ang.start_ray A h.2) ang rfl rfl (Ray.pt_pt_toDir_eq_ray_toDir h) -theorem value_eq_of_lies_on_ray_pt_pt {A B C D O : P} [PtNe A O] [PtNe B O] [PtNe C O] [PtNe D O] (hc : C LiesOn (RAY O A) ) (hd : D LiesOn (RAY O B) ) : ∠ C O D = ∠ A O B := - congrArg value (eq_of_lies_on_ray_pt_pt hc hd) +theorem mk_ray_pt_eq_of_lies_on {A : P} [_h : PtNe A ang.source] (h : A LiesOn ang.end_ray) : mk_ray_pt ang.start_ray A _h.1 = ang := + Angle.ext (mk_ray_pt ang.start_ray A _h.1) ang rfl rfl (Ray.pt_pt_toDir_eq_ray_toDir ⟨h, _h.1⟩) + +theorem mk_pt_ray_eq_of_lies_int {A : P} (h : A LiesInt ang.start_ray) : mk_pt_ray A ang.end_ray h.2 = ang := + Angle.ext (mk_pt_ray A ang.end_ray h.2) ang rfl (Ray.pt_pt_toDir_eq_ray_toDir h) rfl + +theorem mk_pt_ray_eq_of_lies_on {A : P} [_h : PtNe A ang.source] (h : A LiesOn ang.start_ray) : mk_pt_ray A ang.end_ray _h.1 = ang := + Angle.ext (mk_pt_ray A ang.end_ray _h.1) ang rfl (Ray.pt_pt_toDir_eq_ray_toDir ⟨h, _h.1⟩) rfl -theorem mk_start_dirLine_end_dirLine_eq_self_of_isND (h : ang.IsND): mk_dirline_dirline ang.start_dirLine ang.end_dirLine (start_dirLine_not_para_end_dirLine_of_value_ne_zero h) = ang := by - ext - · simp only [mk_dirline_dirline] - sorry - · rfl - · rfl +theorem mk_start_dirLine_end_dirLine_eq_self_of_isND (h : ang.IsND): mk_dirline_dirline ang.start_dirLine ang.end_dirLine (start_dirLine_not_para_end_dirLine_of_value_ne_zero h) = ang := + Angle.ext (mk_dirline_dirline ang.start_dirLine ang.end_dirLine _) ang + (Eq.symm <| inx_of_line_eq_inx (start_dirLine_not_para_end_dirLine_of_value_ne_zero h) + ⟨ang.source_lies_on_start_dirLine, ang.source_lies_on_end_dirLine⟩) rfl rfl end mk_compatibility @@ -448,9 +567,108 @@ theorem eq_start_ray_of_eq_value_eq_end_ray (h : ang₁.end_ray = ang₂.end_ray end cancel +section angle_value + +open AngValue + +variable {ang ang₁ ang₂ : Angle P} {A O B : P} [PtNe A O] [PtNe B O] + +theorem value_eq_zero_of_same_dir (h : ang.dir₁ = ang.dir₂) : ang.value = 0 := by + rw [value, h, vsub_self] + +theorem value_eq_pi_of_eq_neg_dir (h : ang.dir₁ = - ang.dir₂) : ang.value = π := + (eq_neg_of_vsub_eq_pi ang.dir₂ ang.dir₁).mp (by rw [h, neg_neg]) + +theorem value_eq_of_dir_eq (h₁ : ang₁.dir₁ = ang₂.dir₁) (h₂ : ang₁.dir₂ = ang₂.dir₂) : ang₁.value = ang₂.value := by + rw [value, value, h₁, h₂] + +theorem value_toReal_le_pi : ang.value.toReal ≤ π := ang.value.toReal_le_pi + +theorem neg_pi_lt_value_toReal : - π < ang.value.toReal := ang.value.neg_pi_lt_toReal + +theorem dir₂_eq_value_vadd_dir₁ : ang.dir₂ = ang.value +ᵥ ang.dir₁ := + (eq_vadd_iff_vsub_eq ang.dir₂ ang.value ang.dir₁).mpr rfl + +theorem dvalue_eq_dAngDiff : ang.dvalue = DAngDiff ang.proj₁ ang.proj₂ := rfl + +theorem dvalue_eq_dvalue_of_proj_eq_proj (h₁ : ang₁.proj₁ = ang₂.proj₁) (h₂ : ang₁.proj₂ = ang₂.proj₂) : ang₁.dvalue = ang₂.dvalue := by + rw [dvalue_eq_dAngDiff, dvalue_eq_dAngDiff, h₁, h₂] + +theorem dir_perp_iff_dvalue_eq_pi_div_two : ang.dir₁ ⟂ ang.dir₂ ↔ ang.dvalue = ∡[π / 2] := by + apply (eq_vadd_iff_vsub_eq ang.proj₁ ∡[Real.pi / 2] ang.proj₂).trans + nth_rw 1 [← AngDValue.neg_coe_pi_div_two, ← neg_vsub_eq_vsub_rev] + exact neg_inj + +theorem line_pt_pt_perp_iff_dvalue_eq_pi_div_two : LIN O A ⟂ LIN O B ↔ (ANG A O B).dvalue = ∡[π / 2] := + (ANG A O B).dir_perp_iff_dvalue_eq_pi_div_two + +theorem angle_dval_eq_pi_div_two_at_perp_foot (A B C : P) [_h : PtNe B C] (l : Line P) (hb : B LiesOn l) (ha : ¬ A LiesOn l) (hc : C = perp_foot A l) : haveI : PtNe A C := ⟨((pt_ne_iff_not_lies_on_of_eq_perp_foot hc).mpr ha).symm⟩; (ANG A C B).dvalue = ∡[π / 2] := by + haveI : PtNe A C := ⟨((pt_ne_iff_not_lies_on_of_eq_perp_foot hc).mpr ha).symm⟩ + haveI : PtNe B (perp_foot A l) := by + rw [← hc] + exact _h + apply line_pt_pt_perp_iff_dvalue_eq_pi_div_two.mp _ + rw [Line.line_of_pt_pt_eq_rev] + simp only [hc, Line.eq_line_of_pt_pt_of_ne (perp_foot_lies_on_line A l) hb] + exact line_of_self_perp_foot_perp_line_of_not_lies_on ha + +theorem dir_perp_iff_isRight : ang.dir₁ ⟂ ang.dir₂ ↔ ang.IsRight := + dir_perp_iff_dvalue_eq_pi_div_two.trans isRight_iff_coe.symm + +theorem value_eq_pi_of_lies_int_seg_nd {A B C : P} [PtNe C A] (h : B LiesInt (SEG_nd A C)) : ∠ A B C h.2.symm h.3.symm = π := + value_eq_pi_of_eq_neg_dir ((SEG_nd A C).toDir_eq_neg_toDir_of_lies_int h) + +theorem colinear_iff_dvalue_eq_zero : colinear O A B ↔ (ANG A O B).dvalue = 0 := + colinear_iff_toProj_eq_of_ptNe.trans (eq_comm.trans vsub_eq_zero_iff_eq.symm) + +theorem colinear_iff_not_isND : colinear O A B ↔ ¬ (ANG A O B).IsND := + colinear_iff_dvalue_eq_zero.trans not_isND_iff_coe.symm + +theorem not_colinear_iff_isND : ¬ colinear O A B ↔ (ANG A O B).IsND := + colinear_iff_not_isND.not.trans not_not + +theorem colinear_of_angle_eq_zero (h : ∠ A O B = 0) : colinear O A B := + colinear_iff_not_isND.mpr (not_isND_of_eq_zero h) + +theorem colinear_of_angle_eq_pi (h : ∠ A O B = π ) : colinear O A B := + colinear_iff_not_isND.mpr (not_isND_of_eq_pi h) + +end angle_value + +section sin_cos + +open AngValue + +variable {ang : Angle P} + +theorem sin_pos_iff_isPos : 0 < sin ang.value ↔ ang.IsPos := + isPos_iff_zero_lt_sin.symm + +theorem sin_neg_iff_isNeg : sin ang.value < 0 ↔ ang.IsNeg := + isNeg_iff_sin_lt_zero.symm + +theorem sin_ne_zero_iff_isND : sin ang.value ≠ 0 ↔ ang.IsND := + isND_iff_sin_ne_zero.symm + +theorem sin_eq_zero_iff_not_isND : sin ang.value = 0 ↔ ¬ ang.IsND := + not_isND_iff_sin_eq_zero.symm + +theorem cos_pos_iff_isAcu : 0 < cos ang.value ↔ ang.IsAcu := + isAcu_iff_zero_lt_cos.symm + +theorem cos_neg_iff_isObt : cos ang.value < 0 ↔ ang.IsObt := + isObt_iff_cos_lt_zero.symm + +theorem cos_ne_zero_iff_not_isRight : cos ang.value ≠ 0 ↔ ¬ ang.IsRight := + not_isRight_iff_cos_ne_zero.symm + +theorem cos_eq_zero_iff_isRight : cos ang.value = 0 ↔ ang.IsRight := + isRight_iff_cos_eq_zero.symm + +end sin_cos + end Angle -/- theorem - π < angle.value, angle.value ≤ π, -/ /- theorem when angle > 0, IsInt means lies left of start ray + right of end ray; when angle < 0, ... -/ diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex.lean index 32d12f41..aec5dfbf 100644 --- a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex.lean +++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex.lean @@ -3,6 +3,8 @@ import EuclideanGeometry.Foundation.Axiom.Position.Angle /-! # Constructions of an angle +This document discusses the construction of an angle, their properties, and the relationships between them. + -/ noncomputable section @@ -13,25 +15,14 @@ variable {P : Type _} [EuclideanPlane P] namespace Angle -/- whether an angle is acute/right/obtuse. -/ - -def IsRightAngle (ang : Angle P) : Prop := sorry - - -def IsAcuteAngle (ang : Angle P) : Prop := sorry - - -def IsObtuseAngle (ang : Angle P) : Prop := sorry - ---`This section should be rewrite` -/- Supplementary angles -/ -- Define the supplementary angle to be the angle variable (ang : Angle P) --Maybe the name is too long -def supplementary : Angle P where +@[pp_dot] +def suppl : Angle P where source := ang.source dir₁ := ang.dir₁ dir₂ := - ang.dir₂ @@ -40,22 +31,23 @@ def supplementary : Angle P where theorem reverse_ray_iff_sum_of_angle_eq_pi {ang1 : Angle P} {ang2 : Angle P} (h: ang1.end_ray = ang2.start_ray) : ang1.end_ray = ang2.start_ray.reverse ↔ ang1.value + ang2.value = π ∨ ang1.value + ang2.value = -π := by sorry -theorem right_of_supp_of_right (rt : IsRightAngle ang) : IsRightAngle ang.supplementary := by sorry +theorem right_of_suppl_of_right (h : ang.IsRight) : ang.suppl.IsRight := by sorry -theorem acute_of_supp_of_obtuse (rt : IsObtuseAngle ang) : IsRightAngle ang.supplementary := by sorry +theorem acute_of_suplp_of_obtuse (h : ang.IsObt) : ang.suppl.IsAcu := by sorry -theorem obtuse_of_supp_of_acute (rt : IsAcuteAngle ang) : IsRightAngle ang.supplementary := by sorry +theorem obtuse_of_suppl_of_acute (h : ang.IsAcu) : ang.suppl.IsObt := by sorry -theorem IsND_of_supp_of_IsND (nontriv : ang.IsND) : ang.supplementary.IsND := by sorry +theorem IsND_of_suppl_of_IsND (nontriv : ang.IsND) : ang.suppl.IsND := by sorry -def opposite :(Angle P) where +@[pp_dot] +def oppo :(Angle P) where source := ang.source dir₁ := - ang.dir₁ dir₂ := - ang.dir₂ -theorem opposite_eq_supp_of_supp : ang.supplementary.supplementary = ang := by sorry +theorem oppo_eq_supp_of_supp : ang.suppl.suppl = ang := by sorry -theorem IsND_of_oppo_of_IsND (nontriv : ang.IsND) : ang.opposite.IsND := by sorry +theorem IsND_of_oppo_of_IsND (nontriv : ang.IsND) : ang.oppo.IsND := by sorry end Angle @@ -63,32 +55,21 @@ section parallel variable {P : Type _} [EuclideanPlane P] -- should be stated use mod 2pi first, then back to pi or -pi -theorem ang_eq_ang_of_toDir_eq_toDir {ang₁ ang₂ : Angle P} (hs : ang₁.start_ray.toDir = ang₂.start_ray.toDir) (he : ang₁.end_ray.toDir = ang₂.end_ray.toDir) : ang₁.value = ang₂.value := sorry - -theorem start_ray_toDir_eq_toDir_of_ang_eq_ang {ang₁ ang₂ : Angle P} (hs : ang₁.end_ray.toDir = ang₂.end_ray.toDir) (h : ang₁.value = ang₂.value) : ang₁.start_ray.toDir = ang₂.start_ray.toDir := sorry - -theorem end_ray_toDir_eq_toDir_of_ang_eq_ang {ang₁ ang₂ : Angle P} (hs : ang₁.start_ray.toDir = ang₂.start_ray.toDir) (h : ang₁.value = ang₂.value) : ang₁.end_ray.toDir = ang₂.end_ray.toDir := sorry - --- theorem discuss all possible case of end/start.toDir = +- end/start.toDir --- `do we need construction of OppositeAng?` - -structure IsOppositeAng (ang₁ ang₂ : Angle P) : Prop where - start_ray : ang₁.start_ray = ang₂.start_ray.reverse - end_ray : ang₁.end_ray = ang₂.end_ray.reverse +def IsOppoAng (ang₁ ang₂ : Angle P) : Prop := ang₁ = ang₂.oppo structure IsCorrespondingAng (ang₁ ang₂ : Angle P) : Prop where - start_ray : ang₁.start_ray.toDir = ang₂.start_ray.toDir - end_ray : ang₁.end_ray.toDirLine = ang₂.end_ray.toDirLine + start_ray : ang₁.dir₁ = ang₂.dir₁ + end_ray : ang₁.end_dirLine = ang₂.end_dirLine structure IsConsecutiveIntAng (ang₁ ang₂ : Angle P) : Prop where - start_ray : ang₁.start_ray.toDir = ang₂.start_ray.toDir - end_ray : ang₁.end_ray.toDirLine = ang₂.end_ray.toDirLine.reverse + start_ray : ang₁.dir₁ = ang₂.dir₁ + end_ray : ang₁.end_dirLine = ang₂.end_dirLine.reverse structure IsAlternateIntAng (ang₁ ang₂ : Angle P) : Prop where - start_ray : ang₁.start_ray.toDir = - ang₂.start_ray.toDir - end_ray : ang₁.end_ray.toDirLine = ang₂.end_ray.toDirLine.reverse + start_ray : ang₁.dir₁ = - ang₂.dir₁ + end_ray : ang₁.end_dirLine = ang₂.end_dirLine.reverse -theorem IsOppositeAng.symm {ang₁ ang₂ : Angle P} : IsOppositeAng ang₁ ang₂ → IsOppositeAng ang₂ ang₁ := sorry +theorem IsOppoAng.symm {ang₁ ang₂ : Angle P} : IsOppoAng ang₁ ang₂ → IsOppoAng ang₂ ang₁ := sorry theorem IsCorrespondingAng.symm {ang₁ ang₂ : Angle P} : IsCorrespondingAng ang₁ ang₂ → IsCorrespondingAng ang₂ ang₁ := sorry @@ -96,7 +77,7 @@ theorem IsConsecutiveIntAng.symm {ang₁ ang₂ : Angle P} : IsConsecutiveIntAng theorem IsAlternateIntAng.symm {ang₁ ang₂ : Angle P} : IsAlternateIntAng ang₁ ang₂ → IsAlternateIntAng ang₂ ang₁ := sorry -theorem value_eq_of_isoppositeang {ang₁ ang₂ : Angle P} (h : IsOppositeAng ang₁ ang₂) : ang₁.value = ang₂.value := sorry +theorem value_eq_of_isoppoang {ang₁ ang₂ : Angle P} (h : IsOppoAng ang₁ ang₂) : ang₁.value = ang₂.value := sorry theorem value_eq_of_iscorrespondingang {ang₁ ang₂ : Angle P} (h : IsCorrespondingAng ang₁ ang₂) : ang₁.value = ang₂.value := sorry diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex2.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex2.lean index 2f82c45f..a20041dc 100644 --- a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex2.lean +++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex2.lean @@ -11,16 +11,11 @@ variable {P : Type _} [EuclideanPlane P] section AngleValue -/- theorem - π < angle.value, angle.value ≤ π, -/ -theorem val_gt_neg_pi (ang : Angle P) : -π < ang.value.toReal := sorry - -theorem val_le_pi (ang : Angle P) : ang.value.toReal < π := sorry - /- theorem when angle > 0, IsInt means lies left of start ray + right of end ray; when angle < 0, ... -/ end AngleValue -section AngleSum +section angle_sum namespace Angle @@ -34,14 +29,11 @@ theorem ang_eq_ang_add_ang_mod_pi_of_adj_ang (ang₁ ang₂ : Angle P) (h: ang end Angle -end AngleSum - -section colinear +end angle_sum -theorem colinear_of_angle_eq_zero {A O B : P} {h₁ : A ≠ O} {h₂ : B ≠ O} : ∠ A O B h₁ h₂ = 0 → colinear O A B := by sorry +section angle_sub -theorem colinear_of_angle_eq_pi {A O B : P} {h₁ : A ≠ O} {h₂ : B ≠ O} : ∠ A O B h₁ h₂ = π → colinear O A B := by sorry +end angle_sub -end colinear end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex_trash.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex_trash.lean index c0573ce4..4f5e8600 100644 --- a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex_trash.lean @@ -6,13 +6,13 @@ namespace EuclidGeom variable {P : Type _} [EuclideanPlane P] -theorem perp_foot_lies_int_ray_of_acute_ang {A B C : P} (b_ne_a : B ≠ A) (c_ne_a : C ≠ A) (acu : Angle.IsAcuteAngle (ANG B A C b_ne_a c_ne_a)) : (perp_foot C (LIN A B b_ne_a)) LiesInt (RAY A B b_ne_a) := by sorry +theorem perp_foot_lies_int_ray_of_acute_ang {A B C : P} (b_ne_a : B ≠ A) (c_ne_a : C ≠ A) (acu : Angle.IsAcu (ANG B A C b_ne_a c_ne_a)) : (perp_foot C (LIN A B b_ne_a)) LiesInt (RAY A B b_ne_a) := by sorry -theorem ang_acute_of_is_isoceles {A B C : P} (not_colinear_ABC : ¬ colinear A B C) (isoceles_ABC : (▵ A B C).IsIsoceles) : Angle.IsAcuteAngle (ANG C B A (ne_of_not_colinear not_colinear_ABC).1 (ne_of_not_colinear not_colinear_ABC).2.2.symm) := by sorry +theorem ang_acute_of_is_isoceles {A B C : P} (not_colinear_ABC : ¬ colinear A B C) (isoceles_ABC : (▵ A B C).IsIsoceles) : Angle.IsAcu (ANG C B A (ne_of_not_colinear not_colinear_ABC).1 (ne_of_not_colinear not_colinear_ABC).2.2.symm) := by sorry -theorem ang_acute_of_is_isoceles_variant {A B C : P} (not_colinear_ABC : ¬ colinear A B C) (isoceles_ABC : (▵ A B C).IsIsoceles) : Angle.IsAcuteAngle (ANG A C B (ne_of_not_colinear not_colinear_ABC).2.1 (ne_of_not_colinear not_colinear_ABC).1.symm) := by sorry +theorem ang_acute_of_is_isoceles_variant {A B C : P} (not_colinear_ABC : ¬ colinear A B C) (isoceles_ABC : (▵ A B C).IsIsoceles) : Angle.IsAcu (ANG A C B (ne_of_not_colinear not_colinear_ABC).2.1 (ne_of_not_colinear not_colinear_ABC).1.symm) := by sorry -theorem is_acute_of_is_acute_rev {O A B : P} (h1 : A ≠ O) (h2 : B ≠ O) (h3 : Angle.IsAcuteAngle (ANG A O B h1 h2)) : Angle.IsAcuteAngle (ANG B O A h2 h1) := by sorry +theorem is_acute_of_is_acute_rev {O A B : P} (h1 : A ≠ O) (h2 : B ≠ O) (h3 : Angle.IsAcu (ANG A O B h1 h2)) : Angle.IsAcu (ANG B O A h2 h1) := by sorry theorem ang_eq_ang_of_toDir_eq_neg_toDir {ang₁ ang₂ : Angle P} (hs : ang₁.start_ray.toDir = - ang₂.start_ray.toDir) (he : ang₁.end_ray.toDir = - ang₂.end_ray.toDir) : Angle.value ang₁ = Angle.value ang₂ := by sorry diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle_trash.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle_trash.lean index aa2f5011..a19d9e97 100644 --- a/EuclideanGeometry/Foundation/Axiom/Position/Angle_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle_trash.lean @@ -1,5 +1,4 @@ import EuclideanGeometry.Foundation.Axiom.Position.Angle -import EuclideanGeometry.Foundation.Axiom.Linear.Perpendicular import EuclideanGeometry.Foundation.Axiom.Linear.Ray_trash namespace EuclidGeom @@ -8,45 +7,16 @@ open AngValue variable {P : Type _} [EuclideanPlane P] -theorem Angle.sin_pos_iff_isPos (ang : Angle P) : 0 < sin ang.value ↔ ang.IsPos := isPos_iff_zero_lt_sin.symm - theorem end_ray_toDir_rev_toDir_of_ang_rev_ang {ang₁ ang₂ : Angle P} (hs : ang₁.start_ray.toDir = (ang₂.start_ray).reverse.toDir) (h : ang₁.value = ang₂.value) : ang₁.end_ray.toDir = (ang₂.end_ray).reverse.toDir := sorry theorem start_ray_toDir_rev_toDir_of_ang_rev_ang {ang₁ ang₂ : Angle P} (hs : ang₁.end_ray.toDir = (ang₂.end_ray).reverse.toDir) (h : ang₁.value = ang₂.value) : ang₁.start_ray.toDir = (ang₂.start_ray).reverse.toDir := sorry -theorem angle_value_eq_angle (A : P) (ray : Ray P) [h : PtNe A ray.source] : (Angle.mk_ray_pt ray A h.out).value = VecND.angle ray.2.unitVecND (VEC_nd ray.source A) := sorry - theorem ang_eq_ang_of_toDir_rev_toDir {ang₁ ang₂ : Angle P} (hs : ang₁.start_ray.toDir = - ang₂.start_ray.toDir) (he : ang₁.end_ray.toDir = - ang₂.end_ray.toDir) : ang₁.value = ang₂.value := sorry -theorem angle_eq_zero_of_same_dir {A O : P} [h₁ : PtNe A O] : ∠ A O A = 0 := sorry - -theorem eq_ang_of_lies_int_liesint {A A' B B' O: P} [h₁ : PtNe A O] [h₂ : PtNe B O] [h₁' : PtNe A' O] [h₂' : PtNe B' O] (LiesInt1 : A' LiesInt (RAY O A) ) (LiesInt2 : B' LiesInt (RAY O B) ) : ANG A O B = ANG A' O B' := sorry - ---Nailin Guan -theorem neg_value_of_rev_ang {A B O: P} [h₁ : PtNe A O] [h₂ : PtNe B O] : ∠ A O B = -∠ B O A := sorry - theorem neg_dvalue_of_rev_ang {A B O: P} (h₁ : A ≠ O) (h₂ : B ≠ O) : (ANG A O B h₁ h₂).dvalue = -(ANG B O A h₂ h₁).dvalue := sorry --- WangJingTing -namespace Angle - -theorem end_ray_eq_value_vadd_start_ray (ang : Angle P) : ang.dir₂ = ang.value +ᵥ ang.dir₁ := sorry -def mk_start_ray (ang : Angle P) (ray : Ray P) (h : ang.source = ray.source) : Angle P := Angle.mk_two_ray_of_eq_source ang.start_ray ray h - -def mk_end_ray (ang : Angle P) (ray : Ray P) (h : ang.source = ray.source) : Angle P := Angle.mk_two_ray_of_eq_source ray ang.end_ray h.symm - -theorem value_eq_vsub (ray₁ : Ray P) (ray₂ : Ray P) (h: ray₁.source = ray₂.source) : (Angle.mk_two_ray_of_eq_source ray₁ ray₂ h).value = ray₂.toDir -ᵥ ray₁.toDir := sorry - -theorem mk_strat_ray_value_eq_vsub (ang : Angle P) (ray : Ray P) (h : ang.source = ray.source) : (Angle.mk_start_ray ang ray h).value = ray.toDir -ᵥ ang.dir₁ := sorry - -theorem mk_end_ray_value_eq_vsub (ang : Angle P) (ray : Ray P) (h : ang.source = ray.source) : (Angle.mk_end_ray ang ray h).value = ang.dir₂ -ᵥ ray.toDir := sorry +namespace Angle end Angle -theorem dvalue_eq_ang_rays_perp {ang : Angle P} (h : ang.dvalue = ∡[π / 2]) : ang.start_ray ⟂ ang.end_ray := by - show ang.start_ray.toProj = ∡[π / 2] +ᵥ ang.end_ray.toProj - sorry - -theorem liesint_segnd_value_eq_pi {A B C : P} (hne : B ≠ A) (h : C LiesInt (SEG_nd A B hne)) : ∠ A C B h.2.symm h.3.symm = π := sorry - end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean b/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean index 4be7a546..c895f11a 100644 --- a/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean +++ b/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean @@ -84,10 +84,8 @@ theorem wedge_pos_iff_angle_pos (A B C : P) (nd : ¬colinear A B C) : (0 < wedge rw [sin_pos_iff_isPos] at h3 exact h3 rw [wedge_eq_length_mul_length_mul_sin (bnea := ⟨(ne_of_not_colinear nd).2.2⟩) (cnea := ⟨(ne_of_not_colinear nd).2.1.symm⟩)] - intro h0 - have h3 : 0 < sin ((Angle.mk_pt_pt_pt B A C (ne_of_not_colinear nd).2.2 (ne_of_not_colinear nd).2.1.symm).value) := (sin_pos_iff_isPos (Angle.mk_pt_pt_pt B A C (ne_of_not_colinear nd).2.2 (ne_of_not_colinear nd).2.1.symm)).mpr h0 field_simp - exact h3 + exact sin_pos_iff_isPos.mpr end wedge @@ -103,12 +101,13 @@ theorem odist'_eq_zero_iff_exist_real_vec_eq_smul {A : P} {ray : Ray P} : odist' theorem odist'_eq_length_mul_sin (A : P) (ray : Ray P) [h : PtNe A ray.source] : odist' A ray = (SEG ray.source A).length * sin ((Angle.mk_ray_pt ray A h.out).value) := by rw [odist',Angle.value] - have h0 : (Angle.mk_ray_pt ray A h.out).value = VecND.angle ray.2.unitVecND (VEC_nd ray.source A) := angle_value_eq_angle A ray have h2 : (VEC_nd ray.source A).1 = VEC ray.source A := rfl - have h3 : ‖ray.toDir.unitVecND‖ = 1 := by simp + have h3 : ‖ray.toDir.unitVecND‖ = 1 := by rw [Dir.norm_unitVecND] have h4 : (SEG ray.source A).length = ‖VEC_nd ray.source A‖ := Seg.length_eq_norm_toVec - rw [← h2, ← VecND.norm_mul_sin ray.2.unitVecND (VEC_nd ray.source A),h3,h4,← h0] - ring_nf + rw [← h2, ← VecND.norm_mul_sin ray.2.unitVecND (VEC_nd ray.source A), h3, h4, one_mul] + simp only [mk_ray_pt_dir₂, mk_ray_pt_dir₁, mul_eq_mul_left_iff, VecND.norm_ne_zero, or_false] + congr + nth_rw 2 [← Dir.unitVecND_toDir ray.toDir] rfl theorem wedge_eq_length_mul_odist' (A B C : P) [bnea : PtNe B A] : (wedge A B C) = (SEG A B).length * odist' C (RAY A B) := by diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean index dc7a8799..5c7209cf 100644 --- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean +++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean @@ -418,9 +418,9 @@ theorem angle₁_neg_iff_not_cclock : ¬ tr_nd.is_cclock ↔ tr_nd.angle₁.valu simp only [negcc, not_not] have negval : tr_nd.angle₁.value = -tr_nd.flip_vertices.angle₁.value := by calc - tr_nd.angle₁.value = ∠ tr_nd.point₂ tr_nd.point₁ tr_nd.point₃ := by rfl - _= -∠ tr_nd.point₃ tr_nd.point₁ tr_nd.point₂ := by exact neg_value_of_rev_ang - _= -tr_nd.flip_vertices.angle₁.value := by rfl + tr_nd.angle₁.value = ∠ tr_nd.point₂ tr_nd.point₁ tr_nd.point₃ := rfl + _ = -∠ tr_nd.point₃ tr_nd.point₁ tr_nd.point₂ := Angle.neg_value_of_rev_ang + _ = -tr_nd.flip_vertices.angle₁.value := rfl have h : tr_nd.angle₁.value.IsNeg = tr_nd.flip_vertices.angle₁.value.IsPos := by simp only [negval, neg_isNeg_iff_isPos] simp only [h] diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean index 5687ee4f..b7140af6 100644 --- a/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean +++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean @@ -526,13 +526,12 @@ theorem IsACongr.not_nd_of_not_nd (h : tr₁.IsACongr tr₂) (nnd : ¬ tr₁.IsN fun nd ↦ nnd (h.symm.nd_of_nd nd) theorem not_nd_of_acongr_self (h : tr.IsACongr tr) : ¬ tr.IsND := by - by_contra nd + intro nd let tr_nd : TriangleND P := ⟨tr, nd⟩ - have temp := ((dite_prop_iff_and _).mp h.4).1 ⟨nd,nd⟩ - have eq : Angle.value tr_nd.angle₁ = 0 ∨ Angle.value tr_nd.angle₁ = π := AngValue.eq_neg_self_iff.mp temp - cases eq with - | inl eq => exact nd (colinear_of_angle_eq_zero eq) - | inr eq => exact nd (colinear_of_angle_eq_pi eq) + haveI : PtNe tr.point₂ tr.point₁ := tr_nd.nontriv₃ + haveI : PtNe tr.point₃ tr.point₁ := tr_nd.nontriv₂.symm + exact nd <| colinear_iff_not_isND.mpr <| + eq_neg_self_iff_not_isND.mp (((dite_prop_iff_and _).mp h.4).1 ⟨nd, nd⟩) theorem acongr_self_of_not_nd (nnd : ¬ tr.IsND) : tr.IsACongr tr where edge₁ := rfl @@ -872,11 +871,8 @@ theorem congr_of_HL (h₁ : tr_nd₁.angle₁.value = ↑(π / 2)) (h₂ : tr_nd have : Seg.length (edge₃ tr_nd₁) * Seg.length (edge₃ tr_nd₁) = Seg.length (edge₃ tr_nd₂) * Seg.length (edge₃ tr_nd₂) := by rw [<-sq ,<-sq] exact pyth₂.symm - have pos : 0 ≤ Seg.length (edge₃ tr_nd₁) := length_nonneg - have pos' : 0 ≤ Seg.length (edge₃ tr_nd₂) := length_nonneg - have : Seg.length (edge₃ tr_nd₁) = Seg.length (edge₃ tr_nd₂) := (mul_self_inj pos pos').mp this rw [<-h₂] at h₁ - exact congr_of_SAS e₂ h₁ this + exact congr_of_SAS e₂ h₁ ((mul_self_inj (edge₃ tr_nd₁).length_nonneg (edge₃ tr_nd₂).length_nonneg).mp this) theorem acongr_of_HL (h₁ : tr_nd₁.angle₁.value = ↑(π / 2)) (h₂ : tr_nd₂.angle₁.value = ↑ (- π / 2)) (e₁ : tr_nd₁.edge₁.length = tr_nd₂.edge₁.length) (e₂ : tr_nd₁.edge₂.length = tr_nd₂.edge₂.length) : tr_nd₁ ≅ₐ tr_nd₂ := by have pyth := Pythagoras_of_tr_nd tr_nd₁ (Or.inl h₁) @@ -885,10 +881,8 @@ theorem acongr_of_HL (h₁ : tr_nd₁.angle₁.value = ↑(π / 2)) (h₂ : tr_n have : Seg.length (edge₃ tr_nd₁) * Seg.length (edge₃ tr_nd₁) = Seg.length (edge₃ tr_nd₂) * Seg.length (edge₃ tr_nd₂) := by rw [<-sq ,<-sq] exact pyth₂.symm - have pos : 0 ≤ Seg.length (edge₃ tr_nd₁) := length_nonneg - have pos' : 0 ≤ Seg.length (edge₃ tr_nd₂) := length_nonneg have : Seg.length (edge₃ tr_nd₁) = Seg.length (edge₃ tr_nd₂) := by - exact (mul_self_inj pos pos').mp this + exact (mul_self_inj (edge₃ tr_nd₁).length_nonneg (edge₃ tr_nd₂).length_nonneg).mp this have eq_neg : tr_nd₁.angle₁.value = - tr_nd₂.angle₁.value := by simp only [h₁, h₂] norm_cast diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Similarity.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Similarity.lean index 0bb10a53..3eac3dbc 100644 --- a/EuclideanGeometry/Foundation/Axiom/Triangle/Similarity.lean +++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Similarity.lean @@ -383,7 +383,7 @@ theorem sim_of_SAS (tr₁ tr₂ : TriangleND P) (e : tr₁.edge₂.length / tr abel rw [<-two_smul ℕ (Angle.value tr₂.angle₁),<-two_smul ℕ _] at this rw [two_nsmul_coe_pi] at this - have nd := not_isND_iff_two_nsmul_eq_zero.mpr this + have nd := two_nsmul_eq_zero_iff_not_isND.mp this rw [cclock_of_eq_angle tr₁ tr₂ a] at cc exfalso apply nd @@ -402,7 +402,7 @@ theorem sim_of_SAS (tr₁ tr₂ : TriangleND P) (e : tr₁.edge₂.length / tr abel rw [<-two_smul ℕ (Angle.value tr₂.angle₁),<-two_smul ℕ _] at this rw [neg_coe_pi,two_nsmul_coe_pi] at this - have nd := not_isND_iff_two_nsmul_eq_zero.mpr this + have nd := two_nsmul_eq_zero_iff_not_isND.mp this rw [cclock_of_eq_angle tr₁ tr₂ a] at cc exfalso apply nd @@ -473,7 +473,7 @@ theorem asim_of_SAS (tr₁ tr₂ : TriangleND P) (e : tr₁.edge₂.length / tr simp only [comm,sub_self, zero_sub] at eq_zero rw [sub_eq_add_neg,<-neg_add] at eq_zero rw [<-two_smul ℕ (Angle.value tr₂.angle₁),neg_eq_zero] at eq_zero - have nd := not_isND_iff_two_nsmul_eq_zero.mpr eq_zero + have nd := two_nsmul_eq_zero_iff_not_isND.mp eq_zero rw [clock_of_eq_neg_angle tr₁ tr₂ a] at cc exfalso apply nd @@ -496,7 +496,7 @@ theorem asim_of_SAS (tr₁ tr₂ : TriangleND P) (e : tr₁.edge₂.length / tr simp only [comm,sub_self, zero_sub] at eq_zero rw [sub_eq_add_neg,<-neg_add] at eq_zero rw [<-two_smul ℕ (Angle.value tr₂.angle₁),neg_eq_zero] at eq_zero - have nd := not_isND_iff_two_nsmul_eq_zero.mpr eq_zero + have nd := two_nsmul_eq_zero_iff_not_isND.mp eq_zero rw [clock_of_eq_neg_angle tr₁ tr₂ a] at cc push_neg at cc exfalso diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram.lean b/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram.lean index 72ab5055..7bf36203 100644 --- a/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram.lean +++ b/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram.lean @@ -1130,8 +1130,8 @@ theorem qdr_cvx_is_prg_nd_of_diag_inx_eq_mid_eq_mid (h' : qdr_cvx.diag_nd₁₃. have h: qdr_cvx.diag_nd₂₄.1.midpoint ≠ qdr_cvx.point₄ := by apply SegND.midpt_ne_target rw [qdr_cvx_eq_midpoint_of_diag₂₄] at h exact h - have prep₁_pre: (SEG_nd qdr_cvx.point₁ midpoint nd₁₅).length = (SEG_nd midpoint qdr_cvx.point₃ nd₃₅.symm).length := dist_target_eq_dist_source_of_midpt (seg := qdr_cvx.diag₁₃) - have prep₁_pre': (SEG_nd qdr_cvx.point₁ midpoint nd₁₅).length = (SEG_nd midpoint qdr_cvx.point₁ nd₁₅.symm).length := by apply length_of_rev_eq_length' + have prep₁_pre: (SEG_nd qdr_cvx.point₁ midpoint nd₁₅).length = (SEG_nd midpoint qdr_cvx.point₃ nd₃₅.symm).length := (qdr_cvx.diag₁₃).dist_target_eq_dist_source_of_midpt + have prep₁_pre': (SEG_nd qdr_cvx.point₁ midpoint nd₁₅).length = (SEG_nd midpoint qdr_cvx.point₁ nd₁₅.symm).length := length_of_rev_eq_length' sorry constructor exact qdr_cvx.not_colinear₁₂₃ diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/Quadrilateral.lean b/EuclideanGeometry/Foundation/Construction/Polygon/Quadrilateral.lean index db584e6c..36ca429f 100644 --- a/EuclideanGeometry/Foundation/Construction/Polygon/Quadrilateral.lean +++ b/EuclideanGeometry/Foundation/Construction/Polygon/Quadrilateral.lean @@ -28,6 +28,8 @@ Of course many definitions work on these classes already, but without necessarit noncomputable section namespace EuclidGeom +open Angle + /-- Class of Quadrilateral: A quadrilateral consists of four points; it is the generalized quadrilateral formed by these four points -/ @[ext] structure Quadrilateral (P : Type _) [EuclideanPlane P] where @@ -391,8 +393,7 @@ instance nd₁₃ : PtNe qdr_cvx.point₃ qdr_cvx.point₁ := Fact.mk <| by by_contra h have g : qdr_cvx.angle₂.value = 0 := by unfold Quadrilateral_nd.angle₂ - simp only [h] - exact angle_eq_zero_of_same_dir + simp only [h, pt_pt_pt_value_eq_zero_of_same_pt] have k₁ : ¬ qdr_cvx.angle₂.value.IsPos := by rw [g] exact AngValue.not_zero_isPos diff --git a/EuclideanGeometry/Foundation/Construction/Triangle/AngleBisector.lean b/EuclideanGeometry/Foundation/Construction/Triangle/AngleBisector.lean index 36ab158f..4e0ea66f 100644 --- a/EuclideanGeometry/Foundation/Construction/Triangle/AngleBisector.lean +++ b/EuclideanGeometry/Foundation/Construction/Triangle/AngleBisector.lean @@ -28,8 +28,8 @@ structure IsAngBis (ang : Angle P) (ray : Ray P) : Prop where eq_source : ang.source = ray.source eq_value : (mk_dir₁ ang ray.toDir).value = (mk_dir₂ ang ray.toDir).value -- `the definition of same_sgn should be rewrite, using btw`. - -- For example, change it to `sbtw ang.dir₁ ray.toDir ang.dir₂ ∨ (ray.toDir =ang.dir₁ ∧ ray.toDir = ang.dir₂)`. - same_sgn : ((Angle.mk_start_ray ang ray eq_source).value.IsPos ∧ ang.value.IsPos) ∨ ((Angle.mk_start_ray ang ray eq_source).value.IsNeg ∧ ang.value.IsNeg) ∨ ((Angle.mk_start_ray ang ray eq_source).value = ↑(π/2) ∧ ang.value = π ) ∨ ((Angle.mk_start_ray ang ray eq_source).value = 0 ∧ ang.value = 0) + -- May change it to `- π / 2 < (mk_dir₁ ang ray.toDir).value ≤ π / 2`. + same_sgn : ((mk_dir₁ ang ray.toDir).value.IsPos ∧ ang.value.IsPos) ∨ ((mk_dir₁ ang ray.toDir).value.IsNeg ∧ ang.value.IsNeg) ∨ ((mk_dir₁ ang ray.toDir).value = ↑(π/2) ∧ ang.value = π ) ∨ ((mk_dir₁ ang ray.toDir).value = 0 ∧ ang.value = 0) structure IsAngBisLine (ang : Angle P) (l : Line P) : Prop where @@ -61,16 +61,16 @@ namespace Angle theorem eq_source {ang : Angle P} : ang.source = ang.AngBis.source := rfl -theorem value_angBis_eq_half_value {ang : Angle P} : (Angle.mk_start_ray ang ang.AngBis rfl).value = ang.value.half := by - simp only [mk_strat_ray_value_eq_vsub, AngBis, vadd_vsub] +theorem value_angBis_eq_half_value {ang : Angle P} : (mk_dir₁ ang ang.AngBis.toDir).value = ang.value.half := by + simp only [mk_dir₁_value, AngBis, vadd_vsub] -theorem mk_start_ray_value_eq_half_angvalue {ang : Angle P} : (Angle.mk_start_ray ang ang.AngBis rfl).value.toReal = ang.value.toReal / 2 := +theorem mk_start_ray_value_eq_half_angvalue {ang : Angle P} : (mk_dir₁ ang ang.AngBis.toDir).value.toReal = ang.value.toReal / 2 := (Eq.congr_right (ang.value.half_toReal).symm).mpr (congrArg toReal ang.value_angBis_eq_half_value) theorem angbis_is_angbis {ang : Angle P} : IsAngBis ang ang.AngBis where eq_source := rfl eq_value := by - simp only [value_mk_dir₁, value_mk_dir₂, AngBis, vadd_vsub, vsub_vadd_eq_vsub_sub] + simp only [mk_dir₁_value, mk_dir₂_value, AngBis, vadd_vsub, vsub_vadd_eq_vsub_sub] exact sub_half_eq_half.symm same_sgn := by have g : (ang.value.IsPos) ∨ (ang.value.IsNeg) ∨ (ang.value = π) ∨ (ang.value = 0) := by @@ -110,7 +110,7 @@ theorem ang_source_rev_eq_source_bis {ang : Angle P} {r : Ray P} (h : IsAngBis a theorem nonpi_bisector_eq_bisector_of_rev {ang : Angle P} {r : Ray P} (h : IsAngBis ang r) (nonpi : ang.value ≠ π ): IsAngBis ang.reverse r where eq_source := h.eq_source eq_value := by - simp only [value_mk_dir₁, value_mk_dir₂, reverse] + simp only [mk_dir₁_value, mk_dir₂_value, reverse] rw [← neg_vsub_eq_vsub_rev ang.dir₂ r.toDir, ← neg_vsub_eq_vsub_rev r.toDir ang.dir₁] exact neg_inj.mpr h.eq_value.symm same_sgn := sorry /- by @@ -167,8 +167,8 @@ namespace TriangleND theorem angbisline_of_angle₁_angle₂_not_parallel {tri_nd : TriangleND P} : ¬ tri_nd.angle₁.AngBis.toLine ∥ tri_nd.angle₂.AngBis.toLine := by by_contra g - let A₁ := (Angle.mk_start_ray tri_nd.angle₁ tri_nd.angle₁.AngBis tri_nd.angle₁.eq_source).reverse - let A₂ := Angle.mk_end_ray tri_nd.angle₂ tri_nd.angle₂.AngBis tri_nd.angle₂.eq_source + let A₁ := (mk_dir₁ tri_nd.angle₁ tri_nd.angle₁.AngBis.toDir).reverse + let A₂ := mk_dir₂ tri_nd.angle₂ tri_nd.angle₂.AngBis.toDir have sr : A₁.start_ray.toDir = A₂.start_ray.toDir := by have h₁ : A₁.start_ray = tri_nd.angle₁.AngBis := rfl have h₂ : A₂.start_ray = tri_nd.angle₂.AngBis := rfl @@ -184,11 +184,8 @@ theorem angbisline_of_angle₁_angle₂_not_parallel {tri_nd : TriangleND P} : have h₅ : tri_nd.edge_nd₃.reverse.toDirLine.reverse = tri_nd.edge_nd₃.reverse.reverse.toDirLine := by rw [SegND.toDirLine_rev_eq_rev_toDirLine] have h₆ : tri_nd.edge_nd₃.reverse.reverse.toDirLine = tri_nd.edge_nd₃.toDirLine := rfl rw [h₆] at h₅ - exact id h₅.symm - have g₁ : IsConsecutiveIntAng A₁ A₂ := by - constructor - · rw [sr] - · rw [er] + exact h₅.symm + have g₁ : IsConsecutiveIntAng A₁ A₂ := ⟨sr, er⟩ have g₂ : A₁.value - A₂.value = π := by rw [value_sub_eq_pi_of_isconsecutiveintang g₁] sorry