[Julia] 证明Ceva定理

hbghlyj

Ceva's Theorem
准备工作与这帖相同, 打开Jupyter notebook.
将下面的命令粘贴到Cell, 按Shift+Enter执行:
引入SymPy

1. using Pkg;
2. Pkg.activate(".");
3. Pkg.add("SymPy")
4. using SymPy

复制代码

定义一些基本的几何对象。

1. import Base: isequal, ==
3. abstract type GeoObject end
4. abstract type GeoShape <: GeoObject end
6. struct Point <: GeoObject
7.     x::Number
8.     y::Number
9. end
10. (==)(p1::Point, p2::Point) = p1.x==p2.x && p1.y==p2.y
12. struct Triangle <: GeoShape
13.     A::Point
14.     B::Point
15.     C::Point
16. end
17. Triangle(ax, ay, bx, by, cx, cy) = Triangle(Point(ax, ay), Point(bx, by), Point(cx, cy))
18. (==)(t1::Triangle, t2::Triangle) = vertices(t1) == vertices(t2)
20. function vertices(tri::Triangle)
21.     [tri.A, tri.B, tri.C]
22. end
24. struct Edge <: GeoShape
25.     src::Point
26.     dst::Point
27. end
29. function edges(tri::Triangle)
30.     elist = Edge[]
31.     pts = vertices(tri)
32.     for i in 1:length(pts)-1
33.         push!(elist, Edge(pts[i], pts[i+1]))
34.     end
35.     push!(elist, Edge(pts[length(pts)], pts[1]))
36.     elist
37. end

复制代码

计算两点距离的函数

1. function squaredist(A, B)
2.     d = (A.x-B.x)^2+(A.y-B.y)^2
3.     if d isa Sym
4.         simplify(d)
5.     else
6.         d
7.     end
8. end;

复制代码

计算两线交点的函数

1. function concurrent(e1::Edge, e2::Edge)
2.     @vars x y
4.     eqs = Sym[]
5.     for e in [e1,e2]
6.         eq = (x-e.src.x)*(y-e.dst.y) - (x-e.dst.x)*(y-e.src.y)
7.         push!(eqs, eq)
8.     end
10.     sol = solve(eqs, [x,y])
12.     if length(sol) == 0
13.         return nothing
14.     else
15.         return Point(simplify(sol[x]), simplify(sol[y]))
16.     end
17. end

复制代码

下面的函数ceva(Triangle(A, B, C), O)输出([A, B, C, D, E, F], [BD, DC, CE, EA, AF, FB])

1. function ceva(tri, O)
2.     A, B, C = vertices(tri)
3.     AB, BC, CA = edges(tri)
4.     AO, BO, CO = [Edge(pt, O) for pt in vertices(tri)]
5.     D, E, F = [concurrent(epair...) for epair in zip([BC, CA, AB], [AO, BO, CO])]
7.     # This mean no such points can be found. (This is possible)
8.     if D == nothing || E == nothing || F == nothing
9.         return nothing, nothing
10.     end
12.     elist = [Edge(pts...) for pts in zip([B, D, C, E, A, F], [D, C, E, A, F, B])]
13.     ([A, B, C, D, E, F], elist)
14. end

复制代码

定义线段的 “长度平方”

1. squarelength(e::Edge) = squaredist(e.src, e.dst)

复制代码

检查六个长度平方满足Ceva等式的函数

1. function ceva_check(BD, DC, CE, EA, AF, FB)
2.     eq = Eq(BD*CE*AF, DC*EA*FB)
3.     N(simplify(eq))
4. end

复制代码

证明Ceva定理

1. function ceva_proof()
2.     @vars bx by cx cy
4.     A = Point(1, 0); B = Point(bx, by); C = Point(cx, cy); O = Point(0, 0)
5.     tri = Triangle(A, B, C)
7.     plist, elist = ceva(tri, O)
8.     ceva_check(squarelength.(elist)...)
9. end

复制代码

输出true