From 431dc1a1284a7e148ac9c1bfc3b8847dce1734fa Mon Sep 17 00:00:00 2001 From: negiizhao Date: Sat, 20 Jan 2024 21:57:25 +0800 Subject: [PATCH] `Type _` -> `Type*` (#297) * `Type _` -> `Type*` * fix * Revert "fix" This reverts commit 208bdd1475ed16c3faaa63ab23c95757be9cafe0. * fix * more --- EuclideanGeometry/Check.lean | 18 +-- EuclideanGeometry/Example/AOPS/Chap2.lean | 2 +- EuclideanGeometry/Example/AOPS/Chap3.lean | 2 +- EuclideanGeometry/Example/AOPS/Chap3a.lean | 2 +- EuclideanGeometry/Example/AOPS/Chap5.lean | 2 +- EuclideanGeometry/Example/AOPS/Chap5a.lean | 10 +- .../Example/ArefWernick/Chap1.lean | 2 +- .../Example/ArefWernick/Chap1a.lean | 2 +- .../Congruence_Exercise_ygr/Problem_1.lean | 24 ++-- .../Congruence_Exercise_ygr/Problem_2.lean | 12 +- .../Congruence_Exercise_ygr/Problem_3.lean | 4 +- .../Congruence_Exercise_ygr/Problem_4.lean | 20 +-- .../Congruence_Exercise_ygr/Problem_6.lean | 2 +- .../Congruence_Exercise_ygr/Problem_7.lean | 2 +- .../Congruence_Exercise_ygr/Problem_8.lean | 2 +- EuclideanGeometry/Example/ExerciseXT8.lean | 2 +- .../Example/SCHAUM/Problem1.1.lean | 6 +- .../Example/SCHAUM/Problem1.10.lean | 2 +- .../Example/SCHAUM/Problem1.11.lean | 6 +- .../Example/SCHAUM/Problem1.12.lean | 6 +- .../Example/SCHAUM/Problem1.13.lean | 2 +- .../Example/SCHAUM/Problem1.14.lean | 18 +-- .../Example/SCHAUM/Problem1.2'.lean | 10 +- .../Example/SCHAUM/Problem1.2.lean | 2 +- .../Example/SCHAUM/Problem1.3.lean | 12 +- .../Example/SCHAUM/Problem1.4.lean | 2 +- .../Example/SCHAUM/Problem1.5.lean | 4 +- .../Example/SCHAUM/Problem1.6.lean | 4 +- .../Example/SCHAUM/Problem1.7.lean | 4 +- .../Example/SCHAUM/Problem1.8.lean | 4 +- .../Example/SCHAUM/Problem1.9.lean | 10 +- EuclideanGeometry/Example/ShanZun-Ex1a.lean | 2 +- EuclideanGeometry/Example/ShanZun-Ex1b.lean | 2 +- EuclideanGeometry/Example/ShanZun/Ex1.lean | 2 +- EuclideanGeometry/Example/ShanZun/Ex1a.lean | 2 +- EuclideanGeometry/Example/ShanZun/Ex1b.lean | 2 +- EuclideanGeometry/Example/ShanZun/Ex1c'.lean | 8 +- EuclideanGeometry/Example/ShanZun/Ex1c.lean | 2 +- EuclideanGeometry/Example/ShanZun/Ex1d.lean | 2 +- EuclideanGeometry/Example/ShanZun/Ex1e'.lean | 10 +- EuclideanGeometry/Example/ShanZun/Ex1e.lean | 2 +- EuclideanGeometry/Example/ShanZun/Ex1f'.lean | 124 +++++++++--------- EuclideanGeometry/Example/ShanZun/Ex1f.lean | 2 +- EuclideanGeometry/Example/ShanZun/Ex1h'.lean | 8 +- EuclideanGeometry/Example/ShanZun/Ex1h.lean | 2 +- .../Foundation/Axiom/Basic/Plane.lean | 4 +- .../Foundation/Axiom/Basic/Plane_trash.lean | 2 +- .../Foundation/Axiom/Circle/Basic.lean | 8 +- .../Foundation/Axiom/Circle/CCPosition.lean | 4 +- .../Foundation/Axiom/Circle/CirclePower.lean | 4 +- .../Axiom/Circle/InscribedAngle.lean | 2 +- .../Foundation/Axiom/Circle/LCPosition.lean | 4 +- .../Foundation/Axiom/Isometry/Rotation.lean | 2 +- .../Axiom/Isometry/Translation_ex.lean | 2 +- .../Foundation/Axiom/Linear/Class.lean | 10 +- .../Foundation/Axiom/Linear/Collinear.lean | 4 +- .../Axiom/Linear/Collinear_trash.lean | 2 +- .../Foundation/Axiom/Linear/Line.lean | 8 +- .../Foundation/Axiom/Linear/Line_trash.lean | 2 +- .../Foundation/Axiom/Linear/Parallel.lean | 7 +- .../Axiom/Linear/Parallel_trash.lean | 2 +- .../Axiom/Linear/Perpendicular.lean | 2 +- .../Axiom/Linear/Perpendicular_trash.lean | 2 +- .../Foundation/Axiom/Linear/Ratio.lean | 2 +- .../Foundation/Axiom/Linear/Ray.lean | 10 +- .../Foundation/Axiom/Linear/Ray_trash.lean | 2 +- .../Foundation/Axiom/Position/Angle.lean | 2 +- .../Foundation/Axiom/Position/Angle_ex.lean | 4 +- .../Foundation/Axiom/Position/Angle_ex2.lean | 2 +- .../Axiom/Position/Angle_ex_trash.lean | 2 +- .../Axiom/Position/Angle_trash.lean | 2 +- .../Axiom/Position/Convex_trash.lean | 2 +- .../Axiom/Position/Orientation_ex.lean | 2 +- .../Axiom/Position/Orientation_trash.lean | 2 +- .../Foundation/Axiom/Triangle/Basic.lean | 14 +- .../Foundation/Axiom/Triangle/Basic_ex.lean | 2 +- .../Axiom/Triangle/Basic_trash.lean | 2 +- .../Foundation/Axiom/Triangle/Congruence.lean | 2 +- .../Axiom/Triangle/Congruence_trash.lean | 2 +- .../Axiom/Triangle/IsocelesTriangle.lean | 2 +- .../Triangle/IsocelesTriangle_trash.lean | 2 +- .../Foundation/Axiom/Triangle/Similarity.lean | 2 +- .../ComputationTool/Ceva_converse.lean | 4 +- .../ComputationTool/Oarea_method.lean | 2 +- .../Construction/Polygon/GeneralPolygon.lean | 6 +- .../Construction/Polygon/Parallelogram.lean | 80 +++++------ .../Polygon/Parallelogram_old.lean | 78 +++++------ .../Polygon/Parallelogram_trash.lean | 2 +- .../Construction/Polygon/Quadrilateral.lean | 58 ++++---- .../Construction/Polygon/Rectangle.lean | 2 +- .../Construction/Polygon/Rhombus.lean | 2 +- .../Construction/Polygon/Square.lean | 2 +- .../Construction/Polygon/Trapezoid.lean | 2 +- .../Construction/Triangle/AngleBisector.lean | 2 +- .../Construction/Triangle/Centroid.lean | 2 +- .../Construction/Triangle/Orthocenter.lean | 2 +- .../Triangle/PerpendicularBisector.lean | 2 +- .../Tactic/Collinear/perm_collinear.lean | 2 +- .../Tactic/Congruence/Congruence.lean | 2 +- .../Foundation/Tactic/PointNe/Ptne.lean | 2 +- EuclideanGeometry/Unused/Class_old.lean | 24 ++-- EuclideanGeometry/Unused/Congruence.lean | 2 +- EuclideanGeometry/Unused/Line.lean | 8 +- EuclideanGeometry/Unused/Parallel.lean | 8 +- EuclideanGeometry/Unused/Parallelogram.lean | 18 +-- .../Unused/Tactic.Congruence.lean | 2 +- EuclideanGeometry/Unused/Unused.lean | 84 ++++++------ Plan_files/Memo/AngValue.lean | 2 +- Plan_files/Memo/LinearObjects.lean | 16 +-- 109 files changed, 456 insertions(+), 461 deletions(-) diff --git a/EuclideanGeometry/Check.lean b/EuclideanGeometry/Check.lean index 2550a369a..f4eac78fa 100644 --- a/EuclideanGeometry/Check.lean +++ b/EuclideanGeometry/Check.lean @@ -9,13 +9,13 @@ Here exhibits unfamiliar codes for learning. -/ section HEq -def T {A A' B : Type _} (e : A = A') (f : A → B) : A' → B := by +def T {A A' B : Type*} (e : A = A') (f : A → B) : A' → B := by rw [← e] exact f -theorem heq {A A' B : Type _} (e : A = A') (f : A → B) : HEq f (T e f) := by +theorem heq {A A' B : Type*} (e : A = A') (f : A → B) : HEq f (T e f) := by subst e rfl -theorem heq' {g : Type _ → Type _ } {A A' B : Type _} (e : g A = g A') (f : g A → B) : HEq f (T e f) := by +theorem heq' {g : Type* → Type* } {A A' B : Type*} (e : g A = g A') (f : g A → B) : HEq f (T e f) := by exact heq e f #check heq @@ -24,13 +24,13 @@ theorem heq' {g : Type _ → Type _ } {A A' B : Type _} (e : g A = g A') (f : g #check Eq.ndrec #check Eq.mpr -theorem heq_funext' {c₁ c₂ d : Type _} (e : c₁ = c₂) {f₁ : c₁ → d} {f₂ : c₂ → d} (h : ∀ (s : c₁) (t : c₂), (HEq s t) → f₁ s = f₂ t) : HEq f₁ f₂ := by +theorem heq_funext' {c₁ c₂ d : Type*} (e : c₁ = c₂) {f₁ : c₁ → d} {f₂ : c₂ → d} (h : ∀ (s : c₁) (t : c₂), (HEq s t) → f₁ s = f₂ t) : HEq f₁ f₂ := by exact Function.hfunext e (fun s t g => (heq_of_eq (h s t g))) -theorem heq_funext_prop {c₁ c₂ : Prop} {d : Type _} (e : c₁ = c₂) {f₁ : c₁ → d} {f₂ : c₂ → d} (h : ∀ (s : c₁) (t : c₂), f₁ s = f₂ t) : HEq f₁ f₂ := by +theorem heq_funext_prop {c₁ c₂ : Prop} {d : Type*} (e : c₁ = c₂) {f₁ : c₁ → d} {f₂ : c₂ → d} (h : ∀ (s : c₁) (t : c₂), f₁ s = f₂ t) : HEq f₁ f₂ := by exact Function.hfunext e (fun s t _ => (heq_of_eq (h s t))) -theorem heq_funext {c₁ c₂ d: Sort _} (e : c₁ = c₂) {f₁ : c₁ → d} {f₂ : c₂ → d} (h : ∀ (s : c₁) (t : c₂), f₁ s = f₂ t) : HEq f₁ f₂ := Function.hfunext e (fun _ _ _ => (heq_of_eq (h _ _))) +theorem heq_funext {c₁ c₂ d: Sort*} (e : c₁ = c₂) {f₁ : c₁ → d} {f₂ : c₂ → d} (h : ∀ (s : c₁) (t : c₂), f₁ s = f₂ t) : HEq f₁ f₂ := Function.hfunext e (fun _ _ _ => (heq_of_eq (h _ _))) end HEq @@ -49,7 +49,7 @@ namespace EuclidGeom /- check instance VAdd-/ section VAddCheck -variable (P : Type _) [EuclidGeom.EuclideanPlane P] (l : Ray P) +variable (P : Type*) [EuclidGeom.EuclideanPlane P] (l : Ray P) #check l.toDir.toVec #check @AddAction.toVAdd _ _ _ (@AddTorsor.toAddAction _ _ _ (@NormedAddTorsor.toAddTorsor _ P _ _ _)) @@ -64,7 +64,7 @@ end raymk /- check angle notation-/ section anglecheck -variable {P : Type _} [h : EuclideanPlane P] (O : P) (A : P) (B : P) +variable {P : Type*} [h : EuclideanPlane P] (O : P) (A : P) (B : P) #check ANG A O B variable (l : GDirSeg P) @@ -72,7 +72,7 @@ variable (l : GDirSeg P) end anglecheck -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] theorem test_is_on (A : P) (seg : Seg P) : (p LiesOn seg) = (Seg.IsOn p seg) := rfl diff --git a/EuclideanGeometry/Example/AOPS/Chap2.lean b/EuclideanGeometry/Example/AOPS/Chap2.lean index f9ae9e6ac..5adfb333c 100644 --- a/EuclideanGeometry/Example/AOPS/Chap2.lean +++ b/EuclideanGeometry/Example/AOPS/Chap2.lean @@ -6,7 +6,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace AOPS_Problem_2_14 diff --git a/EuclideanGeometry/Example/AOPS/Chap3.lean b/EuclideanGeometry/Example/AOPS/Chap3.lean index 9f909bedf..f3bf01d85 100644 --- a/EuclideanGeometry/Example/AOPS/Chap3.lean +++ b/EuclideanGeometry/Example/AOPS/Chap3.lean @@ -6,7 +6,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Exercise_3_4_4 diff --git a/EuclideanGeometry/Example/AOPS/Chap3a.lean b/EuclideanGeometry/Example/AOPS/Chap3a.lean index 96569e41e..51c158940 100644 --- a/EuclideanGeometry/Example/AOPS/Chap3a.lean +++ b/EuclideanGeometry/Example/AOPS/Chap3a.lean @@ -6,7 +6,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace AOPS_Problem_3_21 /- Let $\triangle ABC$ be a regular triangle, and let $P$, $Q$, $R$ be three points in the interior of $\triangle ABC$ such that diff --git a/EuclideanGeometry/Example/AOPS/Chap5.lean b/EuclideanGeometry/Example/AOPS/Chap5.lean index 759421704..68ddc24ce 100644 --- a/EuclideanGeometry/Example/AOPS/Chap5.lean +++ b/EuclideanGeometry/Example/AOPS/Chap5.lean @@ -4,7 +4,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace AOPS_Problem_5_7 /- Let $\triangle ABC$ be a triangle, and let $D$, $E$ be two points in the interior of $AB$ and $AC$ respectively such that $DE\parallel BC$ . $X$ lies inside $AB$ and $Y$ lies on the ray $XE$ so that $AY\parallel XC$ diff --git a/EuclideanGeometry/Example/AOPS/Chap5a.lean b/EuclideanGeometry/Example/AOPS/Chap5a.lean index 66c256dfd..fe7cb28b0 100644 --- a/EuclideanGeometry/Example/AOPS/Chap5a.lean +++ b/EuclideanGeometry/Example/AOPS/Chap5a.lean @@ -6,14 +6,14 @@ noncomputable section namespace EuclidGeom namespace AOPS -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace AOPS_Problem_5_7 /- Let $\triangle ABC$ be a triangle, and let $D$, $E$ be two points in the interior of $AB$ and $AC$ respectively such that $DE\parallel BC$ . $X$ lies inside $AB$ and $Y$ lies on the ray $XE$ so that $AY\parallel XC$ Prove that $\frac{EY}{EX}=\frac{AD}{DB}$ -/ -structure Setting (Plane : Type _) [EuclideanPlane Plane] where +structure Setting (Plane : Type*) [EuclideanPlane Plane] where -- Let $\triangle ABC$ be a nontrivial triangle A : Plane B : Plane @@ -55,7 +55,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where hY₂ : (LIN A Y Y_ne_A)∥(LIN X C X_ne_C.symm) --$\frac{EY}{EX}=\frac{AD}{DB}$ -theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.E e.Y).length/(SEG e.E e.X).length = (SEG e.A e.D).length/(SEG e.D e.B).length := sorry +theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.E e.Y).length/(SEG e.E e.X).length = (SEG e.A e.D).length/(SEG e.D e.B).length := sorry end AOPS_Problem_5_7 @@ -81,7 +81,7 @@ namespace AOPS_Exercise_5_3_2 Prove that $IJ\prar BC$-/ --It is simpler to use vectors but I think we should avoid vectors. -structure Setting (Plane : Type _) [EuclideanPlane Plane] where +structure Setting (Plane : Type*) [EuclideanPlane Plane] where -- Let $\triangle ABC$ be a nontrivial triangle A : Plane B : Plane @@ -122,7 +122,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where -- Claim : $J \ne I$ J_ne_I : J ≠ I := sorry --$IJ\parallel BC$ -theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : LIN e.I e.J e.J_ne_I ∥ LIN e.B e.C e.C_ne_B := sorry +theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : LIN e.I e.J e.J_ne_I ∥ LIN e.B e.C e.C_ne_B := sorry end AOPS_Exercise_5_3_2 end AOPS diff --git a/EuclideanGeometry/Example/ArefWernick/Chap1.lean b/EuclideanGeometry/Example/ArefWernick/Chap1.lean index 94f7d8396..cd20a7a9c 100644 --- a/EuclideanGeometry/Example/ArefWernick/Chap1.lean +++ b/EuclideanGeometry/Example/ArefWernick/Chap1.lean @@ -6,7 +6,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Aref_Wernick_Exercise_1_1 /- Two triangles are congruent if two sides and the enclosed median in one triangle are respectively equal to two sides and the enclosed median of the other. diff --git a/EuclideanGeometry/Example/ArefWernick/Chap1a.lean b/EuclideanGeometry/Example/ArefWernick/Chap1a.lean index 60b9b2763..aac66e7f1 100644 --- a/EuclideanGeometry/Example/ArefWernick/Chap1a.lean +++ b/EuclideanGeometry/Example/ArefWernick/Chap1a.lean @@ -8,7 +8,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Aref_Wernick_Exercise_1_1 /- Two triangles are congruent if two sides and the enclosed median in one triangle are respectively equal to two sides and the enclosed median of the other. diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_1.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_1.lean index d903e31a2..8eb419d05 100644 --- a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_1.lean +++ b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_1.lean @@ -12,7 +12,7 @@ $C, D$ lies in segment $BF$, $AB \parallel DE$, $AB = DF$, $BC = DE$. Prove that $∠ BAC = ∠ EFD$. -/ -structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where +structure Setting1 (Plane : Type*) [EuclideanPlane Plane] where -- $C, D$ lies in segment $BF$, they lies on the same line $l$. B : Plane C : Plane @@ -34,26 +34,26 @@ structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where -- $BC = DE$ h₂ : (SEG B C).length = (SEG D E).length attribute [instance] Setting1.B_ne_F -lemma hnd₁ {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: ¬ Collinear e.B e.A e.C := by +lemma hnd₁ {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: ¬ Collinear e.B e.A e.C := by apply Collinear.perm₂₁₃.mt exact e.ABC_nd -lemma hnd₂ {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: ¬ Collinear e.D e.F e.E := by +lemma hnd₂ {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: ¬ Collinear e.D e.F e.E := by apply Collinear.perm₃₁₂.mt exact e.EDF_nd -instance A_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.A e.B := ⟨(ne_of_not_collinear hnd₁).2.2⟩ -instance D_ne_E {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.D e.E := ⟨(ne_of_not_collinear hnd₂).2.1⟩ -instance A_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.A e.C := ⟨(ne_of_not_collinear hnd₁).1.symm⟩ -instance E_ne_F {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.E e.F := ⟨(ne_of_not_collinear hnd₂).1⟩ -instance D_ne_F {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.D e.F := ⟨(ne_of_not_collinear hnd₂).2.2.symm⟩ -instance B_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.B e.C := ⟨(ne_of_not_collinear hnd₁).2.1⟩ -instance D_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.D e.B := ⟨(ne_vertex_of_lies_int_seg_nd e.D_int).1⟩ +instance A_ne_B {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.A e.B := ⟨(ne_of_not_collinear hnd₁).2.2⟩ +instance D_ne_E {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.D e.E := ⟨(ne_of_not_collinear hnd₂).2.1⟩ +instance A_ne_C {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.A e.C := ⟨(ne_of_not_collinear hnd₁).1.symm⟩ +instance E_ne_F {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.E e.F := ⟨(ne_of_not_collinear hnd₂).1⟩ +instance D_ne_F {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.D e.F := ⟨(ne_of_not_collinear hnd₂).2.2.symm⟩ +instance B_ne_C {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.B e.C := ⟨(ne_of_not_collinear hnd₁).2.1⟩ +instance D_ne_B {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: PtNe e.D e.B := ⟨(ne_vertex_of_lies_int_seg_nd e.D_int).1⟩ -structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plane where +structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where -- $AB ∥ DE$ hpr : (SEG_nd B A) ∥ (SEG_nd D E) -- Prove that $∠ BAC = ∠ EFD$. -theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : ∠ e.B e.A e.C = ∠ e.E e.F e.D := by +theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : ∠ e.B e.A e.C = ∠ e.E e.F e.D := by /- $\angle ABC$ and $\angle EDF$ are corresponding angles,thus equal. In $\triangle BAC \congr_a \triangle DFE$. diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_2.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_2.lean index ed7feca46..c91a74ea7 100644 --- a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_2.lean +++ b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_2.lean @@ -11,7 +11,7 @@ namespace Problem_2 Given $AB = DC$, $DB = AC$, $B,C$ is on the same side of line $AD$. Prove that $∠B = ∠ C$. -/ -structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where +structure Setting1 (Plane : Type*) [EuclideanPlane Plane] where -- $AB = DC$, $DB = AC$. A : Plane B : Plane @@ -26,12 +26,12 @@ structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where -- $B,C$ is on the same side of line $AD$. B_side : IsOnRightSide B (SEG_nd A D D_ne_A) C_side : IsOnRightSide C (SEG_nd A D D_ne_A) -lemma a_ne_b {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: e.A ≠ e.B := (ne_of_not_collinear e.hnd₁).1 -lemma a_ne_c {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: e.A ≠ e.C := (ne_of_not_collinear e.hnd₂).2.2.symm -lemma b_ne_d {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: e.B ≠ e.D := (ne_of_not_collinear e.hnd₁).2.2 -lemma c_ne_d {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: e.C ≠ e.D :=(ne_of_not_collinear e.hnd₂).1.symm +lemma a_ne_b {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: e.A ≠ e.B := (ne_of_not_collinear e.hnd₁).1 +lemma a_ne_c {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: e.A ≠ e.C := (ne_of_not_collinear e.hnd₂).2.2.symm +lemma b_ne_d {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: e.B ≠ e.D := (ne_of_not_collinear e.hnd₁).2.2 +lemma c_ne_d {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: e.C ≠ e.D :=(ne_of_not_collinear e.hnd₂).1.symm -- Prove that $∠B = ∠ C$. -theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: ∠ e.A e.B e.D a_ne_b b_ne_d.symm = -∠ e.D e.C e.A c_ne_d.symm a_ne_c := by +theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: ∠ e.A e.B e.D a_ne_b b_ne_d.symm = -∠ e.D e.C e.A c_ne_d.symm a_ne_c := by -- Use SSS to prove that $\triangle DBA \congr \triangle ACD$ or $\triangle DBA \congr_a \triangle ACD$. have h : (TRI_nd e.D e.B e.A e.hnd₁) ≅ₐ (TRI_nd e.A e.C e.D e.hnd₂) := by apply TriangleND.acongr_of_SSS_of_ne_orientation diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_3.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_3.lean index f0d4570b9..586948fe6 100644 --- a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_3.lean +++ b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_3.lean @@ -12,7 +12,7 @@ namespace Problem_3 In (convex) quadrilateral $A B D C$,$AB = AC$, $BD = CD$. Prove that $\angle A B D = -\angle A C D$ -/ -structure Setting (Plane : Type _) [EuclideanPlane Plane] where +structure Setting (Plane : Type*) [EuclideanPlane Plane] where --In (convex) quadrilateral $A B D C$,$AB = AC$, $BD = CD$. A : Plane B : Plane @@ -27,7 +27,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where --$A \ne C$ and $D \ne B$ for $\angle A C D$ A_ne_C : A ≠ C := (Quadrilateral_cvx.nd₁₄ (QDR_cvx A B D C cvx_ABDC)).symm D_ne_C : D ≠ C := (Quadrilateral_cvx.nd₃₄ (QDR_cvx A B D C cvx_ABDC)).symm -theorem Result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : ∠ e.A e.B e.D (e.A_ne_B) (e.D_ne_B) = - ∠ e.A e.C e.D (e.A_ne_C) (e.D_ne_C):= by +theorem Result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : ∠ e.A e.B e.D (e.A_ne_B) (e.D_ne_B) = - ∠ e.A e.C e.D (e.A_ne_C) (e.D_ne_C):= by /- Because $AB = AC$ ,we have $\angle A B C = -\angle A C B$. Because $DB = DC$ ,we have $\angle D B C = -\angle D C B$ diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_4.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_4.lean index 702112665..cfaf1bc01 100644 --- a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_4.lean +++ b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_4.lean @@ -12,7 +12,7 @@ $A,D$ are on the opposite side of line $BC$,which satisfies $BD \parallel CA$, $ $E$ liesint $BC$ and $BE = AC$ Prove that $\angle B D E = -\angle C B A $. -/ -structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where +structure Setting1 (Plane : Type*) [EuclideanPlane Plane] where A : Plane B : Plane C : Plane @@ -22,11 +22,11 @@ structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where hnd₂ : ¬ Collinear B C D --$A,D$ are on the opposite side of line $BC$,which satisfies $BD \para CA$(lemma needed), $BD = BC$ BD_eq_BC : (SEG B D).length = (SEG B C).length -instance B_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.B e.C := ⟨(ne_of_not_collinear e.hnd₁).2.2.symm⟩ -instance D_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.D e.B := ⟨(ne_of_not_collinear e.hnd₂).2.1.symm⟩ -instance A_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.C := ⟨(ne_of_not_collinear e.hnd₁).1⟩ +instance B_ne_C {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.B e.C := ⟨(ne_of_not_collinear e.hnd₁).2.2.symm⟩ +instance D_ne_B {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.D e.B := ⟨(ne_of_not_collinear e.hnd₂).2.1.symm⟩ +instance A_ne_C {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : PtNe e.A e.C := ⟨(ne_of_not_collinear e.hnd₁).1⟩ -structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plane where +structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where --$BD \para CA$ BD_para_CA : (SEG_nd B D) ∥ (SEG_nd C A) --$A,D$ are on the opposite side of line $BC$ @@ -36,12 +36,12 @@ structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plan E : Plane E_int : E LiesInt (SEG_nd B C) E_position : (SEG B E).length = (SEG A C).length -lemma hnd₃ {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane}: ¬ Collinear e.B e.E e.D := by sorry -instance E_ne_D {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.E e.D := ⟨(ne_of_not_collinear hnd₃).1.symm⟩ -instance A_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear e.hnd₁).2.1.symm⟩ -instance B_ne_E {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.B e.E := ⟨(ne_of_not_collinear hnd₃).2.2.symm⟩ +lemma hnd₃ {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane}: ¬ Collinear e.B e.E e.D := by sorry +instance E_ne_D {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.E e.D := ⟨(ne_of_not_collinear hnd₃).1.symm⟩ +instance A_ne_B {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.A e.B := ⟨(ne_of_not_collinear e.hnd₁).2.1.symm⟩ +instance B_ne_E {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.B e.E := ⟨(ne_of_not_collinear hnd₃).2.2.symm⟩ --Prove that $\angle B D E = -\angle C B A $. -theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : ∠ e.B e.D e.E = -∠ e.C e.B e.A := by +theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : ∠ e.B e.D e.E = -∠ e.C e.B e.A := by /- Because $BD \parallel CA$,($A,D$ are on the opposite side of line $BC$), $\angle D B E $ and $\angle A C B$ are Alternate Interior Angle, thus equal. diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_6.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_6.lean index 9dccc8911..65f9615c3 100644 --- a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_6.lean +++ b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_6.lean @@ -4,7 +4,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Wuwowuji_Problem_1_6 /- diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_7.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_7.lean index 79b270528..8b4496c6f 100644 --- a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_7.lean +++ b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_7.lean @@ -4,7 +4,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Wuwowuji_Problem_1_7 /- diff --git a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_8.lean b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_8.lean index 71f28a7da..f21ecb84f 100644 --- a/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_8.lean +++ b/EuclideanGeometry/Example/Congruence_Exercise_ygr/Problem_8.lean @@ -4,7 +4,7 @@ noncomputable section namespace EuclidGeom -variable {Plane : Type _} [EuclideanPlane Plane] +variable {Plane : Type*} [EuclideanPlane Plane] namespace Wuwowuji_Problem_1_8 /- diff --git a/EuclideanGeometry/Example/ExerciseXT8.lean b/EuclideanGeometry/Example/ExerciseXT8.lean index bf515faa0..42c5b5e9d 100644 --- a/EuclideanGeometry/Example/ExerciseXT8.lean +++ b/EuclideanGeometry/Example/ExerciseXT8.lean @@ -5,7 +5,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.1.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.1.lean index 0c6cafd32..f535b322e 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.1.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.1.lean @@ -4,7 +4,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Schaum @@ -26,7 +26,7 @@ variable {E_ray_position : (SEG A E).length = (SEG A D).length} --Let $M$ be the midpoint of $BC$. variable {M : P} {median_M_position : M = (SEG B C).midpoint} -/ -structure Setting (Plane : Type _) [EuclideanPlane Plane] where +structure Setting (Plane : Type*) [EuclideanPlane Plane] where --Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$. A : Plane B : Plane @@ -46,7 +46,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where midpoint_M : M = (SEG B C).midpoint --Prove that $DM = EM$. -theorem Result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.D e.M).length = (SEG e.E e.M).length := by +theorem Result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.D e.M).length = (SEG e.E e.M).length := by /-In the isoceles triangle $ABC$, we have $AB = AC$. Meanwhile $AE = AD$ We have $BD = AB - AD = AC - AE = CE$. diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.10.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.10.lean index bec0d6141..332421670 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.10.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.10.lean @@ -4,7 +4,7 @@ noncomputable section namespace EuclidGeom -variable {Plane : Type _} [EuclideanPlane Plane] +variable {Plane : Type*} [EuclideanPlane Plane] namespace SCHAUM_Problem_1_10 /- diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.11.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.11.lean index 935d4c0f6..39f7e787c 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.11.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.11.lean @@ -4,14 +4,14 @@ noncomputable section namespace EuclidGeom -variable {Plane : Type _} [EuclideanPlane Plane] +variable {Plane : Type*} [EuclideanPlane Plane] namespace SCHAUM_Problem_1_11 /- If $ABCD$ is a parallelogram and $EFCD$ is a parallelogram, then $ABFE$ is a parallelogram. -/ -structure Setting (Plane : Type _) [EuclideanPlane Plane] where +structure Setting (Plane : Type*) [EuclideanPlane Plane] where -- $ABCD$ is a parallelogram. A : Plane B : Plane @@ -23,7 +23,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where F : Plane EFCD_IsPRG : (QDR E F C D) IsPRG -- Prove that $ABFE$ is a parallelogram. -theorem result (Plane : Type _) [EuclideanPlane Plane] (e : Setting Plane) : (QDR e.A e.B e.F e.E) IsPRG := by +theorem result (Plane : Type*) [EuclideanPlane Plane] (e : Setting Plane) : (QDR e.A e.B e.F e.E) IsPRG := by /- Because $ABCD$ is a parallelogram, $\overarrow{AB} = \overarrow{DC}$. Because $EFCD$ is a parallelogram, $\overarrow{EF} = \overarrow{DC}$. diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.12.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.12.lean index b5bd0fee3..089039358 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.12.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.12.lean @@ -4,7 +4,7 @@ noncomputable section namespace EuclidGeom -variable {Plane : Type _} [EuclideanPlane Plane] +variable {Plane : Type*} [EuclideanPlane Plane] namespace SCHAUM_Problem_1_12 /- @@ -15,7 +15,7 @@ Prove that $ABCD$ is a parallelogram. -/ -structure Setting (Plane : Type _) [EuclideanPlane Plane] where +structure Setting (Plane : Type*) [EuclideanPlane Plane] where -- Let $ABCD$ be a convex quadrilateral. A : Plane B : Plane @@ -33,7 +33,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where BC_eq_DA : (SEG B C).length = (SEG D A).length -- Prove that $ABCD$ is a parallelogram. -theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (QDR e.A e.B e.C e.D) IsPRG_nd := by +theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : (QDR e.A e.B e.C e.D) IsPRG_nd := by sorry diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.13.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.13.lean index 2c41adc0f..d82919252 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.13.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.13.lean @@ -4,7 +4,7 @@ noncomputable section namespace EuclidGeom -variable {Plane : Type _} [EuclideanPlane Plane] +variable {Plane : Type*} [EuclideanPlane Plane] namespace SCHAUM_Problem_1_13 /- diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.14.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.14.lean index baa4828cf..7f4717656 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.14.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.14.lean @@ -6,7 +6,7 @@ noncomputable section namespace EuclidGeom -variable {Plane : Type _} [EuclideanPlane Plane] +variable {Plane : Type*} [EuclideanPlane Plane] namespace SCHAUM_Problem_1_14 /- @@ -15,7 +15,7 @@ Let $ABCD$ be a parallelogram. Let $P$ and $Q$ be points on the segments $AB$ an Prove that $PM = QN$ and $PM \parallel QN$. -/ -structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where +structure Setting1 (Plane : Type*) [EuclideanPlane Plane] where -- Let $ABCD$ be a parallelogram. A : Plane B : Plane @@ -37,23 +37,23 @@ structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where perp_foot_N : N = perp_foot Q (LIN B D D_ne_B) -- Because $P$ is not on line $BD$, $M$, the foot of the perpendicular from $P$ to the diagonal $BD$ doesn't equal to $P$. -lemma not_P_lieson_BD {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : ¬ e.P LiesOn (LIN e.B e.D e.D_ne_B) := sorry -lemma not_Q_lieson_BD {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : ¬ e.Q LiesOn (LIN e.B e.D e.D_ne_B) := sorry -lemma M_ne_P {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : e.M ≠ e.P := by +lemma not_P_lieson_BD {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : ¬ e.P LiesOn (LIN e.B e.D e.D_ne_B) := sorry +lemma not_Q_lieson_BD {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : ¬ e.Q LiesOn (LIN e.B e.D e.D_ne_B) := sorry +lemma M_ne_P {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : e.M ≠ e.P := by simp only [e.perp_foot_M] exact (perp_foot_eq_self_iff_lies_on e.P (LIN e.B e.D e.D_ne_B)).not.mpr (not_P_lieson_BD) -lemma N_ne_Q {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : e.N ≠ e.Q := by +lemma N_ne_Q {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : e.N ≠ e.Q := by simp only [e.perp_foot_N] exact (perp_foot_eq_self_iff_lies_on e.Q (LIN e.B e.D e.D_ne_B)).not.mpr (not_Q_lieson_BD) -structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends (Setting1 Plane) where +structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends (Setting1 Plane) where not_P_lieson_BD : ¬ P LiesOn (LIN B D D_ne_B) := not_P_lieson_BD not_Q_lieson_BD : ¬ Q LiesOn (LIN B D D_ne_B) := not_Q_lieson_BD M_ne_P : M ≠ P := M_ne_P N_ne_Q : N ≠ Q := N_ne_Q -- Prove that $PM = QN$. -theorem result1 {Plane : Type _} [EuclideanPlane Plane] (e : Setting2 Plane) : (SEG e.P e.M).length = (SEG e.Q e.N).length := by +theorem result1 {Plane : Type*} [EuclideanPlane Plane] (e : Setting2 Plane) : (SEG e.P e.M).length = (SEG e.Q e.N).length := by /- Because quadrilateral $ABCD$ is a parallelogram, $AB \parallel CD$, thus the alternate interior angle $\angle ABD = \angle CDB$, therefore $\angle PBM = \angle ABD = \angle CDB = \angle QDN$. Also, $\angle BMP = \pm\frac{\pi}{2}$, $\angle DNQ = \pm\frac{\pi}{2}$ because $M$ and $N$ are the foot of perpendicular from $P$, $Q$ to $BD$, respectively. @@ -77,7 +77,7 @@ theorem result1 {Plane : Type _} [EuclideanPlane Plane] (e : Setting2 Plane) : ( exact MBP_congr_NCQ.edge₂ -- Prove that $PM \parallel QN$. -theorem result2 {Plane : Type _} [EuclideanPlane Plane] (e : Setting2 Plane) : (LIN e.P e.M e.M_ne_P) ∥ (LIN e.Q e.N e.N_ne_Q) := by +theorem result2 {Plane : Type*} [EuclideanPlane Plane] (e : Setting2 Plane) : (LIN e.P e.M e.M_ne_P) ∥ (LIN e.Q e.N e.N_ne_Q) := by -- We have $PM \perp BD$ because $M$ is the perpendicular foot from $P$ to $BD$. have PM_perp_BD : LIN e.P e.M e.M_ne_P ⟂ LIN e.B e.D e.D_ne_B := by simp only [e.perp_foot_M] diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.2'.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.2'.lean index d7dfb41ac..62a7b09b1 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.2'.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.2'.lean @@ -14,7 +14,7 @@ Let $Q$ be the foot of perpendicular from $E$ to $BC$. Prove that $DP = EQ$. -/ -structure Setting (Plane : Type _) [EuclideanPlane Plane] where +structure Setting (Plane : Type*) [EuclideanPlane Plane] where -- Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$. A : Plane B : Plane @@ -41,7 +41,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where hQ : Q = perp_foot E (LIN B C B_ne_C.symm) /- # Another Style of Setting-/ -structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where +structure Setting1 (Plane : Type*) [EuclideanPlane Plane] where -- Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$. A : Plane B : Plane @@ -58,11 +58,11 @@ structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where AE_eq_AD : (SEG A E).length = (SEG A D).length -- Claim: $B \ne C$. -lemma B_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane}: e.B ≠ e.C := by +lemma B_ne_C {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane}: e.B ≠ e.C := by -- This is because vertices $B, C$ of a nondegenerate triangle are distinct. exact (ne_of_not_collinear e.not_collinear_ABC).1.symm -structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plane where +structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where B_ne_C : B ≠ C := B_ne_C -- Let $P$ be the foot of perpendicular from $D$ to $BC$. P : Plane @@ -72,7 +72,7 @@ structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plan hQ : Q = perp_foot E (LIN B C B_ne_C.symm) -- Prove that $DP = EQ$. -theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.D e.P).length = (SEG e.E e.Q).length := by +theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.D e.P).length = (SEG e.E e.Q).length := by /- In the isoceles triangle $ABC$, we have $AB = AC$. Thus we have $BD = AB - AD = AC - AE = CE$. diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.2.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.2.lean index e5d1e2847..89f4c2eb9 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.2.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.2.lean @@ -4,7 +4,7 @@ noncomputable section namespace EuclidGeom -variable {Plane : Type _} [EuclideanPlane Plane] +variable {Plane : Type*} [EuclideanPlane Plane] namespace Problem1_2_ /-Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$.Let $D$ be a point on $AB$. diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.3.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.3.lean index 9c6b6b83b..8aedf2099 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.3.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.3.lean @@ -30,7 +30,7 @@ lemma b_ne_c : B ≠ C := (ne_of_not_collinear hnd).1.symm lemma c_ne_b : C ≠ B := (ne_of_not_collinear hnd).1 --Prove that $∠ D A B = ∠ C A E$. -/ -structure Setting (Plane : Type _) [EuclideanPlane Plane] where +structure Setting (Plane : Type*) [EuclideanPlane Plane] where --Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$. A : Plane B : Plane @@ -53,13 +53,13 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where C_ne_B : C ≠ B := (ne_of_not_collinear not_collinear_ABC).1 --Points not equal for angles ∠ A B D and ∠ A C E namespace Setting -lemma D_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : e.D ≠ e.A := sorry -lemma E_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : e.E ≠ e.A := sorry -lemma D_ne_B {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : e.D ≠ e.B := e.D_Int_BC.2.1 -lemma E_ne_C {Plane : Type _} [EuclideanPlane Plane] {e : Setting Plane} : e.E ≠ e.C := e.E_Int_BC.2.2 +lemma D_ne_A {Plane : Type*} [EuclideanPlane Plane] {e : Setting Plane} : e.D ≠ e.A := sorry +lemma E_ne_A {Plane : Type*} [EuclideanPlane Plane] {e : Setting Plane} : e.E ≠ e.A := sorry +lemma D_ne_B {Plane : Type*} [EuclideanPlane Plane] {e : Setting Plane} : e.D ≠ e.B := e.D_Int_BC.2.1 +lemma E_ne_C {Plane : Type*} [EuclideanPlane Plane] {e : Setting Plane} : e.E ≠ e.C := e.E_Int_BC.2.2 end Setting --Prove that $∠ D A B = ∠ C A E$. -theorem Result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : ∠ e.D e.A e.B (e.D_ne_A) (e.B_ne_A)= ∠ e.C e.A e.E (e.C_ne_A) (e.E_ne_A) := by +theorem Result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : ∠ e.D e.A e.B (e.D_ne_A) (e.B_ne_A)= ∠ e.C e.A e.E (e.C_ne_A) (e.E_ne_A) := by /-In the isoceles triangle $ABC$ we have $AB = AC$. Beacause $BD = CE$ we have $DB = EC$. In the isoceles triangle $A B C$, we have $\angle A B C = -\angle A C B$. diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.4.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.4.lean index 36557861a..8aa92dfa1 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.4.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.4.lean @@ -4,7 +4,7 @@ noncomputable section namespace EuclidGeom -variable {Plane : Type _} [EuclideanPlane Plane] +variable {Plane : Type*} [EuclideanPlane Plane] namespace Problem1_4_ /-Let $B$ $D$ be points on segment $AF$, such that $AD = BF$. Let $C$ be a point. diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.5.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.5.lean index f4a16f22f..a06987c58 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.5.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.5.lean @@ -18,7 +18,7 @@ such that $AP = CR$ and $AS = CQ$. Prove that $PQRS$ is a parallelogram. -/ -structure Setting (Plane : Type _) [EuclideanPlane Plane] where +structure Setting (Plane : Type*) [EuclideanPlane Plane] where --Let $ABCD$ be a parallelogram A : Plane B : Plane @@ -42,7 +42,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where --such that $AS = CQ$ AS_eq_CQ : (SEG A S).length = (SEG C Q).length --Prove that $PQRS$ is a parallelogram -theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (QDR e.P e.Q e.R e.S).IsParallelogram_nd := by +theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : (QDR e.P e.Q e.R e.S).IsParallelogram_nd := by /- In parallelogram $ABCD$, we have $AB, DC$ are of the same direction. Since $P$ lies on $AB$, we have $AP, AB$ are of the same direction. diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.6.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.6.lean index ae808e8c1..4960c43ba 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.6.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.6.lean @@ -13,7 +13,7 @@ Let $ABCD$ be a parallelogram, and let $P$, $Q$ be points on the segments $AB$ a Prove that $PB = QD$. -/ -structure Setting (Plane : Type _) [EuclideanPlane Plane] where +structure Setting (Plane : Type*) [EuclideanPlane Plane] where --Let $ABCD$ be a parallelogram A : Plane B : Plane @@ -29,7 +29,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where --such that $AP = CQ$ AP_eq_CQ : (SEG A P).length = (SEG C Q).length --Prove that $PB = QD$ -theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.P e.B).length = (SEG e.Q e.D).length := by +theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.P e.B).length = (SEG e.Q e.D).length := by /- In the parallelogram $ABCD$ we have $AB = CD$. Therefore, $PB = AB - AP = CD - CQ = QD$. diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.7.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.7.lean index cf69a53ac..22402e406 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.7.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.7.lean @@ -18,7 +18,7 @@ Let $D$ and $E$ be points on the segment $BC$ such that $BD = CE$. Prove that the height of $D$ to $AB$ is the same as the height of $E$ to $AC$. -/ -structure Setting (Plane : Type _) [EuclideanPlane Plane] where +structure Setting (Plane : Type*) [EuclideanPlane Plane] where --Let $\triangle ABC$ be an isoceles triangle in which $AB = AC$ A : Plane B : Plane @@ -49,7 +49,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where he : Y = perp_foot E (LIN A C C_ne_A) --Prove that $DX = EY$. -theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.D e.X).length = (SEG e.E e.Y).length := by +theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.D e.X).length = (SEG e.E e.Y).length := by /- In isoceles triangle $ABC$, we have $\angle ABC$ and $\angle ACB$ are acute. From $D$ lies on $BC$ and $\angle ABC$ is acute, we know that $X$ lies on ray $BA$, so $\angle XBD$ is the same as $\angle ABC$. diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.8.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.8.lean index 9d238f9fb..1a6913e3b 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.8.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.8.lean @@ -16,7 +16,7 @@ such that $CD = AE$. Prove that $AD = BE$ -/ -structure Setting (Plane : Type _) [EuclideanPlane Plane] where +structure Setting (Plane : Type*) [EuclideanPlane Plane] where --Let $\triangle ABC$ be a regular triangle. A : Plane B : Plane @@ -44,7 +44,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where --such that $CD = AE$ CD_eq_AE : ((SEG C D).length = (SEG A E).length) --Prove that $AD = BE$ -theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : ((SEG e.A e.D).length = (SEG e.B e.E).length):= by +theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : ((SEG e.A e.D).length = (SEG e.B e.E).length):= by /- In regular triangle $ABC$, $\angle ABC = \angle BCA$. Since $D$ lies on the extension of $BC$, we know that $\angle ABD$ is the same as $\angle ABC$. diff --git a/EuclideanGeometry/Example/SCHAUM/Problem1.9.lean b/EuclideanGeometry/Example/SCHAUM/Problem1.9.lean index 94021f158..5595e27c9 100644 --- a/EuclideanGeometry/Example/SCHAUM/Problem1.9.lean +++ b/EuclideanGeometry/Example/SCHAUM/Problem1.9.lean @@ -17,7 +17,7 @@ Let $\triangle ABC$ be an isoceles triangle in which $AB = AC$. Let $E$ be a poi Prove that $\angle EAX = \angle XAC$. -/ -structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where +structure Setting1 (Plane : Type*) [EuclideanPlane Plane] where -- Let $\triangle ABC$ be an isoceles triangle in which $AB = AC$. A : Plane B : Plane @@ -52,7 +52,7 @@ structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where X : Plane X_int_la : X LiesInt l_a -- Claim $E \ne A$ -lemma E_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : e.E ≠ e.A := by +lemma E_ne_A {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : e.E ≠ e.A := by -- This is because $E$ lies on the extension of $BA$ and $A$ is the source of that ray. -- We have $E$ is not equal to the source of the extension of $BA$, since $E$ lies on the extension of $BA$. have h1 : e.E ≠ e.BA_ext.source := e.E_int_ext.2 @@ -60,19 +60,19 @@ lemma E_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : e.E have h2 : e.A = e.BA_ext.source := by simp only [e.hlba]; rfl simp only [h2]; exact h1 -- Claim : $X \ne A$ -lemma X_ne_A {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : e.X ≠ e.A := by +lemma X_ne_A {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : e.X ≠ e.A := by -- This is because $X$ lies on $l_a$ and $A$ is the source of that ray. -- We have $X$ is not equal to the source $l_a$, since $X$ lies on the extension of $BA$. have h1 : e.X ≠ e.l_a.source := e.X_int_la.2 -- We have $A$ is the source of $l_a$ by definition. have h2 : e.A = e.l_a.source := by simp only [e.hla] simp only [h2]; exact h1 -structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plane where +structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where E_ne_A : E ≠ A := E_ne_A X_ne_A : X ≠ A := X_ne_A -- Prove that $\angle EAX = \angle XAC$ -theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting2 Plane) : ∠ e.E e.A e.X e.E_ne_A e.X_ne_A = ∠ e.X e.A e.C e.X_ne_A e.C_ne_A := by +theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting2 Plane) : ∠ e.E e.A e.X e.E_ne_A e.X_ne_A = ∠ e.X e.A e.C e.X_ne_A e.C_ne_A := by /- As $AX$ has the same direction as $BC$ and that $E$ is on the extension of $BA$, we know that $\angle EAX = \angle ABC$. In isoceles triangle $ABC$, $\angle ABC = - \angle ACB$. diff --git a/EuclideanGeometry/Example/ShanZun-Ex1a.lean b/EuclideanGeometry/Example/ShanZun-Ex1a.lean index 892148a39..cca59132e 100644 --- a/EuclideanGeometry/Example/ShanZun-Ex1a.lean +++ b/EuclideanGeometry/Example/ShanZun-Ex1a.lean @@ -6,7 +6,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Shan_Problem_1_3 /- Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$. Let $D$ be a point in the extension of $AB$ such that $BD = AB$. Let $E$ be the midpoint of $AB$. diff --git a/EuclideanGeometry/Example/ShanZun-Ex1b.lean b/EuclideanGeometry/Example/ShanZun-Ex1b.lean index 2ced19d98..0c68efb0f 100644 --- a/EuclideanGeometry/Example/ShanZun-Ex1b.lean +++ b/EuclideanGeometry/Example/ShanZun-Ex1b.lean @@ -6,7 +6,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Shan_Problem_1_5 /- In $\triangle ABC$, let $AD$ be the median. Let $E$ be a point on $AD$ such that $BE = AC$. The line $BE$ intersects $AC$ at $F$. diff --git a/EuclideanGeometry/Example/ShanZun/Ex1.lean b/EuclideanGeometry/Example/ShanZun/Ex1.lean index 1accc03ed..d51004779 100644 --- a/EuclideanGeometry/Example/ShanZun/Ex1.lean +++ b/EuclideanGeometry/Example/ShanZun/Ex1.lean @@ -6,7 +6,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Shan_Problem_1_1 /- In $\triangle ABC$, let $AD$ be the height and $AE$ be the angle bisector of $\triangle ABC$. diff --git a/EuclideanGeometry/Example/ShanZun/Ex1a.lean b/EuclideanGeometry/Example/ShanZun/Ex1a.lean index 18510ab58..20216c431 100644 --- a/EuclideanGeometry/Example/ShanZun/Ex1a.lean +++ b/EuclideanGeometry/Example/ShanZun/Ex1a.lean @@ -6,7 +6,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Shan_Problem_1_3 /- Let $\triangle ABC$ be an isosceles triangle in which $AB = AC$. diff --git a/EuclideanGeometry/Example/ShanZun/Ex1b.lean b/EuclideanGeometry/Example/ShanZun/Ex1b.lean index f6e7f0326..cb6600227 100644 --- a/EuclideanGeometry/Example/ShanZun/Ex1b.lean +++ b/EuclideanGeometry/Example/ShanZun/Ex1b.lean @@ -6,7 +6,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Shan_Problem_1_5 /- In $\triangle ABC$, let $AD$ be the median. Let $E$ be a point on $AD$ such that $BE = AC$. The line $BE$ intersects $AC$ at $F$. diff --git a/EuclideanGeometry/Example/ShanZun/Ex1c'.lean b/EuclideanGeometry/Example/ShanZun/Ex1c'.lean index a972254f3..39371ac41 100644 --- a/EuclideanGeometry/Example/ShanZun/Ex1c'.lean +++ b/EuclideanGeometry/Example/ShanZun/Ex1c'.lean @@ -13,7 +13,7 @@ namespace Shan_Problem_1_7 Prove that $CD = AB / 2$. -/ -structure Setting (Plane : Type _) [EuclideanPlane Plane] where +structure Setting (Plane : Type*) [EuclideanPlane Plane] where -- Let $\triangle ABC$ be a nontrivial triangle in which $\angle ACB= \pi/2$. A : Plane B : Plane @@ -35,7 +35,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where D : Plane hD : D = (SEG A B).midpoint -theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.C e.D).length = (SEG e.A e.B).length/2 := by +theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : (SEG e.C e.D).length = (SEG e.A e.B).length/2 := by have D_ne_A: e.D ≠ e.A := by rw[e.hD] apply (SegND.midpt_lies_int (seg_nd := SEG_nd e.A e.B (e.B_ne_A))).2.1 @@ -179,7 +179,7 @@ namespace Shan_Problem_1_8 Prove that $FG \perp DE$. -/ -structure Setting (Plane : Type _) [EuclideanPlane Plane] where +structure Setting (Plane : Type*) [EuclideanPlane Plane] where -- Let $\triangle ABC$ be a nontrivial triangle in which $\angle ACB= \pi/2$. A : Plane B : Plane @@ -212,7 +212,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where E_ne_D : E ≠ D := sorry -- Theorem : $FG \perp DE$ -theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) :(SEG_nd e.F e.G e.G_ne_F) ⟂ (SEG_nd e.D e.E e.E_ne_D) := sorry +theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) :(SEG_nd e.F e.G e.G_ne_F) ⟂ (SEG_nd e.D e.E e.E_ne_D) := sorry end Shan_Problem_1_8 diff --git a/EuclideanGeometry/Example/ShanZun/Ex1c.lean b/EuclideanGeometry/Example/ShanZun/Ex1c.lean index 5676b29a2..c27d2f6d0 100644 --- a/EuclideanGeometry/Example/ShanZun/Ex1c.lean +++ b/EuclideanGeometry/Example/ShanZun/Ex1c.lean @@ -6,7 +6,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Shan_Problem_1_7 /- In $\triangle ABC$, $\angle ACB = \pi /2$. Let $D$ be the midpoint of $AB$. diff --git a/EuclideanGeometry/Example/ShanZun/Ex1d.lean b/EuclideanGeometry/Example/ShanZun/Ex1d.lean index 3785e5ee3..111f1600d 100644 --- a/EuclideanGeometry/Example/ShanZun/Ex1d.lean +++ b/EuclideanGeometry/Example/ShanZun/Ex1d.lean @@ -6,7 +6,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Shan_Problem_1_9 /- In $\triangle ABC$, assume that $\angle CBA = 2\cdot \angle ACB$. Let $AD$ be the height and $AE$ the median. diff --git a/EuclideanGeometry/Example/ShanZun/Ex1e'.lean b/EuclideanGeometry/Example/ShanZun/Ex1e'.lean index 3524919c0..488207e28 100644 --- a/EuclideanGeometry/Example/ShanZun/Ex1e'.lean +++ b/EuclideanGeometry/Example/ShanZun/Ex1e'.lean @@ -10,7 +10,7 @@ namespace Shan_Problem_2_13 the perpendicular line passing through $D$ of the bisector of $\angle BAC$ intersects $AB,AC$ at $E,F$ respectively. Prove that $BE=CF=\frac{1}{2}|AB-AC|$. -/ -structure Setting (Plane : Type _) [EuclideanPlane Plane] where +structure Setting (Plane : Type*) [EuclideanPlane Plane] where -- Let $\triangle ABC$ be a nontrivial triangle A : Plane B : Plane @@ -43,7 +43,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where -- Theorem : $BE=CF=\frac{1}{2}|AB-AC|$ -theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) :(SEG e.B e.E).length=|((SEG e.A e.B).length-(SEG e.A e.C).length)|/2 ∧ (SEG e.C e.F).length = |((SEG e.A e.B).length-(SEG e.A e.C).length)|/2 := sorry +theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) :(SEG e.B e.E).length=|((SEG e.A e.B).length-(SEG e.A e.C).length)|/2 ∧ (SEG e.C e.F).length = |((SEG e.A e.B).length-(SEG e.A e.C).length)|/2 := sorry end Shan_Problem_2_13 @@ -52,7 +52,7 @@ namespace Shan_Problem_2_18 $CE$ be the bisector of $\angle ACB$ and $CF$ be the median. Prove that $E$ liesInt $DF$ -/ -structure Setting (Plane : Type _) [EuclideanPlane Plane] where +structure Setting (Plane : Type*) [EuclideanPlane Plane] where -- Let $\triangle ABC$ be a nontrivial triangle A : Plane B : Plane @@ -87,11 +87,11 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where --Claim : $F\ne C$ F_ne_C : F ≠ C := sorry -theorem result1 {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : e.E LiesInt (SEG e.D e.F) := sorry +theorem result1 {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : e.E LiesInt (SEG e.D e.F) := sorry -- Theorem : $CE$ is the bisector of $\angle FCD$ -theorem result2 {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : ∠ e.F e.C e.E e.F_ne_C e.E_ne_C = ∠ e.E e.C e.D e.E_ne_C e.D_ne_C := sorry +theorem result2 {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : ∠ e.F e.C e.E e.F_ne_C e.E_ne_C = ∠ e.E e.C e.D e.E_ne_C e.D_ne_C := sorry end Shan_Problem_2_18 diff --git a/EuclideanGeometry/Example/ShanZun/Ex1e.lean b/EuclideanGeometry/Example/ShanZun/Ex1e.lean index d3af9003c..0cb852358 100644 --- a/EuclideanGeometry/Example/ShanZun/Ex1e.lean +++ b/EuclideanGeometry/Example/ShanZun/Ex1e.lean @@ -4,7 +4,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Shan_Problem_2_13 /- In $\triangle ABC$. Let $D$ be the midpoint of segment $BC$, diff --git a/EuclideanGeometry/Example/ShanZun/Ex1f'.lean b/EuclideanGeometry/Example/ShanZun/Ex1f'.lean index f5a9e9be5..519fc7fee 100644 --- a/EuclideanGeometry/Example/ShanZun/Ex1f'.lean +++ b/EuclideanGeometry/Example/ShanZun/Ex1f'.lean @@ -5,7 +5,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Shan_Problem_2_11 /- Let $\triangle ABC$ be a regular triangle, @@ -13,7 +13,7 @@ Let $E$ be a point on the extension of $BA$ and $D$ a point on the extension of such that $AE = BD$, connect $CE,DE$ Prove that $CE = DE$ -/ -structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where +structure Setting1 (Plane : Type*) [EuclideanPlane Plane] where -- Let $\triangle ABC$ be a regular triangle A : Plane B : Plane @@ -21,11 +21,11 @@ structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where hnd : ¬ Collinear A B C hreg : (▵ A B C).IsRegular -- Claim: $A \ne B$ and $B \ne C$ and $C \ne A$. -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⟩ +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 +structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where -- Let $E$ be a point on the extension of $BA$ and $D$ a point on the extension of $BC$ D : Plane E : Plane @@ -35,7 +35,7 @@ structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plan h : (SEG A E).length = (SEG B D).length -- Theorem : $CE = DE$ -theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : (SEG e.C e.E).length = (SEG e.D e.E).length := by +theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : (SEG e.C e.E).length = (SEG e.D e.E).length := by /- Extend $BD$ to $F$ such that $DF = BC$. Then $BF = BD + DF = AE + AB = BE$, and $\angle FBE = 60^{\circ}$ or $-60^{\circ}$. @@ -176,18 +176,18 @@ $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 +structure Setting1 (Plane : Type*) [EuclideanPlane Plane] where -- We have triangle $\triangle ABC$ A : Plane B : Plane C : Plane hnd : ¬ Collinear A B C -- Claim: $A \ne B$ and $B \ne C$ and $C \ne A$. -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⟩ +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 +structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where -- $D$ is midpoint of $BA$, $E$ is midpoint of $BC$ D : Plane E : Plane @@ -200,16 +200,16 @@ structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plan 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$ -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⟩ +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 +structure Setting3 (Plane : Type*) [EuclideanPlane Plane] extends Setting2 Plane where -- $H$ is the intersection of line $DF$ and $EG$ H : Plane hh : is_inx H (LIN D F) (LIN E G) -- Theorem : quadrilateral $ABCH$ is parallelogram -theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting3 Plane} : QDR e.A e.B e.C e.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 @@ -220,18 +220,18 @@ $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 +structure Setting1 (Plane : Type*) [EuclideanPlane Plane] where -- We have triangle $\triangle ABC$ A : Plane B : Plane C : Plane hnd : ¬ Collinear A B C -- Claim: $A \ne B$ and $B \ne C$ and $C \ne A$. -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⟩ +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 +structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where -- $D,E$ are points in $AB,AC$ respectively D : Plane E : Plane @@ -245,18 +245,18 @@ structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plan -- We have $FB = CG$ hedge : (SEG F B).length = (SEG C G).length -- Claim : $F \ne A$ and $E \ne B$ -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⟩ +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 +structure Setting3 (Plane : Type*) [EuclideanPlane Plane] extends Setting2 Plane where -- We have $AF \parallel BE$ hpara : (SEG_nd A F) ∥ (SEG_nd B E) -- Claim: $G \ne A$ and $D \ne C$ -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⟩ +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 Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting3 Plane} : (SEG_nd e.A e.G) ∥ (SEG_nd e.C e.D) := 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 @@ -267,7 +267,7 @@ $BE, CF$ are heights, such that $AE = 2 EC$ Prove that $AF = 3 FB$ -/ -structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where +structure Setting1 (Plane : Type*) [EuclideanPlane Plane] where -- We have acute triangle $\triangle ABC$ A : Plane B : Plane @@ -275,11 +275,11 @@ structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where hnd : ¬ Collinear A B C hacute : TriangleND.IsAcute (TRI_nd A B C hnd) -- Claim: $A \ne B$ and $B \ne C$ and $C \ne A$. -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⟩ +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 +structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where -- $D,E$ are points in $AB,AC$ respectively E : Plane F : Plane @@ -289,7 +289,7 @@ structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plan h : (SEG A E).length = 2 * (SEG E C).length -- Theorem : $AF = 3 FB$ -theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : (SEG e.A e.F).length = 3 * (SEG e.F e.B).length := sorry +theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : (SEG e.A e.F).length = 3 * (SEG e.F e.B).length := sorry end Shan_Problem_2_37 @@ -298,37 +298,37 @@ namespace Shan_Problem_2_38 let the angle bisectors of $\angle ADB$ and $\angle ADC$ intersect $AB$ and $AC$ at $E,F$, Prove that $EF \parallel BC$-/ -structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where +structure Setting1 (Plane : Type*) [EuclideanPlane Plane] where -- We have triangle $\triangle ABC$ A : Plane B : Plane C : Plane hnd : ¬ Collinear A B C -- Claim: $A \ne B$ and $B \ne C$ and $C \ne A$. -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⟩ +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 +structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where -- $D$ is the midpoint of $BC$ D : Plane hd : D = (SEG B C).midpoint -- Claim: $A \ne D$ and $B \ne D$ and $C \ne D$ -instance A_ne_D {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.A e.D := ⟨sorry⟩ -instance B_ne_D {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.B e.D := ⟨sorry⟩ -instance C_ne_D {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.C e.D := ⟨sorry⟩ +instance A_ne_D {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.A e.D := ⟨sorry⟩ +instance B_ne_D {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.B e.D := ⟨sorry⟩ +instance C_ne_D {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : PtNe e.C e.D := ⟨sorry⟩ -structure Setting3 (Plane : Type _) [EuclideanPlane Plane] extends Setting2 Plane where +structure Setting3 (Plane : Type*) [EuclideanPlane Plane] extends Setting2 Plane where -- let the angle bisectors of $\angle ADB$ and $\angle ADC$ intersect $AB$ and $AC$ at $E,F$ E : Plane F : Plane he : is_inx E (ANG A D B).AngBis (SEG A B) hf : is_inx F (ANG A D C).AngBis (SEG A C) -- Claim: $F \ne E$ -instance F_ne_E {Plane : Type _} [EuclideanPlane Plane] {e : Setting3 Plane} : PtNe e.F e.E := ⟨sorry⟩ +instance F_ne_E {Plane : Type*} [EuclideanPlane Plane] {e : Setting3 Plane} : PtNe e.F e.E := ⟨sorry⟩ -- Theorem : $EF \parallel BC$ -theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting3 Plane} : (SEG_nd e.E e.F) ∥ (SEG_nd e.B e.C) := sorry +theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting3 Plane} : (SEG_nd e.E e.F) ∥ (SEG_nd e.B e.C) := sorry end Shan_Problem_2_38 @@ -338,7 +338,7 @@ $E$ lies on $AC$ such that $AE = 2 CE$, $CD,BE$ intersects at $O$ Prove that $OE = \frac{1}{4} BE$-/ -structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where +structure Setting1 (Plane : Type*) [EuclideanPlane Plane] where -- We have triangle $\triangle ABC$ A : Plane B : Plane @@ -355,7 +355,7 @@ structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where ho : is_inx O (SEG C D) (SEG B E) -- Theorem : $OE = \frac{1}{4} BE$ -theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : (SEG e.O e.E).length = (1 / 4) * (SEG e.B e.E).length := sorry +theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : (SEG e.O e.E).length = (1 / 4) * (SEG e.B e.E).length := sorry end Shan_Problem_2_42 @@ -364,18 +364,18 @@ namespace Shan_Problem_2_43 The parallel line to $AC$ of $E,F$ intersect $BC$ at $G,H$ respectively, Prove that $EG + FH = AC$-/ -structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where +structure Setting1 (Plane : Type*) [EuclideanPlane Plane] where -- We have triangle $\triangle ABC$ A : Plane B : Plane C : Plane hnd : ¬ Collinear A B C -- Claim: $A \ne B$ and $B \ne C$ and $C \ne A$. -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⟩ +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 +structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where -- $E,F$ lies on $AB$ such that $AE = FB$ E : Plane F : Plane @@ -395,7 +395,7 @@ structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plan hh : is_inx H l₂ (SEG B C) -- Theorem : $EG + FH = AC$ -theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : (SEG e.E e.G).length + (SEG e.F e.H).length = (SEG e.A e.C).length := sorry +theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : (SEG e.E e.G).length + (SEG e.F e.H).length = (SEG e.A e.C).length := sorry end Shan_Problem_2_43 @@ -404,7 +404,7 @@ namespace Shan_Problem_2_44 $A₁,B₁,C₁$ are points on line $l₁$ such that $AA₁ \parallel BB₁ \parallel CC₁$. Prove that $BB₁ = \frac{n}{m+n} AA₁ + \frac{m}{m+n} CC₁$-/ -structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where +structure Setting1 (Plane : Type*) [EuclideanPlane Plane] where -- We have line $l$ and points $A,B,C$ lies on $l l : Line Plane A : Plane @@ -434,7 +434,7 @@ structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where hpara₂ : (SEG_nd B B₁) ∥ (SEG_nd C C₁) -- Theorem : $BB₁ = \frac{n}{m+n} AA₁ + \frac{m}{m+n} CC₁$ -theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : (SEG e.B e.B₁).length = (e.n / (e.m+e.n)) * (SEG e.A e.A₁).length + (e.m/(e.m+e.n)) * (SEG e.C e.C₁).length := sorry +theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : (SEG e.B e.B₁).length = (e.n / (e.m+e.n)) * (SEG e.A e.A₁).length + (e.m/(e.m+e.n)) * (SEG e.C e.C₁).length := sorry end Shan_Problem_2_44 @@ -442,7 +442,7 @@ namespace Shan_Problem_2_48 /- $ABCD$ are convex quadrilateral, $AC$ and $BD$ intersect at $E$, Prove that area of $\triangle ABD$ : area of $\triangle CBD = AE : CE$ -/ -structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where +structure Setting1 (Plane : Type*) [EuclideanPlane Plane] where -- We have convex quadrilateral $ABCD$ A : Plane B : Plane @@ -455,7 +455,7 @@ structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where -- Theorem : area of $\triangle ABC :$ area of $\triangle DBC = AE : DE$ -theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting1 Plane} : Triangle.area (▵ e.A e.B e.D) / Triangle.area (▵ e.C e.B e.D) = (SEG e.A e.E).length / (SEG e.D e.E).length := sorry +theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting1 Plane} : Triangle.area (▵ e.A e.B e.D) / Triangle.area (▵ e.C e.B e.D) = (SEG e.A e.E).length / (SEG e.D e.E).length := sorry end Shan_Problem_2_48 @@ -464,18 +464,18 @@ namespace Shan_Problem_2_52 the angle bisector of $\angle ABC$ intersect $AD$ and $AC$ at $M,N$ respectively, Prove that $AB^2 - AN^2 = BM \times BN$-/ -structure Setting1 (Plane : Type _) [EuclideanPlane Plane] where +structure Setting1 (Plane : Type*) [EuclideanPlane Plane] where -- Let triangle $\triangle ABC$ A : Plane B : Plane C : Plane hnd : ¬ Collinear A B C -- Claim: $A \ne B$ and $B \ne C$ and $C \ne A$. -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⟩ +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 +structure Setting2 (Plane : Type*) [EuclideanPlane Plane] extends Setting1 Plane where --$\triangle ABC$ is a right triangle with $\angle BAC = 90^{circ}$ hright : ∠ B A C = ↑ (π / 2) -- $AD$ is the height of $\triangle ABC$ @@ -490,6 +490,6 @@ structure Setting2 (Plane : Type _) [EuclideanPlane Plane] extends Setting1 Plan hn : is_inx N (SEG A C) l -- Theorem : $AB^2 - AN^2 = BM \times BN$ -theorem Result {Plane : Type _} [EuclideanPlane Plane] {e : Setting2 Plane} : (SEG e.A e.B).length * (SEG e.A e.B).length - (SEG e.A e.N).length * (SEG e.A e.N).length = (SEG e.B e.M).length * (SEG e.B e.N).length := sorry +theorem Result {Plane : Type*} [EuclideanPlane Plane] {e : Setting2 Plane} : (SEG e.A e.B).length * (SEG e.A e.B).length - (SEG e.A e.N).length * (SEG e.A e.N).length = (SEG e.B e.M).length * (SEG e.B e.N).length := sorry end Shan_Problem_2_52 diff --git a/EuclideanGeometry/Example/ShanZun/Ex1f.lean b/EuclideanGeometry/Example/ShanZun/Ex1f.lean index 905be2b9f..0b6842b86 100644 --- a/EuclideanGeometry/Example/ShanZun/Ex1f.lean +++ b/EuclideanGeometry/Example/ShanZun/Ex1f.lean @@ -5,7 +5,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Shan_Problem_2_11 /- Let $\triangle ABC$ be a regular triangle, diff --git a/EuclideanGeometry/Example/ShanZun/Ex1h'.lean b/EuclideanGeometry/Example/ShanZun/Ex1h'.lean index c8da9eab3..ebb6547d3 100644 --- a/EuclideanGeometry/Example/ShanZun/Ex1h'.lean +++ b/EuclideanGeometry/Example/ShanZun/Ex1h'.lean @@ -9,7 +9,7 @@ namespace Shan_Problem_2_21 /- In a parallelogram ABCD, E and F lies on the segment AC, and $AE=FC$ Prove that $DE\parallel BF$ -/ -structure Setting (Plane : Type _) [EuclideanPlane Plane] where +structure Setting (Plane : Type*) [EuclideanPlane Plane] where -- Let $ ABCD$ be a nontrivial parallelogram A : Plane B : Plane @@ -52,7 +52,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where -- $DE \parallel BF $ -theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) : (LIN e.D e.E e.E_ne_D) ∥ (LIN e.B e.F e.F_ne_B):= by +theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) : (LIN e.D e.E e.E_ne_D) ∥ (LIN e.B e.F e.F_ne_B):= by -- $\ang BAE=\ang DCF$ have ang_BAE_eq_ang_DCF : ∠ e.B e.A e.E e.B_ne_A e.E_ne_A = ∠ e.D e.C e.F e.D_ne_C e.F_ne_C := sorry @@ -67,7 +67,7 @@ end Shan_Problem_2_21 namespace Shan_Problem_2_23 /- In a parallelogram ABCD, E is the midpoint of the segment BC, and F is the midpoint of the segment AD. Let G, H be the intersection of AC with BF and DE respectively. Prove that $AG=GH=HC$ -/ -structure Setting (Plane : Type _) [EuclideanPlane Plane] where +structure Setting (Plane : Type*) [EuclideanPlane Plane] where -- Let $ ABCD$ be a nontrivial parallelogram A : Plane B : Plane @@ -105,7 +105,7 @@ structure Setting (Plane : Type _) [EuclideanPlane Plane] where hH : is_inx H (LIN A C C_ne_A) (LIN D E E_ne_D) --The pair of points (G,H) divides the segement AC into three segments with the same length. -theorem result {Plane : Type _} [EuclideanPlane Plane] (e : Setting Plane) :(SEG e.A e.G).length=(SEG e.G e.H).length ∧ (SEG e.A e.G).length=(SEG e.H e.C).length := by +theorem result {Plane : Type*} [EuclideanPlane Plane] (e : Setting Plane) :(SEG e.A e.G).length=(SEG e.G e.H).length ∧ (SEG e.A e.G).length=(SEG e.H e.C).length := by -- $▵AFG$ is nontrivial have AFG_nd : ¬ Collinear e.A e.F e.G := sorry -- $▵CBG$ is nontrivial diff --git a/EuclideanGeometry/Example/ShanZun/Ex1h.lean b/EuclideanGeometry/Example/ShanZun/Ex1h.lean index b1f7bb12b..d2194a96e 100644 --- a/EuclideanGeometry/Example/ShanZun/Ex1h.lean +++ b/EuclideanGeometry/Example/ShanZun/Ex1h.lean @@ -4,7 +4,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Shan_Problem_2_21 /- In a parallelelogram ABCD, E and F lies on the segment AC, and $AE=FC$ diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Plane.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Plane.lean index 586a909a1..4d6edc07b 100644 --- a/EuclideanGeometry/Foundation/Axiom/Basic/Plane.lean +++ b/EuclideanGeometry/Foundation/Axiom/Basic/Plane.lean @@ -29,9 +29,9 @@ noncomputable section namespace EuclidGeom /- Define Euclidean plane as normed vector space over ℝ of dimension 2 -/ -class EuclideanPlane (P : Type _) extends MetricSpace P, NormedAddTorsor Vec P +class EuclideanPlane (P : Type*) extends MetricSpace P, NormedAddTorsor Vec P -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] def Vec.mkPtPt (A B : P) : Vec := (B -ᵥ A) diff --git a/EuclideanGeometry/Foundation/Axiom/Basic/Plane_trash.lean b/EuclideanGeometry/Foundation/Axiom/Basic/Plane_trash.lean index b3e64077d..f7978916a 100644 --- a/EuclideanGeometry/Foundation/Axiom/Basic/Plane_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Basic/Plane_trash.lean @@ -3,7 +3,7 @@ import EuclideanGeometry.Foundation.Axiom.Basic.Plane noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] /- point reflection -/ def pt_flip (A O : P) : P := (VEC A O) +ᵥ O diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean index c265c216b..51108663f 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/Basic.lean @@ -9,12 +9,12 @@ namespace EuclidGeom /- Class of Circles-/ @[ext] -structure Circle (P : Type _) [EuclideanPlane P] where +structure Circle (P : Type*) [EuclideanPlane P] where center : P radius : ℝ rad_pos : 0 < radius -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Circle @@ -277,7 +277,7 @@ section arc variable (ω : Circle P) @[ext] -structure Arc (P : Type _) [EuclideanPlane P] (ω : Circle P) where +structure Arc (P : Type*) [EuclideanPlane P] (ω : Circle P) where source : P target : P ison : (source LiesOn ω) ∧ (target LiesOn ω) @@ -375,7 +375,7 @@ end arc section chord @[ext] -structure Chord (P : Type _) [EuclideanPlane P] (ω : Circle P) where +structure Chord (P : Type*) [EuclideanPlane P] (ω : Circle P) where toSegND : SegND P ison : (toSegND.source LiesOn ω) ∧ (toSegND.target LiesOn ω) diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean index ae7d018c2..785d18ac7 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/CCPosition.lean @@ -4,7 +4,7 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.Congruence_trash noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] section position @@ -251,7 +251,7 @@ lemma intersected_centers_distinct {ω₁ : Circle P} {ω₂ : Circle P} (h : ω end CC @[ext] -structure CCInxpts (P : Type _) [EuclideanPlane P] where +structure CCInxpts (P : Type*) [EuclideanPlane P] where left : P right : P diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean b/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean index 528118a57..eeb5dc58a 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/CirclePower.lean @@ -6,7 +6,7 @@ import EuclideanGeometry.Foundation.Axiom.Circle.InscribedAngle noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] open DirLC CC Angle @@ -50,7 +50,7 @@ section tangent namespace Circle @[ext] -structure Tangents (P : Type _) [EuclideanPlane P] where +structure Tangents (P : Type*) [EuclideanPlane P] where left : P right : P diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/InscribedAngle.lean b/EuclideanGeometry/Foundation/Axiom/Circle/InscribedAngle.lean index 3580d66e7..5f5f02bba 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/InscribedAngle.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/InscribedAngle.lean @@ -5,7 +5,7 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.IsocelesTriangle_trash noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] open AngValue Angle diff --git a/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean b/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean index 9309acaf6..39353dde0 100644 --- a/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean +++ b/EuclideanGeometry/Foundation/Axiom/Circle/LCPosition.lean @@ -3,7 +3,7 @@ import EuclideanGeometry.Foundation.Axiom.Circle.Basic noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] section DirLC @@ -66,7 +66,7 @@ theorem pt_liesint_intersect {l : DirLine P} {ω : Circle P} {A : P} (h₁ : A L end DirLC @[ext] -structure DirLCInxpts (P : Type _) [EuclideanPlane P] where +structure DirLCInxpts (P : Type*) [EuclideanPlane P] where front : P back : P diff --git a/EuclideanGeometry/Foundation/Axiom/Isometry/Rotation.lean b/EuclideanGeometry/Foundation/Axiom/Isometry/Rotation.lean index 8ff5d9dcd..348d9f2d3 100644 --- a/EuclideanGeometry/Foundation/Axiom/Isometry/Rotation.lean +++ b/EuclideanGeometry/Foundation/Axiom/Isometry/Rotation.lean @@ -4,6 +4,6 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Ray namespace EuclidGeom -variable {P: Type _} [EuclideanPlane P] (o : P) +variable {P: Type*} [EuclideanPlane P] (o : P) end EuclidGeom \ No newline at end of file diff --git a/EuclideanGeometry/Foundation/Axiom/Isometry/Translation_ex.lean b/EuclideanGeometry/Foundation/Axiom/Isometry/Translation_ex.lean index 6b90a3fe2..14b8c570b 100644 --- a/EuclideanGeometry/Foundation/Axiom/Isometry/Translation_ex.lean +++ b/EuclideanGeometry/Foundation/Axiom/Isometry/Translation_ex.lean @@ -7,7 +7,7 @@ noncomputable section namespace EuclidGeom -variable {P: Type _} [EuclideanPlane P] (v : Vec) +variable {P: Type*} [EuclideanPlane P] (v : Vec) -- We fix the amount of translation to be v diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Class.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Class.lean index 873d60ac3..16498448f 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Class.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Class.lean @@ -44,7 +44,7 @@ namespace EuclidGeom class LinFig (α : Type*) (P : outParam <| Type*) [outParam <| EuclideanPlane P] extends Fig α P where collinear' : ∀ {A B C : P} {F : α}, A LiesOn F → B LiesOn F → C LiesOn F → Collinear A B C -class ProjObj (β : Type _) where +class ProjObj (β : Type*) where toProj : β → Proj -- the information here is abundant, choose toProj' + a field carrier_to_proj_eq_to_proj is also enough. Or even ∃ A B ∈ carrier, A ≠ B is enough. toProj' can be defined later. However, we choose to write this way in order to avoid `∃` and use as many rfl as possible. @@ -54,7 +54,7 @@ class ProjFig (α : Type*) (P : outParam <| Type*) [outParam <| EuclideanPlane P carrier_subset_toLine {F} : carrier F ⊆ (toLine F).carrier toLine_toProj_eq_toProj {F} : (toLine F).toProj = toProj' F -class DirObj (β : Type _) extends ProjObj β where +class DirObj (β : Type*) extends ProjObj β where toDir : β → Dir toDir_toProj_eq_toProj : ∀ {G : β}, (toDir G).toProj = toProj G @@ -69,7 +69,7 @@ class DirFig (α : Type*) (P : outParam <| Type*) [outParam <| EuclideanPlane P] toDirLine_rev_eq_to_rev_toDirLine {F} : ((toDirLine F).reverse = toDirLine (reverse F)) section fig_to_obj -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] instance {α} [ProjFig α P] : ProjObj α where toProj := ProjFig.toProj' @@ -86,7 +86,7 @@ export DirFig (toDir' toDirLine toDir_toProj_eq_toProj toDirLine_toLine_eq_toLin export DirObj (toDir) section instances -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] -- Fun Fact: Vec is none of these. Id is LinFig. instance : DirObj VecND where @@ -167,7 +167,7 @@ section theorems open Line DirLine -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] theorem carrier_toProj_eq_toProj {α} {A B : P} [ProjFig α P] {F : α} [_h : PtNe B A] (ha : A LiesOn F) (hb : B LiesOn F) : (SEG_nd A B).toProj = toProj' F := (toProj_eq_seg_nd_toProj_of_lies_on (carrier_subset_toLine ha) (carrier_subset_toLine hb)).trans toLine_toProj_eq_toProj diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Collinear.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Collinear.lean index 5b9927a26..a5d6d0307 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Collinear.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Collinear.lean @@ -8,7 +8,7 @@ namespace EuclidGeom open Classical -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] section Collinear @@ -214,7 +214,7 @@ Note that we do not need all reverse, extension line,... here. instead we should end compatibility /-- There exists three points $A$, $B$, $C$ on the plane such that they are not collinear. -/ -theorem nontriv_of_plane {H : Type _} [h : EuclideanPlane H] : ∃ A B C : H, ¬(Collinear A B C) := by +theorem nontriv_of_plane {H : Type*} [h : EuclideanPlane H] : ∃ A B C : H, ¬(Collinear A B C) := by rcases h.nonempty with ⟨A⟩ let B := (⟨1, 0⟩ : Vec) +ᵥ A let C := (⟨0, 1⟩ : Vec) +ᵥ A diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Collinear_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Collinear_trash.lean index acea84c26..d34a6120a 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Collinear_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Collinear_trash.lean @@ -4,7 +4,7 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Parallel namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean index bd9375677..0275cff38 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean @@ -6,7 +6,7 @@ namespace EuclidGeom section setoid -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] -- `Future change plan` Change this to "structure" instead of "and". /-- We say that rays $r$ and $r'$ \emph{induce the same directed line} if, (1) they have the same direction, and (2) the source of $r'$ lies on $r$ or the reverse range of $r$.-/ @@ -128,12 +128,12 @@ theorem same_dir_line_le_same_extn_line : same_dir_line.setoid (P := P) ≤ same end setoid /-- A \emph{directed line} is the equivalence class of rays with the same directed lines. -/ -def DirLine (P : Type _) [EuclideanPlane P] := Quotient (@same_dir_line.setoid P _) +def DirLine (P : Type*) [EuclideanPlane P] := Quotient (@same_dir_line.setoid P _) /-- A \emph{line} is the equivalence class of rays with the same exetnsion lines. -/ -def Line (P : Type _) [EuclideanPlane P] := Quotient (@same_extn_line.setoid P _) +def Line (P : Type*) [EuclideanPlane P] := Quotient (@same_extn_line.setoid P _) -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] section make diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean index 946d6c376..46bbffcb1 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Line_trash.lean @@ -3,7 +3,7 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Ray_trash namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] theorem pt_flip_collinear {A B O : P} (h : B = pt_flip A O) : Collinear A O B := by apply Collinear.perm₁₃₂ diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean index b6532902c..eb632a219 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel.lean @@ -20,7 +20,7 @@ namespace EuclidGeom open Line -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] /- /-- A linear object is one of the following five types: a nondegenerate vector, a direction, a ray, a nondegenerate segment, or a line. In the following, we define natural ways to view a nondegenerate vector, a direction, a ray, a nondegenerate segment or a line, as a linear object. @@ -525,13 +525,10 @@ theorem inx_eq_of_same_extn_line {a₁ b₁ a₂ b₂ : Ray P} (g₁ : same_extn (inx_lies_on_fst_extn_line a₂ b₂ h₂) ha1 (inx_lies_on_snd_extn_line a₂ b₂ h₂) hb1 exact h₂ (congrArg Line.toProj heq) --- This theorem deals only with `HEq` -theorem heq_funext {c₁ c₂ d: Sort _} (e : c₁ = c₂) {f₁ : c₁ → d} {f₂ : c₂ → d} (h : ∀ (s : c₁) (t : c₂), f₁ s = f₂ t) : HEq f₁ f₂ := Function.hfunext e (fun _ _ _ => (heq_of_eq (h _ _))) - theorem heq_of_inx_of_extn_line (a₁ b₁ a₂ b₂ : Ray P) (h₁ : same_extn_line a₁ a₂) (h₂ : same_extn_line b₁ b₂) : HEq (fun h => inx_of_extn_line a₁ b₁ h) (fun h => inx_of_extn_line a₂ b₂ h) := by have e : (Ray.toProj a₁ ≠ Ray.toProj b₁) = (Ray.toProj a₂ ≠ Ray.toProj b₂) := by rw [h₁.1, h₂.1] - exact @heq_funext (Ray.toProj a₁ ≠ Ray.toProj b₁) (Ray.toProj a₂ ≠ Ray.toProj b₂) P e (fun h => inx_of_extn_line a₁ b₁ h) (fun h => inx_of_extn_line a₂ b₂ h) (inx_eq_of_same_extn_line h₁ h₂) + exact Function.hfunext e fun _ _ _ ↦ heq_of_eq <| inx_eq_of_same_extn_line h₁ h₂ _ _ /-- Given two unparallel lines, this function returns the intersection point of these two lines. -/ def Line.inx (l₁ l₂ : Line P) (h : ¬ l₁ ∥ l₂) : P := @Quotient.hrecOn₂ (Ray P) (Ray P) same_extn_line.setoid same_extn_line.setoid (fun l l' => (Line.toProj l ≠ Line.toProj l') → P) l₁ l₂ inx_of_extn_line heq_of_inx_of_extn_line h diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean index aa5c8f6d1..ef5da3795 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Parallel_trash.lean @@ -3,7 +3,7 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Parallel namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Parallel diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean index f488dea9b..a85328fc9 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular.lean @@ -5,7 +5,7 @@ namespace EuclidGeom open Line -variable {P : Type _} [EuclideanPlane P] {α β γ : Type*} [ProjObj α] [ProjObj β] [ProjObj γ] +variable {P : Type*} [EuclideanPlane P] {α β γ : Type*} [ProjObj α] [ProjObj β] [ProjObj γ] {l₁ : α} {l₂ : β} {l₃ : γ} /-- This defines two projective objects to be perpendicular, i.e. their associated projective directions are perpendicular. -/ diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular_trash.lean index 763d87c16..9576df469 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Perpendicular_trash.lean @@ -6,6 +6,6 @@ namespace EuclidGeom open Line -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Ratio.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Ratio.lean index 88ee7b7f0..de14085cc 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Ratio.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Ratio.lean @@ -5,7 +5,7 @@ namespace EuclidGeom open Classical -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] section ratio diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean index 4301cbca9..80d3ab015 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Ray.lean @@ -54,7 +54,7 @@ section definition /-- A \emph{ray} consists of a pair of a point $P$ and a direction; it is the ray that starts at the point and extends in the given direction. -/ @[ext] -structure Ray (P : Type _) [EuclideanPlane P] where +structure Ray (P : Type*) [EuclideanPlane P] where /-- returns the source of the ray. -/ source : P /-- returns the direction of the ray. -/ @@ -66,7 +66,7 @@ alias Ray.mk_pt_dir := Ray.mk /-- A \emph{Segment} consists of a pair of points: the source and the target; it is the segment from the source to the target. (We allow the source and the target to be the same.) -/ @[ext] -structure Seg (P : Type _) [EuclideanPlane P] where +structure Seg (P : Type*) [EuclideanPlane P] where /-- returns the source of the segment. -/ source : P /-- returns the target of the segment. -/ @@ -77,17 +77,17 @@ attribute [pp_dot] Seg.source Seg.target namespace Seg /-- Given a segment $AB$, this function returns whether the segment $AB$ is nondegenerate, i.e. whether $A \neq B$. -/ -def IsND {P : Type _} [EuclideanPlane P] (seg : Seg P) : Prop := seg.target ≠ seg.source +def IsND {P : Type*} [EuclideanPlane P] (seg : Seg P) : Prop := seg.target ≠ seg.source end Seg /-- A \emph{nondegenerate segment} is a segment $AB$ that is nondegenerate, i.e. $A \neq B$. -/ -def SegND (P : Type _) [EuclideanPlane P] := {seg : Seg P // seg.IsND} +def SegND (P : Type*) [EuclideanPlane P] := {seg : Seg P // seg.IsND} end definition -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] section make diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean index 0998cf365..843bce727 100644 --- a/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Linear/Ray_trash.lean @@ -5,7 +5,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] (seg_nd : SegND P) +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 diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean index 92dfe8739..39de2ef30 100644 --- a/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean +++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle.lean @@ -35,7 +35,7 @@ structure Angle (P : Type*) [EuclideanPlane P] where attribute [pp_dot] Angle.source Angle.dir₁ Angle.dir₂ -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Angle diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex.lean index 029b11e56..527345c77 100644 --- a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex.lean +++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex.lean @@ -11,7 +11,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Angle @@ -261,7 +261,7 @@ end Angle section Parallel -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] -- should be stated use mod 2pi first, then back to pi or -pi structure IsCorrespondingAng (ang₁ ang₂ : Angle P) : Prop where diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex2.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex2.lean index d0f0601e8..92401e6f1 100644 --- a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex2.lean +++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex2.lean @@ -5,7 +5,7 @@ noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex_trash.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex_trash.lean index b22e6eb74..b7b9b708f 100644 --- a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex_trash.lean @@ -4,7 +4,7 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Perpendicular namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +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.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 diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle_trash.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle_trash.lean index 6521a3c3f..747b12379 100644 --- a/EuclideanGeometry/Foundation/Axiom/Position/Angle_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Position/Angle_trash.lean @@ -5,7 +5,7 @@ namespace EuclidGeom open AngValue -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Angle diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Convex_trash.lean b/EuclideanGeometry/Foundation/Axiom/Position/Convex_trash.lean index 430552bd0..44a79e62d 100644 --- a/EuclideanGeometry/Foundation/Axiom/Position/Convex_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Position/Convex_trash.lean @@ -5,7 +5,7 @@ import EuclideanGeometry.Foundation.Construction.Polygon.Quadrilateral noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] theorem cvx_of_inscribed_to_cvx {X Y Z W A B C D : P} (h : (QDR A B C D).IsConvex) (h1 : X LiesInt (SEG A B)) (h2 : Y LiesInt (SEG B C)) (h3 : Z LiesInt (SEG C D)) (h4 : W LiesInt (SEG D A)) : (QDR X Y Z W).IsConvex := by sorry diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Orientation_ex.lean b/EuclideanGeometry/Foundation/Axiom/Position/Orientation_ex.lean index e9b18b2ac..f5b9e5499 100644 --- a/EuclideanGeometry/Foundation/Axiom/Position/Orientation_ex.lean +++ b/EuclideanGeometry/Foundation/Axiom/Position/Orientation_ex.lean @@ -5,7 +5,7 @@ import EuclideanGeometry.Foundation.Axiom.Position.Angle_ex noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] theorem pts_are_distinct_of_two_rays_of_angle (ang : Angle P) (nontriv : ang.IsND) (A B : P) (ha : A LiesInt ang.start_ray) (hb : B LiesInt ang.end_ray) : A ≠ B := by sorry diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean b/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean index 678443575..0eb4a4ce9 100644 --- a/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Position/Orientation_trash.lean @@ -2,7 +2,7 @@ import EuclideanGeometry.Foundation.Axiom.Position.Orientation namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] theorem liesonleft_iff_liesonright_reverse {A : P} {l : DirLine P} : A LiesOnLeft l ↔ A LiesOnRight l.reverse := by have : odist A l.reverse = -odist A l := by diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean index 1be335db0..334817cc8 100644 --- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean +++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean @@ -1,8 +1,6 @@ import EuclideanGeometry.Foundation.Axiom.Position.Orientation import EuclideanGeometry.Foundation.Axiom.Linear.Collinear -universe u - noncomputable section namespace EuclidGeom @@ -11,14 +9,14 @@ open AngValue /- Class of generalized triangles -/ @[ext] -structure Triangle (P : Type u) [EuclideanPlane P] where +structure Triangle (P : Type*) [EuclideanPlane P] where point₁ : P point₂ : P point₃ : P namespace Triangle -variable {P : Type u} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] --implies 1 left of 23, 2 left of 31 -- not is_cclock implies 1 right of 23, ..., ... @@ -42,11 +40,11 @@ def IsND (tr : Triangle P) : Prop := ¬ Collinear tr.1 tr.2 tr.3 end Triangle -def TriangleND (P : Type u) [EuclideanPlane P] := { tr : Triangle P // tr.IsND } +def TriangleND (P : Type*) [EuclideanPlane P] := { tr : Triangle P // tr.IsND } namespace TriangleND -variable {P : Type u} [EuclideanPlane P] (tr_nd : TriangleND P) +variable {P : Type*} [EuclideanPlane P] (tr_nd : TriangleND P) @[pp_dot] abbrev point₁ : P := tr_nd.1.1 @@ -102,7 +100,7 @@ def angle₃ : Angle P := ANG tr_nd.point₁ tr_nd.point₃ tr_nd.point₂ end TriangleND -variable {P : Type u} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] namespace Triangle @@ -156,7 +154,7 @@ instance : IntFig Triangle where end TriangleND -variable {P : Type _} [EuclideanPlane P] (tr : Triangle P) (tr_nd : TriangleND P) +variable {P : Type*} [EuclideanPlane P] (tr : Triangle P) (tr_nd : TriangleND P) namespace Triangle diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean index cc32fc557..79ee4857c 100644 --- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean +++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_ex.lean @@ -3,7 +3,7 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.Basic noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] (tr : Triangle P) (tr_nd : TriangleND P) +variable {P : Type*} [EuclideanPlane P] (tr : Triangle P) (tr_nd : TriangleND P) --perm and flip is moved to the main file diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_trash.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_trash.lean index d546e59dd..96eee676f 100644 --- a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic_trash.lean @@ -4,7 +4,7 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.Basic_ex namespace EuclidGeom open AngValue -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] structure TriangleND.IsAcute (tr_nd : TriangleND P) : Prop where angle₁ : tr_nd.angle₁.IsAcu diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean index 2f3ce4f21..0ac9ad38f 100644 --- a/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean +++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence.lean @@ -11,7 +11,7 @@ namespace EuclidGeom /- congruences of triangles, separate definitions for reversing orientation or not, (requiring all sides and angles being the same)-/ -variable {P : Type _} [EuclideanPlane P] {tr tr₁ tr₂ tr₃ : Triangle P} {tr_nd tr_nd₁ tr_nd₂ tr_nd₃ : TriangleND P} +variable {P : Type*} [EuclideanPlane P] {tr tr₁ tr₂ tr₃ : Triangle P} {tr_nd tr_nd₁ tr_nd₂ tr_nd₃ : TriangleND P} open Classical AngValue Angle diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence_trash.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence_trash.lean index 42524a134..86a556fa2 100644 --- a/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Congruence_trash.lean @@ -3,7 +3,7 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.Congruence noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] theorem Triangle.IsCongr.unique_of_eq_eq {tr₁ tr₂ : Triangle P} (h : tr₁.IsCongr tr₂) (p₁ : tr₁.point₁ = tr₂.point₁) (p₂ : tr₁.point₂ = tr₂.point₂) [hne : PtNe tr₁.point₁ tr₁.point₂] : tr₁.point₃ = tr₂.point₃ := sorry diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle.lean index ee5762027..5c1a893d0 100644 --- a/EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle.lean +++ b/EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle.lean @@ -9,7 +9,7 @@ import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] -- Prefer to define IsIsocelesTriangle than to just state the properties. Isoceles triangle by definition has a prefered orientation diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle_trash.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle_trash.lean index eed2a4059..442e51272 100644 --- a/EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle_trash.lean +++ b/EuclideanGeometry/Foundation/Axiom/Triangle/IsocelesTriangle_trash.lean @@ -3,7 +3,7 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.IsocelesTriangle noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] lemma isoceles_tri_pts_ne {tri : Triangle P} (h : tri.IsIsoceles) (hne : tri.point₂ ≠ tri.point₃) : (tri.point₁ ≠ tri.point₂) ∧ (tri.point₁ ≠ tri.point₃) := sorry diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Similarity.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Similarity.lean index e25e8a457..765ede2fb 100644 --- a/EuclideanGeometry/Foundation/Axiom/Triangle/Similarity.lean +++ b/EuclideanGeometry/Foundation/Axiom/Triangle/Similarity.lean @@ -4,7 +4,7 @@ import EuclideanGeometry.Foundation.Axiom.Basic.Angle noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] {tr₁ tr₂ tr₃ : TriangleND P} +variable {P : Type*} [EuclideanPlane P] {tr₁ tr₂ tr₃ : TriangleND P} open TriangleND AngValue diff --git a/EuclideanGeometry/Foundation/Construction/ComputationTool/Ceva_converse.lean b/EuclideanGeometry/Foundation/Construction/ComputationTool/Ceva_converse.lean index 5b6da2ab1..1f36b5f28 100644 --- a/EuclideanGeometry/Foundation/Construction/ComputationTool/Ceva_converse.lean +++ b/EuclideanGeometry/Foundation/Construction/ComputationTool/Ceva_converse.lean @@ -8,7 +8,7 @@ open Classical section Ceva's_converse_theorem -structure Setting (P : Type _) [EuclideanPlane P] where +structure Setting (P : Type*) [EuclideanPlane P] where -- Let $\triangle ABC$ be a nondegenerate triangle. A : P B : P @@ -32,7 +32,7 @@ structure Setting (P : Type _) [EuclideanPlane P] where -- $\frac{EB}{EC} \cdot \frac{FC}{FA} \cdot \frac{GA}{GB} = -1$. ratio_mul_eq_minus_one : (divratio E B C) * (divratio F C A) * (divratio G A B) = -1 -theorem Ceva_converse_theorem {P : Type _} [EuclideanPlane P] (e : Setting P) : ∃ (X : P), (X LiesOn (LIN e.A e.E e.E_ne_A)) ∧ (X LiesOn (LIN e.B e.F e.F_ne_B)) ∧ (X LiesOn (LIN e.C e.G e.G_ne_C)) := by +theorem Ceva_converse_theorem {P : Type*} [EuclideanPlane P] (e : Setting P) : ∃ (X : P), (X LiesOn (LIN e.A e.E e.E_ne_A)) ∧ (X LiesOn (LIN e.B e.F e.F_ne_B)) ∧ (X LiesOn (LIN e.C e.G e.G_ne_C)) := by let D := Line.inx (LIN e.A e.E (TriangleND.points_ne_of_collinear_of_not_collinear1 e.not_collinear_ABC e.collinear_EBC)) (LIN e.B e.F (TriangleND.points_ne_of_collinear_of_not_collinear2 e.not_collinear_ABC e.collinear_FCA)) (TriangleND.not_parallel_of_not_collinear_of_collinear_collinear e.not_collinear_ABC e.collinear_EBC e.collinear_FCA) have ratiomul : (divratio e.E e.B e.C) * (divratio e.F e.C e.A) * (divratio e.G e.A e.B) = -1 := e.ratio_mul_eq_minus_one have E_ne_C : e.E ≠ e.C := by diff --git a/EuclideanGeometry/Foundation/Construction/ComputationTool/Oarea_method.lean b/EuclideanGeometry/Foundation/Construction/ComputationTool/Oarea_method.lean index 40a3ee284..d3e476b78 100644 --- a/EuclideanGeometry/Foundation/Construction/ComputationTool/Oarea_method.lean +++ b/EuclideanGeometry/Foundation/Construction/ComputationTool/Oarea_method.lean @@ -6,7 +6,7 @@ namespace EuclidGeom open Classical -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] section oarea_method diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/GeneralPolygon.lean b/EuclideanGeometry/Foundation/Construction/Polygon/GeneralPolygon.lean index 2789a4ad5..d4204cd1c 100644 --- a/EuclideanGeometry/Foundation/Construction/Polygon/GeneralPolygon.lean +++ b/EuclideanGeometry/Foundation/Construction/Polygon/GeneralPolygon.lean @@ -6,10 +6,10 @@ import EuclideanGeometry.Foundation.Construction.Polygon.Quadrilateral noncomputable section namespace EuclidGeom -structure Polygon (P : Type _) [EuclideanPlane P] where +structure Polygon (P : Type*) [EuclideanPlane P] where -structure ConvexPolygon (P : Type _) [EuclideanPlane P] extends Polygon P where +structure ConvexPolygon (P : Type*) [EuclideanPlane P] extends Polygon P where -structure RegularPolygon (P : Type _) [EuclideanPlane P] extends ConvexPolygon P where +structure RegularPolygon (P : Type*) [EuclideanPlane P] extends ConvexPolygon P where end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram.lean b/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram.lean index 2154c02e4..cfec47f66 100644 --- a/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram.lean +++ b/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram.lean @@ -38,20 +38,20 @@ In this section we define two types of parallelograms. 'parallel_nd' deals with -- /-- A QuadrilateralND satisfies IsPara if two sets of opposite sides are parallel respectively. -/ -- @[pp_dot] --- def QuadrilateralND.IsParaPara {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := ( qdr_nd.edgeND₁₂ ∥ qdr_nd.edgeND₃₄) ∧ (qdr_nd.edgeND₁₄ ∥ qdr_nd.edgeND₂₃) +-- def QuadrilateralND.IsParaPara {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := ( qdr_nd.edgeND₁₂ ∥ qdr_nd.edgeND₃₄) ∧ (qdr_nd.edgeND₁₄ ∥ qdr_nd.edgeND₂₃) -- -- scoped postfix : 50 "IsParaPara" => QuadrilateralND.IsParaPara -- /-- A quadrilateral satisfies IsPara if it is a QuadrilateralND and satisfies IsPara as a QuadrilateralND. -/ -- @[pp_dot] --- def Quadrilateral.IsParaPara {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by +-- def Quadrilateral.IsParaPara {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by -- by_cases h : qdr.IsND -- · exact (QuadrilateralND.mk_nd h).IsParaPara -- · exact False /-- A quadrilateral satisfies IsPara if it is a QuadrilateralND and satisfies IsPara as a QuadrilateralND. -/ @[pp_dot] -def Quadrilateral.IsParaPara {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by +def Quadrilateral.IsParaPara {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by by_cases h : qdr.IsND · have qdr_nd : QuadrilateralND P := QDR_nd' h exact (qdr_nd.edgeND₁₂ ∥ qdr_nd.edgeND₃₄) ∧ (qdr_nd.edgeND₄₁ ∥ qdr_nd.edgeND₂₃) @@ -59,67 +59,67 @@ def Quadrilateral.IsParaPara {P : Type _} [EuclideanPlane P] (qdr : Quadrilatera /-- A quadrilateral is called parallelogram if VEC qdr.point₁ qdr.point₂ = VEC qdr.point₄ qdr.point₃.-/ @[pp_dot] -def Quadrilateral.IsPrg {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := VEC qdr.point₁ qdr.point₂ = VEC qdr.point₄ qdr.point₃ +def Quadrilateral.IsPrg {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := VEC qdr.point₁ qdr.point₂ = VEC qdr.point₄ qdr.point₃ scoped postfix : 50 "IsPrg" => Quadrilateral.IsPrg -- `shall we define this?` -- /-- A QuadrilateralND is called parallelogram if VEC qdr.point₁ qdr.point₂ = VEC qdr.point₄ qdr.point₃.-/ -- @[pp_dot] --- def QuadrilateralND.IsPrg {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := VEC qdr_nd.point₁ qdr_nd.point₂ = VEC qdr_nd.point₄ qdr_nd.point₃ +-- def QuadrilateralND.IsPrg {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := VEC qdr_nd.point₁ qdr_nd.point₂ = VEC qdr_nd.point₄ qdr_nd.point₃ -- scoped postfix : 50 "nd_IsPrg" => QuadrilateralND.IsPrg /-- We define parallelogram as a structure. -/ @[ext] -structure Parallelogram (P : Type _) [EuclideanPlane P] extends Quadrilateral P where +structure Parallelogram (P : Type*) [EuclideanPlane P] extends Quadrilateral P where is_parallelogram : toQuadrilateral IsPrg /-- Make a parallelogram with 4 points on a plane, and using condition IsPrg. -/ -def Parallelogram.mk_pt_pt_pt_pt {P : Type _} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D) IsPrg) : Parallelogram P where +def Parallelogram.mk_pt_pt_pt_pt {P : Type*} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D) IsPrg) : Parallelogram P where toQuadrilateral := (QDR A B C D) is_parallelogram := h scoped notation "PRG" => Parallelogram.mk_pt_pt_pt_pt /-- Make a parallelogram with a quadrilateral, and using condition IsPrg. -/ -def Parallelogram.mk_isPrg {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsPrg) : Parallelogram P where +def Parallelogram.mk_isPrg {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsPrg) : Parallelogram P where toQuadrilateral := qdr is_parallelogram := h scoped notation "PRG'" => Parallelogram.mk_isPrg /-- Vectors point₁ point₂ and point₄ point₃ in a parallelogram are equal. -/ -theorem Parallelogram.eq_vec_of_isPrg {P : Type _} [EuclideanPlane P] {prg : Parallelogram P} : VEC prg.point₁ prg.point₂ = VEC prg.point₄ prg.point₃ := prg.is_parallelogram +theorem Parallelogram.eq_vec_of_isPrg {P : Type*} [EuclideanPlane P] {prg : Parallelogram P} : VEC prg.point₁ prg.point₂ = VEC prg.point₄ prg.point₃ := prg.is_parallelogram /-- Vectors point₁ point₄ and point₂ point₃ in a parallelogram are equal. -/ -theorem Parallelogram.eq_vec_of_isPrg' {P : Type _} [EuclideanPlane P] {prg : Parallelogram P} : VEC prg.point₁ prg.point₄ = VEC prg.point₂ prg.point₃ := by rw [← vec_add_vec prg.point₁ prg.point₂ prg.point₄, ← vec_add_vec prg.point₂ prg.point₄ prg.point₃, prg.is_parallelogram, add_comm] +theorem Parallelogram.eq_vec_of_isPrg' {P : Type*} [EuclideanPlane P] {prg : Parallelogram P} : VEC prg.point₁ prg.point₄ = VEC prg.point₂ prg.point₃ := by rw [← vec_add_vec prg.point₁ prg.point₂ prg.point₄, ← vec_add_vec prg.point₂ prg.point₄ prg.point₃, prg.is_parallelogram, add_comm] /-- A parallelogram which satisfies Prallelogram.InGPos satisfies IsParaPara. -/ -theorem Parallelogram.parapara_of_gpos {P : Type _} [EuclideanPlane P] {prg : Parallelogram P} (InGPos : prg.InGPos): prg.IsParaPara:= by +theorem Parallelogram.parapara_of_gpos {P : Type*} [EuclideanPlane P] {prg : Parallelogram P} (InGPos : prg.InGPos): prg.IsParaPara:= by unfold Quadrilateral.IsParaPara sorry /-- A parallelogram which satisfies Prallelogram.InGPos is convex. -/ -theorem Parallelogram.cvx_of_gpos {P : Type _} [EuclideanPlane P] {prg : Parallelogram P} (InGPos : prg.InGPos): prg.IsConvex:= by sorry +theorem Parallelogram.cvx_of_gpos {P : Type*} [EuclideanPlane P] {prg : Parallelogram P} (InGPos : prg.InGPos): prg.IsConvex:= by sorry /-- We define parallelogram_nd as a structure. -/ @[ext] -structure ParallelogramND (P : Type _) [EuclideanPlane P] extends Quadrilateral_cvx P, Parallelogram P +structure ParallelogramND (P : Type*) [EuclideanPlane P] extends Quadrilateral_cvx P, Parallelogram P /-- A quadrilateral is parallelogram_nd if it is both convex and satisfies qualities of a parallelogram. This definition is in agreement with the structure above. -/ @[pp_dot] -def Quadrilateral.IsPrgND {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := qdr IsConvex ∧ qdr IsPrg +def Quadrilateral.IsPrgND {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := qdr IsConvex ∧ qdr IsPrg scoped postfix : 50 "IsPrgND" => Quadrilateral.IsPrgND -- /-- A QuadrilateralND is parallelogram_nd if its toQuadrilateral is both convex and satisfies qualities of a parallelogram. -/ -- @[pp_dot] --- def QuadrilateralND.IsPrgND {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := Quadrilateral.IsPrgND qdr_nd.toQuadrilateral +-- def QuadrilateralND.IsPrgND {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := Quadrilateral.IsPrgND qdr_nd.toQuadrilateral -- scoped postfix : 50 "nd_IsPrgND" => QuadrilateralND.IsPrgND -theorem QuadrilateralND.parapara_iff_para_para {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : (qdr_nd.IsParaPara) ↔ (qdr_nd.edgeND₁₂ ∥ qdr_nd.edgeND₃₄) ∧ (qdr_nd.edgeND₄₁ ∥ qdr_nd.edgeND₂₃) := by +theorem QuadrilateralND.parapara_iff_para_para {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : (qdr_nd.IsParaPara) ↔ (qdr_nd.edgeND₁₂ ∥ qdr_nd.edgeND₃₄) ∧ (qdr_nd.edgeND₄₁ ∥ qdr_nd.edgeND₂₃) := by constructor unfold Quadrilateral.IsParaPara simp only [dite_true, qdr_nd.nd, and_imp] @@ -129,10 +129,10 @@ theorem QuadrilateralND.parapara_iff_para_para {P : Type _} [EuclideanPlane P] ( exact fun a a_1 ↦ { left := a, right := a_1 } /-- A parallelogram_nd satisfies InGPos. -/ -theorem ParallelogramND.gpos_of_prgnd {P : Type _} [EuclideanPlane P] (prg_nd : ParallelogramND P) : prg_nd.InGPos := ⟨prg_nd.not_collinear₁₂₃, prg_nd.not_collinear₂₃₄, prg_nd.not_collinear₃₄₁, prg_nd.not_collinear₄₁₂⟩ +theorem ParallelogramND.gpos_of_prgnd {P : Type*} [EuclideanPlane P] (prg_nd : ParallelogramND P) : prg_nd.InGPos := ⟨prg_nd.not_collinear₁₂₃, prg_nd.not_collinear₂₃₄, prg_nd.not_collinear₃₄₁, prg_nd.not_collinear₄₁₂⟩ /-- A parallelogram_nd satisfies IsParaPara. -/ -theorem ParallelogramND.parapara_of_prgnd {P : Type _} [EuclideanPlane P] (prg_nd : ParallelogramND P) : prg_nd.IsParaPara := by +theorem ParallelogramND.parapara_of_prgnd {P : Type*} [EuclideanPlane P] (prg_nd : ParallelogramND P) : prg_nd.IsParaPara := by unfold Quadrilateral.IsParaPara simp only [dite_true, prg_nd.nd] unfold Parallel @@ -144,14 +144,14 @@ theorem ParallelogramND.parapara_of_prgnd {P : Type _} [EuclideanPlane P] (prg_n sorry sorry -def ParallelogramND.mk_pt_pt_pt_pt {P : Type _} [EuclideanPlane P] (A B C D : P) (h: (QDR A B C D) IsPrgND) : ParallelogramND P where +def ParallelogramND.mk_pt_pt_pt_pt {P : Type*} [EuclideanPlane P] (A B C D : P) (h: (QDR A B C D) IsPrgND) : ParallelogramND P where toQuadrilateral := (QDR A B C D) nd := h.left; convex := h.left is_parallelogram := h.right scoped notation "PRG_nd" => ParallelogramND.mk_pt_pt_pt_pt -def ParallelogramND.mk_isPrgND {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsPrgND) : ParallelogramND P where +def ParallelogramND.mk_isPrgND {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsPrgND) : ParallelogramND P where toQuadrilateral := qdr nd := h.left; convex := h.left is_parallelogram := h.right @@ -160,7 +160,7 @@ scoped notation "PRG_nd'" => ParallelogramND.mk_isPrgND /- Using the property above, we leave such a shortcut in a way people usually sense a parallelogram. A quadrilateral A B C D is parallelogram_nd if it is ND, is a parallelogram, and satisfies InGPos. -def ParallelogramND.mk_prgND_of_gpos {P : Type _} [EuclideanPlane P] {prg : Parallelogram P} (gpos: prg.InGPos): ParallelogramND P where +def ParallelogramND.mk_prgND_of_gpos {P : Type*} [EuclideanPlane P] {prg : Parallelogram P} (gpos: prg.InGPos): ParallelogramND P where toQuadrilateral := prg.toQuadrilateral nd := sorry convex := sorry @@ -170,7 +170,7 @@ def ParallelogramND.mk_prgND_of_gpos {P : Type _} [EuclideanPlane P] {prg : Para scoped notation "non_triv_PRG_nd" => ParallelogramND.mk_prgND_of_gpos A quadrilateral A B C D is parallelogram_nd if it is ND, is a parallelogram, and satisfies IsParaPara. ---def ParallelogramND.mk_prgND_of_para {P : Type _} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsPrg) (IsPara: (QDR_nd A B C D h).IsParaPara): ParallelogramND P where +--def ParallelogramND.mk_prgND_of_para {P : Type*} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsPrg) (IsPara: (QDR_nd A B C D h).IsParaPara): ParallelogramND P where point₁ := A; point₂ := B; point₃ := C; point₄ := D nd := h convex := sorry @@ -180,14 +180,14 @@ A quadrilateral A B C D is parallelogram_nd if it is ND, is a parallelogram, and scoped notation "IsParaPara_PRG_nd" => ParallelogramND.mk_parallelogram_para here is two theorem using first version of definition of PRG_nd, may not useful currently. -theorem Quadrilateral.IsPrg_nd_redef {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) (h: qdr.IsND) (h': qdr IsPrg) (h': (((QuadrilateralND.mk_nd h).angle₁.value.IsPos ∧ (QuadrilateralND.mk_nd h).angle₃.value.IsPos) ∨ ((QuadrilateralND.mk_nd h).angle₁.value.IsNeg ∧ (QuadrilateralND.mk_nd h).angle₃.value.IsNeg) ∨ ((QuadrilateralND.mk_nd h).angle₂.value.IsPos ∧ (QuadrilateralND.mk_nd h).angle₄.value.IsPos) ∨ ((QuadrilateralND.mk_nd h).angle₂.value.IsNeg ∧ (QuadrilateralND.mk_nd h).angle₄.value.IsNeg))) : (QuadrilateralND.mk_nd h).IsPrgND := sorry +theorem Quadrilateral.IsPrg_nd_redef {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) (h: qdr.IsND) (h': qdr IsPrg) (h': (((QuadrilateralND.mk_nd h).angle₁.value.IsPos ∧ (QuadrilateralND.mk_nd h).angle₃.value.IsPos) ∨ ((QuadrilateralND.mk_nd h).angle₁.value.IsNeg ∧ (QuadrilateralND.mk_nd h).angle₃.value.IsNeg) ∨ ((QuadrilateralND.mk_nd h).angle₂.value.IsPos ∧ (QuadrilateralND.mk_nd h).angle₄.value.IsPos) ∨ ((QuadrilateralND.mk_nd h).angle₂.value.IsNeg ∧ (QuadrilateralND.mk_nd h).angle₄.value.IsNeg))) : (QuadrilateralND.mk_nd h).IsPrgND := sorry -theorem Parallelogram.parallelogramIs_nd_redef {P : Type _} [EuclideanPlane P] (prg : Parallelogram P) (h': prg.1.IsND) (k: ((QuadrilateralND.mk_nd h').angle₁.value.IsPos ∧ (QuadrilateralND.mk_nd h').angle₃.value.IsPos) ∨ ((QuadrilateralND.mk_nd h').angle₁.value.IsNeg ∧ (QuadrilateralND.mk_nd h').angle₃.value.IsNeg) ∨ ((QuadrilateralND.mk_nd h').angle₂.value.IsPos ∧ (QuadrilateralND.mk_nd h').angle₄.value.IsPos) ∨ ((QuadrilateralND.mk_nd h').angle₂.value.IsNeg ∧ (QuadrilateralND.mk_nd h').angle₄.value.IsNeg)) : (QuadrilateralND.mk_nd h').IsPrgND := sorry +theorem Parallelogram.parallelogramIs_nd_redef {P : Type*} [EuclideanPlane P] (prg : Parallelogram P) (h': prg.1.IsND) (k: ((QuadrilateralND.mk_nd h').angle₁.value.IsPos ∧ (QuadrilateralND.mk_nd h').angle₃.value.IsPos) ∨ ((QuadrilateralND.mk_nd h').angle₁.value.IsNeg ∧ (QuadrilateralND.mk_nd h').angle₃.value.IsNeg) ∨ ((QuadrilateralND.mk_nd h').angle₂.value.IsPos ∧ (QuadrilateralND.mk_nd h').angle₄.value.IsPos) ∨ ((QuadrilateralND.mk_nd h').angle₂.value.IsNeg ∧ (QuadrilateralND.mk_nd h').angle₄.value.IsNeg)) : (QuadrilateralND.mk_nd h').IsPrgND := sorry -/ section perm -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] variable (qdr : Quadrilateral P) variable (qdr_nd : QuadrilateralND P) variable (qdr_cvx : Quadrilateral_cvx P) @@ -219,7 +219,7 @@ end perm section flip -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] variable (qdr : Quadrilateral P) variable (qdr_nd : QuadrilateralND P) variable (qdr_cvx : Quadrilateral_cvx P) @@ -251,7 +251,7 @@ end flip section criteria_prgND_of_prg -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] variable (qdr_nd : QuadrilateralND P) variable (prg : Parallelogram P) @@ -288,7 +288,7 @@ end criteria_prgND_of_prg section criteria_prgND_of_qdrND -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] variable {A B C D : P} (nd : (QDR A B C D).IsND) variable (qdr : Quadrilateral P) (qdr_nd : QuadrilateralND P) @@ -330,12 +330,12 @@ end criteria_prgND_of_qdrND section criteria_prg_of_qdrND -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] variable {A B C D: P} variable (nd : (QDR A B C D).IsND) variable (cvx : (QDR A B C D).IsConvex) -variable {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) -variable {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) +variable {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) +variable {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) -- `why this theorem used two set of parallel and equal?` /-- If edgeND₁₂ and edgeND₃₄ of a QuadrilateralND are equal in value and parallel, and so do edgeND₁₄ and edgeND₂₃, then it is a parallelogram. -/ @@ -354,12 +354,12 @@ end criteria_prg_of_qdrND section criteria_prgND_of_qdrcvx -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] variable {A B C D : P} variable (nd : (QDR A B C D).IsND) variable (cvx : (QDR A B C D).IsConvex) -variable {P : Type _} [EuclideanPlane P] (qdr_cvx : Quadrilateral_cvx P) -variable {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) +variable {P : Type*} [EuclideanPlane P] (qdr_cvx : Quadrilateral_cvx P) +variable {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) /-- If edgeND₁₂ and edgeND₃₄ of a quadrilateral_cvx are parallel, and so do edgeND₁₄ and edgeND₂₃, then it is a parallelogram_nd. -/ theorem qdrcvx_is_prgND_of_parapara (h₁ : qdr_cvx.IsParaPara) : qdr_cvx.IsPrgND := by sorry @@ -387,10 +387,10 @@ end criteria_prgND_of_qdrcvx section property -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] variable {A B C D : P} -variable {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) -variable {P : Type _} [EuclideanPlane P] (prg : Parallelogram P) +variable {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) +variable {P : Type*} [EuclideanPlane P] (prg : Parallelogram P) /-- The lengths of segments point₁ point₂ and point₃ point₄ in a parallelogram are equal. -/ theorem eq_length_of_isPrg : (prg.edge₁₂).length = (prg.edge₃₄).length := by sorry @@ -415,10 +415,10 @@ end property section property_nd -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] variable {A B C D : P} -variable {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) -variable {P : Type _} [EuclideanPlane P] (prg_nd : ParallelogramND P) +variable {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) +variable {P : Type*} [EuclideanPlane P] (prg_nd : ParallelogramND P) /-- In a parallelogram_nd, edgeND₁₂ and edge₃₄ are parallel. -/ theorem para_of_isPrgND : prg_nd.edgeND₁₂ ∥ prg_nd.edgeND₃₄ := (prg_nd.parapara_iff_para_para.mp prg_nd.parapara_of_prgnd).left diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_old.lean b/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_old.lean index afdc5a6d4..a3c62b87f 100644 --- a/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_old.lean +++ b/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_old.lean @@ -34,7 +34,7 @@ In this section we define two types of parallelogram. 'parallel_nd' deals with t -/ @[pp_dot] -structure Quadrilateral_nd.Parallelogram_GPt {P : Type _} [EuclideanPlane P] (qdr_nd : Quadrilateral_nd P) : Prop where +structure Quadrilateral_nd.Parallelogram_GPt {P : Type*} [EuclideanPlane P] (qdr_nd : Quadrilateral_nd P) : Prop where not_collinear₁₂₃: ( ¬ Collinear qdr_nd.point₁ qdr_nd.point₂ qdr_nd.point₃) not_collinear₂₃₄: ( ¬ Collinear qdr_nd.point₂ qdr_nd.point₃ qdr_nd.point₄) not_collinear₃₄₁: ( ¬ Collinear qdr_nd.point₃ qdr_nd.point₄ qdr_nd.point₁) @@ -42,18 +42,18 @@ structure Quadrilateral_nd.Parallelogram_GPt {P : Type _} [EuclideanPlane P] (qd /-- A quadrilateral is called parallelogram if VEC qdr.point₁ qdr.point₂ = VEC qdr.point₄ qdr.point₃.-/ @[pp_dot] -def Quadrilateral.IsParallelogram {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := VEC qdr.point₁ qdr.point₂ = VEC qdr.point₄ qdr.point₃ +def Quadrilateral.IsParallelogram {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := VEC qdr.point₁ qdr.point₂ = VEC qdr.point₄ qdr.point₃ /-- A quadrilateral satisfies IsParallelogram_para if two sets of opposite sides are parallel respectively. -/ @[pp_dot] -def QuadrilateralND.IsParallelogram_para {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := ( qdr_nd.edgeND₁₂ ∥ qdr_nd.edgeND₃₄) ∧ (qdr_nd.edgeND₁₄ ∥ qdr_nd.edgeND₂₃) +def QuadrilateralND.IsParallelogram_para {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := ( qdr_nd.edgeND₁₂ ∥ qdr_nd.edgeND₃₄) ∧ (qdr_nd.edgeND₁₄ ∥ qdr_nd.edgeND₂₃) /-- A quadrilateral satisfies IsParallelogram_nd if it satisfies both IsParallelogram_para and Parallelogram_GPt. It is now what we commonly call parallelogram.-/ @[pp_dot] -def QuadrilateralND.IsParallelogram_nd {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := qdr_nd.IsParallelogram_para ∧ qdr_nd.Parallelogram_non_triv +def QuadrilateralND.IsParallelogram_nd {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := qdr_nd.IsParallelogram_para ∧ qdr_nd.Parallelogram_non_triv @[pp_dot] -def Quadrilateral.IsParallelogram_nd {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by +def Quadrilateral.IsParallelogram_nd {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by by_cases h : qdr.IsND · exact (QuadrilateralND.mk_nd h).IsParallelogram_nd · exact False @@ -65,28 +65,28 @@ scoped postfix : 50 "IsParallelogram_nd" => QuadrilateralND.IsParallelogram_nd /-- We define parallelogram as a structure.-/ @[ext] -structure Parallelogram (P : Type _) [EuclideanPlane P] extends Quadrilateral P where +structure Parallelogram (P : Type*) [EuclideanPlane P] extends Quadrilateral P where is_parallelogram : toQuadrilateral IsParallelogram /-- We define parallelogram_nd as a structure.-/ @[ext] -structure Parallelogram_nd (P : Type _) [EuclideanPlane P] extends Quadrilateral_nd P, Parallelogram P where +structure Parallelogram_nd (P : Type*) [EuclideanPlane P] extends Quadrilateral_nd P, Parallelogram P where is_parallelogram_para : toQuadrilateral_nd IsParallelogram_para is_parallelogram_GPt : toQuadrilateral_nd IsParallelogram_GPt /-- We would also like to introduce a shortcut in proving statements concerning parallelograms - that is perm, the same technique used in Quadrilateral.lean. If qdr IsParallelogram, then its perm also IsParallelogram. -/ -theorem qdr_is_parallelogram_perm_iff (P : Type _) [EuclideanPlane P] (qdr : Quadrilateral P) :(qdr.IsParallelogram) ↔ ((qdr.perm).IsParallelogram) := by +theorem qdr_is_parallelogram_perm_iff (P : Type*) [EuclideanPlane P] (qdr : Quadrilateral P) :(qdr.IsParallelogram) ↔ ((qdr.perm).IsParallelogram) := by sorry /-- If qdr IsParallelogram_nd, then its perm also IsParallelogram_nd. -/ -theorem qdr_is_parallelogram_nd_perm_iff (P : Type _) [EuclideanPlane P] (qdr : Quadrilateral P) :(qdr.IsParallelogram_nd) ↔ ((qdr.perm).IsParallelogram_nd) := by +theorem qdr_is_parallelogram_nd_perm_iff (P : Type*) [EuclideanPlane P] (qdr : Quadrilateral P) :(qdr.IsParallelogram_nd) ↔ ((qdr.perm).IsParallelogram_nd) := by sorry /-- If qdr_nd IsParallelogram, then its perm also IsParallelogram. -/ -theorem qdr_nd_is_parallelogram_perm_iff (P : Type _) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) :(qdr_nd.IsParallelogram) ↔ ((qdr_nd.perm).IsParallelogram) := by sorry +theorem qdr_nd_is_parallelogram_perm_iff (P : Type*) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) :(qdr_nd.IsParallelogram) ↔ ((qdr_nd.perm).IsParallelogram) := by sorry /-- If qdr_nd IsParallelogram_nd, then its perm also IsParallelogram. -/ -theorem qdr_nd_is_parallelogram_nd_perm_iff (P : Type _) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) :(qdr_nd.IsParallelogram_nd) ↔ ((qdr_nd.perm).IsParallelogram_nd) := by +theorem qdr_nd_is_parallelogram_nd_perm_iff (P : Type*) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) :(qdr_nd.IsParallelogram_nd) ↔ ((qdr_nd.perm).IsParallelogram_nd) := by constructor intro h unfold QuadrilateralND.IsParallelogram_nd @@ -149,11 +149,11 @@ theorem qdr_nd_is_parallelogram_nd_perm_iff (P : Type _) [EuclideanPlane P] (qdr exact z /-- If prg IsParallelogram_nd, then its perm also IsParallelogram_nd. -/ -theorem prg_is_parallelogram_nd_perm_iff (P : Type _) [EuclideanPlane P] (prg : Parallelogram P) :(prg.IsParallelogram_nd) ↔ ((prg.perm).IsParallelogram_nd) := by +theorem prg_is_parallelogram_nd_perm_iff (P : Type*) [EuclideanPlane P] (prg : Parallelogram P) :(prg.IsParallelogram_nd) ↔ ((prg.perm).IsParallelogram_nd) := by sorry /-- If qdr_nd is non-degenerate and is a parallelogram, and its 1st, 2nd and 3rd points are not collinear, then qdr_nd is a parallelogram_nd.-/ -theorem Parallelogram_not_collinear₁₂₃ (P : Type _) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) (para: qdr_nd.1 IsParallelogram) (h: ¬ Collinear qdr_nd.point₁ qdr_nd.point₂ qdr_nd.point₃) : qdr_nd IsParallelogram_nd := by +theorem Parallelogram_not_collinear₁₂₃ (P : Type*) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) (para: qdr_nd.1 IsParallelogram) (h: ¬ Collinear qdr_nd.point₁ qdr_nd.point₂ qdr_nd.point₃) : qdr_nd IsParallelogram_nd := by have hba : qdr_nd.point₂ ≠ qdr_nd.point₁ := by unfold collinear at h @@ -312,24 +312,24 @@ theorem Parallelogram_not_collinear₁₂₃ (P : Type _) [EuclideanPlane P] (qd simp [Collinear.perm₂₁₃ m₇] at m₆ /-- If qdr_nd is non-degenerate and is a parallelogram, and its 2nd, 3rd and 4th points are not collinear, then qdr_nd is a parallelogram_nd.-/ -theorem Parallelogram_not_collinear₂₃₄ (P : Type _) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) (para: qdr_nd.1 IsParallelogram) (h: ¬ Collinear qdr_nd.point₂ qdr_nd.point₃ qdr_nd.point₄) : qdr_nd IsParallelogram_nd := by +theorem Parallelogram_not_collinear₂₃₄ (P : Type*) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) (para: qdr_nd.1 IsParallelogram) (h: ¬ Collinear qdr_nd.point₂ qdr_nd.point₃ qdr_nd.point₄) : qdr_nd IsParallelogram_nd := by sorry /-- If qdr_nd is non-degenerate and is a parallelogram, and its 3rd, 4th and 1st points are not collinear, then qdr_nd is a parallelogram_nd.-/ -theorem Parallelogram_not_collinear₃₄₁ (P : Type _) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) (para: qdr_nd.1 IsParallelogram) (h: ¬ Collinear qdr_nd.point₃ qdr_nd.point₄ qdr_nd.point₁) : qdr_nd IsParallelogram_nd := by +theorem Parallelogram_not_collinear₃₄₁ (P : Type*) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) (para: qdr_nd.1 IsParallelogram) (h: ¬ Collinear qdr_nd.point₃ qdr_nd.point₄ qdr_nd.point₁) : qdr_nd IsParallelogram_nd := by sorry /-- If qdr_nd is non-degenerate and is a parallelogram, and its 4th, 1st and 2nd points are not collinear, then qdr_nd is a parallelogram_nd.-/ -theorem Parallelogram_not_collinear₄₁₂ (P : Type _) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) (para: qdr_nd.1 IsParallelogram) (h: ¬ Collinear qdr_nd.point₄ qdr_nd.point₁ qdr_nd.point₂) : qdr_nd IsParallelogram_nd := by +theorem Parallelogram_not_collinear₄₁₂ (P : Type*) [EuclideanPlane P] (qdr_nd : QuadrilateralND P) (para: qdr_nd.1 IsParallelogram) (h: ¬ Collinear qdr_nd.point₄ qdr_nd.point₁ qdr_nd.point₂) : qdr_nd IsParallelogram_nd := by sorry /-- Make a parallelogram with 4 points on a plane.-/ -def Parallelogram.mk_pt_pt_pt_pt {P : Type _} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D) IsParallelogram) : Parallelogram P where +def Parallelogram.mk_pt_pt_pt_pt {P : Type*} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D) IsParallelogram) : Parallelogram P where toQuadrilateral := (QDR A B C D) is_parallelogram := h /-- Make a parallelogram_nd with 4 points on a plane, and using condition non_collinear₁₂₃.-/ -def Parallelogram_nd.mk_pt_pt_pt_pt₄ {P : Type _} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsParallelogram) (non_collinear₁₂₃: ¬ Collinear A B C) : Parallelogram_nd P where +def Parallelogram_nd.mk_pt_pt_pt_pt₄ {P : Type*} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsParallelogram) (non_collinear₁₂₃: ¬ Collinear A B C) : Parallelogram_nd P where toQuadrilateral := (QDR A B C D) is_parallelogram := h' nd := h @@ -337,7 +337,7 @@ def Parallelogram_nd.mk_pt_pt_pt_pt₄ {P : Type _} [EuclideanPlane P] (A B C D is_parallelogram_GPt := sorry /-- Make a parallelogram_nd with 4 points on a plane, and using condition non_collinear₂₃₄.-/ -def Parallelogram_nd.mk_pt_pt_pt_pt₁ {P : Type _} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsParallelogram) (non_collinear₂₃₄: ¬ Collinear B C D) : Parallelogram_nd P where +def Parallelogram_nd.mk_pt_pt_pt_pt₁ {P : Type*} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsParallelogram) (non_collinear₂₃₄: ¬ Collinear B C D) : Parallelogram_nd P where toQuadrilateral := (QDR A B C D) is_parallelogram := h' nd := h @@ -345,7 +345,7 @@ def Parallelogram_nd.mk_pt_pt_pt_pt₁ {P : Type _} [EuclideanPlane P] (A B C D is_parallelogram_GPt := sorry /-- Make a parallelogram_nd with 4 points on a plane, and using condition non_collinear₃₄₁.-/ -def Parallelogram_nd.mk_pt_pt_pt_pt₂ {P : Type _} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsParallelogram) (non_collinear₃₄₁: ¬ Collinear C D A) : Parallelogram_nd P where +def Parallelogram_nd.mk_pt_pt_pt_pt₂ {P : Type*} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsParallelogram) (non_collinear₃₄₁: ¬ Collinear C D A) : Parallelogram_nd P where toQuadrilateral := (QDR A B C D) is_parallelogram := h' nd := h @@ -353,7 +353,7 @@ def Parallelogram_nd.mk_pt_pt_pt_pt₂ {P : Type _} [EuclideanPlane P] (A B C D is_parallelogram_GPt := sorry /-- Make a parallelogram_nd with 4 points on a plane, and using condition non_collinear₄₁₂.-/ -def Parallelogram_nd.mk_pt_pt_pt_pt₃ {P : Type _} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsParallelogram) (non_collinear₄₁₂: ¬ Collinear D A B) : Parallelogram_nd P where +def Parallelogram_nd.mk_pt_pt_pt_pt₃ {P : Type*} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsParallelogram) (non_collinear₄₁₂: ¬ Collinear D A B) : Parallelogram_nd P where toQuadrilateral := (QDR A B C D) is_parallelogram := h' nd := h @@ -361,7 +361,7 @@ def Parallelogram_nd.mk_pt_pt_pt_pt₃ {P : Type _} [EuclideanPlane P] (A B C D is_parallelogram_GPt := sorry /-- Make a parallelogram_nd with 4 points on a plane.-/ -def Parallelogram_nd.mk_pt_pt_pt_pt {P : Type _} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsParallelogram) (non_collinear: (QuadrilateralND.mk_nd h) IsParallelogram_non_triv) : Parallelogram_nd P where +def Parallelogram_nd.mk_pt_pt_pt_pt {P : Type*} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) (h': (QDR A B C D) IsParallelogram) (non_collinear: (QuadrilateralND.mk_nd h) IsParallelogram_non_triv) : Parallelogram_nd P where toQuadrilateral := (QDR A B C D) is_parallelogram := h' nd := h @@ -376,12 +376,12 @@ scoped notation "PRG_nd₄" => Parallelogram_nd.mk_pt_pt_pt_pt₄ scoped notation "PRG_nd" => Parallelogram_nd.mk_pt_pt_pt_pt /-- Make parallelogram with a quadrilateral.-/ -def mk_parallelogram {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) : Parallelogram P where +def mk_parallelogram {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) : Parallelogram P where toQuadrilateral := qdr is_parallelogram := h /-- Make parallelogram_nd with a quadrilateral, using condition non_collinear₁₂₃.-/ -def mk_parallelogram_nd₄ {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) (h': qdr.IsND) (non_collinear₁₂₃: ¬ Collinear qdr.1 qdr.2 qdr.3) : Parallelogram_nd P where +def mk_parallelogram_nd₄ {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) (h': qdr.IsND) (non_collinear₁₂₃: ¬ Collinear qdr.1 qdr.2 qdr.3) : Parallelogram_nd P where toQuadrilateral := qdr is_parallelogram := h nd := h' @@ -389,7 +389,7 @@ def mk_parallelogram_nd₄ {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral is_parallelogram_GPt := sorry /-- Make parallelogram_nd with a quadrilateral, using condition non_collinear₂₃₄.-/ -def mk_parallelogram_nd₁ {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) (h': qdr.IsND) (non_collinear₂₃₄: ¬ Collinear qdr.2 qdr.3 qdr.4) : Parallelogram_nd P where +def mk_parallelogram_nd₁ {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) (h': qdr.IsND) (non_collinear₂₃₄: ¬ Collinear qdr.2 qdr.3 qdr.4) : Parallelogram_nd P where toQuadrilateral := qdr is_parallelogram := h nd := h' @@ -397,7 +397,7 @@ def mk_parallelogram_nd₁ {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral is_parallelogram_GPt := sorry /-- Make parallelogram_nd with a quadrilateral, using condition non_collinear₃₁₄.-/ -def mk_parallelogram_nd₂ {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) (h': qdr.IsND) (non_collinear₃₄₁: ¬ Collinear qdr.3 qdr.4 qdr.1) : Parallelogram_nd P where +def mk_parallelogram_nd₂ {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) (h': qdr.IsND) (non_collinear₃₄₁: ¬ Collinear qdr.3 qdr.4 qdr.1) : Parallelogram_nd P where toQuadrilateral := qdr is_parallelogram := h nd := h' @@ -405,7 +405,7 @@ def mk_parallelogram_nd₂ {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral is_parallelogram_GPt := sorry /-- Make parallelogram_nd with a quadrilateral, using condition non_collinear₄₁₂.-/ -def mk_parallelogram_nd₃ {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) (h': qdr.IsND) (non_collinear₄₁₂: ¬ Collinear qdr.4 qdr.1 qdr.2) : Parallelogram_nd P where +def mk_parallelogram_nd₃ {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) (h': qdr.IsND) (non_collinear₄₁₂: ¬ Collinear qdr.4 qdr.1 qdr.2) : Parallelogram_nd P where toQuadrilateral := qdr is_parallelogram := h nd := h' @@ -413,7 +413,7 @@ def mk_parallelogram_nd₃ {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral is_parallelogram_GPt := sorry /-- Make parallelogram_nd with a quadrilateral.-/ -def mk_parallelogram_nd {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) (h': qdr.IsND) (non_collinear: (QuadrilateralND.mk_nd h') IsParallelogram_non_triv) : Parallelogram_nd P where +def mk_parallelogram_nd {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr IsParallelogram) (h': qdr.IsND) (non_collinear: (QuadrilateralND.mk_nd h') IsParallelogram_non_triv) : Parallelogram_nd P where toQuadrilateral := qdr is_parallelogram := h nd := h' @@ -421,7 +421,7 @@ def mk_parallelogram_nd {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} is_parallelogram_GPt := sorry /-- Here is also a quite odd definition of a quadrilateral or parallelogram being parallelogram_nd, concerning angle being positive or negative. As it may be useful when discussing cclocks, it is reserved in form of the two theorems below.-/ -theorem Quadrilateral.IsParallelogram_nd_redef {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) (h: qdr.IsND) (h': qdr IsParallelogram) (h': (((QuadrilateralND.mk_nd h).angle₁.value.IsPos ∧ (QuadrilateralND.mk_nd h).angle₃.value.IsPos) ∨ ((QuadrilateralND.mk_nd h).angle₁.value.IsNeg ∧ (QuadrilateralND.mk_nd h).angle₃.value.IsNeg) ∨ ((QuadrilateralND.mk_nd h).angle₂.value.IsPos ∧ (QuadrilateralND.mk_nd h).angle₄.value.IsPos) ∨ ((QuadrilateralND.mk_nd h).angle₂.value.IsNeg ∧ (QuadrilateralND.mk_nd h).angle₄.value.IsNeg))) : (QuadrilateralND.mk_nd h) IsParallelogram_nd := sorry +theorem Quadrilateral.IsParallelogram_nd_redef {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) (h: qdr.IsND) (h': qdr IsParallelogram) (h': (((QuadrilateralND.mk_nd h).angle₁.value.IsPos ∧ (QuadrilateralND.mk_nd h).angle₃.value.IsPos) ∨ ((QuadrilateralND.mk_nd h).angle₁.value.IsNeg ∧ (QuadrilateralND.mk_nd h).angle₃.value.IsNeg) ∨ ((QuadrilateralND.mk_nd h).angle₂.value.IsPos ∧ (QuadrilateralND.mk_nd h).angle₄.value.IsPos) ∨ ((QuadrilateralND.mk_nd h).angle₂.value.IsNeg ∧ (QuadrilateralND.mk_nd h).angle₄.value.IsNeg))) : (QuadrilateralND.mk_nd h) IsParallelogram_nd := sorry /-- @@ -433,13 +433,13 @@ The route from qdr to parallelogram will not be seperated from the main discussi -/ @[pp_dot] -theorem Parallelogram.ParallelogramIs_nd_redef {P : Type _} [EuclideanPlane P] (qdr_para : Parallelogram P) (h': qdr_para.1.IsND) (k: ((QuadrilateralND.mk_nd h').angle₁.value.IsPos ∧ (QuadrilateralND.mk_nd h').angle₃.value.IsPos) ∨ ((QuadrilateralND.mk_nd h').angle₁.value.IsNeg ∧ (QuadrilateralND.mk_nd h').angle₃.value.IsNeg) ∨ ((QuadrilateralND.mk_nd h').angle₂.value.IsPos ∧ (QuadrilateralND.mk_nd h').angle₄.value.IsPos) ∨ ((QuadrilateralND.mk_nd h').angle₂.value.IsNeg ∧ (QuadrilateralND.mk_nd h').angle₄.value.IsNeg)) : (QuadrilateralND.mk_nd h') IsParallelogram_nd := sorry +theorem Parallelogram.ParallelogramIs_nd_redef {P : Type*} [EuclideanPlane P] (qdr_para : Parallelogram P) (h': qdr_para.1.IsND) (k: ((QuadrilateralND.mk_nd h').angle₁.value.IsPos ∧ (QuadrilateralND.mk_nd h').angle₃.value.IsPos) ∨ ((QuadrilateralND.mk_nd h').angle₁.value.IsNeg ∧ (QuadrilateralND.mk_nd h').angle₃.value.IsNeg) ∨ ((QuadrilateralND.mk_nd h').angle₂.value.IsPos ∧ (QuadrilateralND.mk_nd h').angle₄.value.IsPos) ∨ ((QuadrilateralND.mk_nd h').angle₂.value.IsNeg ∧ (QuadrilateralND.mk_nd h').angle₄.value.IsNeg)) : (QuadrilateralND.mk_nd h') IsParallelogram_nd := sorry -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] section criteria_prg_nd_of_qdr_nd -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] variable {A B C D : P} (nd : (QDR A B C D).IsND) (cvx : (QDR A B C D).IsConvex) variable (qdr : Quadrilateral P) (qdr_nd : QuadrilateralND P) (qdr_cvx : Quadrilateral_cvx P) @@ -610,8 +610,8 @@ section criteria_prg_of_qdr_nd variable {A B C D: P} variable (nd : (QDR A B C D).IsND) variable (cvx : (QDR A B C D).IsConvex) -variable {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) -variable {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) +variable {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) +variable {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) /-- Given QuadrilateralND qdr_nd, and qdr_nd.edgeND₁₂ ∥ qdr_nd.edgeND₃₄ and (qdr_nd.edgeND₁₂).length = (qdr_nd.edgeND₃₄).length, and qdr_nd.edgeND₁₄ ∥ qdr_nd.edgeND₂₃ and (qdr_nd.edgeND₁₄).length = (qdr_nd.edgeND₂₃).length, qdr_nd is a Parallelogram. -/ theorem qdr_nd_is_prg_of_para_eq_length_para_eq_length (h₁ : qdr_nd.edgeND₁₂ ∥ qdr_nd.edgeND₃₄) (h₂ : qdr_nd.edgeND₁₂.length = qdr_nd.edgeND₃₄.length) (H₁ : qdr_nd.edgeND₁₄ ∥ qdr_nd.edgeND₂₃) (h₂ : qdr_nd.edgeND₁₄.length = qdr_nd.edgeND₂₃.length): qdr_nd.IsParallelogram := by @@ -636,8 +636,8 @@ section criteria_prg_nd_of_qdr_cvx variable {A B C D: P} variable (nd : (QDR A B C D).IsND) variable (cvx : (QDR_nd A B C D nd).IsConvex) -variable {P : Type _} [EuclideanPlane P] (qdr_cvx : Quadrilateral_cvx P) -variable {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) +variable {P : Type*} [EuclideanPlane P] (qdr_cvx : Quadrilateral_cvx P) +variable {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) /-- Given Quadrilateral_cvx qdr_cvx, qdr_cvx.edgeND₁₂ ∥ qdr_cvx.edgeND₃₄ and qdr_cvx.edgeND₁₄ ∥ qdr_cvx.edgeND₂₃, then qdr_cvx is a Parallelogram_nd. -/ theorem qdr_cvx_is_prg_nd_of_para_para (h₁ : qdr_cvx.edgeND₁₂ ∥ qdr_cvx.edgeND₃₄) (h₂ : qdr_cvx.edgeND₁₄ ∥ qdr_cvx.edgeND₂₃) : qdr_cvx.IsParallelogram_nd := by @@ -1136,7 +1136,7 @@ end criteria_prg_nd_of_qdr_cvx section property variable {A B C D : P} -variable {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) +variable {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) /-- Given Quadrilateral qdr IsPRG_nd, Quadrilateral qdr IsConvex. -/ theorem is_convex_of_is_prg_nd (h : qdr.IsParallelogram_nd) : qdr.IsConvex := by @@ -1302,8 +1302,8 @@ end property section property_nd variable {A B C D : P} -variable {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) -variable {P : Type _} [EuclideanPlane P] (prg_nd : Parallelogram_nd P) +variable {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) +variable {P : Type*} [EuclideanPlane P] (prg_nd : Parallelogram_nd P) /-- Given Quadrilateral qdr IsPRG_nd, Quadrilateral qdr IsND. -/ diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_trash.lean b/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_trash.lean index aeaa69960..eb4a71dec 100644 --- a/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_trash.lean +++ b/EuclideanGeometry/Foundation/Construction/Polygon/Parallelogram_trash.lean @@ -2,7 +2,7 @@ import EuclideanGeometry.Foundation.Construction.Polygon.Parallelogram namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] theorem vec_eq_of_eq_dir_and_eq_length {A B C D : P} (h1 : B ≠ A) (h2 : D ≠ C) (h3 : (SEG_nd A B h1).toDir = (SEG_nd C D h2).toDir) (h4 : (SEG A B).length = (SEG C D).length) : VEC A B = VEC C D := by sorry diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/Quadrilateral.lean b/EuclideanGeometry/Foundation/Construction/Polygon/Quadrilateral.lean index 9259e36d6..83e64e0a6 100644 --- a/EuclideanGeometry/Foundation/Construction/Polygon/Quadrilateral.lean +++ b/EuclideanGeometry/Foundation/Construction/Polygon/Quadrilateral.lean @@ -32,7 +32,7 @@ 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 +structure Quadrilateral (P : Type*) [EuclideanPlane P] where point₁ : P point₂ : P point₃ : P @@ -42,7 +42,7 @@ structure Quadrilateral (P : Type _) [EuclideanPlane P] where scoped notation "QDR" => Quadrilateral.mk namespace Quadrilateral -variable {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} +variable {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} /-- Given a quadrilateral qdr, qdr.edge₁₂ is the edge from the first point to the second point of a quadrilateral. -/ @[pp_dot] @@ -102,7 +102,7 @@ end Quadrilateral A quadrilateral is called non-degenerate if the points that adjacent is not same -/ @[pp_dot] -structure Quadrilateral.IsND {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop where +structure Quadrilateral.IsND {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop where nd₁₂ : (qdr.2 ≠ qdr.1) nd₂₃ : (qdr.3 ≠ qdr.2) nd₃₄ : (qdr.4 ≠ qdr.3) @@ -112,17 +112,17 @@ structure Quadrilateral.IsND {P : Type _} [EuclideanPlane P] (qdr : Quadrilatera Class of nd Quadrilateral: A nd quadrilateral is quadrilateral with the property of nd. -/ @[ext] -structure QuadrilateralND (P : Type _) [EuclideanPlane P] extends Quadrilateral P where +structure QuadrilateralND (P : Type*) [EuclideanPlane P] extends Quadrilateral P where nd : toQuadrilateral.IsND -def QuadrilateralND.mk_pt_pt_pt_pt_nd {P : Type _} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) : QuadrilateralND P where +def QuadrilateralND.mk_pt_pt_pt_pt_nd {P : Type*} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsND) : QuadrilateralND P where toQuadrilateral := (QDR A B C D) nd := h scoped notation "QDR_nd" => QuadrilateralND.mk_pt_pt_pt_pt_nd /-- Given a property that a quadrilateral qdr is nd, this function returns qdr itself as an object in the class of nd quadrilateral -/ -def QuadrilateralND.mk_nd {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr.IsND) : QuadrilateralND P where +def QuadrilateralND.mk_nd {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr.IsND) : QuadrilateralND P where toQuadrilateral := qdr nd := h @@ -130,7 +130,7 @@ scoped notation "QDR_nd'" => QuadrilateralND.mk_nd /-- A quadrilateral satisfies InGPos if every 3 vertices are not collinear. -/ @[pp_dot] -structure Quadrilateral.InGPos {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop where +structure Quadrilateral.InGPos {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop where not_collinear₁₂₃: ( ¬ Collinear qdr.point₁ qdr.point₂ qdr.point₃) not_collinear₂₃₄: ( ¬ Collinear qdr.point₂ qdr.point₃ qdr.point₄) not_collinear₃₄₁: ( ¬ Collinear qdr.point₃ qdr.point₄ qdr.point₁) @@ -143,7 +143,7 @@ namespace QuadrilateralND section property_nd -- properties of nd quadrilateral `to be added` -variable {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) +variable {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) /-- The edge from the first point to the second point of a QuadrilateralND is non-degenerate. -/ instance nd₁₂ : PtNe qdr_nd.1.2 qdr_nd.1.1 := Fact.mk qdr_nd.nd.nd₁₂ @@ -253,14 +253,14 @@ theorem flip_angle₄_value_eq_neg_angle₂ : qdr_nd.flip.angle₄.value = - qdr end property_nd /-- A Quadrilateral which satisfies InGPos satisfies IsND. -/ -theorem nd_of_gpos {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (InGPos : qdr.InGPos): qdr.IsND:= by +theorem nd_of_gpos {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (InGPos : qdr.InGPos): qdr.IsND:= by constructor · exact (ne_of_not_collinear InGPos.not_collinear₁₂₃).right.right · exact (ne_of_not_collinear InGPos.not_collinear₂₃₄).right.right · exact (ne_of_not_collinear InGPos.not_collinear₃₄₁).right.right · exact (ne_of_not_collinear InGPos.not_collinear₄₁₂).right.right.symm -instance {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} : Coe qdr.InGPos qdr.IsND := {coe := nd_of_gpos} +instance {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} : Coe qdr.InGPos qdr.IsND := {coe := nd_of_gpos} end QuadrilateralND @@ -268,16 +268,16 @@ end QuadrilateralND A Quadrilateral is called convex if it's ND and four angles have the same sign. -/ -- @[pp_dot] --- def QuadrilateralND.IsConvex {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := (qdr_nd.angle₁.value.IsPos ∧ qdr_nd.angle₂.value.IsPos ∧ qdr_nd.angle₃.value.IsPos ∧ qdr_nd.angle₄.value.IsPos) ∨ (qdr_nd.angle₁.value.IsNeg ∧ qdr_nd.angle₂.value.IsNeg ∧ qdr_nd.angle₃.value.IsNeg ∧ qdr_nd.angle₄.value.IsNeg) +-- def QuadrilateralND.IsConvex {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : Prop := (qdr_nd.angle₁.value.IsPos ∧ qdr_nd.angle₂.value.IsPos ∧ qdr_nd.angle₃.value.IsPos ∧ qdr_nd.angle₄.value.IsPos) ∨ (qdr_nd.angle₁.value.IsNeg ∧ qdr_nd.angle₂.value.IsNeg ∧ qdr_nd.angle₃.value.IsNeg ∧ qdr_nd.angle₄.value.IsNeg) -- @[pp_dot] --- def Quadrilateral.IsConvex {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by +-- def Quadrilateral.IsConvex {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by -- by_cases h : qdr.IsND -- · exact (QuadrilateralND.mk_nd h).IsConvex -- · exact False @[pp_dot] -def Quadrilateral.IsConvex {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by +def Quadrilateral.IsConvex {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by by_cases h : qdr.IsND · have qdr_nd : QuadrilateralND P := QDR_nd' h exact (qdr_nd.angle₁.value.IsPos ∧ qdr_nd.angle₂.value.IsPos ∧ qdr_nd.angle₃.value.IsPos ∧ qdr_nd.angle₄.value.IsPos) ∨ (qdr_nd.angle₁.value.IsNeg ∧ qdr_nd.angle₂.value.IsNeg ∧ qdr_nd.angle₃.value.IsNeg ∧ qdr_nd.angle₄.value.IsNeg) @@ -285,51 +285,51 @@ def Quadrilateral.IsConvex {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral scoped postfix : 50 "IsConvex" => Quadrilateral.IsConvex -theorem Quadrilateral.isND_of_is_convex {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr.IsConvex) : qdr.IsND := by +theorem Quadrilateral.isND_of_is_convex {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr.IsConvex) : qdr.IsND := by by_contra g unfold Quadrilateral.IsConvex at h simp only [g, dite_false] at h -instance {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} : Coe qdr.IsConvex qdr.IsND := {coe := Quadrilateral.isND_of_is_convex} +instance {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} : Coe qdr.IsConvex qdr.IsND := {coe := Quadrilateral.isND_of_is_convex} --- theorem QuadrilateralND.toqdr_cvx_of_cvx {P : Type _} [EuclideanPlane P] {qdr_nd : QuadrilateralND P} (h : qdr_nd.IsConvex) : qdr_nd.toQuadrilateral.IsConvex := by +-- theorem QuadrilateralND.toqdr_cvx_of_cvx {P : Type*} [EuclideanPlane P] {qdr_nd : QuadrilateralND P} (h : qdr_nd.IsConvex) : qdr_nd.toQuadrilateral.IsConvex := by -- have k : qdr_nd.toQuadrilateral.IsND := qdr_nd.nd -- have l : qdr_nd = (QDR_nd' k) := rfl -- rw [l] at h -- unfold Quadrilateral.IsConvex -- simp only [k, h, dite_eq_ite, ite_true] --- instance {P : Type _} [EuclideanPlane P] {qdr_nd : QuadrilateralND P} : Coe qdr_nd.IsConvex qdr_nd.toQuadrilateral.IsConvex := {coe := QuadrilateralND.toqdr_cvx_of_cvx} +-- instance {P : Type*} [EuclideanPlane P] {qdr_nd : QuadrilateralND P} : Coe qdr_nd.IsConvex qdr_nd.toQuadrilateral.IsConvex := {coe := QuadrilateralND.toqdr_cvx_of_cvx} -theorem Quadrilateral.nd_cvx_iff_cvx {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : qdr_nd.IsConvex ↔ (qdr_nd.angle₁.value.IsPos ∧ qdr_nd.angle₂.value.IsPos ∧ qdr_nd.angle₃.value.IsPos ∧ qdr_nd.angle₄.value.IsPos) ∨ (qdr_nd.angle₁.value.IsNeg ∧ qdr_nd.angle₂.value.IsNeg ∧ qdr_nd.angle₃.value.IsNeg ∧ qdr_nd.angle₄.value.IsNeg) := by +theorem Quadrilateral.nd_cvx_iff_cvx {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : qdr_nd.IsConvex ↔ (qdr_nd.angle₁.value.IsPos ∧ qdr_nd.angle₂.value.IsPos ∧ qdr_nd.angle₃.value.IsPos ∧ qdr_nd.angle₄.value.IsPos) ∨ (qdr_nd.angle₁.value.IsNeg ∧ qdr_nd.angle₂.value.IsNeg ∧ qdr_nd.angle₃.value.IsNeg ∧ qdr_nd.angle₄.value.IsNeg) := by unfold Quadrilateral.IsConvex have nd : qdr_nd.toQuadrilateral.IsND := qdr_nd.nd simp only [nd, dite_true] rfl -theorem Quadrilateral_cvx.nd_is_convex_iff_is_convex {P : Type _} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : qdr_nd.IsConvex ↔ qdr_nd.toQuadrilateral.IsConvex := by +theorem Quadrilateral_cvx.nd_is_convex_iff_is_convex {P : Type*} [EuclideanPlane P] (qdr_nd : QuadrilateralND P) : qdr_nd.IsConvex ↔ qdr_nd.toQuadrilateral.IsConvex := by unfold Quadrilateral.IsConvex simp only [qdr_nd.nd, dite_true] -instance {P : Type _} [EuclideanPlane P] {qdr_nd : QuadrilateralND P} : Coe qdr_nd.IsConvex qdr_nd.toQuadrilateral.IsConvex := {coe := (Quadrilateral_cvx.nd_is_convex_iff_is_convex qdr_nd).mp} +instance {P : Type*} [EuclideanPlane P] {qdr_nd : QuadrilateralND P} : Coe qdr_nd.IsConvex qdr_nd.toQuadrilateral.IsConvex := {coe := (Quadrilateral_cvx.nd_is_convex_iff_is_convex qdr_nd).mp} -instance {P : Type _} [EuclideanPlane P] {qdr_nd : QuadrilateralND P} : Coe qdr_nd.toQuadrilateral.IsConvex qdr_nd.IsConvex := {coe := (Quadrilateral_cvx.nd_is_convex_iff_is_convex qdr_nd).mpr} +instance {P : Type*} [EuclideanPlane P] {qdr_nd : QuadrilateralND P} : Coe qdr_nd.toQuadrilateral.IsConvex qdr_nd.IsConvex := {coe := (Quadrilateral_cvx.nd_is_convex_iff_is_convex qdr_nd).mpr} /-- Class of Convex Quadrilateral: A convex quadrilateral is quadrilateral with the property of convex. -/ @[ext] -structure Quadrilateral_cvx (P : Type _) [EuclideanPlane P] extends QuadrilateralND P where +structure Quadrilateral_cvx (P : Type*) [EuclideanPlane P] extends QuadrilateralND P where convex : toQuadrilateral.IsConvex -def Quadrilateral_cvx.mk_pt_pt_pt_pt_convex {P : Type _} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsConvex) : Quadrilateral_cvx P where +def Quadrilateral_cvx.mk_pt_pt_pt_pt_convex {P : Type*} [EuclideanPlane P] (A B C D : P) (h : (QDR A B C D).IsConvex) : Quadrilateral_cvx P where toQuadrilateral := (QDR A B C D) nd := h convex := h scoped notation "QDR_cvx" => Quadrilateral_cvx.mk_pt_pt_pt_pt_convex -def Quadrilateral_cvx.mk_cvx {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr.IsConvex) : Quadrilateral_cvx P where +def Quadrilateral_cvx.mk_cvx {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr.IsConvex) : Quadrilateral_cvx P where toQuadrilateralND := QDR_nd' h convex := h @@ -337,15 +337,15 @@ scoped notation "QDR_cvx'" => Quadrilateral_cvx.mk_cvx namespace Quadrilateral_cvx --- def mk_is_convex {P : Type _} [EuclideanPlane P] {A B C D : P} (h : (QDR A B C D).IsConvex) : Quadrilateral_cvx P := mk_pt_pt_pt_pt_convex A B C D h +-- def mk_is_convex {P : Type*} [EuclideanPlane P] {A B C D : P} (h : (QDR A B C D).IsConvex) : Quadrilateral_cvx P := mk_pt_pt_pt_pt_convex A B C D h -- /-- Given a property that a quadrilateral qdr is convex, this function returns qdr itself as an object in the class of convex quadrilateral-/ --- def mk_nd_is_convex {P : Type _} [EuclideanPlane P] {qdr_nd : QuadrilateralND P} (h : qdr_nd.IsConvex) : Quadrilateral_cvx P where +-- def mk_nd_is_convex {P : Type*} [EuclideanPlane P] {qdr_nd : QuadrilateralND P} (h : qdr_nd.IsConvex) : Quadrilateral_cvx P where -- toQuadrilateralND := qdr_nd -- convex := h section criteria_cvx -variable {P : Type _} [EuclideanPlane P] {A B C D : P} +variable {P : Type*} [EuclideanPlane P] {A B C D : P} structure is_convex_of_three_sides_of_same_side' where qdr_nd : QuadrilateralND P @@ -389,7 +389,7 @@ end criteria_cvx section property_cvx -- properties of convex quadrilateral `to be added` -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] variable (qdr : Quadrilateral P) variable (qdr_nd : QuadrilateralND P) variable (qdr_cvx : Quadrilateral_cvx P) @@ -573,7 +573,7 @@ end Quadrilateral_cvx section criteria -- the criteria of a quadrilateral being convex `to be added` -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] end criteria diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/Rectangle.lean b/EuclideanGeometry/Foundation/Construction/Polygon/Rectangle.lean index 7e197a8e8..7f4909710 100644 --- a/EuclideanGeometry/Foundation/Construction/Polygon/Rectangle.lean +++ b/EuclideanGeometry/Foundation/Construction/Polygon/Rectangle.lean @@ -7,6 +7,6 @@ noncomputable section namespace EuclidGeom @[ext] -structure Rectangle (P : Type _) [EuclideanPlane P] extends Parallelogram P where +structure Rectangle (P : Type*) [EuclideanPlane P] extends Parallelogram P where end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/Rhombus.lean b/EuclideanGeometry/Foundation/Construction/Polygon/Rhombus.lean index 771543700..1019c15b4 100644 --- a/EuclideanGeometry/Foundation/Construction/Polygon/Rhombus.lean +++ b/EuclideanGeometry/Foundation/Construction/Polygon/Rhombus.lean @@ -7,6 +7,6 @@ noncomputable section namespace EuclidGeom @[ext] -structure Rhombus (P : Type _) [EuclideanPlane P] extends Parallelogram P where +structure Rhombus (P : Type*) [EuclideanPlane P] extends Parallelogram P where end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/Square.lean b/EuclideanGeometry/Foundation/Construction/Polygon/Square.lean index 5f77f8a8f..6041b074c 100644 --- a/EuclideanGeometry/Foundation/Construction/Polygon/Square.lean +++ b/EuclideanGeometry/Foundation/Construction/Polygon/Square.lean @@ -8,6 +8,6 @@ noncomputable section namespace EuclidGeom @[ext] -structure Square (P : Type _) [EuclideanPlane P] extends Rhombus P, Rectangle P +structure Square (P : Type*) [EuclideanPlane P] extends Rhombus P, Rectangle P end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Construction/Polygon/Trapezoid.lean b/EuclideanGeometry/Foundation/Construction/Polygon/Trapezoid.lean index 18037cf42..50bb5529e 100644 --- a/EuclideanGeometry/Foundation/Construction/Polygon/Trapezoid.lean +++ b/EuclideanGeometry/Foundation/Construction/Polygon/Trapezoid.lean @@ -7,6 +7,6 @@ noncomputable section namespace EuclidGeom @[ext] -structure Trapezoid (P : Type _) [EuclideanPlane P] extends Quadrilateral_cvx P where +structure Trapezoid (P : Type*) [EuclideanPlane P] extends Quadrilateral_cvx P where end EuclidGeom diff --git a/EuclideanGeometry/Foundation/Construction/Triangle/AngleBisector.lean b/EuclideanGeometry/Foundation/Construction/Triangle/AngleBisector.lean index 544ec0065..117407da4 100644 --- a/EuclideanGeometry/Foundation/Construction/Triangle/AngleBisector.lean +++ b/EuclideanGeometry/Foundation/Construction/Triangle/AngleBisector.lean @@ -14,7 +14,7 @@ namespace EuclidGeom open AngValue Angle -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] -- Feel free to change the name of the theorems and comments into better ones, or add sections to better organize theorems. -- `Currently, the theorems are not well-organized, please follow the plan file to write and add theorems in this file into the plan file if they are not already in the plan` diff --git a/EuclideanGeometry/Foundation/Construction/Triangle/Centroid.lean b/EuclideanGeometry/Foundation/Construction/Triangle/Centroid.lean index 58801fa23..85619ccc3 100644 --- a/EuclideanGeometry/Foundation/Construction/Triangle/Centroid.lean +++ b/EuclideanGeometry/Foundation/Construction/Triangle/Centroid.lean @@ -6,7 +6,7 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.Basic noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] def TriangleND.Median1 (tr_nd : TriangleND P) : SegND P := sorry diff --git a/EuclideanGeometry/Foundation/Construction/Triangle/Orthocenter.lean b/EuclideanGeometry/Foundation/Construction/Triangle/Orthocenter.lean index f04b18f3b..846da6934 100644 --- a/EuclideanGeometry/Foundation/Construction/Triangle/Orthocenter.lean +++ b/EuclideanGeometry/Foundation/Construction/Triangle/Orthocenter.lean @@ -6,7 +6,7 @@ import EuclideanGeometry.Foundation.Axiom.Triangle.Basic noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] def TriangleND.Height1 (tr_nd : TriangleND P) : SegND P := sorry diff --git a/EuclideanGeometry/Foundation/Construction/Triangle/PerpendicularBisector.lean b/EuclideanGeometry/Foundation/Construction/Triangle/PerpendicularBisector.lean index a98caa2ef..27238406e 100644 --- a/EuclideanGeometry/Foundation/Construction/Triangle/PerpendicularBisector.lean +++ b/EuclideanGeometry/Foundation/Construction/Triangle/PerpendicularBisector.lean @@ -8,7 +8,7 @@ import EuclideanGeometry.Foundation.Axiom.Circle.Basic noncomputable section namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] structure IsPerpBis (seg_nd : SegND P) (line : Line P) : Prop where diff --git a/EuclideanGeometry/Foundation/Tactic/Collinear/perm_collinear.lean b/EuclideanGeometry/Foundation/Tactic/Collinear/perm_collinear.lean index 4f2cedaaf..4c092a989 100644 --- a/EuclideanGeometry/Foundation/Tactic/Collinear/perm_collinear.lean +++ b/EuclideanGeometry/Foundation/Tactic/Collinear/perm_collinear.lean @@ -4,7 +4,7 @@ namespace EuclidGeom open Lean Lean.Meta Lean.Elab Lean.Elab.Tactic Qq -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] def extractCollinear (expr : Q(Prop)) : MetaM (Option Expr) := match expr with diff --git a/EuclideanGeometry/Foundation/Tactic/Congruence/Congruence.lean b/EuclideanGeometry/Foundation/Tactic/Congruence/Congruence.lean index d7eb079d5..8da84e155 100644 --- a/EuclideanGeometry/Foundation/Tactic/Congruence/Congruence.lean +++ b/EuclideanGeometry/Foundation/Tactic/Congruence/Congruence.lean @@ -113,7 +113,7 @@ end acongr section examples -variable {P : Type _} [EuclideanPlane P] {tr_nd₁ tr_nd₂ : TriangleND P} +variable {P : Type*} [EuclideanPlane P] {tr_nd₁ tr_nd₂ : TriangleND P} example (a₁ : tr_nd₁.angle₁.value = tr_nd₂.angle₁.value) (e₂ : tr_nd₁.edge₂.length = tr_nd₂.edge₂.length) (e₃ : tr_nd₁.edge₃.length = tr_nd₂.edge₃.length) : tr_nd₁.IsCongr tr_nd₂ := by diff --git a/EuclideanGeometry/Foundation/Tactic/PointNe/Ptne.lean b/EuclideanGeometry/Foundation/Tactic/PointNe/Ptne.lean index a01acc1e6..442070568 100644 --- a/EuclideanGeometry/Foundation/Tactic/PointNe/Ptne.lean +++ b/EuclideanGeometry/Foundation/Tactic/PointNe/Ptne.lean @@ -7,7 +7,7 @@ namespace EuclidGeom /- congruences of triangles, separate definitions for reversing orientation or not, (requiring all sides and angles being the same)-/ -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] diff --git a/EuclideanGeometry/Unused/Class_old.lean b/EuclideanGeometry/Unused/Class_old.lean index b31ce66fe..3be0bb434 100644 --- a/EuclideanGeometry/Unused/Class_old.lean +++ b/EuclideanGeometry/Unused/Class_old.lean @@ -5,24 +5,24 @@ import EuclideanGeometry.Foundation.Axiom.Basic.Plane noncomputable section namespace EuclidGeom --- class PlaneFigure (P: Type _) [EuclideanPlane P] (α : Type _) where +-- class PlaneFigure (P: Type*) [EuclideanPlane P] (α : Type*) where -class Carrier (P: Type _) [EuclideanPlane P] (α : Type _) where +class Carrier (P: Type*) [EuclideanPlane P] (α : Type*) where carrier : α → Set P -class Interior (P: Type _) [EuclideanPlane P] (α : Type _) where +class Interior (P: Type*) [EuclideanPlane P] (α : Type*) where interior : α → Set P -def lies_on {P : Type _} [EuclideanPlane P] {α : Type _} [Carrier P α] (A : P) (F : α) := A ∈ (Carrier.carrier F) +def lies_on {P : Type*} [EuclideanPlane P] {α : Type*} [Carrier P α] (A : P) (F : α) := A ∈ (Carrier.carrier F) -def lies_int {P : Type _} [EuclideanPlane P] {α : Type _} [Interior P α] (A : P) (F : α) := A ∈ (Interior.interior F) +def lies_int {P : Type*} [EuclideanPlane P] {α : Type*} [Interior P α] (A : P) (F : α) := A ∈ (Interior.interior F) --- def lies_in {P : Type _} [EuclideanPlane P] {α : Type _} [Carrier P α] [Interior P α] (A : P) (F : α) : Prop := lies_int A F ∨ lies_on A F +-- def lies_in {P : Type*} [EuclideanPlane P] {α : Type*} [Carrier P α] [Interior P α] (A : P) (F : α) : Prop := lies_int A F ∨ lies_on A F -def is_inx {P : Type _} [EuclideanPlane P] {α β: Type _} [Carrier P α] [Carrier P β] (A : P) (F : α) (G : β) := A ∈ (Carrier.carrier F) ∧ A ∈ (Carrier.carrier G) +def is_inx {P : Type*} [EuclideanPlane P] {α β: Type*} [Carrier P α] [Carrier P β] (A : P) (F : α) (G : β) := A ∈ (Carrier.carrier F) ∧ A ∈ (Carrier.carrier G) -theorem is_inx.symm {P : Type _} [EuclideanPlane P] {α β: Type _} [Carrier P α] [Carrier P β] {A : P} {F : α} {G : β} (h : is_inx A F G) : is_inx A G F := And.symm h +theorem is_inx.symm {P : Type*} [EuclideanPlane P] {α β: Type*} [Carrier P α] [Carrier P β] {A : P} {F : α} {G : β} (h : is_inx A F G) : is_inx A G F := And.symm h scoped infix : 50 " LiesOn " => lies_on scoped infix : 50 " LiesInt " => lies_int @@ -31,21 +31,21 @@ scoped infix : 50 " LiesInt " => lies_int section compatibility -theorem ne_of_lieson_and_not_lieson {P : Type _} [EuclideanPlane P] {α : Type _} [Carrier P α] {F : α} {X Y : P} (hx : X LiesOn F) (hy : ¬ Y LiesOn F) : X ≠ Y := by +theorem ne_of_lieson_and_not_lieson {P : Type*} [EuclideanPlane P] {α : Type*} [Carrier P α] {F : α} {X Y : P} (hx : X LiesOn F) (hy : ¬ Y LiesOn F) : X ≠ Y := by by_contra h rw [h] at hx tauto -theorem ne_of_liesint_and_not_liesint {P : Type _} [EuclideanPlane P] {α : Type _} [Interior P α] {F : α} {X Y : P} (hx : X LiesInt F) (hy : ¬ Y LiesInt F) : X ≠ Y := by +theorem ne_of_liesint_and_not_liesint {P : Type*} [EuclideanPlane P] {α : Type*} [Interior P α] {F : α} {X Y : P} (hx : X LiesInt F) (hy : ¬ Y LiesInt F) : X ≠ Y := by by_contra h rw [h] at hx tauto end compatibility /- Three figures concurrent at a point -/ -def concurrent {P : Type _} [EuclideanPlane P] {α β γ: Type _} [Carrier P α] [Carrier P β] [Carrier P γ] (A : P) (F : α) (G : β) (H : γ) : Prop := A LiesOn F ∧ A LiesOn G ∧ A LiesOn H +def concurrent {P : Type*} [EuclideanPlane P] {α β γ: Type*} [Carrier P α] [Carrier P β] [Carrier P γ] (A : P) (F : α) (G : β) (H : γ) : Prop := A LiesOn F ∧ A LiesOn G ∧ A LiesOn H -class Convex2D (P: Type _) [EuclideanPlane P] (α : Type _) extends (Carrier P α), (Interior P α) where +class Convex2D (P: Type*) [EuclideanPlane P] (α : Type*) extends (Carrier P α), (Interior P α) where convexity : ∀ (F : α) (A B : P), (A LiesOn F) → (B LiesOn F) → ∃ (t : ℝ), t • (B -ᵥ A) +ᵥ A LiesOn F int_of_carrier : ∀ (F : α) (A : P), (A LiesInt F) → ∃ (B₁ B₂ B₃ : P) (t₁ t₂ t₃ : ℝ), (B₁ LiesOn F) ∧ (B₂ LiesOn F) ∧ (B₃ LiesOn F) ∧ (0 < t₁) ∧ (0 < t₂) ∧ (0 < t₃) ∧ (t₁ • VEC A B₁ + t₂ • VEC A B₂ + t₃ • VEC A B₃ = 0) diff --git a/EuclideanGeometry/Unused/Congruence.lean b/EuclideanGeometry/Unused/Congruence.lean index af52f3cac..a46c32ea7 100644 --- a/EuclideanGeometry/Unused/Congruence.lean +++ b/EuclideanGeometry/Unused/Congruence.lean @@ -13,7 +13,7 @@ namespace EuclidGeom /- congruences of triangles, separate definitions for reversing orientation or not, (requiring all sides and angles being the same)-/ -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] -- only define congrence for TriangleND --def IsCongr (tr_nd₁ tr_nd₂: TriangleND P) : Prop := (tr_nd₁.1.edge₁.length = tr_nd₂.1.edge₁.length ∧ tr_nd₁.1.edge₂.length = tr_nd₂.1.edge₂.length ∧ tr_nd₁.1.edge₃.length = tr_nd₂.1.edge₃.length ∧ tr_nd₁.angle₁.value = tr_nd₂.angle₁.value ∧ tr_nd₁.angle₂.value = tr_nd₂.angle₂.value ∧ tr_nd₁.angle₃.value = tr_nd₂.angle₃.value) def IsCongr (tr₁ tr₂: Triangle P) : Prop := by diff --git a/EuclideanGeometry/Unused/Line.lean b/EuclideanGeometry/Unused/Line.lean index 186216a78..93e0afafb 100644 --- a/EuclideanGeometry/Unused/Line.lean +++ b/EuclideanGeometry/Unused/Line.lean @@ -4,7 +4,7 @@ noncomputable section namespace EuclidGeom @[ext] -class Line (P : Type _) [EuclideanPlane P] where +class Line (P : Type*) [EuclideanPlane P] where carrier : Set P linear : ∀ (A B C : P), (A ∈ carrier) → (B ∈ carrier) → (C ∈ carrier) → Collinear A B C maximal : ∀ (A B : P), (A ∈ carrier) → (B ∈ carrier) → (B ≠ A) → (∀ (C : P), Collinear A B C → (C ∈ carrier)) @@ -12,7 +12,7 @@ class Line (P : Type _) [EuclideanPlane P] where namespace Line -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] -- define a line from two points @@ -71,7 +71,7 @@ scoped notation "LIN" => Line.mk_pt_pt namespace Line -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] /- Def of point lies on a line, LiesInt is not defined -/ protected def IsOn (a : P) (l : Line P) : Prop := @@ -83,7 +83,7 @@ instance : Carrier P (Line P) where end Line -- Now we introduce useful theorems to avoid using more unfolds in further proofs. -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] section Compaitiblity_of_coercions_of_mk_pt_pt diff --git a/EuclideanGeometry/Unused/Parallel.lean b/EuclideanGeometry/Unused/Parallel.lean index 70a113509..b8e39c674 100644 --- a/EuclideanGeometry/Unused/Parallel.lean +++ b/EuclideanGeometry/Unused/Parallel.lean @@ -3,14 +3,14 @@ import EuclideanGeometry.Foundation.Axiom.Linear.Line noncomputable section namespace EuclidGeom -inductive LinearObj (P : Type _) [EuclideanPlane P] where +inductive LinearObj (P : Type*) [EuclideanPlane P] where | vec_nd (v : VecND) | dir (v : Dir) | ray (r : Ray P) | seg_nd (s : SegND P) | line (l : Line P) -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] section coercion @@ -61,9 +61,9 @@ scoped infix : 50 " LiesOnarObj " => LinearObj.IsOnLinearObj -- Our definition of parallel for LinearObj is very general. Not only can it apply to different types of Objs, but also include degenerate cases, such as ⊆(inclusions), =(equal). -def Parallel' {α β: Type _} (l₁ : α) (l₂ : β) [Coe α (LinearObj P)] [Coe β (LinearObj P)] : Prop := LinearObj.toProj (P := P) (Coe.coe l₁) = LinearObj.toProj (P := P) (Coe.coe l₂) +def Parallel' {α β: Type*} (l₁ : α) (l₂ : β) [Coe α (LinearObj P)] [Coe β (LinearObj P)] : Prop := LinearObj.toProj (P := P) (Coe.coe l₁) = LinearObj.toProj (P := P) (Coe.coe l₂) --- class PlaneFigure' (P : Type _) [EuclideanPlane P] {α : Type _} where +-- class PlaneFigure' (P : Type*) [EuclideanPlane P] {α : Type*} where -- instance : PlaneFigure' P (LinearObj P) where diff --git a/EuclideanGeometry/Unused/Parallelogram.lean b/EuclideanGeometry/Unused/Parallelogram.lean index 319900a3c..9252bcfef 100644 --- a/EuclideanGeometry/Unused/Parallelogram.lean +++ b/EuclideanGeometry/Unused/Parallelogram.lean @@ -6,14 +6,14 @@ import EuclideanGeometry.Foundation.Construction.Polygon.Quadrilateral noncomputable section namespace EuclidGeom -class Parallelogram (P : Type _) [EuclideanPlane P] extends Quadrilateral_cvx P where +class Parallelogram (P : Type*) [EuclideanPlane P] extends Quadrilateral_cvx P where para : LinearObj.seg_nd toQuadrilateral_cvx.edgeND₁₂ ∥ toQuadrilateral_cvx.edgeND₃₄ para' : LinearObj.seg_nd toQuadrilateral_cvx.edgeND₂₃ ∥ toQuadrilateral_cvx.edgeND₄₁ /- section make namespace Parallelogram -/- +/- construct parallelgram from (protected def) 1. a point and 2 VecND that is not parallel 2. 3 point that is not collinear @@ -23,19 +23,19 @@ end Parallelogram end make -/ -def Quadrilateral_cvx.is_parallelogram {P : Type _} [EuclideanPlane P] (qdr_cvx : Quadrilateral_cvx P) : Prop := (LinearObj.seg_nd qdr_cvx.edgeND₁₂ ∥ qdr_cvx.edgeND₃₄) ∧ (LinearObj.seg_nd qdr_cvx.edgeND₂₃ ∥ qdr_cvx.edgeND₄₁) +def Quadrilateral_cvx.is_parallelogram {P : Type*} [EuclideanPlane P] (qdr_cvx : Quadrilateral_cvx P) : Prop := (LinearObj.seg_nd qdr_cvx.edgeND₁₂ ∥ qdr_cvx.edgeND₃₄) ∧ (LinearObj.seg_nd qdr_cvx.edgeND₂₃ ∥ qdr_cvx.edgeND₄₁) -def Quadrilateral.is_parallelogram {P : Type _} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by - by_cases qdr.IsConvex +def Quadrilateral.is_parallelogram {P : Type*} [EuclideanPlane P] (qdr : Quadrilateral P) : Prop := by + by_cases qdr.IsConvex · exact (Quadrilateral_cvx.mk_is_convex h).is_parallelogram - · exact False + · exact False theorem Parallelogram.is_parallelgram : sorry := sorry -def Parallelogram.mk_is_parallelgram {P : Type _} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr.is_parallelogram) : Parallelogram P := sorry +def Parallelogram.mk_is_parallelgram {P : Type*} [EuclideanPlane P] {qdr : Quadrilateral P} (h : qdr.is_parallelogram) : Parallelogram P := sorry section criteria -/- +/- -/ @@ -48,7 +48,7 @@ end property end EuclidGeom /- - nd₁₃ : point₃ ≠ point₁ + nd₁₃ : point₃ ≠ point₁ nd₂₄ : point₄ ≠ point₂ diag_not_para : ¬ SEG_nd point₂ point₄ nd₂₄ ∥ (LinearObj.seg_nd (SEG_nd point₁ point₃ nd₁₃)) diag_intx : Line.inx (SEG_nd point₁ point₃ nd₁₃).toLine (SEG_nd point₂ point₄ nd₂₄).toLine diag_not_para LiesInt (SEG point₁ point₃) ∧ Line.inx (SEG_nd point₁ point₃ nd₁₃).toLine (SEG_nd point₂ point₄ nd₂₄).toLine diag_not_para LiesInt (SEG point₂ point₄) diff --git a/EuclideanGeometry/Unused/Tactic.Congruence.lean b/EuclideanGeometry/Unused/Tactic.Congruence.lean index 293416911..4cb1204f9 100644 --- a/EuclideanGeometry/Unused/Tactic.Congruence.lean +++ b/EuclideanGeometry/Unused/Tactic.Congruence.lean @@ -59,7 +59,7 @@ def evalCongrSa : Tactic := fun stx => logInfo "`congr_sa` doesn't close any goals" | _ => throwUnsupportedSyntax -example {P : Type _} [EuclideanPlane P] {tr_nd₁ tr_nd₂ : TriangleND P} +example {P : Type*} [EuclideanPlane P] {tr_nd₁ tr_nd₂ : TriangleND P} (e₂ : tr_nd₁.1.edge₂.length = tr_nd₂.1.edge₂.length) (a₁ : tr_nd₁.angle₁.value = tr_nd₂.angle₁.value) (e₃ : tr_nd₁.1.edge₃.length = tr_nd₂.1.edge₃.length) diff --git a/EuclideanGeometry/Unused/Unused.lean b/EuclideanGeometry/Unused/Unused.lean index 97a83b27e..79376a0d7 100644 --- a/EuclideanGeometry/Unused/Unused.lean +++ b/EuclideanGeometry/Unused/Unused.lean @@ -8,12 +8,12 @@ namespace EuclidGeom /- Another way of defining 2DVecSpace before define EuclideanPlane，-/ section Cartesian2dVectorSpace /- -/ -class Cartesian2dVectorSpace (V : Type _) extends NormedAddCommGroup V, InnerProductSpace ℝ V where +class Cartesian2dVectorSpace (V : Type*) extends NormedAddCommGroup V, InnerProductSpace ℝ V where dim_two : FiniteDimensional.finrank ℝ V = 2 basis : Basis (Fin 2) ℝ V orthonormal : Orthonormal ℝ basis -variable {V : Type _} [h : Cartesian2dVectorSpace V] +variable {V : Type*} [h : Cartesian2dVectorSpace V] def x_coordinate (v : V) := (Basis.coord h.basis 0).toFun v @@ -85,7 +85,7 @@ end Pythagoras section Pythagoras -theorem Pythagoras_of_ne_ne_perp' (P : Type _) [EuclideanPlane P] {A B C : P} (hab : B ≠ A) (hac : C ≠ A) (h : (SegND.toProj ⟨SEG A B, hab⟩).perp = (SegND.toProj ⟨SEG A C, hac⟩)) : (SEG A B).length ^ 2 + (SEG A C).length ^ 2 = (SEG B C).length ^ 2 := by +theorem Pythagoras_of_ne_ne_perp' (P : Type*) [EuclideanPlane P] {A B C : P} (hab : B ≠ A) (hac : C ≠ A) (h : (SegND.toProj ⟨SEG A B, hab⟩).perp = (SegND.toProj ⟨SEG A C, hac⟩)) : (SEG A B).length ^ 2 + (SEG A C).length ^ 2 = (SEG B C).length ^ 2 := by have i : Vec.InnerProductSpace.Core.inner (VEC A B) (VEC A C) = 0 := inner_eq_zero_of_toProj_perp_eq_toProj (SegND.toVecND ⟨SEG A B, hab⟩) (SegND.toVecND ⟨SEG A C, hac⟩) h rw [Seg.length_sq_eq_inner_toVec_toVec (SEG A B), Seg.length_sq_eq_inner_toVec_toVec (SEG A C), Seg.length_sq_eq_inner_toVec_toVec (SEG B C)] simp only [seg_toVec_eq_vec] @@ -97,7 +97,7 @@ theorem Pythagoras_of_ne_ne_perp' (P : Type _) [EuclideanPlane P] {A B C : P} (h rw [← zero_add ((VEC A B).fst * (VEC A B).fst), ← zero_add ((VEC A B).fst * (VEC A B).fst), ← neg_zero, ← i] ring -theorem Pythagoras_of_perp_foot' (P : Type _) [EuclideanPlane P] (A B : P) {l : Line P} (h : B LiesOn l) : (SEG A (perp_foot A l)).length ^ 2 + (SEG B (perp_foot A l)).length ^ 2 = (SEG A B).length ^ 2 := by +theorem Pythagoras_of_perp_foot' (P : Type*) [EuclideanPlane P] (A B : P) {l : Line P} (h : B LiesOn l) : (SEG A (perp_foot A l)).length ^ 2 + (SEG B (perp_foot A l)).length ^ 2 = (SEG A B).length ^ 2 := by sorry end Pythagoras @@ -106,23 +106,23 @@ end Pythagoras /- unused sketch of undirected lines, segments-/ section undirected -class Line' (P : Type _) [EuclideanPlane P] where +class Line' (P : Type*) [EuclideanPlane P] where -- What is a line??? to be affine subspaces of dimension 1, citing affine vector spaces? -- carrier : Set P -- linearity -class GSeg' (P : Type _) [EuclideanPlane P] where +class GSeg' (P : Type*) [EuclideanPlane P] where -- a multiset of 2 points? or just never mention this? -class Seg' (P : Type _) [EuclideanPlane P] where +class Seg' (P : Type*) [EuclideanPlane P] where -- a multiset of 2 diff points? or just never mention this? -- carrier -def IsOnLine' {P : Type _} [EuclideanPlane P] (a : P) (l : Line' P) : Prop := sorry +def IsOnLine' {P : Type*} [EuclideanPlane P] (a : P) (l : Line' P) : Prop := sorry infixl : 50 "LiesOn" => IsOnLine' -instance {P : Type _} [EuclideanPlane P] : Coe (Ray P) (Line' P) where +instance {P : Type*} [EuclideanPlane P] : Coe (Ray P) (Line' P) where coe := sorry end undirected @@ -131,19 +131,19 @@ section angle namespace Angle open Classical -noncomputable def angle_of_three_points' {P : Type _} [h : EuclideanPlane P] (A O B : P) : ℝ := if ((A = O) ∨ (B = O)) then 0 else AngValue.toReal (value (mk_pt_pt_pt A O B sorry sorry)) +noncomputable def angle_of_three_points' {P : Type*} [h : EuclideanPlane P] (A O B : P) : ℝ := if ((A = O) ∨ (B = O)) then 0 else AngValue.toReal (value (mk_pt_pt_pt A O B sorry sorry)) end Angle end angle section nondeg /- Directed segment -/ -class DSeg (P : Type _) [EuclideanPlane P] extends Ray P, Seg P where +class DSeg (P : Type*) [EuclideanPlane P] extends Ray P, Seg P where on_ray : IsOnRay target toRay non_triv : target ≠ source /- Define a point lies on an oriented segment, a line, a segment, immediate consequences -/ -def IsOnDSeg {P : Type _} [EuclideanPlane P] (a : P) (l : DSeg P) : Prop := +def IsOnDSeg {P : Type*} [EuclideanPlane P] (a : P) (l : DSeg P) : Prop := ∃ (t : ℝ), 0 ≤ t ∧ t ≤ 1 ∧ a = t • (l.target -ᵥ l.source) +ᵥ l.source end nondeg @@ -152,12 +152,12 @@ scoped infix : 50 " LiesOnDSeg " => IsOnDSeg section nondeg -instance {P : Type _} [EuclideanPlane P] : Coe (DSeg P) (Seg P) where +instance {P : Type*} [EuclideanPlane P] : Coe (DSeg P) (Seg P) where coe := fun _ => DSeg.toSeg /- def of DirSeg from GDirSeg if length ≠ 0 -/ --- def Seg.toDSeg_of_nontriv {P : Type _} [EuclideanPlane P] (l : Seg P) (nontriv : l.target ≠ l.source): DSeg P where +-- def Seg.toDSeg_of_nontriv {P : Type*} [EuclideanPlane P] (l : Seg P) (nontriv : l.target ≠ l.source): DSeg P where -- source := l.source -- target := l.target -- toDir := Vec.toDir (l.target -ᵥ l.source) (vsub_ne_zero.mpr nontriv) @@ -166,16 +166,16 @@ instance {P : Type _} [EuclideanPlane P] : Coe (DSeg P) (Seg P) where -- theorems "if p LiesOnDSeg l, then p LiesOn l.toRay and p LiesOn l.toSeg" --- theorem DSeg.pt_on_toRay_of_pt_on_DSeg {P : Type _} [EuclideanPlane P] (p : P) (l : DSeg P) (lieson : p LiesOnDSeg l) : p LiesOn l.toRay := sorry +-- theorem DSeg.pt_on_toRay_of_pt_on_DSeg {P : Type*} [EuclideanPlane P] (p : P) (l : DSeg P) (lieson : p LiesOnDSeg l) : p LiesOn l.toRay := sorry -theorem DSeg.pt_on_toseg_of_pt_on_DSeg {P : Type _} [EuclideanPlane P] (p : P) (l : DSeg P) (lieson : p LiesOnDSeg l) : p LiesOn l.toSeg := sorry +theorem DSeg.pt_on_toseg_of_pt_on_DSeg {P : Type*} [EuclideanPlane P] (p : P) (l : DSeg P) (lieson : p LiesOnDSeg l) : p LiesOn l.toSeg := sorry -- mk method of DirSeg giving 2 distinct point -def DSeg.mk_pt_pt {P : Type _} [EuclideanPlane P] (A B : P) (h : B ≠ A) : DSeg P := sorry +def DSeg.mk_pt_pt {P : Type*} [EuclideanPlane P] (A B : P) (h : B ≠ A) : DSeg P := sorry namespace DSeg -variable {P: Type _} [EuclideanPlane P] (seg : DSeg P) (gseg : Seg P) +variable {P: Type*} [EuclideanPlane P] (seg : DSeg P) (gseg : Seg P) -- source and targets are on generalized directed segments theorem source_lies_on_seg : seg.source LiesOnDSeg seg := by sorry @@ -202,7 +202,7 @@ theorem DSeg.rev_toseg_eq_toseg_rev : seg.reverse.toSeg = (seg.toSeg).reverse := -- theorem Seg.rev_toDSeg_eq_toDSeg_rev (nontriv : gseg.target ≠ gseg.source) : (gseg.reverse).toDSeg_of_nontriv (Seg.nontriv_of_rev_of_nontriv gseg nontriv) = (gseg.toDSeg_of_nontriv nontriv).reverse := sorry -variable {P: Type _} [EuclideanPlane P] (v : ℝ × ℝ) (seg : DSeg P) +variable {P: Type*} [EuclideanPlane P] (v : ℝ × ℝ) (seg : DSeg P) -- parallel translate a directed segments @@ -220,7 +220,7 @@ end nondeg section pos_neg_ray -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] def IsOnPosSide (A : P) (ray : Ray P) : Prop := by by_cases A = ray.source @@ -246,7 +246,7 @@ open Classical /- Class of generalized triangles -/ /- -class Triangle' (P : Type _) [EuclideanPlane P] where +class Triangle' (P : Type*) [EuclideanPlane P] where point₁ : P point₂ : P point₃ : P @@ -254,7 +254,7 @@ class Triangle' (P : Type _) [EuclideanPlane P] where namespace Triangle -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] def nontriv₁ (tr : Triangle P) := (ne_of_not_collinear tr.nontriv).1 @@ -288,7 +288,7 @@ end nondeg_tri section Collinear -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] theorem collinear_ACB_of_collinear_ABC {A B C : P} (h : Collinear A B C): Collinear A C B := sorry @@ -304,11 +304,11 @@ end Collinear /-! section HasFallsOn -class HasFallsOn (α β : Type _) [HasLiesOn P α] [HasLiesOn P β] where +class HasFallsOn (α β : Type*) [HasLiesOn P α] [HasLiesOn P β] where falls_on : α → β → Prop lies_on_falls_on : ∀ (p : P) (A : α) (B : β), HasLiesOn.lies_on p A → falls_on A B → HasLiesOn.lies_on p B -class HasFallsIn (α β : Type _) [HasLiesIn P α] [HasLiesIn P β] where +class HasFallsIn (α β : Type*) [HasLiesIn P α] [HasLiesIn P β] where falls_in : α → β → Prop lies_in_falls_in : ∀ (p : P) (A : α) (B : β), HasLiesIn.lies_in p A → falls_in A B → HasLiesIn.lies_in p B @@ -322,9 +322,9 @@ end HasFallsOn -- scoped notation A "LiesInt" F => HasLiesInt.lies_int A F -def IsFallsOn {α β : Type _} (A : α) (B : β) [HasLiesOn P α] [HasLiesOn P β] : Prop := ∀ (A : P), (A LiesOn A) → (A LiesOn B) +def IsFallsOn {α β : Type*} (A : α) (B : β) [HasLiesOn P α] [HasLiesOn P β] : Prop := ∀ (A : P), (A LiesOn A) → (A LiesOn B) -def IsFallsIn {α β : Type _} (A : α) (B : β) [HasLiesIn P α] [HasLiesIn P β] : Prop := ∀ (A : P), (A LiesIn A) → (A LiesIn B) +def IsFallsIn {α β : Type*} (A : α) (B : β) [HasLiesIn P α] [HasLiesIn P β] : Prop := ∀ (A : P), (A LiesIn A) → (A LiesIn B) -- LiesOn → LiesInt is FallsInt ? @@ -333,60 +333,60 @@ scoped notation A "FallsIn" B "Over" P => IsFallsIn P A B namespace IsFallsOn -protected theorem refl {P : Type _} {α : Type _} (A : α) [HasLiesOn P α] : A FallsOn A Over P := by tauto +protected theorem refl {P : Type*} {α : Type*} (A : α) [HasLiesOn P α] : A FallsOn A Over P := by tauto -protected theorem trans {P : Type _} {α β γ : Type _} (A : α) (B : β) (C : γ) [HasLiesOn P α] [HasLiesOn P β] [HasLiesOn P γ] : (A FallsOn B Over P) → (B FallsOn C Over P) → (A FallsOn C Over P) := by tauto +protected theorem trans {P : Type*} {α β γ : Type*} (A : α) (B : β) (C : γ) [HasLiesOn P α] [HasLiesOn P β] [HasLiesOn P γ] : (A FallsOn B Over P) → (B FallsOn C Over P) → (A FallsOn C Over P) := by tauto end IsFallsOn namespace IsFallsIn -protected theorem refl {P : Type _} {α : Type _} (A : α) [HasLiesIn P α] : A FallsIn A Over P := by tauto +protected theorem refl {P : Type*} {α : Type*} (A : α) [HasLiesIn P α] : A FallsIn A Over P := by tauto -protected theorem trans {P : Type _} {α β γ : Type _} (A : α) (B : β) (C : γ) [HasLiesIn P α] [HasLiesIn P β] [HasLiesIn P γ] : (A FallsIn B Over P) → (B FallsIn C Over P) → (A FallsIn C Over P) := by tauto +protected theorem trans {P : Type*} {α β γ : Type*} (A : α) (B : β) (C : γ) [HasLiesIn P α] [HasLiesIn P β] [HasLiesIn P γ] : (A FallsIn B Over P) → (B FallsIn C Over P) → (A FallsIn C Over P) := by tauto end IsFallsIn -def IsIntersectionPoint {P : Type _} {α β : Type _} (A : P) (A : α) (B : β) [HasLiesOn P α] [HasLiesOn P β] := (A LiesOn A) ∧ (A LiesOn B) +def IsIntersectionPoint {P : Type*} {α β : Type*} (A : P) (A : α) (B : β) [HasLiesOn P α] [HasLiesOn P β] := (A LiesOn A) ∧ (A LiesOn B) scoped notation p "IsIntersectionOf" A B => IsIntersectionPoint p A B /- -class HasProj (α : Type _) where +class HasProj (α : Type*) where toProj : (α → Proj) -def Parallel {α β : Type _} (A : α) (B : β) [HasProj α] [HasProj β] : Prop := HasProj.toProj A = HasProj.toProj B +def Parallel {α β : Type*} (A : α) (B : β) [HasProj α] [HasProj β] : Prop := HasProj.toProj A = HasProj.toProj B scoped notation A "IsParallelTo" B => Parallel A B scoped notation A "∥" B => Parallel A B namespace Parallel -protected theorem refl {α : Type _} (A : α) [HasProj α] : A ∥ A := rfl +protected theorem refl {α : Type*} (A : α) [HasProj α] : A ∥ A := rfl -protected theorem symm {α β : Type _} (A : α) (B : β) [HasProj α] [HasProj β] : (A ∥ B) → (B ∥ A) := Eq.symm +protected theorem symm {α β : Type*} (A : α) (B : β) [HasProj α] [HasProj β] : (A ∥ B) → (B ∥ A) := Eq.symm -protected theorem trans {α β γ : Type _} (A : α) (B : β) (C : γ) [HasProj α] [HasProj β] [HasProj γ]: (A ∥ B) → (B ∥ C) → (A ∥ C) := Eq.trans +protected theorem trans {α β γ : Type*} (A : α) (B : β) (C : γ) [HasProj α] [HasProj β] [HasProj γ]: (A ∥ B) → (B ∥ C) → (A ∥ C) := Eq.trans end Parallel -def Perpendicular {α β : Type _} (A : α) (B : β) [HasProj α] [HasProj β] : Prop := sorry +def Perpendicular {α β : Type*} (A : α) (B : β) [HasProj α] [HasProj β] : Prop := sorry scoped notation A "IsPerpendicularTo" B => Perpendicular A B scoped notation A "⟂" B => Perpendicular A B namespace Perpendicular -protected theorem irrefl {α : Type _} (A : α) [HasProj α] : ¬ (A ⟂ A) := by sorry +protected theorem irrefl {α : Type*} (A : α) [HasProj α] : ¬ (A ⟂ A) := by sorry -protected theorem symm {α β : Type _} (A : α) (B : β) [HasProj α] [HasProj β] : (A ⟂ B) → (B ⟂ A) := sorry +protected theorem symm {α β : Type*} (A : α) (B : β) [HasProj α] [HasProj β] : (A ⟂ B) → (B ⟂ A) := sorry end Perpendicular -theorem parallel_of_perp_perp {α β γ : Type _} (A : α) (B : β) (C : γ) [HasProj α] [HasProj β] [HasProj γ] : (A ⟂ B) → (B ⟂ C) → (A ∥ C) := sorry +theorem parallel_of_perp_perp {α β γ : Type*} (A : α) (B : β) (C : γ) [HasProj α] [HasProj β] [HasProj γ] : (A ⟂ B) → (B ⟂ C) → (A ∥ C) := sorry -/ -/ -structure IsAngBis {P : Type _} [EuclideanPlane P] (ang : Angle P) (ray : Ray P) : Prop where intro :: +structure IsAngBis {P : Type*} [EuclideanPlane P] (ang : Angle P) (ray : Ray P) : Prop where intro :: eq_vtx : ang.source = ray.source bisect_ang : 2 * (Angle.mk ang.start_ray ray eq_vtx).value = ang.value diff --git a/Plan_files/Memo/AngValue.lean b/Plan_files/Memo/AngValue.lean index ab115d5eb..8e0a2e706 100644 --- a/Plan_files/Memo/AngValue.lean +++ b/Plan_files/Memo/AngValue.lean @@ -32,7 +32,7 @@ Note that `ℝ` is also used for representing the value of an angle (Algeraic Va -- The following suggestions may be bad. They are postponed. * `Dir` + `DirObj` + `P` to `DirObj` : Rotation of `DirObj` * `Proj` + `ProjObj` + `P` to `DirObj` : Rotation of `ProjObj` -* `Rotation` : the general rotation's type is `{P : Type _} [EuclideanPlane P] (O : P) (dir : Dir) [Figure α] (F : α P) : α P` `Maybe wrap outside a theorem use AngValue instead of Dir is better?` +* `Rotation` : the general rotation's type is `{P : Type*} [EuclideanPlane P] (O : P) (dir : Dir) [Figure α] (F : α P) : α P` `Maybe wrap outside a theorem use AngValue instead of Dir is better?` ### Detailed Sections diff --git a/Plan_files/Memo/LinearObjects.lean b/Plan_files/Memo/LinearObjects.lean index ab783dc6b..0edb58e74 100644 --- a/Plan_files/Memo/LinearObjects.lean +++ b/Plan_files/Memo/LinearObjects.lean @@ -60,21 +60,21 @@ toDirLine toLine carrier compatibility can be shown in general -- Experiments of classes namespace EuclidGeom -variable {P : Type _} [EuclideanPlane P] +variable {P : Type*} [EuclideanPlane P] -class ProjObj (P : Type _) [EuclideanPlane P] (α : Type _)where +class ProjObj (P : Type*) [EuclideanPlane P] (α : Type*)where toProj : α → Proj instance : ProjObj P (Line P) where toProj := Line.toProj -def to_Proj {P: Type _} [EuclideanPlane P] (l : Line P) : Proj := ProjObj.toProj P l +def to_Proj {P: Type*} [EuclideanPlane P] (l : Line P) : Proj := ProjObj.toProj P l -def toProj' ⦃P : Type _⦄ {α: Type _} [EuclideanPlane P] [ProjObj P α] (l : α) : Proj := ProjObj.toProj P l +def toProj' ⦃P : Type*⦄ {α: Type*} [EuclideanPlane P] [ProjObj P α] (l : α) : Proj := ProjObj.toProj P l -example {P : Type _} [EuclideanPlane P] (l : Line P) : l.toProj = to_Proj l := rfl +example {P : Type*} [EuclideanPlane P] (l : Line P) : l.toProj = to_Proj l := rfl -def to_Line {P : Type _ } {α: Type _} [EuclideanPlane P] ⦃h : ProjObj P α⦄ (l : α) : Line P := sorry +def to_Line {P : Type* } {α: Type*} [EuclideanPlane P] ⦃h : ProjObj P α⦄ (l : α) : Line P := sorry variable (l : Line P) -- same name enables both writing style without overload @@ -96,8 +96,8 @@ macro_rules #check Seg.carrier -- This is Plane Figure -class PlaneFig (F : (P : Type _) -> [ EuclideanPlane P] -> Type _) where - carrier : {P : Type _} -> [EuclideanPlane P] -> F P -> Set P +class PlaneFig (F : (P : Type*) -> [ EuclideanPlane P] -> Type*) where + carrier : {P : Type*} -> [EuclideanPlane P] -> F P -> Set P instance : PlaneFig Seg where carrier := Seg.carrier