- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
- 12
- 13
- 14
- 15
- 16
- 17
- 18
- 19
- 20
- 21
- 22
- 23
- 24
- 25
- 26
- 27
- 28
- 29
- 30
- 31
- 32
- 33
- 34
- 35
- 36
- 37
- 38
- 39
- 40
- 41
- 42
- 43
- 44
- 45
- 46
- 47
- 48
- 49
- 50
- 51
- 52
- 53
- 54
- 55
- 56
- 57
- 58
- 59
- 60
- 61
- 62
- 63
- 64
- 65
- 66
- 67
- 68
- 69
- 70
- 71
- 72
- 73
- 74
- 75
- 76
- 77
- 78
- 79
- 80
- 81
- 82
- 83
- 84
- 85
- 86
- 87
- 88
(set-logic UF)
; https://smtlib.cs.uiowa.edu/logics.shtml
; UF for the extension allowing free sort and function symbols
(set-option :produce-proofs true)
(declare-sort M_wff)
; AND2
(declare-fun M_a2 (M_wff M_wff) M_wff)
; AND3
(declare-fun M_a3 (M_wff M_wff M_wff) M_wff)
; (AND2 a b) <=> (AND2 b a)
(assert
(forall ( (a M_wff) (b M_wff) )
(=
(M_a2 a b)
(M_a2 b a)
)
)
)
; (AND2 a a) <=> a
(assert
(forall ( (a M_wff) )
(=
(M_a2 a a)
a
)
)
)
; (AND2 a (AND2 b c)) <=> (AND3 a b c)
(assert
(forall ( (a M_wff) (b M_wff) (c M_wff) )
(=
(M_a2 a (M_a2 b c))
(M_a3 a b c)
)
)
)
; (AND3 a b c) <=> (AND3 b a c)
(assert
(forall ( (a M_wff) (b M_wff) (c M_wff) )
(=
(M_a3 a b c)
(M_a3 b a c)
)
)
)
; IMPL - implication
(declare-fun M_impl (M_wff M_wff) M_wff)
; http://us.metamath.org/ileuni/ax-1.html
; Axiom Simp
; (IMPL a (IMPL b a)) <=> (AND2 a b)
(assert
(forall ( (a M_wff) (b M_wff) )
(=
(M_impl a (M_impl b a))
(M_a2 a b)
)
)
)
...
Весь код не влазит.
https://rise4fun.com/Z3/GnfIH
https://paste.debian.net/hidden/38ef8493/ (запасная ссылка)
Переписывал Metamath на язык из SMT солверов https://smtlib.cs.uiowa.edu/language.shtml
Z3 даже умеет доказывать какую-то питушню там.
Follow us!
Вроде Снаут упоминал какой-то плагин, который курицу конвертит в SMT для сольвера, а потом пруф обратно импортирует?
Какое прелестное название! А какие ассоциации возникают )))
И даже если правильно, реализациии Gallina-интерпретатора на SMT-языке нет. Да и вообще, какие там есть реализации Gallina-интерпретатора, сколько есть таких реализаций и на каких языках?
А нафига. Он же от SMT сольвера пруф получает. И если этот пруф проходит проверку, то в общем-то пофиг и на корректность плагина и на корректность сольвера.
З.Ы. Сорок тысяч обезьян, рандомно стучащих по клаве -- тоже вполне валидный способ доказывать теоремы.
Если некая хрень неправильно переводит из одного языка в другой, получает некое доказательство которое оно тоже неправильно переводит, но которое по случайному стечению обстоятельств оказывается правильным для той теоремы (баги аннигилировались как-то, хуй знает) - это тоже не очень хорошая ситуация.
Там, имхо, очень далеко до "почти". https://www.absint.com/compcert/structure.htm
https://www.absint.com/compcert/compcert_diagram.png - всё что выше пунктира - не доказано, а просто запрограммировано на OCaml.
Еще одна попытка сделать формально доказанный компилятор сишечки - это в рамках Metamath Zero пытаются какой-то компилятор MMC сделать https://youtu.be/CxS0ONDfWJg?t=218
https://stackoverflow.com/a/14589567
> Line 21 is syntactically correct if and only if the N in IsPrime<N> is prime. Otherwise, typen is an integer, not a template, so typen<1>() is parsed as (typen<1)>() which is syntactically incorrect because () is not a syntactically valid expression.
Ой мама, как же весело наверное писать для крестов полноценный IDE с кодинсайтом
Почему? В итоге ведь всё нормально получилось, обезьянки наебашили правильный пруф для конкретной задачи вопреки теории вероятности. Пруф от этого не стал каким-то зашкваренным, он ведь проходит проверку.
Ну в каких-то других ситуациях, где звёзды не так удачно лягут, ты увидишь багу и пофиксишь.
Но надо б конечно себя переосилить и разобраться в этом Coq чтоб более обоснованно его раскритиковать
Мне, наоборот, metamath коммьюнити претит. Бегают с лозунгами, прямо как растоманы: "у нас самая большая библиотека в 100500 лемм!!!" А на самом деле, у них тупо нет тактик, и они в библиотеку высрали все промежуточные леммы, большая часть которых никакого интереса не представляет.
Как-то на HN (когда ещё туда ходил срать) мне один мета-математик доказывал, что теория типов — "хуйня, ибо из-за неё медленно!"
Я не на комьюнити смотрю, а на свойства языка. Язык Metamath для меня выглядит куда более понятным, чем язык Gallina, и проверятель пруфов для Metamath написать явно проще. Вот взять например этот мануал:
https://coq.github.io/doc/master/refman/language/core/basic.html#lexical-conventions
Читаем:
> Numbers are sequences of digits with an optional fractional part and exponent, optionally preceded by a minus sign. Hexadecimal numbers start with 0x or 0X. bigint are integers; numbers without fractional nor exponent parts. bignat are non-negative integers. Underscores embedded in the digits are ignored, for example 1_000_000 is the same as 1000000.
Какие такие числа? Я ни про какие числа не знаю. Какая там аксиоматика? Арифметика Пеано или Пресбургера?
> integer and natural are limited to the range that fits into an OCaml integer (63-bit integers on most architectures). bigint and bignat have no range limitation.
OCaml? Я не хочу знать ни про какой OCaml и мне совершенно не должно быть важно, какие там в нем лимиты для каких-то чисел.
Ладно, читаем дальше.
>Keywords
> The following character sequences are keywords defined in the main Coq grammar that cannot be used as identifiers (even when starting Coq with the -noinit command-line flag):
Эмм, че? Что такое Fixpoint? А что такое CoFixpoint? Зачем это нужно?
Допустим я хочу свой интерпретатор Gallina имплементнуть, в каком месте мне надо читать о точном семантическом смысле Fixpoint и CoFixpoint? Зачем вводить подобную питушню на уровне базового языка??? Это же можно описать как некие аксиомы и теоремы, которые там как-то вычисляются. Почему не начинать с более базовых вещей?
И та, и другая там есть в стандартной либе. Тактика `lia` работает с последней.
> Что такое Fixpoint?
Структурная рекурсия.
> А что такое CoFixpoint?
Структурная ко-рекурсия.
> Зачем это нужно?
Ну а зачем нужна рекурсия?
> Почему не начинать с более базовых вещей?
Это и есть базовые вещи в CoC.
> Это же можно описать как некие аксиомы и теоремы, которые там как-то вычисляются.
В Coq нет ни "теорем", ни "аксиом"! Только функции и термы. Это не ма-те-ма-тическая питушня, а функциональный язык программирования, с помощью которого можно творить ма-те-ма-тическую питушню. Короче, попробуй сам и поймёшь.
> Структурная ко-рекурсия.
В Metamath ничего этого нет.
И определил Питуз базовую питулю переписывания термов, и научил различать правильное и неправильное доказательство, и сказал, что всё остальное человек должен сделать своими руками
> Ну а зачем нужна рекурсия?
У меня на контроллерах не нужна, от нее стек быстро кончается. В Metamath тоже нет никакой рекурсии как базового понятия, и ничего, работает вроде. Зачем ее вводить как базовую сущность?
> Это и есть базовые вещи в CoC.
Зачем надо делать так, если можно начать с простого, а потом через простое выразить исчисление конструкций?
> В Coq нет ни "теорем", ни "аксиом"! Только функции и термы. Это не ма-те-ма-тическая питушня, а функциональный язык программирования, с помощью которого можно творить ма-те-ма-тическую питушню.
Ну хорошо, есть функции и термы. А где это это формально определено? Предположим я упоролся и хочу написать свою альтернативную реализацию Gallina на сишечке - что мне прочитать, чтоб по мотивам прочитанного я мог написать питушню на сишке, которая будет полностью соответствовать семантике той Gallina которая в доверенном ядре этого Coq?
[[citation needed]] Емнип, в metamаth можно запилить теорию Фреге, и он её сожрёт и не подавится.
У меня в Coq никаких брадобреев нет, поэтому я за Coq.
Не слышал про теорию Фреге. Знаю что есть теорема Фреге (P → (Q→R)) → ((P→Q) → (P→R)), и в metamath она есть http://us.metamath.org/ileuni/ax-2.html
> У меня в Coq никаких брадобреев нет, поэтому я за Coq.
Мы это вроде уже обсуждали. Брадобреи возникают в наивной теории множеств. В ZFC и IZF они не возникают, но могут быть другие парадоксы, это да. Но формальная система в Coq от каких-либо парадоксов тоже не застрахован, так что тут условия равны.
Я про наивную теорию множеств. Он её придумал.
> Но формальная система в Coq от каких-либо парадоксов тоже не застрахован
Теория типов как раз именно от этого и страхует.
> так что тут условия равны
Так что нет.
Эмм, но ведь нет же. Разве теория типов позволяет доказать непротиворечивость теории типов? Чем доказывается непротиворечивость теории типов?
См "вторая теорема Гёделя"
Ничем, но парадоксов в ней ещё не нашли.
Теория типов, как считается, изолирует систему от попадания зашкваренных частиц.
"как считается", да. Четкого доказательства этому нет, да и не может быть.
Верно. Но это ещё не повод переходить на PHP.
Тактики - дело наживное. Меня больше волнует тот факт, что написать свой Gallina-интерпретатор (альтернативное доверенное ядро проверки питушни) - нихуя не просто, какие-то неподвижные точки прямо в сам язык встроены. Зачем? Зачем? Почему это не теоремы-аксиомы? Почему не сделать максимально простое доверенное ядро, а там уж на него навешивать всякие неподвижные точки, кванторы-шманторы, типы и прочую такую питулю?
> Как-то на HN (когда ещё туда ходил срать) мне один мета-математик доказывал, что теория типов — "хуйня, ибо из-за неё медленно!"
"Теория типов хуйня потому что медленно" - хуёвая доебка, согласен. Я до теорий типов могу доебаться намного лучше.
Ты путаешь куритсу с яйтсом. Ключевое слово Theorem в Coq — синоним определения функции. Axiom — примерно тоже, но без определеления. В Coq довольно много заумных ключевых слов, которые зачастую несут чисто декоративную функцию, но ядро языка при этом весьма простое.
Ещё бы не застревать на задачах со звёздочками... Сраный перфекционизм почему-то не даёт забить на них и идти дальше, а решить ума не хватает.
вот вроде бы пофиксил немного...
Доказательство там конечно совершенно нечитаемый пиздец, выглядит оно вот так:
1005:(resolution ((not (= (M_a2 (M_impl @sk0 @sk1) (M_impl @sk1 @sk2)) (M_a2 (M_impl @sk0 @sk1) (M_impl (M_impl @sk0 @sk1) (M_impl @sk1 @sk2))))) (not (= (M_a2 (M_impl @sk0 @sk1) (M_impl (M_impl @sk0 @sk1) (M_impl @sk1 @sk2))) (M_a2 (M_impl (M_impl @sk0 @sk1) (M_impl @sk1 @sk2)) (M_impl @sk0 @sk1)))) (not (= (M_a3 (M_impl (M_impl @sk0 @sk1) (M_impl @sk1 @sk2)) (M_impl @sk0 @sk1) (M_impl @sk0 @sk1)) (M_a2 (M_impl (M_impl @sk0 @sk1) (M_impl @sk1 @sk2)) (M_a2 (M_impl @sk0 @sk1) (M_impl @sk0 @sk1))))) (not (= (M_a3 (M_impl @sk0 @sk1) (M_impl (M_impl @sk0 @sk1) (M_impl @sk1 @sk2)) (M_impl @sk0 @sk1)) (M_a3 (M_impl (M_impl @sk0 @sk1) (M_impl @sk1 @sk2)) (M_impl @sk0 @sk1) (M_impl @sk0 @sk1)))) (not (= (M_a2 (M_impl @sk0 @sk1) (M_a2 (M_impl (M_impl @sk0 @sk1) (M_impl @sk1 @sk2)) (M_impl @sk0 @sk1))) (M_a3 (M_impl @sk0 @sk1) (M_impl (M_impl @sk0 @sk1) (M_impl @sk1 @sk2)) (M_impl @sk0 @sk1)))) (not (= (M_a2 (M_impl @sk0 @sk1) (M_a2 (M_impl (M_impl @sk1 @sk2) (M_impl @sk0 @sk1)) (M_impl @sk1 @sk2))) (M_a3 (M_impl @sk0 @sk1) (M_impl (M_impl @sk1 @sk2) (M_impl @sk0 @sk1)) (M_impl @sk1 @sk2)))) (not (= (M_a3 (M_impl (M_impl @sk1 @sk2) (M_impl @sk0 @sk1)) (M_impl @sk0 @sk1) (M_impl @sk1 @sk2)) (M_a3 (M_impl @sk0 @sk1) (M_impl (M_impl @sk1 @sk2) (M_impl @sk0 @sk1)) (M_impl @sk1 @sk2)))) (not (= (M_a2 (M_impl (M_impl @sk1 @sk2)...
> не осиливают
А как тогда вообще эти авто-пруверы юзать, если они на такой тривиальной теореме сливаются?
Я думаю что авто-пруверы под такую питушню не затачивались, никто не придумывал специальных эвристик под ситуации когда там реализовывали через ассерты систему Гильберта и через эту внутреннюю систему Гильберта доказывали хуиту описанную через эту систему Гильберта. Быть может, если как-нибудь переформулировать эту хуиту в более удобоваримую форму, всякие другие SMT-решатели тоже будут что-то там доказывать.
Разворачивается в... барабанная дробь...
SMT солверы нужны для байтоёбства, зачем их юзать для абстрактной питушни?
А если я ему какое-нибудь sha в виде системы уравнений запишу, он найдёт что было на входе у хеша?
> SMT солверы нужны для байтоёбства, зачем их юзать для абстрактной питушни?
Байтоебство изоморфно абстрактной питушне.
(<=> a b) это значит что для доказывания можно свободно переписывать "b" на "a", и переписывать "a" на "b"
не убирает ничего лишнего, а лишь нарашивает питушню в списке. И доказательство что из "x" выводимо "y" это когда из питушни "x" можно сконструировать "(& y ... некаяхуйня ... )" или когда из "(& y ... некаяхуйня ...)" можно сконструировать x
Тут конечно надо заметить, что модус поненс от этого не становится неинвертируемым. Т.е. если есть (& a b) то из него можно синтезнуть (& a (-> a b), и из (& a (-> a b)) можно тоже обратно синтезнуть (& a b). Это я лишь к тому, что не было b, а теперь он появился.
лучше так.
И да, такую вот переписывающую питушню реализовать достаточно просто. А сколько надо проебать времени, чтобы реализовать свою альтернативную Gallina из этого Coq, чтоб это был standalone executable компилирующийся из сишки?
Это я к тому, что курица -- это всё-таки компроммисс между практичностью и минимальностью, чтобы и в кресты не скатиться и на голом переписывании термов не ебашить.
Любую хуитень можно назвать каким-то компромиссом. Для кого-то сишка -- "компромисс между практичностью и минимальностью", для кого-то кресты -- "компромисс между практичностью и минимальностью", для кого-то еще - ассемблер (а есть еще машинные коды, которые в HEX-редакторе можно руками вбивать). И как определить, чей компромисс более компромиссный?
https://www.youtube.com/watch?v=FtcQrFvnZxs
Понятно.
Настоящий сишник даже под "SMT" пишет как на няшной.
Но придётся принять ислам аксиому индукции?
M_a2 это ж по сути хрень для выражений, которые являются истинными в данном контексте. См. https://en.wikipedia.org/wiki/Hilbert_system