Эксперимент 002: решение задач по планиметрии с помощью модуля "Planimetrics Calculus" библиотеки Kone

(Проект эксперимента доступен здесь.)

Задачи по планиметрии развились как отдельное интересное направление головоломок. Некоторые находят изысканные решения сложных задач, понятные всякому, кто помнит школьную геометрию. Некоторые развивают такие мощные инструменты как вычисления в комплексных числах и проективные движения, чтобы быстрее решать трудные задачи и иногда обобщать их. Некоторые тренируют компьютерные программы, которые могут решать задачи по геометрии или придумывать новые.

В библиотеке Kone есть модуль "Planimetrics Calculus", который позволяет исследовать задачи, описываемые определённым образом, с точки зрения многочленов в проективном пространстве. Этот эксперимент служит списком примеров и испытательным полигонов этого модуля.

Но сначала короткое теоретическое введение: о чём речь?

Пусть нам дано векторное пространство $V$ над полем $K$ . Рассмотрим отношение эквивалентности $\sim$ на $V \setminus \{\overline{0}\}$ , что $v \sim u$ тогда и только тогда, когда есть $k \in K \setminus \{0\}$ , что $v = ku$ . Тогда фактор-множество $V/\sim$ называется проективизацией $V$ и просто проективным пространством и обозначается $\mathrm{P}(V)$ .

Если выбрать в $V$ любой базис, то можно ввести координаты. Правда, $\sim$ отождествляет точки с пропорциональными координатами. Т.е. $(x_1, \dots, x_n) \sim (\lambda x_1, \dots, \lambda x_n)$ . Тогда можно отождествить такие наборы координат с точностью до пропорциональности. Такие "координаты" всякой точки проективного пространства $\mathrm{P}(V)$ называются однородными координатами этой точки и обозначаются $(x_1 : x_2 : \dots : x_n)$ . Аналогично можно ввести однородные координаты гиперпространства.

Давайте заметим, что прямая проходящая через точки $(x_1 : x_2 : x_3)$ и $(y_1 : y_2 : y_3)$ имеет вид

(x_2 y_3 - x_3 y_2 : x_3 y_1 - x_1 y_3 : x_1 y_2 - x_2 y_1)

Т.е. выражается как три однородных многочлен второй степени от $x_1$ , $x_2$ , $x_3$ и $y_1$ , $y_2$ , $y_3$ . А если мы вложим обычную плоскость в проективную отображением $(x, y) \mapsto (x : y : 1)$ , то такими же многочленами можно выразить середину отрезка меж этих точек, серединный перпендикуляр и даже центр окружности, проходящей через три данные точки. При этом и условия коллинеарности точек, конкурентности прямых и другие тоже описываются многочленами. Т.е. если нам даны какие-то случайные объекты (точки и прямые), мы на них построили таким образом новые объекты и про какие-то объекты что-нибудь спросим, то это условие получится многочленами от координат изначальных объектов. А значит верным всегда тогда и только тогда, когда многочлен нулевой.

Таким образом мы покажем, как на основе этого модуля-фреймворка проверять верность теорем из планиметрии.

Время экспериментов!

Каждый эксперимент начнётся с шаблона

fun main(): Unit = koneContextRegistry.inPlanimetricsCalculationSpaceScopeFor(rationalType) {
    ...
}

Не бойтесь, это всего лишь настройка окружения для нашей задачи.

Сюжет: прямая Эйлера

(Файл eulerLine.kt.)

Возьмём случайный треугольник $\triangle ABC$ :

val A by Point
val B by Point
val C by Point

И возьмём вв нём центроид $M$ , ортоцентр $H$ и центр описанный окружности $O$ .

val M = centroid(A, B, C)
val H = orthocenter(A, B, C)
val O = circumcenter(A, B, C)

Просто проверим, что они лежат на одной прямой.

println(collinearityTest(M, H, O))

Эта строка возвращает true, т.е. они реально лежат на одной прямой! И эта прямая называется прямой Эйлера.

В библиотеке есть функция для вычисления и прямой Эйлера.

val l = eulerLine(A, B, C)

Можно проверить, что это реально прямая Эйлера, проверив лежат ли на ней $M$ , $H$ и $O$ .

for (P in listOf(M, H, O)) println(P isLyingOn l)

Выведется трижды true.

Также можно провести прямую через, например, $H$ и $O$ и проверить $l$ на совпадение с полученной прямой:

println(l equalsTo lineThrough(O, H))

Сюжет: теорема Дезарга

(Файл desarguesTheorem.kt.)

В этом сюжете мы попытаемся доказать прямую и обратную теоремы Дезарга за один раз.

В задаче фигурируют два треугольника случайного расположения. Давайте определим их по их вершинам:

val A1 by Point
val B1 by Point
val C1 by Point
val A2 by Point
val B2 by Point
val C2 by Point

Под капотом декларация

val P by Point

заводит переменные P_x, P_y и P_z, превращает их в многочлены (т.е. многочлен $1 \cdot P_x$ и т.д.) и создаёт объект точки, однородные координаты которой — три полученных многочлена.

Теперь ~~проведём~~ вычислим прямые $a := \overline{A_1A_2}$ , $b := \overline{B_1B_2}$ и $c := \overline{C_1C_2}$ :

val a = lineThrough(A1, A2)
val b = lineThrough(B1, B2)
val c = lineThrough(C1, C2)

Под капотом lineThrough просто берёт многочлены-координаты двух полученных точек и вычисляет от них выражение из теоретического введения.

Теперь вычислим точки пересечения пар прямых $A' := \overline{B_1 C_1} \cap \overline{B_2 C_2}$ , $B' := \overline{C_1 A_1} \cap \overline{C_2 A_2}$ и $C' := \overline{A_1 B_1} \cap \overline{A_2 B_2}$ :

val Aprime = intersectionOf(lineThrough(B1, C1), lineThrough(B2, C2))
val Bprime = intersectionOf(lineThrough(C1, A1), lineThrough(C2, A2))
val Cprime = intersectionOf(lineThrough(A1, B1), lineThrough(A2, B2))

Вспомним, что теорема Дезарга говорит, что $a$ , $b$ и $c$ конкурентны тогда и только тогда, когда $A'$ , $B'$ и $C'$ коллинеарны. Давайте докажем это. Но сделаем следующий неожиданный ход. Вычислим такие условия:

условие конкурентности $a$ $a$ , $b$ $b$ и $c$ $c$ , умноженное на условие коллинеарности $A_1$ $A_{1}$ , $B_1$ $B_{1}$ и $C_1$ $C_{1}$ и на условие коллинеарности $A_2$ $A_{2}$ , $B_2$ $B_{2}$ и $C_2$ $C_{2}$ :
```
concurrencyCondition(a, b, c) * collinearityCondition(A1, B1, C1) * collinearityCondition(A2, B2, C2)
```
условие коллинеарности $A'$ $A^{'}$ , $B'$ $B^{'}$ и $C'$ $C^{'}$ :
```
collinearityCondition(Aprime, Bprime, Cprime)
```

Теперь давайте проверим их равенство:

calculate {
    val condition1 = concurrencyCondition(a, b, c) * collinearityCondition(A1, B1, C1) * collinearityCondition(A2, B2, C2)
    val condition2 = collinearityCondition(Aprime, Bprime, Cprime)
    println(condition1 eq condition2)
    println()
}

(calculate нужен, чтобы войти в область работы с многочленами, т.е. чтобы их умножать и приравнивать.) Выведется true. Т.е. многочлены абсолютно равны (а не просто пропорциональны).

Это чудо означает, что первое условие выполняется (т.е. его многочлен зануляется) тогда и только тогда, когда выполняется второе условие. При этом первое условие выполняется, когда выполняется хотя бы одно из следующих условий:

$a$ , $b$ и $c$ конкурентны,
$A_1$ , $B_1$ и $C_1$ коллинеарны,
$A_2$ , $B_2$ и $C_2$ коллинеарны. Если отбросить второй и третий пункт, то получим исходную требуемую равносильность. При этом эти два пункта просто указывают на возможные вырождаемости рисунка, при которых достигается коллинеарность $A'$ , $B'$ и $C'$ . Но все предполагают, что всё-таки рисунок не вырожден с самого начала, поэтому всё хорошо. Теорема доказана!

Завершение

Этот эксперимент не является каким-то цельным сюжетом, а состоит из множества мелких сюжетов. Больше сюжетов можно найти в других файлах этого проекта. Также этот фреймворк пока ещё является нестабильным, и есть довольно глобальные планы по его развитию. А вместе с этим пока не заканчивается и этот эксперимент.

Но сначала короткое теоретическое введение: о чём речь?​

Время экспериментов!​

Сюжет: прямая Эйлера​

Сюжет: теорема Дезарга​

Завершение​

Но сначала короткое теоретическое введение: о чём речь?

Время экспериментов!

Сюжет: прямая Эйлера

Сюжет: теорема Дезарга

Завершение