Ceva's theorem

Project.toml

@@ -10,7 +10,10 @@ Plots = "91a5bcdd-55d7-5caf-9e0b-520d859cae80"
 SymPy = "24249f21-da20-56a4-8eb1-6a02cf4ae2e6"
 
 [compat]
-julia = "1"
+CodeTracking = "0.5.11"
+Plots = "1.2"
+SymPy = "1.0"
+julia = "1.4"
 
 [extras]
 Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"

docs/make.jl

@@ -19,10 +19,11 @@ makedocs(sitename="Plane Geometry in Julia",
                    "Summary" => "theorem/index.md",
                    "Napoleon" => "theorem/Napoleon.md",
                    "Centroid" => "theorem/Centroid.md",
+                   "Ceva" => "theorem/Ceva.md",
                   ],
                   "Utitlies" => "util.md",
                   "Ackowledgement" => "thanks.md",
                  ],
          format = Documenter.HTML(assets = ["assets/custom.css"]),
-         doctest = false
+         doctest = true
         )

docs/src/definition/distance.md

@@ -52,7 +52,11 @@ scatter!(shape([A, B, mid]), leg=false, aspect_ratio=:equal,
 ## Concurrent Point
 
 ```@docs
-concurrent
+concurrent(::Vector{Edge})
+```
+
+```@docs
+concurrent(::Edge, ::Edge)
 ```
 
 ### Source Code

docs/src/definition/index.md

@@ -5,6 +5,7 @@ Here are the geometric concepts defined in PlaneGeometry.jl.
 ```@contents
 Pages = [
     "elementary.md",
+    "distance.md",
     "triangle.md",
     "circle.md",
     ]

docs/src/theorem/Centroid.md

@@ -1,12 +1,13 @@
 # Centroid Exists Theorem
 
-See [Napoleon's Theorem](Napoleon.md) for an example with more explanations.
+See [Napoleon's Theorem](Napoleon.md) for an example with more detailed explanations of how to prove
+theorems with Julia.
 
 ```@setup 1
 using 
     PlaneGeometry, 
     PlaneGeometry.Theorems, 
-    PlaneGeometry.Theorems.Napoleon,
+    PlaneGeometry.Theorems.Centroid,
     Plots
 ```
 

docs/src/theorem/Ceva.md

@@ -0,0 +1,74 @@
+# Ceva's Theorem
+
+See [Napoleon's Theorem](Napoleon.md) for an example with more detailed explanations of how to prove
+theorems with Julia.
+
+```@setup 1
+using 
+    PlaneGeometry, 
+    PlaneGeometry.Theorems, 
+    PlaneGeometry.Theorems.Ceva,
+    Plots
+```
+
+```@contents
+Pages = ["Ceva.md"]
+```
+
+## The Theorem
+
+```@docs
+PlaneGeometry.Theorems.Ceva
+```
+
+## Finding the ceva and medians
+
+```@docs
+ceva
+```
+```@example 1
+@code_md ceva(Triangle(), Point()) # hide
+```
+
+## Examples
+
+```@docs
+ceva_draw(::Triangle, ::Point)
+```
+
+```@example 1
+A = Point(0,0); B = Point(1, 3); C = Point(4,2); O = Point(2, 2)
+plt, hold = ceva_draw(Triangle(A, B, C), O)
+does_thmhold(hold)
+savefig("ceva-plot-1.svg"); nothing # hide
+```
+
+![ceva-plot-1.svg](ceva-plot-1.svg)
+
+```@docs
+ceva_rand()
+```
+
+```@example 1
+plt, hold = ceva_rand()
+does_thmhold(hold)
+savefig("ceva-plot-2.svg"); nothing # hide
+```
+![ceva-plot-2.svg](ceva-plot-2.svg)
+
+```@example 1
+plt, hold = ceva_rand()
+does_thmhold(hold)
+savefig("ceva-plot-3.svg"); nothing # hide
+```
+![ceva-plot-3.svg](ceva-plot-3.svg)
+
+## Proof
+
+```@example 1
+@code_md ceva_proof() # hide
+```
+
+```@example 1
+does_thmhold(ceva_proof())
+```

docs/src/theorem/index.md

@@ -6,5 +6,7 @@ the future 😉️.
 ```@contents
 Pages = [
     "Napoleon.md",
+    "Centroid.md",
+    "Ceva.md",
     ]
 ```

src/PlaneGeometry.jl

@@ -39,12 +39,18 @@ using .GeoPlots
 export 
     plot, plot!, shape
 
+using .Theorems.Ceva
+export 
+    ceva_proof, ceva_draw, ceva_rand, ceva, ceva_check
+
 function __init__()
-    global A, B, C
+    global A, B, C, O, tri
 
-    A = Point(0, 0); 
-    B = Point(1, 3); 
-    C = Point(4, 2);
+    A = Point(0, 0)
+    B = Point(1, 3)
+    C = Point(4, 2)
+    O = Point(2, 2)
+    tri = Triangle(A, B, C)
 end
 
 end # module

src/distance.jl

@@ -41,6 +41,7 @@ end
 Find the midpoint between `A` and `B`.
 
 # Examples
+
 ```jldoctest
 julia> midpoint(Point(0, 0), Point(2,4))
 Point(1, 2)
@@ -56,7 +57,14 @@ end
 """
     concurrent(edgelist::Vector{Edge})
 
-Find the point where all `edges` (lines) intersect if such point exists. Return nothing otherwise.
+Find the point where all edges (lines) in `edgelist` intersect if such point exists. Return nothing otherwise.
+
+# Examples
+
+```jldoctest
+julia> concurrent([Edge(Point(0,1), Point(1,1)), Edge(Point(0,1), Point(1,0))])
+Point(0, 1)
+```
 """
 function concurrent(edgelist::Vector{Edge})
     enum = length(edgelist)
@@ -81,3 +89,19 @@ function concurrent(edgelist::Vector{Edge})
         return Point(simplify(sol[x]), simplify(sol[y]))
     end
 end
+
+"""
+    concurrent(e1::Edge, e2::Edge)
+
+Find the point the edges `e1` and `e2` intersect if such point exists. Return nothing otherwise.
+
+# Examples
+
+```jldoctest
+julia> concurrent(Edge(Point(0,1), Point(1,1)), Edge(Point(0,1), Point(1,0)))
+Point(0, 1)
+```
+"""
+function concurrent(e1::Edge, e2::Edge)
+    return concurrent([e1, e2])
+end

src/elementary.jl

@@ -1,4 +1,4 @@
-import Base: isequal, ==, show
+import Base: isequal, ==, show, *, length, >
 using SymPy
 
 "A plane geometric object."
@@ -122,6 +122,18 @@ function edges(tri::Triangle)
     elist
 end
 
+"Mulitpliy the lengths of two edges."
+(*)(e1::Edge, e2::Edge) = length(e1) * length(e2)
+
+"Mulitpliy a number and an edges length."
+(*)(s1::Sym, e2::Edge) = s1 * length(e2)
+
+"Compare lengths of two edges."
+(>)(e1::Edge, e2::Edge) = length(e1) > length(e2)
+
+"Find the length of an edge."
+length(e::Edge) = distance(e.src, e.dst)
+
 """
     Circle(c, r) 
     

src/theorem/Centroid.jl

@@ -46,7 +46,7 @@ end
 """
     centroid_draw(A, B, C)
 
-Verify Napoleon's theorem.
+Verify Centroid Exists theorem.
 """
 function centroid_draw(A, B, C)
     tri = Triangle(A, B, C)
@@ -57,7 +57,7 @@ end
 """
     centroid_draw(xA, yA, xB, yB, xC, yC)
 
-Verify Napoleon's theorem.
+Verify Centroid Exists theorem.
 """
 function centroid_draw(xA, yA, xB, yB, xC, yC)
     A = Point(xA, yA); 

src/theorem/Ceva.jl

@@ -0,0 +1,138 @@
+"""
+[Ceva's theorem](https://en.wikipedia.org/wiki/Ceva%27s_theorem) is a theorem about triangles in
+plane geometry. Given a triangle `ABC`, let the lines `AO`, `BO` and `CO` be drawn from the vertices
+to a common point `O` (not on one of the sides of `ABC`), to meet opposite sides at `D`, `E` and `F`
+respectively.  (The segments `AD`, `BE`, and `CF` are known as
+[cevians](https://en.wikipedia.org/wiki/Cevian).) Then, using signed lengths of segments,
+```math
+BD \\times CE \\times AF = DC \\times EA \\times FB.
+```
+"""
+module Ceva
+
+using Plots
+using SymPy
+using PlaneGeometry
+using PlaneGeometry.GeoPlots
+
+export 
+    ceva_proof, ceva_draw, ceva_rand, ceva, ceva_check
+
+"""
+    ceva_draw(📐️, O)
+
+Verify Ceva's Theorem for the triangle `📐️`.
+"""
+function ceva_draw(tri, O)
+
+    plist, elist = ceva(tri, O)
+    A, B, C, D, E, F = plist
+    push!(plist, O)
+
+    plt = plot(tri, fill=(0, :green), aspect_ratio=:equal, fillalpha= 0.2, leg=false)
+
+    plt = scatter!(shape(plist), 
+            leg=false, 
+            aspect_ratio=:equal, 
+            color=:red,
+            series_annotations = text.(['A':'F'..., 'O'], :bottom))
+
+    AD, BE, CF = [Edge(epair...) for epair in zip([A, B, C], [D, E, F])]
+
+    for e in [AD, BE, CF]
+        plot!(e, color=:orange, leg=false)
+    end
+
+    plt, ceva_check(elist...)
+end
+
+"""
+    ceva_rand()
+
+Verify Ceva's Theorem for a random triangle.
+"""
+function ceva_rand()
+    pts = rand(0:1//10:1,6);
+    A, B, C = [Point(pts[i], pts[i+3]) for i in 1:3]
+
+    # Choose O within ABC so the picture looks nicer
+    ptx = [pt.x for pt in [A, B, C]]
+    pty = [pt.y for pt in [A, B, C]]
+    xmin, xmax = N.([f(ptx...) for f in [min, max]])
+    ymin, ymax = N.([f(pty...) for f in [min, max]])
+
+    tri = Triangle(A, B, C)
+    AB, BC, CA = edges(tri)
+
+    # Use rejections sampling until the point is in ABC
+    while true
+        x = rand(xmin:1//100:xmax)
+        y = rand(ymin:1//100:ymax)
+        O = Point(x, y)
+
+        plist, elist = ceva(tri, O)
+
+        # We are unlucky
+        if plist == nothing
+            continue
+        end
+
+        BD, DC, CE, EA, AF, FB = elist
+
+        if BD > BC || DC > BC || CE > CA || EA > CA || AF > AB || FB > AB
+            # This mean O is not in ABC
+            continue
+        end
+
+        return ceva_draw(Triangle(A, B, C), O)
+    end
+end
+
+"""
+    ceva_proof()
+
+Prove Ceva's Theorem.
+"""
+function ceva_proof()
+    @vars by cx positive=true
+    @vars cy ox oy
+
+    A = Point(0, 0); B = Point(0, by); C = Point(cx, cy); O = Point(ox, oy)
+    tri = Triangle(A, B, C)
+
+    plist, elist = ceva(tri, O)
+    ceva_check(elist...)
+end
+
+
+"""
+    ceva(Triangle(A, B, C), O)
+
+Returns `([A, B, C, D, E, F], [BD, DC, CE, EA, AF, FB])`. 
+"""
+function ceva(tri, O)
+    A, B, C = vertices(tri)
+    AB, BC, CA = edges(tri)
+    AO, BO, CO = [Edge(pt, O) for pt in vertices(tri)]
+    D, E, F = [concurrent(epair...) for epair in zip([BC, CA, AB], [AO, BO, CO])]
+
+    # This mean no such points can be found. (This is possible)
+    if D == nothing || E == nothing || F == nothing
+        return nothing, nothing
+    end
+
+    elist = [Edge(pts...) for pts in zip([B, D, C, E, A, F], [D, C, E, A, F, B])]
+    ([A, B, C, D, E, F], elist)
+end
+
+"""
+    ceva_check(BD, DC, CE, EA, AF, FB)
+
+Check if the line segments satisfies Ceva's theorem.
+"""
+function ceva_check(BD, DC, CE, EA, AF, FB) 
+    eq = Eq((BD*CE*AF)^2, (DC*EA*FB)^2)
+    N(simplify(eq))
+end
+
+end