Пруфчекинг

[george66]

На меня сошло вдохновение и я формализовал свои доказательства в Coq. Общее впечатление -- это как вышивать крестиком, стоя на голове. В своё время делал общие обзоры на мехмате МГУ, вот здесь видео (Zoom во время карантина) и некоторые тексты по Coq и Metamath
https://cloud.mail.ru/public/H97n/Lt8W6MoqU
https://cloud.mail.ru/public/u4GW/oiuEMf2y9
По Metamath, возможно, не всё будет понятно (я перед этим делал живой доклад), там приложена книжка Мартин-Лёфа, прочитайте там про системы Поста, после этого Metamath легко будет понять (детали объясню). Среди популярных пруфчекеров Coq, Isabelle, Lean похожи друг на друга, а Metamath резко отличается. Coq, Isabelle, Lean дают некоторую сильную теорию (вроде ZF, но более удобную для практической записи доказательств) и предлагают всё записывать в ней. Формально записанные доказательства похожи на программы на функциональных языках (вроде Haskell). Также там берётся за основу принцип Пуанкаре "не надо доказывать то, что можно проверить вычислением". Если мы хотим в Coq доказать $2\times 2=4$, достаточно написать слово reflexivity. Потому что Coq, прежде чем доказывать равенство, вычисляет обе его части до упора и получает $4=4$. Помните школьные упражнения "раскрыть скобки, упростить и сократить"? Вот Coq постоянно это делает, а пользователь должен находить, что мешает и делать сам, где Coq не может (понять сообщения Coq об ошибках -- то ещё искусство). Metamath устроен совсем по-другому, он даёт минимум (чуть улучшенные производящие системы Поста), там можно с нуля выписывать любые аксиомы и доказывать $2\times 2=4$ шаг за шагом из аксиом Пеано. Многим это нравится, на сайте Metamath выложено огромное количество формализованных теорем. Но при попытке самостоятельно формализовать подстановку и кванторные правила Norman Megill (создатель Metamath) впал в отчаянье и взял за основу нестандартную аксиоматику, придуманную стариком Тайтельбаумом, известным под псевдонимом "Тарский". Она проще для формализации, чем обычная, но работать в ней -- цирк, сравнимый с Coq. Итого, удобного пруфчекера пока нет, все пруфчекеры сложны.

[zykov]

Тема интересная.
Прежде чем создавать систему, нужно знать требования (requirements) к ней.

Если получится как-то здесь описать, что из себя представляет "удобный" пруфчекер (список его "удобных" характеристик), то было бы интересно посмотреть.
(Видимо тут важен не сам пруфчекер - это довольно примитивный алгоритм - а способ записи доказательства для него.)

[talash]

george66
А вот это доказательство насколько сложно ввести и проверить через Coq?

Цитата:

1. Несчетность множества точек отрезка $[ 0,1 ]$
Множество $A$ называется несчетным, если оно неэквивалентно множеству натуральных чисел.

Теорема Кантора ... : Множество точек отрезка $[0,1]$ несчетно.

↓Предположим, что множество точек $[0,1]$ счетно: $x_1, x_2, \; \ldots, \; x_n, \; \ldots \; .$ Разделим отрезок $[0,1]$ на $3$ равные части: $[0, \frac {1}{3}]; [\frac {1}{3}; \frac {2}{3}]; [\frac {2}{3}; 1]$, и выберем тот из отрезков, который не содержит $x_1$ ни внутри, ни на границе. Обозначим его через $\Delta_1$, т.е. $x_1$ не принадлежит $\Delta_1$. $\Delta_1$ также поделим на $3$ равные части и выберем ту часть, которая не содержит $x_2$ ни внутри, ни на границе. Обозначим эту часть $\Delta_2$, т.е. $x_2$ не принадлежит $\Delta_ 2$, и $\Delta_2\subset \Delta _1$. Продолжая эту процедуру, мы получим последовательность вложенных друг в друга отрезков $\Delta_1\supset \Delta_2\supset \ldots\supset \Delta_{n-1}\supset \Delta_n\supset \ldots \; .$ Причем длины этих отрезков стремятся к нулю и $\forall n \; x_n\notin \Delta_n$. В силу принципа вложенных отрезков существует точка $c\in \Delta_n$ для $\forall n$, причем $c\ne x_n \; \forall n$. А следовательно, точка $c$ в исходном списке точек отрезка отсутствует, т.е. точка $c$ оказалась незанумерованной. Это противоречие доказывает теорему. ↑

[tolstopuz]

talash в сообщении #1646603 писал(а):

А вот это доказательство насколько сложно ввести и проверить через Coq?

В поставку Coq входит что-то очень похожее: https://github.com/coq/coq/blob/master/ ... ountable.v

[talash]

Я сам в данный момент Coq не осилю. Мне интересно можно ли аналогично доказать через Coq, что бесконечное множество точек
$x_1=0.9, x_2=0.99, x_3=0.999, ...$ не содержит точку $1$.
Такой примерно план. Поделим отрезок $[0, 1]$ на $11$ равных частей и выберем самую правую часть $[\frac{10}{11}, 1]$, он не будет включать в себя $x_1$ потому что $0.9 < \frac{10}{11}$, затем снова поделим на $11$ равных частей и выберем самую правую часть и этот отрезок не будет включать $x_2$ и т.д. По лемме о вложенных отрезках наши отрезки содержат общую точку и это точка $1$, а наше бесконечное множество точек её не содержит. Доказано.

[EminentVictorians]

george66, а с какой целью Вы делали формализацию? Убедиться в истинности, лучше изучить Coq или что-то другое?

[george66]

talash в сообщении #1646708 писал(а):

Я сам в данный момент Coq не осилю. Мне интересно можно ли аналогично доказать через Coq, что бесконечное множество точек
$x_1=0.9, x_2=0.99, x_3=0.999, ...$ не содержит точку $1$.
Такой примерно план. Поделим отрезок $[0, 1]$ на $11$ равных частей и выберем самую правую часть $[\frac{10}{11}, 1]$, он не будет включать в себя $x_1$ потому что $0.9 < \frac{10}{11}$, затем снова поделим на $11$ равных частей и выберем самую правую часть и этот отрезок не будет включать $x_2$ и т.д. По лемме о вложенных отрезках наши отрезки содержат общую точку и это точка $1$, а наше бесконечное множество точек её не содержит. Доказано.

Каждое следующее число получается из предыдущего добавлением 9/10 остатка до единицы. Простой индукцией доказываем, что все они меньше единицы. Если числа считать рациональными, проблем, наверное, никаких. Как говорить в Coq о действительных числах, я не знаю (теория типов Coq достаточно сильная, но интуиционистская логика Coq может создать проблемы).

-- 19.07.2024, 02:12 --

EminentVictorians в сообщении #1646725 писал(а):

george66, а с какой целью Вы делали формализацию? Убедиться в истинности, лучше изучить Coq или что-то другое?

С целью убедить других, что я что-то доказал. Доказательство, как оно есть, никто не понимает и нигде не печатают.

[tolstopuz]

george66 в сообщении #1646752 писал(а):

Как говорить в Coq о действительных числах, я не знаю (теория типов Coq достаточно сильная, но интуиционистская логика Coq может создать проблемы).

Например, вот так :)
https://github.com/coq/coq/blob/master/ ... able.v#L26

Цитата:

(* Here we use axiom total_order_T, which is not constructive *)

[talash]

george66 в сообщении #1646752 писал(а):

Каждое следующее число получается из предыдущего добавлением 9/10 остатка до единицы. Простой индукцией доказываем, что все они меньше единицы.

Далее утверждаем, что поскольку наше множество бесконечное, то туда входит число $0.(9)$, но не входит $1$, как мы доказали ранее. Отсюда следует, что $0.(9) \neq 1$.
Я думаю, что если Coq подтвердит канторовское доказательство, то и это должен подтвердить.

[EminentVictorians]

george66 в сообщении #1646752 писал(а):

Доказательство, как оно есть, никто не понимает и нигде не печатают.

Если не секрет, в чем заключается само утверждение?

[mihaild]

talash в сообщении #1646774 писал(а):

Далее утверждаем, что поскольку наше множество бесконечное, то туда входит число $0.(9)$

Что, простите?

[Ende]

talash в сообщении #1646774 писал(а):

Далее утверждаем, что поскольку наше множество бесконечное, то туда входит число $0.(9)$, но не входит $1$, как мы доказали ранее. Отсюда следует, что $0.(9) \neq 1$.
Я думаю, что если Coq подтвердит канторовское доказательство, то и это должен подтвердить.

Вам неоднократно пытались объяснить, почему $0.(9) = 1$. Недельный бан за агрессивное невежество и захват темы. Если будете продолжать повторять на форуме эту чушь, баны будут следовать по нарастающей.

[epros]

talash в сообщении #1646708 писал(а):

Мне интересно можно ли аналогично доказать через Coq, что бесконечное множество точек
$x_1=0.9, x_2=0.99, x_3=0.999, ...$ не содержит точку $1$.

Бесконечное множество элементов последовательности $x_n=\frac{1}{10^n}$ не содержит $0$, тем не менее, предел этой последовательности равен $0$. Наверное, это никак невозможно понять без программирования доказательства на Coq? Кстати, доказательства обоих утверждений не потребуют определения действительных чисел.

[george66]

И если напишу свой пруфчекер, назову его "Прион" (чтоб мозги сворачивались).

[epros]

Точно, а потом запрограммировать на нём доказательство теоремы Гудстейна в арифметике Пеано второго порядка. Чтобы понять, как работают подстановки формул вместо предикатных переменных, без чего это доказательство невозможно. И тогда мозги свернутся так, что уж не развернуть.