From 9d60254840b9ca5bd7e170a3d258d787c5b1dc46 Mon Sep 17 00:00:00 2001
From: kfc2333 <48116356+kfc2333@users.noreply.github.com>
Date: Sat, 23 Sep 2023 15:37:06 +0800
Subject: [PATCH] Team_D_project_changed_Plane.lean_and_Ray.lean

---
 .../Foundation/Axiom/Basic/Plane.lean         |  60 ++++++++--
 .../Foundation/Axiom/Linear/Ray.lean          | 110 ++++++++++++++++--
 2 files changed, 148 insertions(+), 22 deletions(-)

diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Plane.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Plane.lean
index bf5a2c52..a0b52848 100644
--- a/EuclideanGeometry/Foundation/Axiom/Basic/Plane.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Basic/Plane.lean
@@ -47,28 +47,58 @@ instance : AddTorsor (Vec) P := by infer_instance
 
 /- vector $AB +$ point $A =$ point $B$ -/
 @[simp]
-theorem start_vadd_vec_eq_end (A B : P) : (VEC A B) +ᵥ A = B := sorry
+theorem start_vadd_vec_eq_end (A B : P) : (VEC A B) +ᵥ A = B := by
+  rw [Vec.mk_pt_pt]
+  exact vsub_vadd B A
 
 @[simp]
-theorem vadd_eq_self_iff_vec_eq_zero {A : P} {v : Vec} : v +ᵥ A = A ↔ v = 0 := sorry
+theorem vadd_eq_self_iff_vec_eq_zero {A : P} {v : Vec} : v +ᵥ A = A ↔ v = 0 := by
+  constructor
+  intro h
+  have k : v +ᵥ A -ᵥ A = A-ᵥ A := by
+    rw [h]
+  have u : v +ᵥ A -ᵥ A = v := by
+    simp
+  rw [u] at k
+  simp at k
+  exact k
+  intro h
+  rw[h]
+  simp
 
 @[simp]
-theorem vec_same_eq_zero (A : P) : VEC A A = 0 := sorry
+theorem vec_same_eq_zero (A : P) : VEC A A = 0 := by
+  rw [Vec.mk_pt_pt]
+  simp
 
-theorem neg_vec (A B : P) : - VEC A B = VEC B A := sorry
+theorem neg_vec (A B : P) : - VEC A B = VEC B A := by
+  rw [Vec.mk_pt_pt]
+  rw [Vec.mk_pt_pt]
+  simp
 
-theorem eq_iff_vec_eq_zero (A B : P) : B = A ↔ VEC A B = 0 := sorry
+theorem eq_iff_vec_eq_zero (A B : P) : B = A ↔ VEC A B = 0 := by
+  rw [Vec.mk_pt_pt]
+  exact Iff.symm vsub_eq_zero_iff_eq
 
-theorem ne_iff_vec_ne_zero (A B : P) : B ≠ A ↔ (VEC A B) ≠ 0 := sorry
+theorem ne_iff_vec_ne_zero (A B : P) : B ≠ A ↔ (VEC A B) ≠ 0 := by
+  apply Iff.not
+  exact eq_iff_vec_eq_zero A B
 
 @[simp]
-theorem vec_add_vec (A B C : P) : VEC A B + VEC B C = VEC A C := sorry
+theorem vec_add_vec (A B C : P) : VEC A B + VEC B C = VEC A C := by
+  rw [add_comm]
+  repeat rw [Vec.mk_pt_pt]
+  rw [vsub_add_vsub_cancel]
 
 @[simp]
-theorem vec_of_pt_vadd_pt_eq_vec (A : P) (v : Vec) : (VEC A (v +ᵥ A)) = v := sorry
+theorem vec_of_pt_vadd_pt_eq_vec (A : P) (v : Vec) : (VEC A (v +ᵥ A)) = v := by
+  rw [Vec.mk_pt_pt]
+  exact vadd_vsub v A
 
 @[simp]
-theorem vec_sub_vec (O A B: P) : VEC O B - VEC O A = VEC A B := sorry
+theorem vec_sub_vec (O A B: P) : VEC O B - VEC O A = VEC A B := by
+  repeat rw [Vec.mk_pt_pt]
+  simp
 
 theorem pt_eq_pt_of_eq_smul_smul {O A B : P} {v : Vec} {tA tB : ℝ} (h : tA = tB) (ha : VEC O A = tA • v) (hb : VEC O B = tB • v) : A = B := by
   have hc : VEC A B = VEC O B - VEC O A := Eq.symm (vec_sub_vec O A B)
@@ -76,6 +106,16 @@ theorem pt_eq_pt_of_eq_smul_smul {O A B : P} {v : Vec} {tA tB : ℝ} (h : tA = t
   exact Eq.symm ((eq_iff_vec_eq_zero A B).2 hc)
 
 theorem eq_of_smul_Vec_nd_eq_smul_Vec_nd {v : Vec_nd} {tA tB : ℝ} (e : tA • v.1 = tB • v.1) : tA = tB := by
-  sorry
+  have h : (tA - tB) • v.1 = 0 := by
+    rw [sub_smul]
+    rw [e]
+    simp
+  rw [smul_eq_zero] at h
+  rcases h with x | y
+  linarith
+  have: v.1 ≠ 0 := by
+    apply v.2
+  contradiction
+
 
 end EuclidGeom
\ No newline at end of file
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean
index 8864fef3..1e077281 100644
--- a/EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean
+++ b/EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean
@@ -207,11 +207,24 @@ def Seg.length : ℝ := norm (l.toVec)
 theorem length_nonneg : 0 ≤ l.length := by exact @norm_nonneg _ _ _
 
 -- A generalized directed segment is nontrivial if and only if its length is positive.
-theorem length_pos_iff_nd : 0 < l.length ↔ (l.is_nd) := by sorry
-
-theorem length_ne_zero_iff_nd : 0 ≠ l.length ↔ (l.is_nd) := by sorry
-
-theorem length_pos (l : Seg_nd P): 0 < l.1.length := by sorry
+theorem length_pos_iff_nd : 0 < l.length ↔ (l.is_nd) := by
+  rw [Seg.length]
+  rw [Seg.is_nd]
+  rw [norm_pos_iff]
+  apply Iff.not
+  rw [toVec_eq_zero_of_deg]
+
+theorem length_ne_zero_iff_nd : 0 ≠ l.length ↔ (l.is_nd) := by 
+  rw [Seg.length]
+  rw [Seg.is_nd]
+  apply Iff.not
+  rw [toVec_eq_zero_of_deg]
+  rw [eq_comm]
+  exact norm_eq_zero
+
+theorem length_pos (l : Seg_nd P): 0 < l.1.length := by
+  rw [length_pos_iff_nd]
+  simp only [l.2, not_false_eq_true]
 
 theorem length_sq_eq_inner_toVec_toVec : l.length ^ 2 = inner l.toVec l.toVec := by
   have w : l.length = Real.sqrt (inner l.toVec l.toVec) := by 
@@ -230,7 +243,29 @@ theorem triv_iff_length_eq_zero : (l.target = l.source) ↔ l.length = 0 := by
   exact Iff.trans (toVec_eq_zero_of_deg _)  (@norm_eq_zero _ _).symm
 
 -- If P lies on a generalized directed segment AB, then length(AB) = length(AP) + length(PB)
-theorem length_eq_length_add_length (l : Seg P) (A : P) (lieson : A LiesOn l) : l.length = (SEG l.source A).length + (SEG A l.target).length := sorry
+theorem length_eq_length_add_length (l : Seg P) (A : P) (lieson : A LiesOn l) : l.length = (SEG l.source A).length + (SEG A l.target).length := by
+  unfold Seg.length
+  rw [seg_toVec_eq_vec]
+  rw [seg_toVec_eq_vec]
+  rw [seg_toVec_eq_vec]
+  rcases lieson with ⟨t, ⟨a, b, c⟩ ⟩
+  have h: VEC l.source l.target = VEC l.source A + VEC A l.target := by simp
+  rw [c]
+  have s: VEC A l.target = ( 1 - t ) • VEC l.source l.target := by 
+    rw [c] at h
+    rw [sub_smul]
+    rw [one_smul]
+    exact eq_sub_of_add_eq' (id (Eq.symm h))
+  rw [s]
+  rw [norm_smul]
+  rw [norm_smul]
+  rw [← add_mul]
+  rw [Real.norm_of_nonneg]
+  rw [Real.norm_of_nonneg]
+  linarith
+  simp
+  exact b
+  exact a
 
 end length
 
@@ -257,19 +292,70 @@ section existence
 
 -- Archimedean property I : given a directed segment AB (with A ≠ B), then there exists a point P such that B lies on the directed segment AP and P ≠ B.
 
-theorem Seg_nd.exist_pt_beyond_pt {P : Type _} [EuclideanPlane P] (l : Seg_nd P) : (∃ q : P, l.1.target LiesInt (SEG l.1.source q)) := by sorry
-
+theorem Seg_nd.exist_pt_beyond_pt {P : Type _} [EuclideanPlane P] (l : Seg_nd P) : (∃ q : P, l.1.target LiesInt (SEG l.1.source q)) := by 
+  let h := l.1.toVec +ᵥ l.1.target
+  let half : ℝ := 1/2
+  have c: 0 ≤ half ∧ half ≤ 1 ∧ VEC l.1.source l.1.target = half • VEC l.1.source h := by
+    norm_num
+    rw [seg_toVec_eq_vec]
+    repeat rw [Vec.mk_pt_pt]
+    rw [vadd_vsub_assoc]
+    let t := l.1.target -ᵥ l.1.source
+    have x: t = 1/2 * (t + t) := by
+      calc t = 1/2 * (2 * t) := by simp
+      _ = 1/2 * (t + t) := by rw [two_mul]
+    exact x
+  have a: l.1.target LiesOn SEG l.1.source h := ⟨half, c⟩
+  have b: l.1.target ≠ l.1.source ∧ l.1.target ≠ h := by
+    constructor
+    exact l.2
+    have x: l.1.toVec ≠ 0 := by 
+      rw [seg_toVec_eq_vec]
+      rw [Vec.mk_pt_pt]
+      rw [vsub_ne_zero]
+      exact l.2
+    have y: l.1.target ≠ l.1.toVec +ᵥ l.1.target := by
+      rw [ne_comm]
+      by_contra t
+      simp at t
+      exact x t
+    exact y
+  have k: l.1.target LiesInt SEG l.1.source h := ⟨a, b⟩
+  use h
+ 
 -- Archimedean property II: On an nontrivial directed segment, one can always find a point in its interior.  `This will be moved to later disccusion about midpoint of a segment, as the midpoint is a point in the interior of a nontrivial segment`
 
-theorem nd_of_exist_int_pt (l : Seg P) (p : P) (h : p LiesInt l) : l.is_nd := sorry
+theorem nd_of_exist_int_pt (l : Seg P) (p : P) (h : p LiesInt l) : l.is_nd := by
+  rw [Seg.is_nd]
+  rcases h with ⟨⟨c, d⟩, b⟩
+  rcases b with ⟨p_ne_s, _⟩
+  rcases d with ⟨_, _, e⟩
+  have t: VEC Seg.source p ≠ 0 := by exact Iff.mp (ne_iff_vec_ne_zero Seg.source p) p_ne_s
+  have u: c • VEC Seg.source Seg.target ≠ 0 := by 
+    rw [← e]
+    exact t
+  have v: VEC Seg.source Seg.target ≠ 0 := by
+    exact right_ne_zero_of_smul u
+  exact Iff.mp vsub_ne_zero v
 
 -- If a generalized directed segment contains an interior point, then it is nontrivial
-theorem nd_iff_exist_int_pt (l : Seg P) : ∃ (p : P), p LiesInt l ↔ l.is_nd := sorry
+theorem nd_iff_exist_int_pt (l : Seg P) : (∃ (p : P), p LiesInt l) ↔ l.is_nd := by
+  constructor
+
+  intro h
+  rcases h with ⟨a, b⟩
+  exact nd_of_exist_int_pt l a b
 
-theorem Seg_nd.exist_int_pt (l : Seg_nd P) : ∃ (p : P), p LiesInt l.1 := sorry
+  intro h
+  use l.midpoint
+  exact Seg_nd.midpt_lies_int ⟨l, h⟩
 
-theorem length_pos_iff_exist_int_pt (l : Seg P) : 0 < l.length ↔  ∃ (p : P), p LiesInt l := sorry 
+theorem Seg_nd.exist_int_pt (l : Seg_nd P) : ∃ (p : P), p LiesInt l.1 := by
+  use l.1.midpoint
+  exact midpt_lies_int l
 
+theorem length_pos_iff_exist_int_pt (l : Seg P) : 0 < l.length ↔ (∃ (p : P), p LiesInt l) := by 
+  exact Iff.trans (length_pos_iff_nd _) (nd_iff_exist_int_pt _).symm
 end existence
 
 end EuclidGeom
\ No newline at end of file