Skip to content

Commit

Permalink
Clean the trash of Perpendicular.lean and update Position/Angle
Browse files Browse the repository at this point in the history
  • Loading branch information
mbkybky committed Jan 17, 2024
1 parent ec8c06a commit 45053b6
Showing 7 changed files with 109 additions and 53 deletions.
9 changes: 7 additions & 2 deletions EuclideanGeometry/Example/SCHAUM/Problem1.7.lean
Original file line number Diff line number Diff line change
@@ -135,8 +135,13 @@ Therefore, $DX = EY$.
-- We have $X \ne B$ as X is on the interior of ray $BA$ and therefore different to the source $B$.
have X_ne_B : e.X ≠ e.B := X_int_ray_BA.2
-- We have $X, B, D$ are not collinear because $D$ doesn't lies on line $AB$ and $B$ doesn't coincide with $X$.
have not_collinear_XBD : ¬ collinear e.X e.B e.D := by sorry
/- exact not_collinear_with_perp_foot_of_ne_perp_foot e.D e.B e.X (LIN e.A e.B e.B_ne_A) (Line.snd_pt_lies_on_mk_pt_pt e.B_ne_A) D_not_on_AB e.hd (X_ne_B).symm -/
have not_collinear_XBD : ¬ collinear e.X e.B e.D := by
by_contra h
haveI : PtNe e.X e.B := ⟨X_ne_B⟩
have : e.D LiesOn LIN e.X e.B := Line.pt_pt_maximal h
have : LIN e.X e.B = LIN e.A e.B _ := sorry
have : e.D LiesOn LIN e.A e.B _ := sorry
exact D_not_on_AB this
-- We have $D \ne X$.
have D_ne_X : e.D ≠ e.X := by sorry
-- In isoceles triangle $ABC$, we have $\angle CBA = - \angle BCA$.
3 changes: 0 additions & 3 deletions EuclideanGeometry/Foundation/Axiom/Linear/Line.lean
Original file line number Diff line number Diff line change
@@ -1276,9 +1276,6 @@ end ddist

section order

instance instOrderedAddTorsor (l : DirLine P) : OrderedAddTorsor ℝ l.carrier.Elem :=
AddTorsor.OrderedAddTorsor_of_OrderedAddCommGroup ℝ l.carrier.Elem

instance instLinearOrderedAddTorsor (l : DirLine P) : LinearOrderedAddTorsor ℝ l.carrier.Elem :=
AddTorsor.LinearOrderedAddTorsor_of_LinearOrderedAddCommGroup ℝ l.carrier.Elem

97 changes: 64 additions & 33 deletions EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean
Original file line number Diff line number Diff line change
@@ -263,54 +263,85 @@ theorem Ray.not_rev_para_rev_of_not_para {r r' : Ray P} (h : ¬ r ∥ r') : ¬ r

theorem DirLine.not_rev_para_rev_of_not_para {l l' : DirLine P} (h : ¬ l ∥ l') : ¬ l.reverse ∥ l'.reverse :=
DirFig.not_rev_para_rev_of_not_para h
/-
theorem DirFig.rev_para_of_para (h : l₁ ∥ l₂) : reverse l₁ ∥ l₂ :=
(rev_toProj_eq_toProj l₁).trans h

theorem SegND.rev_para_of_para {s s' : SegND P} (h : s ∥ s') : s.reverse ∥ s' :=
DirFig.rev_para_of_para h
theorem DirFig.para_rev_iff_para : l₁ ∥ reverse l₂ ↔ l₁ ∥ l₂ := sorry

theorem Ray.rev_para_of_para {r r' : Ray P} (h : r ∥ r') : r.reverse ∥ r' :=
DirFig.rev_para_of_para h
@[simp]
theorem SegND.para_rev_iff_para {s s' : SegND P} : s ∥ s'.reverse ↔ s ∥ s' := sorry

theorem DirLine.rev_para_of_para {l l' : DirLine P} (h : l ∥ l') : l.reverse ∥ l' :=
DirFig.rev_para_of_para h
@[simp]
theorem Ray.para_rev_iff_para {r r' : Ray P} : r ∥ r'.reverse ↔ r ∥ r' := sorry

theorem DirFig.not_rev_para_of_not_para (h : ¬ l₁ ∥ l₂) : ¬ reverse l₁ ∥ l₂ :=
fun hn ↦ h ((congrArg ProjObj.toProj rev_rev).symm.trans (rev_para_of_para hn) )
@[simp]
theorem DirLine.para_rev_iff_para {l l' : DirLine P} : l ∥ l'.reverse ↔ l ∥ l' := sorry

theorem SegND.not_rev_para_of_not_para {s s' : SegND P} (h : ¬ ss') : ¬ s.reverses' :=
DirFig.not_rev_para_of_not_para h
theorem DirFig.not_para_rev_iff_not_para : ¬ l₁reverse l₂ ↔ ¬ l₁l₂ :=
para_rev_iff_para.not

theorem Ray.not_rev_para_of_not_para {r r' : Ray P} (h : ¬ r ∥ r') : ¬ r.reverse ∥ r' :=
DirFig.not_rev_para_of_not_para h
@[simp]
theorem SegND.not_para_rev_iff_not_para {s s' : SegND P} : ¬ s ∥ s'.reverse ↔ ¬ s ∥ s' :=
para_rev_iff_para.not

theorem DirLine.not_rev_para_of_not_para {l l' : DirLine P} (h : ¬ l ∥ l') : ¬ l.reverse ∥ l' :=
DirFig.not_rev_para_of_not_para h
@[simp]
theorem Ray.not_para_rev_iff_not_para {r r' : Ray P} : ¬ r ∥ r'.reverse ↔ ¬ r ∥ r' :=
para_rev_iff_para.not

theorem DirFig.rev_para_rev_of_para (h : l₁ ∥ l₂) : reverse l₁ ∥ reverse l₂ :=
rev_para_of_para (para_rev_of_para h)
@[simp]
theorem DirLine.not_para_rev_iff_not_para {l l' : DirLine P} : ¬ l ∥ l'.reverse ↔ ¬ l ∥ l' :=
para_rev_iff_para.not

theorem SegND.rev_para_rev_of_para {s s' : SegND P} (h : s ∥ s') : s.reverse ∥ s'.reverse :=
DirFig.rev_para_rev_of_para h
theorem DirFig.rev_para_iff_para : reverse l₁ ∥ l₂ ↔ l₁ ∥ l₂ := sorry

theorem Ray.rev_para_rev_of_para {r r' : Ray P} (h : r ∥ r') : r.reverse ∥ r'.reverse :=
DirFig.rev_para_rev_of_para h
@[simp]
theorem SegND.rev_para_iff_para {s s' : SegND P} : s.reverse ∥ s' ↔ s ∥ s':= sorry

theorem DirLine.rev_para_rev_of_para {l l' : DirLine P} (h : l ∥ l') : l.reverse ∥ l'.reverse :=
DirFig.rev_para_rev_of_para h
@[simp]
theorem Ray.rev_para_iff_para {r r' : Ray P} : r.reverse ∥ r' ↔ r ∥ r' := sorry

theorem DirFig.not_rev_para_rev_of_not_para (h : ¬ l₁ ∥ l₂) : ¬ reverse l₁ ∥ reverse l₂ :=
not_rev_para_of_not_para (not_para_rev_of_not_para h)
@[simp]
theorem DirLine.rev_para_iff_para {l l' : DirLine P} : l.reverse ∥ l' ↔ l ∥ l' := sorry

theorem SegND.not_rev_para_rev_of_not_para {s s' : SegND P} (h : ¬ s ∥ s') : ¬ s.reverses'.reverse :=
DirFig.not_rev_para_rev_of_not_para h
theorem DirFig.not_rev_para_iff_not_para : ¬ reverse l₁ ∥ l₂ ↔ ¬ l₁l₂ :=
rev_para_iff_para.not

theorem Ray.not_rev_para_rev_of_not_para {r r' : Ray P} (h : ¬ r ∥ r') : ¬ r.reverse ∥ r'.reverse :=
DirFig.not_rev_para_rev_of_not_para h
@[simp]
theorem SegND.not_rev_para_iff_not_para {s s' : SegND P} : ¬ s.reverse ∥ s' ↔ ¬ s ∥ s' :=
rev_para_iff_para.not

theorem DirLine.not_rev_para_rev_of_not_para {l l' : DirLine P} (h : ¬ l ∥ l') : ¬ l.reverse ∥ l'.reverse :=
DirFig.not_rev_para_rev_of_not_para h -/
@[simp]
theorem Ray.not_rev_para_iff_not_para {r r' : Ray P} : ¬ r.reverse ∥ r' ↔ ¬ r ∥ r' :=
rev_para_iff_para.not

@[simp]
theorem DirLine.not_rev_para_iff_not_para {l l' : DirLine P} : ¬ l.reverse ∥ l' ↔ ¬ l ∥ l' :=
rev_para_iff_para.not

theorem DirFig.rev_para_rev_iff_para : reverse l₁ ∥ reverse l₂ ↔ l₁ ∥ l₂ := sorry

@[simp]
theorem SegND.rev_para_rev_iff_para {s s' : SegND P} : s.reverse ∥ s'.reverse ↔ s ∥ s' := sorry

@[simp]
theorem Ray.rev_para_rev_iff_para {r r' : Ray P} : r.reverse ∥ r'.reverse ↔ r ∥ r' := sorry

@[simp]
theorem DirLine.rev_para_rev_iff_para {l l' : DirLine P} : l.reverse ∥ l'.reverse ↔ l ∥ l' :=
sorry

theorem DirFig.not_rev_para_rev_iff_not_para : ¬ reverse l₁ ∥ reverse l₂ ↔ ¬ l₁ ∥ l₂ :=
rev_para_rev_iff_para.not

@[simp]
theorem SegND.not_rev_para_rev_iff_not_para {s s' : SegND P} : ¬ s.reverse ∥ s'.reverse ↔ ¬ s ∥ s' :=
rev_para_rev_iff_para.not

@[simp]
theorem Ray.not_rev_para_rev_iff_not_para {r r' : Ray P} : ¬ r.reverse ∥ r'.reverse ↔ ¬ r ∥ r' :=
rev_para_rev_iff_para.not

@[simp]
theorem DirLine.not_rev_para_rev_iff_not_para {l l' : DirLine P} (h : ¬ l ∥ l') : ¬ l.reverse ∥ l'.reverse :=
DirFig.not_rev_para_rev_of_not_para h

end reverse

6 changes: 5 additions & 1 deletion EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean
Original file line number Diff line number Diff line change
@@ -96,9 +96,13 @@ theorem line_of_self_perp_foot_perp_line_of_not_lies_on {A : P} {l : Line P} (h
theorem dist_eq_zero_iff_lies_on (A : P) (l : Line P) : dist_pt_line A l = 0 ↔ A LiesOn l :=
Seg.length_eq_zero_iff_deg.trans (perp_foot_eq_self_iff_lies_on A l)

-- Maybe the proof of this theorem should require the Pythagorean Theorem.
theorem perp_foot_unique {A B : P} {l : DirLine P} (h : B LiesOn l) [_hne : PtNe A B] (hp : LIN A B ⟂ l) : perp_foot A l = B := sorry

-- `Maybe the proof of following theorems should require the Pythagorean Theorem.`
theorem dist_pt_line_shortest (A B : P) {l : Line P} (h : B LiesOn l) : dist A B ≥ dist_pt_line A l := sorry

theorem eq_dist_eq_perp_foot {A B : P} {l : DirLine P} (h : A LiesOn l) (heq : dist B A = dist_pt_line B l) : A = perp_foot B l := sorry

end Perpendicular_constructions

end EuclidGeom
10 changes: 0 additions & 10 deletions EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular_trash.lean
Original file line number Diff line number Diff line change
@@ -8,14 +8,4 @@ open Line

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


theorem not_collinear_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): ¬ collinear 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

theorem eq_dist_eq_perp_foot {A B : P} {l : DirLine P} (h : A LiesOn l) (heq : dist B A = dist_pt_line B l) : A = perp_foot B l := sorry

end EuclidGeom
16 changes: 14 additions & 2 deletions EuclideanGeometry/Foundation/Axiom/Position/Angle.lean
Original file line number Diff line number Diff line change
@@ -574,8 +574,11 @@ 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 angDiff_eq_zero_of_same_dir {dir₁ dir₂ : Dir} (h : dir₁ = dir₂) : AngDiff dir₁ dir₂ = 0 :=
vsub_eq_zero_iff_eq.mpr h.symm

theorem same_dir_iff_value_eq_zero : ang.dir₁ = ang.dir₂ ↔ ang.value = 0 :=
⟨angDiff_eq_zero_of_same_dir, fun h ↦ (eq_of_vsub_eq_zero h).symm⟩

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])
@@ -611,6 +614,15 @@ theorem dvalue_eq_zero_of_same_dir (h : ang.dir₁ = ang.dir₂) : ang.dvalue =
theorem dvalue_eq_pi_of_eq_neg_dir (h : ang.dir₁ = - ang.dir₂) : ang.dvalue = 0 := by
simp only [dvalue_eq_vsub, toProj_eq_toProj_iff.mpr (.inr h), vsub_self]

theorem dAngDiff_eq_zero_of_same_proj {proj₁ proj₂ : Proj} (h : proj₁ = proj₂) : DAngDiff proj₁ proj₂ = 0 :=
vsub_eq_zero_iff_eq.mpr h.symm

theorem same_proj_iff_dvalue_eq_zero : ang.proj₁ = ang.proj₂ ↔ ang.dvalue = 0 :=
eq_comm.trans vsub_eq_zero_iff_eq.symm

theorem same_proj_iff_isND : ang.proj₁ = ang.proj₂ ↔ ¬ ang.IsND :=
same_proj_iff_dvalue_eq_zero.trans not_isND_iff_coe.symm

theorem dvalue_eq_of_dir_eq (h₁ : ang₁.dir₁ = ang₂.dir₁) (h₂ : ang₁.dir₂ = ang₂.dir₂) : ang₁.dvalue = ang₂.dvalue := by
simp only [dvalue_eq_vsub, congrArg Dir.toProj h₁, congrArg Dir.toProj h₂]

21 changes: 19 additions & 2 deletions EuclideanGeometry/Foundation/Axiom/Position/Angle_ex.lean
Original file line number Diff line number Diff line change
@@ -162,10 +162,14 @@ def IsSuppl (ang₁ ang₂ : Angle P) : Prop := ang₁ = ang₂.suppl

theorem value_add_value_eq_pi_of_isSuppl (h : ang₁.IsSuppl ang₂) : ang₁.value + ang₂.value = π := sorry

theorem dir_eq_neg_dir_of_value_add_eq_pi_of_dir_eq (hs : ang₁.source = ang₂.source) (hd : ang₁.dir₁ = ang₂.dir₂) (hv : ang₁.value + ang₂.value = π) : ang₁.dir₂ = - ang₂.dir₁ := sorry
theorem dir_eq_neg_dir_of_value_add_eq_pi_of_dir_eq (hd : ang₁.dir₁ = ang₂.dir₂) (hv : ang₁.value + ang₂.value = π) : ang₁.dir₂ = - ang₂.dir₁ := sorry

theorem dir_eq_of_value_add_eq_pi_of_dir_eq_neg_dir (hd : ang₁.dir₂ = - ang₂.dir₁) (hv : ang₁.value + ang₂.value = π) : ang₁.dir₁ = ang₂.dir₂ := sorry

theorem isSuppl_of_value_add_eq_pi_of_dir_eq_of_source_eq (hs : ang₁.source = ang₂.source) (hd : ang₁.dir₁ = ang₂.dir₂) (hv : ang₁.value + ang₂.value = π) : ang₁.IsSuppl ang₂ := sorry

theorem isSuppl_of_value_add_eq_pi_of_dir_eq_neg_dir_of_source_eq (hs : ang₁.source = ang₂.source) (hd : ang₁.dir₂ = - ang₂.dir₁) (hv : ang₁.value + ang₂.value = π) : ang₁.IsSuppl ang₂ := sorry

end supplementary

section reverse
@@ -176,7 +180,7 @@ def reverse (ang : Angle P) : Angle P where
dir₁ := ang.dir₂
dir₂ := ang.dir₁

variable {ang : Angle P}
variable {ang ang₁ ang₂ : Angle P}

@[simp]
theorem rev_source : ang.reverse.source = ang.source := rfl
@@ -236,6 +240,19 @@ theorem suppl_rev_oppo_eq_rev_suppl : ang.suppl.reverse.oppo = ang.reverse.suppl

theorem rev_oppo_eq_oppo_rev : ang.reverse.oppo = ang.oppo.reverse := rfl

@[pp_dot]
def IsReverse (ang₁ ang₂ : Angle P) : Prop := ang₁ = ang₂.reverse

theorem value_eq_neg_value_isReverse (h : ang₁.IsReverse ang₂) : ang₁.value = - ang₂.value := sorry
/-
theorem dir_eq_neg_dir_of_value_add_eq_pi_of_dir_eq (hd : ang₁.dir₁ = ang₂.dir₂) (hv : ang₁.value + ang₂.value = π) : ang₁.dir₂ = - ang₂.dir₁ := sorry
theorem dir_eq_of_value_add_eq_pi_of_dir_eq_neg_dir (hd : ang₁.dir₂ = - ang₂.dir₁) (hv : ang₁.value + ang₂.value = π) : ang₁.dir₁ = ang₂.dir₂ := sorry
theorem isSuppl_of_value_add_eq_pi_of_dir_eq_of_source_eq (hs : ang₁.source = ang₂.source) (hd : ang₁.dir₁ = ang₂.dir₂) (hv : ang₁.value + ang₂.value = π) : ang₁.IsSuppl ang₂ := sorry
theorem isSuppl_of_value_add_eq_pi_of_dir_eq_neg_dir_of_source_eq (hs : ang₁.source = ang₂.source) (hd : ang₁.dir₂ = - ang₂.dir₁) (hv : ang₁.value + ang₂.value = π) : ang₁.IsSuppl ang₂ := sorry
-/
end reverse

end Angle

0 comments on commit 45053b6

Please sign in to comment.