Sympy should suffice
I have just received a copy of Instant SymPy Starter, by Ronan Lamy—a no-nonsense guide to the main properties of SymPy, the Python library for symbolic mathematics. This short monograph packs everything you should need, with neat examples included, in about 50 pages. Well-worth its money.
Segments and are equal. Lines and intersect at Form four circumcircles: Prove that the circumcenters form a rhombus, with
Note that if this construction works, it must do so independently of translations, rotations and dilations. We may then assume that is the origin, that the segments have length one, and that for some parameters it is We let SymPy take care of the computation of circumcenters:
import sympy from sympy import * # Point definitions M=Point(0,0) A=Point(2,0) B=Point(1,0) a,theta=symbols('a,theta',real=True,positive=True) C=Point((a+1)*cos(theta),(a+1)*sin(theta)) D=Point(a*cos(theta),a*sin(theta)) #Circumcenters E=Triangle(A,C,M).circumcenter F=Triangle(A,D,M).circumcenter G=Triangle(B,D,M).circumcenter H=Triangle(B,C,M).circumcenter
Finding that the alternate angles are equal in the quadrilateral is pretty straightforward:
In : P=Polygon(E,F,G,H) In : P.angles[E]==P.angles[G] Out: True In : P.angles[F]==P.angles[H] Out: True
To prove it a rhombus, the two sides that coincide on each angle must be equal. This presents us with the first challenge: Note for example that if we naively ask SymPy whether the triangle is equilateral, we get a False statement:
In : Triangle(E,F,G).is_equilateral() Out: False In : F.distance(E) Out: Abs((a/2 - cos(theta))/sin(theta) - (a - 2*cos(theta) + 1)/(2*sin(theta))) In : F.distance(G) Out: sqrt(((a/2 - cos(theta))/sin(theta) - (a - cos(theta))/(2*sin(theta)))**2 + 1/4)
Part of the reason is that we have not indicated anywhere that the parameter theta is to be strictly bounded above by (we did indicate that it must be strictly positive). The other reason is that SymPy does not handle identities well, unless the expressions to be evaluated are perfectly simplified. For example, if we trust the routines of simplification of trigonometric expressions alone, we will not be able to resolve this problem with this technique:
In : trigsimp(F.distance(E)-F.distance(G),deep=True)==0 Out: False
Finding that with SymPy is not that easy either. This is the second challenge.
How would the reader resolve this situation?