jjdishere / eg Goto Github PK

A concept very useful in Position, and is easy to use in LCPosition.

It is a quotient of Ray and Line is a quotient of it.

Some file imports are not necessary, e.g.
B imports A ,and C imports both B and A.

Some file imports from Mathlib. I believe we should try to restrain import form Mathlib only in the file Vector.lean.

So there is a mission to clear all imports in the beginning of all files. After most files in Axiom and Constructions are done.

Should split Dir Proj to another file

Alternatively, we can define inx of x y : Line P in Option P. .none when the are parallel.

still missing a normed space instance, for proving theroems in Vectors.lean

1. def of FallsIn FallsOn (Maybe current class of HasFallsIn is not correct, should provide lots of theorems of FallsIn?) and lots of instances of them.
2. A class of HasInterior is also good.
3. Do we need a class of nondeg seg? for HasProj, then we do not need LinearObj anymore for parallel

Now Lean cannot infer P in l \parallel l' when they have coe but not explicitly declared to coercion to LinearObj.

Task: Make this notation work.

we don't need a class called RTriangle, but we need some basic properties of it.

1. numeric of angles
2. sin cos tan = edge/edge

1. definition of perpendicular (should do this for class LinearObj)
2. relation with parallel
3. construct perpendicular line (seg?) from a point to a line
4. def of distance
5. construct bisector of a seg (with midpoint), first propeties

Too many files in the folder Axiom now, we should rearrange them into smaller folders. How?

still no documentation for most of the file. A documentation provides a working plan and guidance for the file.

the key theorem to many other theorems is that SAS implies congruent
but we have two ways proving SAS and other congruent theorems (both NOT easy)
one way to define congruent:

1. prove Pythagoras theorem by Vector (in which file? perp?)
   -- the Py theorem is a general theorem which is useful in many situations
2. prove cosine theorem (in which file?)
3. prove cos an angle determines an angle in [0, \pi] (in the file angle)
4. use 2) to prove the third edge is of same length, use 3) to prove the rest angles are of same degree (using orientation of TRI)

second way to define congruent: (the same technique Euclid used, but Euclid didn't claim congruent properly)

1. to define isometry as a transition after a rotation
2. prove theorems about things didn't change under rotations and transitions (this step requires one to unfold Vector)
3. prove that any pair of angles with same degree could be translated under an isometry (after acting isometry, we get equal source and Dir)
4. prove SAS just as Euclid did (this might be not easy too)

Now which route is better? And do we need both two routes to define congruent for general objects?

Please read the comments in both file before start to merge files. Similar theorems have been marked and sections has been planned in advance.

We try to redefine line as
Equivalent class of Rays.

As title says.

Sine value of OAngles could be negative if the triangle is clockwise (anti oriented), so the theorem should distinguish those two cases.

we should always 1 - 2 teams doing examples. When Construction is finished, half or more teams should do examples.

During formalization of exercises, we discover many theorems is formalized as
h : A LiesOn (seg_nd).1
however, hypothese are given as
A LiesOn SEG A B
It is inconvenient to use the theorem unless we prove a trivial claim

let seg_nd := \< SEG A B , sorry \>
have A LiesOn seg_nd.1 := by sorry

We should do this in a way that we can directly use LiesOn SEG_nd A B h in hypothesis.

Also do this for TRI_nd?

Use OANG (or ANG) for construction of an oriented angle and use symbol \angle (∠) to represent the value of an angle

We are defining different concept of IsCongr for Triangle and Triangle_nd
use macro

As title says. in position.lean?

A point LiesOn a line splits the line into two rays. This is some how a version of the Archimedean property of the line.

-- Arch property : \any r : \R, \exist s : \R such that s > r.
-- Another note : The Arch prop section now in Line.lean and the real Arch property have different meanings.

As long as tri.2 \ne tri.1, tri.3 \ne tri.1, SAS do holds even when the triangle is degenerate.

Add these theorems into congruence.lean

The cosine theorem is the only theorem using bilinearity currently. With cosine theorem, we instantly get SAS, cos = ratio in a RTriangle, ... (even Pythagoras).

We decided to construct cosine theorem in the following order:

1. prove cos of dir dir = their inner product (in Vector.lean)
2. cos of vec_nd vec_nd = their inner product smul norm smul norm. (search mathlib) (In Vector.lean)
3. cosine theorem of triangle (Trigonometric.lean)
4. cos, sin eq ratio in a RTriangle (using cos^2 + sin^2 = 1, Pythagoras) (Trigonometric.lean)
5. sine theorem of triangle (more than 1 version, using abs of sin, using distance,...) (Trigonometric.lean)
6. SAS, SSS (Congruence.lean)
7. Similarity (Similarity.lean)

In constructions, a theorems can be stated in 2 different form. e.g.

theorem (tri : Triangle P) (h : tri.edge\1 = tri.edge\2) ...

theorem (A B C : P) (h : SEG A B = SEG A C)...

Should we include both version of theorems in most cases?

Example
PNT : point
LIN : line
SEG : segment
SGN : segment nondegenerate
ANG : angle (itself, the oriented angle, value is not a construction)
TRI : triangle
ARC : arc
SQR : square
QDR : quadrilateral
INX : intersection (this is an intersection)

AB//CD implies AB // DC, BA//CD BA//DC...

change Congr to

match tr1.is_nd
 | true => sorry
 | false => sorry

and when is_nd we define a class with 6 fields (instead of using \and).

Does this make using Congr easier?

Do we really need this? One seldom says Int and On together.

File Angle.lean
Define ang.external_angle (whose start ray is ang.end_ray, end ray is ang.start.reverse)
.external_angle.external_angle is not the same angle 对顶角
Write all numeric properties.

File Parallel.lean
内错角 同位角 同旁内角

File 垂直.lean
余角

File RightTriangle.lean
HL判别法
三角函数

Should add these permutation theorems into corresponding file. (using tactics like @[ext])

write theorems in Parallelogram not in A B C D : P, but in prg : Parallelogram P

Thanks to alissa-tung , we get our first tactic. 👍

A major change of IsCongr in on the plan.

1. We need to change the definition of IsCongr in to a structure with 6 fields.
2. we want to support tri_nd, don't do everything using tri_nd.1
3. The tactic congr_sa should accept 3 conditions, we allow them to be .symm and up to permutation.

We are going to need lots of tactics. e. g.

1. deciding colinearity (this is decidable, whether current colinear conditions are enough to derive a given colinear condition. It is more like the tauto tactic),
2. deciding nontrivility of two points (a tactic like simp, and we need add attribute @[simp] to new theorems),
3. auto generating theorems of permutation and flips(this is a macro, like @[ext]),
4. deciding congruence ignoring permutation and flips(this is maybe the most simple tactic, just enumerate all possible cases),
5. auto calculation of angles using theorems (a tactic like linarith [])

When can we write our first tactic? The process form 0 to 1 is harder than from 1 to many.

the tactic colinear, the naive version tactic judging whether 3 points are on the same line, can use a very simple algorithm behaving like "merging bubbles".

the tactic linear_order discuss the "order" relation on a line. More precisely, it is the linear combination relation. A LiesOn SEG B C means there exist 0 \le t \le 1, xA = t xB + (1-t) xC . Can linearize it? by adding new variables? (We can assume every point has coordinate \ge 0 by choosing a sufficient extreme point), so the above example will be translate into

0 \le t
t \le 1
xA = txB + xC - txC
0 \le txB
txB le xB
0 \le txC
txC \le xC

also writing goal (or its negation) into something like xA < xB \le xD (more then one possible case)
Then use linarith to solve it
Or can we define a order and use order?

Just as the title claimed.

High priority after naming convention is decided.

1. use SEG_nd and the fst point is always the center
2. use a center and a radius (with a prove that radius is positive)

key point is that SEG_nd is used more commonly in geometric constructions
-- and that 1) makes the programs shorter (citation needed) (TRY IT!)

After a discussion with cyb, a major change emergence.

1. Vector should be \mathbb{C}, Vec_nd is \mathbb{C} - {0}, Dir is Vec_nd/{\R \ge 0}, Prop is Dir/+-1
2. define the real inner product space structure on Vec

There are cases of point ne problem that our current planned pt_ne tactic cannot solve.

Using convexity:
Let ABC be a triangle (nd), D liesint AB, E liesint AC, F liesint BC, O liesint EF. Then O ne G.
Note that this does not hold if one of D or E of F only lieson LIN instead of SEG.

Using position:
Let A B C D be four points lie on a line, X does not lies on this line, the if angle XCD > XBD > XAD > 0, then A B C D lies in order.

A file in Construction, discuss properties of perp center. (perp line and perp foot is constructed in perpendicular.lean already)

1. def of power
2. def of In On Outside a circle
3. position relation between line and circle (ray and circle)

test

In some sense, the goal of position/convex is to show that every pt inside the incircle of a triangle falls in the triangle, and every pt inside the triangle is inside the circumcircle.

There is another road to do this (incircle):

1. prove that for 2 vec of pos orientation, the determinant is positive. (in vector.lean)
2. prove that for 2 ray the iff condition of they lies in the same side. (in position.lean)
3. prove that for a triangle any angle \ge 0 implies every angle \ge 0 (in Triangle.lean)
4. prove that for a point A lies on left side of a ray l, any point B lies on l.toLine, any point C lies int SEG A B, C lies on left side of the ray l (in position.lean, concurrent with 3)
5. prove that incircle contains in Triangle. (in incircle.lean, not created yet)

Auto-generation of theorems of permutation
the name of the auto-generated theorems should be + 123 132 213 231 312 321

After we develop tactic pt_ne，we shall do a enhanced, convenience version of SEG_nd, LIN, ANG, who fills the condition of nondegenerate automatically SEG_nd' A B := SEG_nd A B (by pt_ne). If failed, the infoview should tell user pt_ne cannot infer B \ne A, try SEG_nd and fill in B \ne A by hand.

1. in ray we need to add a theorem (I forget) :(
2. if C lies on Seg_nd A B .extension, then angle of A D B and A D C are of same sign. (using a
3. Seg_nd A B parallel to ray implies A B lies on same side
4. Seg_nd A B with A B lies on same side of ray implies any point C lies int Seg_nd A B, C is on the same side
5. if A lies on left side B on right side of ray , Seg A B must has intersection with ray.toLine

Instead of

notation "Vec" => \mathbb{R} * \mathbb{R}

we may use

class Vec where
   fst :  \mathbb{R}
   snd :  \mathbb{R}

This will enable us to use instances without messing up with product structure on \mathbb{R} \times \mathbb{R}