Нашли или выдавили из себя код, который нельзя назвать нормальным, на который без улыбки не взглянешь? Не торопитесь его удалять или рефакторить, — запостите его на говнокод.ру, посмеёмся вместе!
+2
Definition idx_compl_r {i : Fin.t N} (j : Fin.t i) : Fin.t N.
remember (fin_to_nat i) as i'.
assert (Hlt : i' < N).
{ rewrite Heqi'. eapply fin_to_nat_lt. }
assert (Heq : i' + (N - i') = N) by lia.
set (j' := Fin.L (N - i') j).
rewrite Heq in j'.
exact j'.
Defined.Ещё один говношедевр. Как кастовать значения типа Fin.t (число в интервале от 1 до N) друг в друга. Разворачивается в 12000 строк кода. "Тому, кто это придумал, надо в голову гвоздь забить".
Запостил: 
CHayT,
27 Августа 2020
Follow us!
Я даже не понял что я изык. «Coq»?
Что такое Ltac? Представь себе парное программирование. Ты приятелю говоришь: так, пили лямду с аргументами a b c. Теперь давай кейз-анализис a. Тут возвращаем это. Тут возвращаем то. Теперь давай зови эту функцию. Ну а тут легко, сам разберёшься.
Ну а потом сорцы проебали, и закоммитили в репу стенограмму твоего монолога. Это Ltac.
этож курица
«Галлина Бланка», буль-буль, буль-буль!
«Галлина Бланка», буль-буль, буль-буль!
«Галлина Бланка», буль-буль, буль-буль!
Ко-ко, ко-ко, ко-ко, ко-ко, «Файн фудс»!
Ко-ко, ко-ко, ко-ко, ко-ко, «Файн фудс»!
Ко-ко, ко-ко, ко-ко, ко-ко, «Файн фудс»!
«Кнорр», вкусен и скор!
ты помнишь
?
- там вот в примере разбирают как доказывают 2 + 2 = 4, и делается это без всяких лямбда-исчислений, типов и прочей хуйни, чисто на term rewriting, просто применяем набор каких-то правил переписывания и одну хуйню трансформируем в другую, вот и все. И при желании всю эту типопитушню можно какими-то говнотермами имитировать, т.е. всякого рода типы можно уже выражать в терминах каких-то разрешенных правил для переписывания терма на терм. Только вот нахуй эти типы нужны? Профит в чем?
"Возня" с типами нужна во-первых для того, чтобы карманный брадобрей не снёс тебе яичко (и чтобы не наступить на другие известные парадоксы). Во-вторых, переписывание термов -- это тупо частный случай того, что можно сотворить в Coq.
У вас охуенный тредик, надо почитат
Так-то от теоремы Гёделя о неполноте никакие типы-хуипы не спасут, сколько ими не обмазывайся.
> Во-вторых, переписывание термов -- это тупо частный случай того, что можно сотворить в Coq.
Нет, не так. Любая хуйня, которую можно сотворить в Coq, может быть выражена некоторой питушней через переписывание термов. Так что это все по-сути равнозначная хуйня, можно и в том же metamath напитушить эмуляцию всей хуйни из Coq, если сильно упороться, и в Coq можно запилить встроенный metamath и через него доказывать хуйню. Это как рассуждать, что первично, курица или яйцо
Она тут вообще не при чём. ТГ говорит о том, что в любой достаточно развитой формальной системе всегда найдутся утверждения, правильность или противоречивость _не удастся доказать_ в рамках этой системы (отсюда "неполнота"). От этого никому ни жарко и не холодно, кроме вымерших верунов в программу Гильберта, ибо подобные утверждения (или обратные им) можно всегда принять как аксиомы, получив тем самым две новые формальные системы, и пойти дальше. Логические же парадоксы уничтожают формальные системы, т.к. с их помощью _можно доказать_ любую фигню. Почувствуй разницу.
> Любая хуйня, которую можно сотворить в Coq, может быть выражена некоторой питушней через переписывание термов.
Это редукционизм. "И метамаф и кок компилируются в машинные коды, поэтому прувить всё надо на них."
Не, нихуя. ТГ говорит что формальная система или неполна (существуют утверждения, которые нельзя ни доказать, ни опровергнуть) или противоречива (сушествуют утверждения, которые можно и доказать, и опровергнуть). И вот если говорить о хуйне с брадобреем, которую называют еще парадоксом Рассела, то это тоже к теореме Гёделя относится т.к. это про противоречивость логической системы Фреге, которая была ранней попыткой аксоиматизации Канторовской теории множеств. Так что ТГ вполне себе имеет отношение к этой всей хрени.
Впрочем похуй, это всё ньюансы. У меня таки вопрос - а каким образом наличие какой-то там хитровыебаной системы типов страхует меня от противоречивой формальной системы (т.е. ситуации, когда одно и то же утверждение можно и доказать, и опровергнуть)? В Coq например были какие-то баги, когда там ложь доказывали https://github.com/clarus/falso
Ты то же самое сейчас сказал. Противоречивые формальные системы бессмысленны с практической точки зрения, поэтому на них не стоит заострять внимание. Про неполные системы я расписал.
> У меня таки вопрос - а каким образом наличие какой-то там хитровыебаной системы типов страхует меня от противоречивой формальной системы
Термы в Coq имеют (невидимый по умолчанию) universe index, и типы выражений обязаны иметь больший индекс, нежели термы, которые они описывают. Таким образом, если ты попытаешься создать тип брадобреев, которые (не)бреют себя, получишь ошибку universe inconsistency.
> В Coq например были какие-то баги, когда там ложь доказывали https://github.com/clarus/falso
Емнип, эта петушня coqchk не проходила. (coqchk является доверенным ядром, а coqtop/coqc — нет). Ставить древнюю версию, чтобы проверить, мне лень. Ну а так, баги бывают, и никто не гарантирует (и не может гарантировать), что в coqchk их нет. Поэтому размер доверенного ядра тайпчекера стараются держать очень маленьким и про все изменения сначала публикуют peer-reviewed статью.
Ну как бы да, это один из возможных вариантов, можно википедию процитировать https://ru.wikipedia.org/wiki/Парадокс_Рассела#Теория_типов_Рассела :
> Первым, кто предложил теорию, свободную от парадокса Рассела, был сам Рассел. Он разработал теорию типов, первая версия которой появилась в книге Рассела «Принципы математики[en]» в 1903 году[24]. В основе этой теории лежит следующая идея: простые объекты в этой теории имеют тип 0, множества простых объектов имеют тип 1, множества множеств простых объектов имеют тип 2 и так далее. Таким образом, ни одно множество не может иметь себя в качестве элемента. Ни множество всех множеств, ни расселовское множество не могут быть определены в этой теории. ....
Конкретно парадокс Рассела решается и без этого, можно просто взять ZF или ZFC, где этого парадокса нет. Если же говорить в общем и целом, может ли какая-то система типов защитить от получения противоречивой формальной системы (а не только защитить от парадокса Рассела) ?
Иными словами, существует ли строгое доказательство, что если мы делаем формальную систему с такой-то системой типов, то она точно будет непротиворечивой?
> на вопрос "зачем нужны типы" ещё Рассел ответил
> может ли какая-то система типов защитить от получения противоречивой формальной системы
Нет, программа Гильберта была направлена на это, и всем известно, чем она кончилась. inb4: ну раз системы типов не гарантируют божественной непротиворечивости, то они не нужны. А вот и нужны. Недаром ко всем динамическим недоязыкам (erlang, python, js, ...) со слезами и соплями потом пытаются сбоку привинтить систему типов.
> можно просто взять ZF или ZFC, где этого парадокса нет
Нахер? Конструктивистская логика тем хороша, что это по сути функциональный язык программирования. "Доказательство" на coq без аксиом можно взять и запустить, это тупо некая чистая тотальная функция. Тем он и красив.
Ну вот допустим я на coq докажу теорему Пифагора. Что будет это доказательство делать, если его взять и запустить? И нахуя его вообще запускать?
Что за хуйню обычно доказывают в этом coq, и каким образом умение "запускать" доказательства дает какой-то профит?
Эм, по джвум сторонам возвращать длину третьей?
Как я уже говорил, доказательство утверждения P в coq — чистая тотальная функция, имеющая тип P.
Тип тотальной чистой функции "A -> B -> C" можно интерпретировать как теорему вида "из A и B следует С". Тип "(A + B) -> C" можно интерпретировать как "из A или B следует С". Допустим, что False — тип без конструкторов. Создать значение с тиким типом нельзя. Тогда функцию типа "A -> False" можно интерпретировать как теорему вида "A неверно" (ибо из A следует какая-то хуйня) или "не A". Таким образом у тебя получается почти что нормальная логика (без исключённого третьего, правда), доказывай ей что хочешь.
Нет, не так. Сам факт существования программы с неким типом — это и есть доказательство. Профит в том, что разница между "вызвать функцию" и "modus ponens", "программированием" и "логикой" стирается, а чем меньше сущностей — тем лучше.
как Coq поймет, что не любые a b c подходят, а только те, что являются сторонами прямоугольного треугольника? (иначе ты как раз получишь ПИФОГОР СОСНУЛЕЙ Т.К. НЕ СОШЛОСЬ!)
Но что можно запихнуть? Угол между двумя сторонами (зная только длины трёх сторон) мы можем посчитать по теореме косинусов. Значит, придётся доказывать теорему косинусов, а она обычно доказывается через теорему Пифагора.
Отпадает. Нужно придумать, как ещё можно описать треугольник.
Верно замечено. Эту часть я опустил (см. "..... -> "), ибо описать "Евклидово пространство" и "треугольник" ещё надо суметь, за этим обращайся к этим ребятам: http://geocoq.github.io/GeoCoq/
Какой хардкор )))
Почему не все 24, интересно…