None Example_of_symbolic_computations

Example of symbolic computations

MoebInv can do a bit more than just draw colorful pictures. Powered by GiNaC symbolic computation engine MoebInv is capable to provide rigorous proof of geometric statements through analytic computations. Here is an example.

If you get an error due to missing libraries then install them as shown in the first section of Software installation notebook

First, we need to load libraries (assuming software installation is already done).

In [1]:
from figure import *
            Python wrappers for MoibInv Library
     ---------------------------------------------
Please cite this software as
V.V. Kisil, MoebInv: C++ libraries for manipulations in non-Euclidean geometry, SoftwareX, 11(2020),100385. doi:10.1016/j.softx.2019.100385.
     ---------------------------------------------

Then, we initialise a figure F with a default Euclidean metric.

In [2]:
F=figure()

We add the unit circle $a$ to the figure by specifying the explicit coefficients $(1, 0, 0, -1)$ of its quadratic equations: $$1\cdot(x^2+y^2)-0\cdot x -0\cdot y -1 =0$$.

In [3]:
a=F.add_cycle(cycle2D(1, [0, 0], -1), "a")

Then, we add the centre $C$ of $a$ as a point:

In [4]:
C=F.add_point(cycle2D(F.get_cycles(a)[0]).center(), "C")

We add a line $l$ tangent to $a$. A straight line is characterised among cycles by its orthogonality to infinity ("passes the infinity"). The line $l$ is not uniquely defined by these two conditions (the tangency and orthogonality) because the point of its contact to $a$ can be arbitrary. Therefore its coefficients contain a free variable like 'symbol255' as can be seen from the figure printout.

In [5]:
l=symbol("l")
F.add_cycle_rel([is_tangent(a),is_orthogonal(F.get_infinity()),only_reals(l)],l)
print(F.string())
infty: {`0, [[0,0]]~infty, 1', -2} --> (C,l);  <-- ()
R: {`0, [[0,1]]~R, 0', -1} --> ();  <-- ()
C: {`1, [[0,0]]~C, 0', 0} --> ();  <-- ()
a: {`1, [[0,0]]~a, -1', 0} --> (l);  <-- ()
l: {`0, [[-1/8*sqrt(8)*cos(t_l)*sqrt(2),-1/64*sqrt(2)*sin(t_l)*sqrt(512)]]~l, 1', `0, [[1/8*sqrt(8)*cos(t_l)*sqrt(2),-1/64*sqrt(2)*sin(t_l)*sqrt(512)]]~l, 1', `0, [[1/8*sqrt(8)*cos(t_l)*sqrt(2),1/64*sqrt(2)*sin(t_l)*sqrt(512)]]~l, 1', `0, [[-1/8*sqrt(8)*cos(t_l)*sqrt(2),1/64*sqrt(2)*sin(t_l)*sqrt(512)]]~l, 1', 1} --> ();  <-- (a|t,infty|o,l|r)
Altogether 8 cycles in 5 cycle_nodes

Note, that the parametrisation of the line (l) uses trigonometric functions in order to avoid square roots appearing in the solutions of quadratic tangency relation. With such substitution automatic simplifications of algebraic expressions are much more efficient.

At the next step we add the point $P$ of contact of the circle $a$ and the line $l$. A point belongs to a cycle if the point is orthogonal the cycle. Also a point is characterised among all cycle by orthogonality to itself. To define the latter reflexive condition we need to ``pre-cook'' its symbol in advance.

In [6]:
P=symbol("P")
P=F.add_cycle_rel([is_orthogonal(P), is_orthogonal(a), is_orthogonal(l), only_reals(P)], P)

Finally we add the radius $r$ passing $P$: it is a straight line (is orthogonal to the infinity) and passes both $P$ and $C$ (is orthogonal to each of them).

In [7]:
r=F.add_cycle_rel([is_orthogonal(P), is_orthogonal(C), is_orthogonal(F.get_infinity())], "r")

Recall, that $r$ depends on the same free parameters as $l$. Now, we check the orthogonality relation between $r$ and $l$. Because some of the above conditions were quadratic (e.g., tangency and self-orthogonality), there are multiple instances of the cycle $r$, each of them is checked separately.

In [8]:
Res=F.check_rel(l,r,"orthogonal")
for i in range(len(Res)):
    print("Tangent and radius are orthogonal: %s" %\
    bool(Res[i].subs(pow(cos(wild(0)),2)==1-pow(sin(wild(0)),2)).normal()))
Tangent and radius are orthogonal: True
Tangent and radius are orthogonal: True
Tangent and radius are orthogonal: True
Tangent and radius are orthogonal: True
Warning: it is safer to avoid substitutions from relational, use Python dictionaries instead
Warning: it is safer to avoid substitutions from relational, use Python dictionaries instead
Warning: it is safer to avoid substitutions from relational, use Python dictionaries instead
Warning: it is safer to avoid substitutions from relational, use Python dictionaries instead

Note, that we had uses the Pythagoras substitution $\cos^2 t = 1 - \sin^2 t$ to assist the CAS with algebraic simplifications.

Another example of analytic proof of a less trivial result is presented here.