diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.1.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.1.lean index 73cd4beb..84b048b6 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.1.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.1.lean @@ -133,7 +133,7 @@ theorem Result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (SE have h₅₁ : -∠ e.E e.C e.M = -∠ e.A e.C e.B := by have inner_h₅₁ : ∠ e.E e.C e.M = ∠ e.A e.C e.B := by symm - apply eq_ang_val_of_lieson_lieson + apply Angle.value_eq_of_lies_on_ray_pt_pt · exact E_int_ray_CA · exact M_int_ray_CB simp only [inner_h₅₁] @@ -141,7 +141,7 @@ theorem Result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (SE rw [← neg_value_of_rev_ang] have inner_h₅₂ : ∠ e.D e.B e.M = ∠ e.A e.B e.C := by symm - apply eq_ang_val_of_lieson_lieson + apply Angle.value_eq_of_lies_on_ray_pt_pt · exact D_int_ray_BA · exact M_int_ray_BC simp only [inner_h₅₂] diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.3.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.3.lean index ed238003..9eb08993 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.3.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.3.lean @@ -110,14 +110,14 @@ theorem Result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : ∠ rw [← neg_value_of_rev_ang (e.A_ne_B) (e.C_ne_B)] have inner_h₂₁ : ∠ e.A e.B e.D (e.A_ne_B) (e.D_ne_B) = ∠ e.A e.B e.C (e.A_ne_B) (e.C_ne_B) := by symm - apply eq_ang_val_of_lieson_lieson + apply Angle.value_eq_of_lies_on_ray_pt_pt ·exact A_int_ray_BA .exact D_int_ray_BC simp only [inner_h₂₁] have h₂₂ : ∠ e.A e.C e.E (e.A_ne_C) (e.E_ne_C) = ∠ e.A e.C e.B (e.A_ne_C) (e.B_ne_C) := by have inner_h₂₂ : ∠ e.A e.C e.E (e.A_ne_C) (e.E_ne_C) = ∠ e.A e.C e.B (e.A_ne_C) (e.B_ne_C) := by symm - apply eq_ang_val_of_lieson_lieson + apply Angle.value_eq_of_lies_on_ray_pt_pt ·exact A_int_ray_CA ·exact E_int_ray_CB simp only [inner_h₂₂] diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.7.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.7.lean index 012cc104..a0245cec 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.7.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.7.lean @@ -182,12 +182,12 @@ Therefore, $DX = EY$. ∠ e.D e.B e.X D_ne_B X_ne_B -- $\angle DBX = \angle CBA$ because $D$ lies on ray $BC$ and $X$ lies on ray $BA$, _= ∠ e.C e.B e.A C_ne_B A_ne_B := by - symm; exact eq_ang_val_of_lieson_lieson C_ne_B A_ne_B D_ne_B X_ne_B D_int_ray_BC X_int_ray_BA + symm; exact Angle.value_eq_of_lies_on_ray_pt_pt C_ne_B A_ne_B D_ne_B X_ne_B D_int_ray_BC X_int_ray_BA -- $\angle CBA = - \angle BCA$, _= - ∠ e.B e.C e.A C_ne_B.symm A_ne_C := angle_CBA_eq_neg_angle_BCA -- $\angle BCA = - \angle ECY$ because $e$ lies on ray $CB$ and $Y$ lies on ray $CA$. _= - ∠ e.E e.C e.Y E_ne_C Y_ne_C := by - simp only [eq_ang_val_of_lieson_lieson C_ne_B.symm A_ne_C E_ne_C Y_ne_C E_int_ray_CB Y_int_ray_CA] + simp only [Angle.value_eq_of_lies_on_ray_pt_pt C_ne_B.symm A_ne_C E_ne_C Y_ne_C E_int_ray_CB Y_int_ray_CA] -- $\triangle XBD \cong_a \triangle YEC$ (by AAS) have triangle_XBD_acongr_triangle_YCE : (TRI_nd e.X e.B e.D not_colinear_XBD) ≅ₐ (TRI_nd e.Y e.C e.E not_colinear_YCE) := by apply acongr_of_AAS_variant diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.8.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.8.lean index dd98e1e7..c0141835 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.8.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.8.lean @@ -89,7 +89,7 @@ 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 eq_ang_val_of_lieson_lieson (e.B_ne_C.symm) e.A_ne_B D_ne_B e.A_ne_B + 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 · 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$. @@ -98,7 +98,7 @@ Therefore, $BD = CE$. exact Triangle.isoceles_of_regular (▵ e.A e.B e.C) e.regular_ABC -- 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 eq_ang_val_of_lieson_lieson A_ne_C e.B_ne_C E_ne_C e.B_ne_C + 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 Ray.snd_pt_lies_int_mk_pt_pt e.C e.B e.B_ne_C -- We have $BD = CE$. diff --git a/EuclideanGeometry/Example/ShanZun/Ex1f.lean b/EuclideanGeometry/Example/ShanZun/Ex1f.lean index 1a5d1571..90508f94 100644 --- a/EuclideanGeometry/Example/ShanZun/Ex1f.lean +++ b/EuclideanGeometry/Example/ShanZun/Ex1f.lean @@ -88,7 +88,7 @@ theorem Shan_Problem_2_11 : (SEG C E).length = (SEG D E).length := by exact (length_eq_length_add_length a_lies_on_be).symm -- $\angle EBF = \angle ABC$ have ang₁ : ∠ F B E f_ne_b e_ne_b = ∠ C B A c_ne_a a_ne_b := by - apply eq_ang_value_of_lies_int_lies_int + apply value_eq_of_lies_on_ray_pt_pt constructor exact SegND.lies_on_toRay_of_lies_on c_lies_on_bf exact b_ne_c.symm diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Angle/FromMathlib.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Angle/FromMathlib.lean index 3d554a95..f26c6fdd 100644 --- a/EuclideanGeometry/Foundation/Axiom/Basic/Angle/FromMathlib.lean +++ b/EuclideanGeometry/Foundation/Axiom/Basic/Angle/FromMathlib.lean @@ -1,4 +1,5 @@ import Mathlib.Analysis.SpecialFunctions.Complex.Circle +import Mathlib.Data.Int.Parity /-! # APIs about Angle from Mathlib @@ -8,6 +9,8 @@ We use `AngValue` as an alias of `Real.Angle`. noncomputable section +attribute [ext] Complex.ext + open Real section Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean index 98d5e2d0..9fe88065 100644 --- a/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean +++ b/EuclideanGeometry/Foundation/Axiom/Basic/Vector.lean @@ -400,7 +400,10 @@ instance innerProductSpace' : InnerProductSpace ℝ Vec where norm_sq_eq_inner v := by simp [norm_sq] conj_symm v₁ v₂ := by simp [Complex.conj_ofReal, mul_comm] add_left v₁ v₂ v₃ := by dsimp; ring - smul_left v₁ v₂ z := by dsimp; simp; ring + smul_left v₁ v₂ z := by + dsimp + simp only [zero_mul, sub_zero, add_zero, conj_trivial] + ring lemma real_inner_apply (v₁ v₂ : Vec) : ⟪v₁, v₂⟫_ℝ = v₁.fst * v₂.fst + v₁.snd * v₂.snd := @@ -1256,6 +1259,9 @@ lemma neg_vsub_left (d₁ d₂ : Dir) : -d₁ -ᵥ d₂ = d₁ -ᵥ d₂ + ∠[ lemma neg_vsub_right (d₁ d₂ : Dir) : d₁ -ᵥ -d₂ = d₁ -ᵥ d₂ + ∠[π] := by rw [← pi_vadd, vsub_vadd_eq_vsub_sub, sub_eq_add_neg, AngValue.neg_coe_pi] +lemma eq_neg_of_vsub_eq_pi (d₁ d₂ : Dir) : d₁ = - d₂ ↔ d₁ -ᵥ d₂ = ∠[π] := + ((pi_vadd d₂).symm.congr_right).trans (eq_vadd_iff_vsub_eq d₁ ∠[π] d₂) + protected abbrev normalize {M : Type*} [AddCommGroup M] [Module ℝ M] {F : Type*} [LinearMapClass F ℝ Vec M] (f : F) : @@ -1464,6 +1470,20 @@ theorem Dir.toProj_eq_toProj_iff_unitVecND {d₁ d₂ : Dir} : conv_lhs => rw [← d₁.unitVecND_toDir, ← d₂.unitVecND_toDir] rw [VecND.toProj_eq_toProj_iff'] +theorem Dir.toProj_eq_toProj_iff_vsub_not_isND {d₁ d₂ : Dir} : d₁.toProj = d₂.toProj ↔ ¬ (d₁ -ᵥ d₂).IsND := + toProj_eq_toProj_iff.trans <| + (or_congr vsub_eq_zero_iff_eq.symm (eq_neg_of_vsub_eq_pi d₁ d₂)).trans AngValue.not_isND_iff.symm + +theorem Dir.toProj_ne_toProj_iff_vsub_isND {d₁ d₂ : Dir} : d₁.toProj ≠ d₂.toProj ↔ (d₁ -ᵥ d₂).IsND := + toProj_eq_toProj_iff_vsub_not_isND.not_left + +theorem Dir.toProj_ne_toProj_iff_neg_vsub_isND {d₁ d₂ : Dir} : d₁.toProj ≠ d₂.toProj ↔ (d₂ -ᵥ d₁).IsND := by + apply toProj_ne_toProj_iff_vsub_isND.trans + rw [← neg_vsub_eq_vsub_rev d₂ d₁, AngValue.neg_isND_iff_isND] + +theorem Dir.toProj_eq_toProj_iff_neg_vsub_not_isND {d₁ d₂ : Dir} : d₁.toProj = d₂.toProj ↔ ¬ (d₂ -ᵥ d₁).IsND := + toProj_ne_toProj_iff_neg_vsub_isND.not_right + @[simp] lemma VecND.neg_toProj (v : VecND) : (-v).toProj = v.toProj := by rw [toProj_eq_toProj_iff'] diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean index f2831ebf..b984b8b7 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean @@ -249,9 +249,9 @@ def CC_Intersected_pts {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Intersec theorem CC_inx_pts_distinct {ω₁ : Circle P} {ω₂ : Circle P} (h : ω₁ Intersect ω₂) : (CC_Intersected_pts h).left ≠ (CC_Intersected_pts h).right := by apply (ne_iff_vec_ne_zero _ _).mpr unfold Vec.mkPtPt CC_Intersected_pts - simp - rw [← sub_smul] - simp + simp only [neg_mul, vadd_vsub_vadd_cancel_right, ne_eq, ← sub_smul] + simp only [add_sub_add_right_eq_sub, sub_neg_eq_add, smul_eq_zero, add_self_eq_zero, mul_eq_zero, + Complex.ofReal_eq_zero, Complex.I_ne_zero, or_false, VecND.ne_zero] push_neg apply Real.sqrt_ne_zero'.mpr have hlt : (radical_axis_dist_to_the_first ω₁ ω₂) ^ 2 < ω₁.radius ^ 2 := by diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean b/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean index 62bb9795..99d5f656 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/IncribedAngle.lean @@ -202,12 +202,10 @@ theorem cangle_eq_two_times_inscribed_angle {p : P} {β : Arc P} (h₁ : p LiesO have : (ANG β.target β.circle.center p).end_ray = (ANG p β.circle.center β.source).start_ray := rfl have hhs : (Angle.sum_adj this).value = ∠ β.target β.circle.center β.source := rfl rw [← hhs, Angle.ang_eq_ang_add_ang_mod_pi_of_adj_ang] - rfl have hsum₂ : ∠ β.source p β.circle.center + ∠ β.circle.center p β.target = ∠ β.source p β.target := by have : (ANG β.source p β.circle.center).end_ray = (ANG β.circle.center p β.target).start_ray := rfl have hhs : (Angle.sum_adj this).value = ∠ β.source p β.target := rfl rw [← hhs, Angle.ang_eq_ang_add_ang_mod_pi_of_adj_ang] - rfl have eq₃ : ∠ β.target β.circle.center β.source + 2 • (∠ β.source p β.target) = 0 := by calc _ = ∠ β.target β.circle.center p + ∠ p β.circle.center β.source + 2 • (∠ β.source p β.circle.center + ∠ β.circle.center p β.target) := by rw [hsum₁, hsum₂] diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean index ed78ca30..903275a1 100644 --- a/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean +++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean @@ -44,7 +44,7 @@ def mk_two_ray_of_eq_source (r : Ray P) (r' : Ray P) (_h : r.source = r'.source) /-- Given vertex $O$ and two distinct points $A$ and $B$, this function returns the angle 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 +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 @@ -90,19 +90,8 @@ abbrev IsObt : Prop := ang.value.IsObt @[pp_dot] abbrev IsRight : Prop := ang.value.IsRight -@[pp_dot] -def start_ray : Ray P := ⟨ang.source, ang.dir₁⟩ - -@[pp_dot] -def end_ray : Ray P := ⟨ang.source, ang.dir₂⟩ - -@[pp_dot] -theorem start_ray_source_eq_end_ray_source : ang.start_ray.source = ang.end_ray.source := rfl - end Angle -theorem angle_value_eq_dir_angle (r r' : Ray P) (h : r.source = r'.source) : (Angle.mk_two_ray_of_eq_source r r' h).value = r'.toDir -ᵥ r.toDir := rfl - /-- 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|$.-/ abbrev value_of_angle_of_three_point_nd (A O B : P) (h₁ : A ≠ O) (h₂ : B ≠ O) : AngValue := @@ -168,22 +157,97 @@ def delabValueOfAngleOfThreePointND : Delab := do namespace Angle -section carrier +section start_end_ray + +variable {ang : Angle P} + +@[pp_dot] +def start_ray (ang : Angle P) : Ray P := ⟨ang.source, ang.dir₁⟩ + +@[pp_dot] +def end_ray (ang : Angle P) : Ray P := ⟨ang.source, ang.dir₂⟩ + +@[pp_dot] +theorem start_ray_source_eq_end_ray_source : ang.start_ray.source = ang.end_ray.source := rfl + +@[simp] +theorem start_ray_toDir : ang.start_ray.toDir = ang.dir₁ := rfl + +@[simp] +theorem end_ray_toDir : ang.end_ray.toDir = ang.dir₂ := rfl + +@[simp] +theorem source_eq_start_ray_source : ang.start_ray.source = ang.source := rfl + +@[simp] +theorem source_eq_end_ray_source : ang.end_ray.source = ang.source := rfl + +theorem source_lies_on_start_ray : ang.source LiesOn ang.start_ray := + ang.start_ray.source_lies_on + +theorem source_lies_on_end_ray : ang.source LiesOn ang.end_ray := + ang.end_ray.source_lies_on +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_reverse_of_value_eq_pi (h : ang.value = π) : ang.start_ray = ang.end_ray.reverse := sorry + +@[pp_dot] +def start_dirLine (ang : Angle P) : DirLine P := DirLine.mk_pt_dir ang.source ang.dir₁ + +@[pp_dot] +def end_dirLine (ang : Angle P) : DirLine P := DirLine.mk_pt_dir ang.source ang.dir₂ + +@[simp] +theorem start_dirLine_toDir : ang.start_dirLine.toDir = ang.dir₁ := rfl + +@[simp] +theorem end_dirLine_toDir : ang.end_dirLine.toDir = ang.dir₂ := rfl + +@[simp] +theorem start_ray_toDirLine_eq_start_dirLine : ang.start_ray.toDirLine = ang.start_dirLine := rfl + +@[simp] +theorem end_ray_toDirLine_eq_end_dirLine : ang.end_ray.toDirLine = ang.end_dirLine := rfl + +theorem source_lies_on_start_dirLine: ang.source LiesOn ang.start_dirLine := + DirLine.pt_lies_on_of_mk_pt_dir ang.source ang.dir₁ + +theorem source_lies_on_end_dirLine : ang.source LiesOn ang.end_dirLine := + DirLine.pt_lies_on_of_mk_pt_dir ang.source ang.dir₂ + +theorem start_dirLine_not_para_end_dirLine_of_value_ne_zero (h : ang.value.IsND) : ¬ ang.start_dirLine ∥ ang.end_dirLine := + start_ray_not_para_end_ray_of_isND h + +theorem start_dirLine_eq_end_dirLine_of_value_eq_zero (h : ang.value = 0) : ang.start_dirLine = ang.end_dirLine := + congrArg Ray.toDirLine (start_ray_eq_end_ray_of_value_eq_zero h) + +theorem start_dirLine_eq_end_dirLine_reverse_of_value_eq_pi (h : ang.value = π) : ang.start_dirLine = ang.end_dirLine.reverse := + congrArg Ray.toDirLine (start_ray_eq_end_ray_reverse_of_value_eq_pi h) + +end start_end_ray + +section carrier +/- -- `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 -/ --- Do we need an abbreviation for `btw ang.dir₁ dir ang.dir₂`? +-- Do we need an abbreviation for `sbtw ang.dir₁ dir ang.dir₂`? 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₂ + /- 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₂ -variable {p : P} {ang : Angle P} +variable {p : P} {ang : Angle P} {d : Dir} {r : Ray P} protected theorem ison_of_isint (h : ang.IsInt p) : ang.IsOn p := by simp only [Angle.IsOn, h.1, dite_false] @@ -213,64 +277,179 @@ theorem lies_on_of_eq (h : p = ang.source) : p LiesOn ang := by 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₂ := (dite_prop_iff_and _).trans ((and_iff_right (fun _ ↦ trivial)).trans (forall_prop_of_true _h.1)) -theorem lies_on_of_lies_on_ray_mk {d : Dir} (hd : btw ang.dir₁ d ang.dir₂) (h : p LiesOn Ray.mk ang.source d) : p LiesOn ang := sorry +example (p : P) {ang : Angle P} [PtNe p ang.source] (h : ang.dir₁ = ang.dir₂) : p LiesOn ang := by + apply lies_on_iff_btw_of_ptNe.mpr + rw [h] + exact btw_rfl_left_right -theorem lies_on_of_lies_on_ray {r : Ray P} (hs : ang.source = r.source) (hd : btw ang.dir₁ r.toDir ang.dir₂) (h : p LiesOn r) : p LiesOn ang := +theorem lies_on_of_lies_on_ray_mk (hd : btw ang.dir₁ d ang.dir₂) (h : p LiesOn Ray.mk ang.source d) : p LiesOn ang := sorry + +theorem lies_on_of_lies_on_ray (hs : ang.source = r.source) (hd : btw ang.dir₁ r.toDir ang.dir₂) (h : p LiesOn r) : p LiesOn ang := lies_on_of_lies_on_ray_mk hd ((congrArg (lies_on p) (congrFun (congrArg Ray.mk hs) r.toDir)).mpr h) theorem lies_on_iff_lies_on_ray : p LiesOn ang ↔ ∃ r : Ray P, (ang.source = r.source ∧ btw ang.dir₁ r.toDir ang.dir₂) ∧ p LiesOn r := sorry -theorem lies_int_of_lies_int_ray_mk {d : Dir} (hd : btw ang.dir₁ d ang.dir₂) (h : p LiesInt Ray.mk ang.source d) : p LiesInt ang := sorry +theorem lies_int_of_lies_int_ray_mk (hd : btw ang.dir₁ d ang.dir₂) (h : p LiesInt Ray.mk ang.source d) : p LiesInt ang := sorry -theorem lies_int_of_lies_int_ray {r : Ray P} (hs : ang.source = r.source) (hd : btw ang.dir₁ r.toDir ang.dir₂) (h : p LiesInt r) : p LiesInt ang := +theorem lies_int_of_lies_int_ray (hs : ang.source = r.source) (hd : btw ang.dir₁ r.toDir ang.dir₂) (h : p LiesInt r) : p LiesInt ang := lies_int_of_lies_int_ray_mk hd ((congrArg (lies_int p) (congrFun (congrArg Ray.mk hs) r.toDir)).mpr h) theorem lies_int_iff_lies_int_ray : p LiesInt ang ↔ ∃ r : Ray P, (ang.source = r.source ∧ btw ang.dir₁ r.toDir ang.dir₂) ∧ p LiesInt r := sorry - + -/ end carrier -section change_dir +section mk_two_ray + +variable (r r' : Ray P) (h : r.source = r'.source) + +theorem source_eq_fst_source_of_mk_two_ray_of_eq_source: (mk_two_ray_of_eq_source r r' h).source = r.source := rfl -variable (ang : Angle P) (d : Dir) +theorem source_eq_snd_source_of_mk_two_ray_of_eq_source : (mk_two_ray_of_eq_source r r' h).source = r'.source := h -def mk_dir₁: Angle P where +@[simp] +theorem mk_two_ray_of_eq_source_dir₁ : (mk_two_ray_of_eq_source r r' h).dir₁ = r.toDir := rfl + +@[simp] +theorem mk_two_ray_of_eq_source_dir₂ : (mk_two_ray_of_eq_source r r' h).dir₂ = r'.toDir := rfl + +@[simp] +theorem mk_two_ray_of_eq_source_start_ray : (mk_two_ray_of_eq_source r r' h).start_ray = r := rfl + +@[simp] +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 + +end mk_two_ray + +section pt_pt_pt + +variable {A O B : P} (ha : A ≠ O) (hb : B ≠ O) + +@[simp] +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 + +@[simp] +theorem mk_pt_pt_pt_dir₂ : (ANG A O B ha hb).dir₂ = (RAY 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 + +@[simp] +theorem mk_pt_pt_pt_end_ray : (ANG A O B ha hb).end_ray = RAY O B hb := rfl + +end pt_pt_pt + +section change_dir + +def mk_dir₁ (ang : Angle P) (d : Dir) : Angle P where source := ang.source dir₁ := ang.dir₁ dir₂ := d -def mk_dir₂ : Angle P where +def mk_dir₂ (ang : Angle P) (d : Dir) : Angle P where source := ang.source dir₁ := d dir₂ := ang.dir₂ -theorem value_mk_dir₁ : (mk_dir₁ ang d).value = d -ᵥ ang.dir₁ := rfl +theorem value_mk_dir₁ (ang : Angle P) (d : Dir) : (mk_dir₁ ang d).value = d -ᵥ ang.dir₁ := rfl -theorem value_mk_dir₂ : (mk_dir₂ ang d).value = ang.dir₂ -ᵥ d := 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} -end change_dir +theorem lies_on_of_lies_on_mk_dir₁ (hd : btw ang.dir₁ d ang.dir₂) (h : p LiesOn mk_dir₁ ang d) : p LiesOn ang := sorry -end Angle +theorem lies_on_mk_dir₁_of_lies_on (hd : btw ang.dir₁ ang.dir₂ d) (h : p LiesOn ang) : p LiesOn mk_dir₁ ang d := sorry + +theorem lies_int_of_lies_int_mk_dir₁ (hd : btw ang.dir₁ d ang.dir₂) (h : p LiesInt mk_dir₁ ang d) : p LiesInt ang := sorry + +theorem lies_int_mk_dir₁_of_lies_int (hd : btw ang.dir₁ ang.dir₂ d) (h : p LiesInt ang) : p LiesInt mk_dir₁ ang d := sorry + +theorem lies_on_of_lies_on_mk_dir₂ (hd : btw ang.dir₁ d ang.dir₂) (h : p LiesOn mk_dir₂ ang d) : p LiesOn ang := sorry + +theorem lies_on_mk_dir₂_of_lies_on (hd : btw ang.dir₂ ang.dir₁ d) (h : p LiesOn ang) : p LiesOn mk_dir₁ ang d := sorry + +theorem lies_int_of_lies_int_mk_dir₂ (hd : btw ang.dir₁ d ang.dir₂) (h : p LiesInt mk_dir₂ ang d) : p LiesInt ang := sorry -theorem end_ray_eq_of_value_eq_of_start_ray_eq {ang₁ ang₂ : Angle P} (h : ang₁.start_ray = ang₂.start_ray) (v : ang₁.value = ang₂.value) : ang₁.end_ray = ang₂.end_ray := sorry /-by - ext : 1 - rw [← ang₁.source_eq_source, ← ang₂.source_eq_source, (congrArg (fun z => z.source)) h] - let g := (congrArg (fun z => AngValue.toDir z)) v - unfold Angle.value DirObj.AngDiff Dir.AngDiff at g - simp only [div_toangvalue_eq_toangvalue_sub, sub_todir_eq_todir_div, toangvalue_todir_eq_self] at g - rw [h] at g - simp only [div_left_inj] at g - exact g-/ +theorem lies_int_mk_dir₂_of_lies_int (hd : btw ang.dir₁ ang.dir₂ d) (h : p LiesInt ang) : p LiesInt mk_dir₂ ang d := sorry -theorem eq_start_ray_of_eq_value_eq_end_ray {ang₁ ang₂ : Angle P} (h : ang₁.end_ray = ang₂.end_ray) (v : ang₁.value = ang₂.value) : ang₁.start_ray = ang₂.start_ray := sorry +theorem lies_on_of_lies_on_of_btw_of_btw {ang₁ : Angle P} {ang₂ : Angle P} (h₁ : btw ang₁.dir₁ ang₂.dir₁ ang₁.dir₂) (h₂ : btw ang₁.dir₁ ang₂.dir₂ ang₁.dir₂) (h : p LiesOn ang₂) : p LiesOn ang₁ := sorry -theorem eq_of_eq_value_eq_start_ray {ang₁ ang₂ : Angle P} (h : ang₁.start_ray = ang₂.start_ray) (v : ang₁.value = ang₂.value) : ang₁ = ang₂ := sorry - --Angle.ext ang₁ ang₂ h (eq_end_ray_of_eq_value_eq_start_ray h v) +theorem lies_int_of_lies_int_of_btw_of_btw {ang₁ : Angle P} {ang₂ : Angle P} (h₁ : btw ang₁.dir₁ ang₂.dir₁ ang₁.dir₂) (h₂ : btw ang₁.dir₁ ang₂.dir₂ ang₁.dir₂) (h : p LiesInt ang₂) : p LiesInt ang₁ := sorry + -/ +end change_dir -- this section should talks about when different making methods make the same angle section mk_compatibility +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 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 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_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 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_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 + end mk_compatibility +section cancel + +variable {ang ang₁ ang₂ : Angle P} + +theorem dir₂_eq_of_value_eq_of_dir₁_eq (hr : ang₁.dir₁ = ang₂.dir₁) (hv : ang₁.value = ang₂.value) : ang₁.dir₂ = ang₂.dir₂ := by + rw [value, hr] at hv + exact vsub_left_cancel hv + +theorem eq_of_value_eq_of_dir₁_eq_of_source_eq (hs : ang₁.source = ang₂.source) (hr : ang₁.dir₁ = ang₂.dir₁) (hv : ang₁.value = ang₂.value) : ang₁ = ang₂ := + Angle.ext ang₁ ang₂ hs hr (dir₂_eq_of_value_eq_of_dir₁_eq hr hv) + +theorem eq_of_value_eq_of_start_ray_eq {ang₁ ang₂ : Angle P} (h : ang₁.start_ray = ang₂.start_ray) (hv : ang₁.value = ang₂.value) : ang₁ = ang₂ := + eq_of_value_eq_of_dir₁_eq_of_source_eq (congrArg Ray.source h) (congrArg Ray.toDir h) hv + +theorem end_ray_eq_of_value_eq_of_start_ray_eq (h : ang₁.start_ray = ang₂.start_ray) (hv : ang₁.value = ang₂.value) : ang₁.end_ray = ang₂.end_ray := + congrArg end_ray (eq_of_value_eq_of_start_ray_eq h hv) + +theorem dir₁_eq_of_value_eq_of_dir₂_eq (hr : ang₁.dir₂ = ang₂.dir₂) (hv : ang₁.value = ang₂.value) : ang₁.dir₁ = ang₂.dir₁ := by + rw [value, hr] at hv + exact vsub_right_cancel hv + +theorem eq_of_value_eq_of_dir₂_eq_of_source_eq (hs : ang₁.source = ang₂.source) (hr : ang₁.dir₂ = ang₂.dir₂) (hv : ang₁.value = ang₂.value) : ang₁ = ang₂ := + Angle.ext ang₁ ang₂ hs (dir₁_eq_of_value_eq_of_dir₂_eq hr hv) hr + +theorem eq_of_value_eq_of_end_ray_eq {ang₁ ang₂ : Angle P} (h : ang₁.end_ray = ang₂.end_ray) (hv : ang₁.value = ang₂.value) : ang₁ = ang₂ := + eq_of_value_eq_of_dir₂_eq_of_source_eq (congrArg Ray.source h) (congrArg Ray.toDir h) hv + +theorem eq_start_ray_of_eq_value_eq_end_ray (h : ang₁.end_ray = ang₂.end_ray) (hv : ang₁.value = ang₂.value) : ang₁.start_ray = ang₂.start_ray := + congrArg start_ray (eq_of_value_eq_of_end_ray_eq h hv) + +end cancel + +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 de7cdbb7..32d12f41 100644 --- a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex.lean +++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex.lean @@ -96,17 +96,17 @@ theorem IsConsecutiveIntAng.symm {ang₁ ang₂ : Angle P} : IsConsecutiveIntAng theorem IsAlternateIntAng.symm {ang₁ ang₂ : Angle P} : IsAlternateIntAng ang₁ ang₂ → IsAlternateIntAng ang₂ ang₁ := sorry -theorem eq_value_of_isoppositeang {ang₁ ang₂ : Angle P} (h : IsOppositeAng ang₁ ang₂) : ang₁.value = ang₂.value := sorry +theorem value_eq_of_isoppositeang {ang₁ ang₂ : Angle P} (h : IsOppositeAng ang₁ ang₂) : ang₁.value = ang₂.value := sorry -theorem eq_value_of_iscorrespondingang {ang₁ ang₂ : Angle P} (h : IsCorrespondingAng 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 theorem value_sub_eq_pi_of_isconsecutiveintang {ang₁ ang₂ : Angle P} (h : IsConsecutiveIntAng ang₁ ang₂) : ang₁.value - ang₂.value = π := sorry --`first mod 2π, then discuss +-? ` -theorem eq_value_of_isalternateintang {ang₁ ang₂ : Angle P} (h : IsAlternateIntAng ang₁ ang₂) : ang₁.value = ang₂.value := sorry +theorem value_eq_of_isalternateintang {ang₁ ang₂ : Angle P} (h : IsAlternateIntAng ang₁ ang₂) : ang₁.value = ang₂.value := sorry /- -- equivlently, this will be much more lengthy -theorem eq_value_of_corresponding_angle {l₁ l₂ l : DirLine P} (h : l₁.toDir = l₂.toDir) (g : ¬ l ∥ l₁) : (Angle.mk_dirline_dirline l₁ l (Ne.symm g)).value = (Angle.mk_dirline_dirline l₂ l (Ne.symm (ne_of_ne_of_eq g (Quotient.sound (h ▸ PM.con.refl _))))).value := sorry +theorem value_eq_of_corresponding_angle {l₁ l₂ l : DirLine P} (h : l₁.toDir = l₂.toDir) (g : ¬ l ∥ l₁) : (Angle.mk_dirline_dirline l₁ l (Ne.symm g)).value = (Angle.mk_dirline_dirline l₂ l (Ne.symm (ne_of_ne_of_eq g (Quotient.sound (h ▸ PM.con.refl _))))).value := sorry -/ end parallel diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle_trash.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle_trash.lean index 0d70cfab..aa2f5011 100644 --- a/EuclideanGeometry/Foundation/Axiom/Position/Angle_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle_trash.lean @@ -22,9 +22,6 @@ theorem angle_eq_zero_of_same_dir {A O : P} [h₁ : PtNe A O] : ∠ A O A = 0 := 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 -theorem eq_ang_value_of_lies_int_lies_int {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) ) : ∠ A O B = ∠ A' O B' := sorry - -theorem eq_ang_val_of_lieson_lieson {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) ) : ∠ A O B = ∠ 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 @@ -33,30 +30,16 @@ theorem neg_dvalue_of_rev_ang {A B O: P} (h₁ : A ≠ O) (h₂ : B ≠ O) : (AN namespace Angle theorem end_ray_eq_value_vadd_start_ray (ang : Angle P) : ang.dir₂ = ang.value +ᵥ ang.dir₁ := sorry --- to replace -/- -theorem end_ray_eq_start_ray_mul_value {ang : Angle P} : ang.dir₂ = ang.dir₁ * ang.value.toDir := sorry --/ - -theorem ang_source_eq_end_ray_source {ang : Angle P} : ang.source = ang.end_ray.source := 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 (by rw[h.symm, ang_source_eq_end_ray_source]) +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 --- to replace -/- -theorem value_eq_angdiff {ray₁ : Ray P} {ray₂ : Ray P} (h: ray₁.source = ray₂.source) : (Angle.mk_two_ray_of_eq_source ray₁ ray₂ h).value = Dir.AngDiff ray₁.toDir ray₂.toDir := sorry - -theorem mk_start_ray_value_eq_angdiff {ang : Angle P} {ray : Ray P} (h : ang.source = ray.source) : (Angle.mk_start_ray ang ray h).value = Dir.AngDiff ang.dir₁ ray.toDir := sorry - -theorem mk_end_ray_value_eq_angdiff {ang : Angle P} {ray : Ray P} (h : ang.source = ray.source) : (Angle.mk_end_ray ang ray h).value = Dir.AngDiff ray.toDir ang.dir₂ := sorry --/ end Angle diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean index 8047862f..b5359cdd 100644 --- a/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean +++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean @@ -13,7 +13,7 @@ namespace EuclidGeom variable {P : Type _} [EuclideanPlane P] {tr tr₁ tr₂ tr₃ : Triangle P} {tr_nd tr_nd₁ tr_nd₂ tr_nd₃ : TriangleND P} -open Classical AngValue +open Classical AngValue Angle -- Do not change `IsCongr, IsACongr` notation into `≅, ≅ₐ` in any theorem with name `IsCongr.some_theorem, IsACongr.some_theorem`, to use `h.some_theorem` when h is of shape `tr₁ ≅ tr₂`. namespace Triangle