Хотите пройтись по стопам Евклида и доказать базу. Я проведу вас в занимательный мир формальной математики на примере самого базового алгоритма Евклида для нахождения наибольшего общего делителя.

Для начала стоит понять что такое число, почему это важно? Без базы ничего не получится. Это как дом без фундамента. По этому стоит задуматься над этим фундаментом.

В Coq можно и нужно понимать как устроены числа. Есть два класса представление чисел: числа Пеано и битовые представления чисел. Каждый имеет свою область применения. Главная разница в том для чего служит модель для формализации свойств или для вычислений.

Почему же представление Пеано так удобно для построения модели? Потому что оно полностью рекурсивное и индуктивное. Что это значит для нас. Что мы легко можем выражать рекурсивные функции при этом с гарантией того что рекурсия когда-то закончится.

Но как же строятся числа Пеано? Тут довольно элегантная модель. Постулируется существование двух сущностей: нуля и операции над числом под названием “следующий” (для кратности обозначают как S). Также несколько аксиом что 1) ноль это число 2) если x это число, то S(x) тоже число 3) для любого x, то S(x) не ноль 4) S - инъективная функция: если S(x) = S(y), то x = y. 5) ввод принципа индукции

Принцип индукции основа всей модели. Он позволяет доказывать свойства над бесконечным количеством чисел. Имея лишь две предпосылки: 1) что свойство выполняется для нуля 2) что если свойство выполняется для x, то оно выполняется для S(x)

Как только модель чисел становится индуктивной, путь к формализации алгоритмов вроде gcd открывается сам собой. Евклид пользовался идеей последовательного уменьшения аргументов. Coq использует ту же идею, но оформляет её как хорошо структурированную рекурсию по числам Пеано.

Определение функции сводится к простому разбору случаев. Если один из аргументов равен нулю, результатом становится второй. Если оба числа положительные, выполняется шаг алгоритма Евклида: из большего вычитается меньшее, после чего рекурсивно вызывается та же функция. Мера (a + b) гарантирует убывание на каждом шаге, поэтому рекурсия корректно завершается. Все обязательства на доказательства завершимости и корректности автоматически решаются стандартной арифметикой.

Обычная индукция здесь неудобна, поэтому вводится принцип сильной индукции. Он основан на единственной предпосылке: если из того, что свойство выполняется для всех a < b , следует выполнение свойства для самого b , то свойство выполняется для всех натуральных чисел. Такой подход позволяет работать со сложными мерами уменьшения, вроде тех, что используются в определении gcd .

База индукции в этой схеме неявная. Для минимального натурального числа просто не существует меньших значений, поэтому требование «свойство выполняется для всех меньших» автоматически истинно. Благодаря линейной структуре натуральных чисел и наличию минимального элемента такой переход корректен.

Таким образом, введение чисел Пеано и принципа сильной индукции завершает первую часть — фундамент полностью очерчен, дальше без излишней абстракции можно переходить к самим доказательствам свойств gcd в Coq. Логично вынести это в отдельную часть, чтобы не смешивать построение модели и работу алгоритма.