Merge pull request #286 from stupidchunchun/master

修改了ShanZun Ex1f‘ 和 Ray.trash
jjdishere · Jan 16, 2024 · 70e6de2 · 70e6de2
2 parents 98c8e5b + 2bcbbed
commit 70e6de2
Show file tree

Hide file tree

Showing 2 changed files with 89 additions and 44 deletions.
diff --git a/EuclideanGeometry/Example/ShanZun/Ex1f'.lean b/EuclideanGeometry/Example/ShanZun/Ex1f'.lean
@@ -50,11 +50,10 @@ theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : (S
   let e.F := Ray.extpoint (SEG_nd e.B e.D).extension (SEG e.B e.C).length
   have DF_eq_CB : (SEG e.D e.F).length = (SEG e.C e.B).length := by
     calc
-      -- $DF = BC$ from above
+      -- $DF = BC$ from defination of $F$
       _ = (SEG e.B e.C).length := by
-        apply seg_length_eq_dist_of_extpoint (SEG_nd e.B e.D).extension
-        simp
-        exact length_nonneg
+        apply Ray.dist_of_extpoint (r := (SEG_nd e.B e.D).extension)
+        exact Seg.length_nonneg
       -- $BC = CB$ by symmetry
       _ = (SEG e.C e.B).length := by
         simp only [length_of_rev_eq_length']
@@ -64,23 +63,23 @@ theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : (S
   haveI E_ne_F : PtNe e.E e.F := sorry
   -- $F$ lies in extension of $BD$
   have F_int_BD_extn : e.F LiesInt (SEG_nd e.B e.D).extension := by
-    apply lies_int_of_pos_extpoint (r := (SEG e.B e.C).length)
+    apply Ray.lies_int_of_eq_pos_extpoint (t := (SEG e.B e.C).length)
+    rw [length_pos_iff_PtNe]
+    exact B_ne_C
     simp
-    intro hh
-    rw [length_pos_iff_nd]
-    -- exact B_ne_C
-    sorry
-    --这里要用instance的B≠C推线段BC非退化，好像不能直接exact
   -- $D$ lies on $BF$ because $F$ lies on extension of $BD$
   have D_on_BF : e.D LiesOn (SEG_nd e.B e.F) :=  SegND.lies_on_of_lies_int (SegND.target_lies_int_seg_source_pt_of_pt_lies_int_extn F_int_BD_extn)
   -- $C$ lies on $BF$ because $C$ lies on $BD$ and $D$ lies on $BF$
+  --这个sorry应该是一些linear Order的东西
   have C_on_BF : e.C LiesOn (SEG_nd e.B e.F) := sorry
   -- $A$ lies on $BE$ because $E$ lies on exxtension of $BA$
   have A_on_BE : e.A LiesOn (SEG_nd e.B e.E) := SegND.lies_on_of_lies_int (SegND.target_lies_int_seg_source_pt_of_pt_lies_int_extn e.he)
   -- $F$ lies on ray $BC$ because $C$ lies on $BF$
   have C_on_ray_BF : e.C LiesOn (RAY e.B e.F) := SegND.lies_on_toRay_of_lies_on C_on_BF
   -- $E$ lies on ray $BA$ because $A$ lies on $BE$
   have A_on_ray_BE : e.A LiesOn (RAY e.B e.E) := SegND.lies_on_toRay_of_lies_on A_on_BE
+  -- $B$ lies on ray $FD$ because $F$ lies on ray $BD$
+  have B_on_ray_FD : e.B LiesOn (RAY e.F e.D) := sorry
   -- $BF = BD + DF = AE + AB = BE$
   have BF_eq_BE : (SEG e.B e.F).length = (SEG e.B e.E).length := by
     calc
@@ -124,22 +123,34 @@ theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : (S
     exact ang_EBF_eq_sixty
     rw[← Seg.length_of_rev_eq_length (seg := (SEG e.B e.E))] at BF_eq_BE
     exact BF_eq_BE.symm
--- $\angle EBC = - \angle EFD$ because $\triangle BFE$ is regular
-  -- 下面1,3sorry留下的是很烦的相同射线推相同角度,第二个sorry需要x=y推出-x=-y
+  -- $\angle FBE = - \angle EFB$ because $\triangle BFE$ is regular
+  have ang_FBE_eq_ang_EFB : ∠ e.F e.B e.E = ∠ e.E e.F e.B := ((regular_tri_iff_eq_angle_of_nd_tri (TRI_nd e.B e.F e.E BFE_not_collinear)).mp BFE_is_regular).1
+  -- $\angle EBC = - \angle EFD$ because $\triangle BFE$ is regular
   have ang_EBC_eq_neg_ang_EFD : ∠ e.E e.B e.C = - ∠ e.E e.F e.D := by
     calc
     --$\angle EBC = \ange EBF$ because they are the same angle
     _ = ∠ e.E e.B e.F := by
       have E_on_ray_BE : e.E LiesOn (SEG_nd e.B e.E).toRay := SegND.lies_on_toRay_of_lies_on SegND.target_lies_on
-      apply Angle.value_eq_of_lies_on_ray_pt_pt
-      exact E_on_ray_BE
-      exact C_on_ray_BF
-    --$\angle EBF = \ange BFE$ because $\triangle BFE$ is regular
-    _ = ∠ e.B e.F e.E := sorry
-    --下面这行证明的是∠ FBE = ∠ EFB, 要转化到这个反过来的我好像还没找到那个定理（就是∠ XYZ = - ∠ ZYX）
-    --exact ((regular_tri_iff_eq_angle_of_nd_tri (TRI_nd e.B e.F e.E BFE_not_collinear)).mp BFE_is_regular).1.symm
-    _ = ∠ e.D e.F e.E := sorry
-    _ = - ∠ e.E e.F e.D := sorry
+      exact Angle.value_eq_of_lies_on_ray_pt_pt E_on_ray_BE C_on_ray_BF
+    --$\angle EBF = - \angle FBE$ by reverse
+    _ = - ∠ e.F e.B e.E := by
+      rw[← Angle.rev_value_eq_neg_value (ang := (ANG e.F e.B e.E))]
+      constructor
+    --$\angle FBE = - \angle EFB$ by the lemma above
+    _ = - ∠ e.E e.F e.B := by
+      simp only[ang_FBE_eq_ang_EFB]
+    --$- \angle EFB = \angle BFE$ by reverse
+    _ = ∠ e.B e.F e.E := by
+      rw[← Angle.rev_value_eq_neg_value (ang := (ANG e.E e.F e.B))]
+      constructor
+    --$\angle BFE = \ange DFE$ because they are the same angle
+    _ = ∠ e.D e.F e.E := by
+      have E_on_ray_FE : e.E LiesOn (SEG_nd e.F e.E).toRay := SegND.lies_on_toRay_of_lies_on SegND.target_lies_on
+      exact Angle.value_eq_of_lies_on_ray_pt_pt B_on_ray_FD E_on_ray_FE
+    --$\angle DFE = - \angle EFD$ by reverse
+    _ = - ∠ e.E e.F e.D := by
+      rw[← Angle.rev_value_eq_neg_value (ang := (ANG e.E e.F e.D))]
+      constructor
   -- $FE = BE$ because $\triangle BFE$ is regular
   have FE_eq_BE : (SEG e.F e.E).length = (SEG e.B e.E).length := by
     calc
@@ -166,24 +177,40 @@ $F,G$ are points of trisection of $AC$,
 line $DF$ and $EG$ intersect at $H$
 Prove that quadrilateral $ABCH$ is parallelogram -/
 
+structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
 -- We have triangle $\triangle ABC$
-variable {A B C : P} {hnd : ¬ collinear A B C}
+  A : Plane
+  B : Plane
+  C : Plane
+  hnd : ¬ collinear A B C
 -- Claim: $A \ne B$ and $B \ne C$ and $C \ne A$.
-lemma A_ne_B : A ≠ B := sorry
-lemma B_ne_C : B ≠ C := sorry
-lemma C_ne_A : C ≠ A := sorry
+instance A_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear e.hnd).2.2.symm⟩
+instance B_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.B e.C := ⟨(ne_of_not_collinear e.hnd).1.symm⟩
+instance C_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.C e.A := ⟨(ne_of_not_collinear e.hnd).2.1.symm⟩
+
+structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plane where
 -- $D$ is midpoint of $BA$, $E$ is midpoint of $BC$
-variable {D E : P} {hd : D = (SEG B A).midpoint} {he : E = (SEG B C).midpoint}
+  D : Plane
+  E : Plane
+  hd : D = (SEG B A).midpoint
+  he : E = (SEG B C).midpoint
 -- $F,G$ are points of trisection of $AC$
-variable {F G : P} {hf : F LiesInt (SegND A C C_ne_A).1} {he : E LiesInt (SegND A C C_ne_A).1} {htri : (SEG A F).length = (SEG F G).length ∧ (SEG F G).length = (SEG G C).length}
+  F : Plane
+  G : Plane
+  hf : F LiesInt (SEG_nd A C)
+  hg : G LiesInt (SEG_nd A C)
+  htri : (SEG A F).length = (SEG F G).length ∧ (SEG F G).length = (SEG G C).length
 -- Claim: $F \ne D$ and $G \ne E$
-lemma f_ne_d : F ≠ D := sorry
-lemma g_ne_e : G ≠ E := sorry
+instance F_ne_D {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.F e.D := ⟨sorry⟩
+instance G_ne_E {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.G e.E := ⟨sorry⟩
+
+structure Setting3 (Plane : Type _) [EuclideanPlane Plane] extends Setting2 Plane where
 -- $H$ is the intersection of line $DF$ and $EG$
-variable {H : P} {hh : is_inx H (LIN D F f_ne_d) (LIN E G g_ne_e)}
+  H : Plane
+  hh : is_inx H (LIN D F) (LIN E G)
 
 -- Theorem : quadrilateral $ABCH$ is parallelogram
-theorem Shan_Problem_2_22 : QDR A B C H IsPRG := sorry
+theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting3 Plane} : QDR e.A e.B e.C e.H IsPRG := sorry
 
 end Shan_Problem_2_22
 
@@ -194,29 +221,43 @@ $F,G$ are points lies on line $BC$,
 such that $FB = CG$ and $AF \parallel BE$ ,
 Prove that $AG \parallel DC$-/
 
+structure Setting1  (Plane : Type _) [EuclideanPlane Plane] where
 -- We have triangle $\triangle ABC$
-variable {A B C : P} {hnd : ¬ collinear A B C}
+  A : Plane
+  B : Plane
+  C : Plane
+  hnd : ¬ collinear A B C
 -- Claim: $A \ne B$ and $B \ne C$ and $C \ne A$.
-lemma A_ne_B : A ≠ B := sorry
-lemma B_ne_C : B ≠ C := sorry
-lemma C_ne_A : C ≠ A := sorry
+instance A_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear e.hnd).2.2.symm⟩
+instance B_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.B e.C := ⟨(ne_of_not_collinear e.hnd).1.symm⟩
+instance C_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.C e.A := ⟨(ne_of_not_collinear e.hnd).2.1.symm⟩
+
+structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plane where
 -- $D,E$ are points in $AB,AC$ respectively
-variable {D E : P} {hd : D LiesInt (SegND A B A_ne_B.symm).1} {he : E LiesInt (SegND A C C_ne_A).1}
+  D : Plane
+  E : Plane
+  hd : D LiesInt (SEG_nd A B)
+  he : E LiesInt (SEG_nd A C)
 -- $F,G$ are points lies on line $BC$
-variable {F G : P} {hf : F LiesOn (LIN B C B_ne_C.symm)} {hg : G LiesOn (LIN B C B_ne_C.symm)}
+  F : Plane
+  G : Plane
+  hf : F LiesOn (LIN B C)
+  hg : G LiesOn (LIN B C)
 -- We have $FB = CG$
-variable {hedge : (SEG F B).length = (SEG C G).length}
+  hedge : (SEG F B).length = (SEG C G).length
 -- Claim : $F \ne A$ and $E \ne B$
-lemma f_ne_a : F ≠ A := sorry
-lemma e_ne_B : E ≠ B := sorry
+instance F_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.F e.A := ⟨sorry⟩
+instance E_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.E e.B := ⟨sorry⟩
+
+structure Setting3 (Plane : Type _) [EuclideanPlane Plane] extends Setting2 Plane where
 -- We have $AF \parallel BE$
-variable {hpara : (SegND A F f_ne_a) ∥ (SegND B E e_ne_B)}
+  hpara : (SEG_nd A F) ∥ (SEG_nd B E)
 -- Claim: $G \ne A$ and $D \ne C$
-lemma g_ne_a : G ≠ A := sorry
-lemma d_ne_C : D ≠ C := sorry
+instance G_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting3 Plane} : PtNe e.G e.A := ⟨sorry⟩
+instance D_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting3 Plane} : PtNe e.D e.C := ⟨sorry⟩
 
 -- Theorem : $AG \parallel DC$
-theorem Shan_Problem_2_36 : (SegND A G g_ne_a) ∥ (SegND C D d_ne_C) := sorry
+theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting3 Plane} : (SEG_nd e.A e.G) ∥ (SEG_nd e.C e.D) := sorry
 
 end Shan_Problem_2_36
 

diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean
@@ -16,4 +16,8 @@ variable {P : Type _} [EuclideanPlane P] (seg_nd : SegND P)
   by the way in_seg shoud be renamed by current naming system
 -/
 
+-- 以前的length_pos_iff_nd不是很好用，现在加一个PtNe的版本,但是PtNe是instance，以后还需要修改
+/-- A segment has positive length if and only if its source is not equal to its target. -/
+theorem length_pos_iff_PtNe {seg : Seg P} : 0 < seg.length ↔ (PtNe seg.source seg.target) := sorry
+
 end EuclidGeom