Натуральный числа в Coq задаются через операции.
Задается некоторый начальный объект, и операция добавления единицы.
Inductive nat : Type :=
| O
| S (n : nat).
*подкрашивает красным редактор
Числа будут выглядеть в виде S(S…(S(0))). Например: S(S(S(0))) - это число 3.
Натуральные числа могут быть записаны в различных системах счисления десятичной, шестнадцатеричной, двоичной и т.д.
Данная запись соответствует способу записи числа в виде вертикальных черточек. А 0 соответствует тому что нет ни одной.
При этом, операция и начальное число могут назвать как угодно например:
Inductive nat : Type :=
| Start
| Next (n : nat).
Натуральны числа описывают класс счетных объектов.
Если заземлить, то-есть сопоставить объекты физического мира, то это может быть например кучка камней.
При этом эти объекты должны быть одного типа.
Если складывать камни и килограммы. Это вызывает онтологический дребезг. Но тут килограммы это не счетный объект, для его описания используются другие числа.
С другой стороны если складывать камни и апельсины, то это странно, но с точки зрения математики это все счетные объекты.
А вто шурупы и апельсины, совсем не хочется считать вместе.
Вычитание от натурального числа единицы задается как
Definition pred (n : nat) : nat :=
match n with
| O => O
| S n' => n'
end.
Соответствует определению, что вычитание единицы от уменьшаемого числа n, это получить такое число n’ к которому если добавить единицу то получится исходное уменьшаемое число n.
Далее, например определим операцию сложения чисел.
Definition plus (a : nat) (b : nat) : nat :=
match a with
| O => O
| S a' => S (plus a' b)
end.
Заземление: есть две кучки камней и берем камень из одной кучки и перекладываем в другую, пока есть что перекладывать. После чего получаем кучку с некоторым числом камней.
Coq является proof assistant. Экзокортексом который должен автоматизировать рутинные операции доказательства у математиков. Функциональный объект проверяющий логические догадки. В сети есть база доказанных с помощью его теорем qarith-stern-brocot/theories at master · rocq-community/qarith-stern-brocot · GitHub.
Для данной заметки было бы интересно, проверить достаточно ли того что уже есть для того что бы доказать, что a + b = b + a.
Для натуральных чисел, это утверждение дается как аксиома. Но здесь натуральное число задается через операцию над ним, через операцию добавления следующего.
Заземление: камни берем из левой кучки и перекладываем в правую, и берем из правой и перекладываем в левую. В обоих случаях получается одинаковый результат, если перевести в черточки на стене.
Для физического мира протяженных в пространстве и времени 4D объектов это интуитивно очевидно. Но вполне могут быть разделы физики, описывающие реальность где это совсем не так.
Интересно, достаточно ли того что уже задано для описания натуральных чисел. Для доказательства коммутативности сложения или надо вводить что то дополнительно.
Функцию логических рассуждений выполняет Coq. Как черный ящик внутри которого “функция логики”, то-есть если скажет что OK. То логические рассуждения можно считать доказанными.
Ссылки:
- Учебник Coq Basics: Functional Programming in Coq
- База доказанных теорем qarith-stern-brocot/theories at master · rocq-community/qarith-stern-brocot · GitHub