- 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 даже умеет доказывать какую-то питушню там.
j123123 28.04.2021 16:21 # 0
bormand 28.04.2021 17:07 # 0
j123123 28.04.2021 17:10 # 0
j123123 28.04.2021 17:13 # 0
bormand 28.04.2021 17:34 # +1
Вроде Снаут упоминал какой-то плагин, который курицу конвертит в SMT для сольвера, а потом пруф обратно импортирует?
CHayT 28.04.2021 17:36 # +2
JloJle4Ka 28.04.2021 17:37 # +1
Какое прелестное название! А какие ассоциации возникают )))
CHayT 29.04.2021 01:01 # +1
j123123 28.04.2021 17:37 # 0
И даже если правильно, реализациии Gallina-интерпретатора на SMT-языке нет. Да и вообще, какие там есть реализации Gallina-интерпретатора, сколько есть таких реализаций и на каких языках?
bormand 28.04.2021 17:40 # +1
А нафига. Он же от SMT сольвера пруф получает. И если этот пруф проходит проверку, то в общем-то пофиг и на корректность плагина и на корректность сольвера.
З.Ы. Сорок тысяч обезьян, рандомно стучащих по клаве -- тоже вполне валидный способ доказывать теоремы.
j123123 28.04.2021 17:43 # +1
Если некая хрень неправильно переводит из одного языка в другой, получает некое доказательство которое оно тоже неправильно переводит, но которое по случайному стечению обстоятельств оказывается правильным для той теоремы (баги аннигилировались как-то, хуй знает) - это тоже не очень хорошая ситуация.
bormand 28.04.2021 17:47 # 0
j123123 28.04.2021 19:53 # 0
Там, имхо, очень далеко до "почти". 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
CHayT 28.04.2021 20:05 # 0
j123123 28.04.2021 19:59 # 0
PolinaAksenova 28.04.2021 21:51 # +1
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.
CHayT 28.04.2021 21:54 # +1
MAKAKA 29.04.2021 00:29 # +1
Ой мама, как же весело наверное писать для крестов полноценный IDE с кодинсайтом
j123123 29.04.2021 05:11 # 0
CHayT 28.04.2021 17:47 # +2
bormand 28.04.2021 17:50 # +2
Почему? В итоге ведь всё нормально получилось, обезьянки наебашили правильный пруф для конкретной задачи вопреки теории вероятности. Пруф от этого не стал каким-то зашкваренным, он ведь проходит проверку.
Ну в каких-то других ситуациях, где звёзды не так удачно лягут, ты увидишь багу и пофиксишь.
CHayT 28.04.2021 17:20 # +2
j123123 28.04.2021 18:27 # +1
Но надо б конечно себя переосилить и разобраться в этом Coq чтоб более обоснованно его раскритиковать
CHayT 28.04.2021 20:12 # 0
Мне, наоборот, metamath коммьюнити претит. Бегают с лозунгами, прямо как растоманы: "у нас самая большая библиотека в 100500 лемм!!!" А на самом деле, у них тупо нет тактик, и они в библиотеку высрали все промежуточные леммы, большая часть которых никакого интереса не представляет.
Как-то на HN (когда ещё туда ходил срать) мне один мета-математик доказывал, что теория типов — "хуйня, ибо из-за неё медленно!"
j123123 29.04.2021 01:03 # 0
Я не на комьюнити смотрю, а на свойства языка. Язык 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? Зачем вводить подобную питушню на уровне базового языка??? Это же можно описать как некие аксиомы и теоремы, которые там как-то вычисляются. Почему не начинать с более базовых вещей?
CHayT 29.04.2021 01:15 # 0
И та, и другая там есть в стандартной либе. Тактика `lia` работает с последней.
> Что такое Fixpoint?
Структурная рекурсия.
> А что такое CoFixpoint?
Структурная ко-рекурсия.
> Зачем это нужно?
Ну а зачем нужна рекурсия?
> Почему не начинать с более базовых вещей?
Это и есть базовые вещи в CoC.
> Это же можно описать как некие аксиомы и теоремы, которые там как-то вычисляются.
В Coq нет ни "теорем", ни "аксиом"! Только функции и термы. Это не ма-те-ма-тическая питушня, а функциональный язык программирования, с помощью которого можно творить ма-те-ма-тическую питушню. Короче, попробуй сам и поймёшь.
j123123 29.04.2021 01:28 # +1
> Структурная ко-рекурсия.
В Metamath ничего этого нет.
И определил Питуз базовую питулю переписывания термов, и научил различать правильное и неправильное доказательство, и сказал, что всё остальное человек должен сделать своими руками
> Ну а зачем нужна рекурсия?
У меня на контроллерах не нужна, от нее стек быстро кончается. В Metamath тоже нет никакой рекурсии как базового понятия, и ничего, работает вроде. Зачем ее вводить как базовую сущность?
> Это и есть базовые вещи в CoC.
Зачем надо делать так, если можно начать с простого, а потом через простое выразить исчисление конструкций?
> В Coq нет ни "теорем", ни "аксиом"! Только функции и термы. Это не ма-те-ма-тическая питушня, а функциональный язык программирования, с помощью которого можно творить ма-те-ма-тическую питушню.
Ну хорошо, есть функции и термы. А где это это формально определено? Предположим я упоролся и хочу написать свою альтернативную реализацию Gallina на сишечке - что мне прочитать, чтоб по мотивам прочитанного я мог написать питушню на сишке, которая будет полностью соответствовать семантике той Gallina которая в доверенном ядре этого Coq?
CHayT 29.04.2021 01:32 # 0
[[citation needed]] Емнип, в metamаth можно запилить теорию Фреге, и он её сожрёт и не подавится.
У меня в Coq никаких брадобреев нет, поэтому я за Coq.
j123123 29.04.2021 01:39 # 0
Не слышал про теорию Фреге. Знаю что есть теорема Фреге (P → (Q→R)) → ((P→Q) → (P→R)), и в metamath она есть http://us.metamath.org/ileuni/ax-2.html
> У меня в Coq никаких брадобреев нет, поэтому я за Coq.
Мы это вроде уже обсуждали. Брадобреи возникают в наивной теории множеств. В ZFC и IZF они не возникают, но могут быть другие парадоксы, это да. Но формальная система в Coq от каких-либо парадоксов тоже не застрахован, так что тут условия равны.
CHayT 29.04.2021 01:44 # 0
Я про наивную теорию множеств. Он её придумал.
> Но формальная система в Coq от каких-либо парадоксов тоже не застрахован
Теория типов как раз именно от этого и страхует.
> так что тут условия равны
Так что нет.
j123123 29.04.2021 01:48 # 0
Эмм, но ведь нет же. Разве теория типов позволяет доказать непротиворечивость теории типов? Чем доказывается непротиворечивость теории типов?
См "вторая теорема Гёделя"
CHayT 29.04.2021 01:58 # 0
Ничем, но парадоксов в ней ещё не нашли.
j123123 29.04.2021 01:59 # 0
j123123 29.04.2021 01:45 # 0
CHayT 29.04.2021 01:55 # 0
Теория типов, как считается, изолирует систему от попадания зашкваренных частиц.
j123123 29.04.2021 01:58 # 0
"как считается", да. Четкого доказательства этому нет, да и не может быть.
CHayT 29.04.2021 02:00 # 0
Верно. Но это ещё не повод переходить на PHP.
j123123 29.04.2021 01:55 # 0
j123123 29.04.2021 01:08 # 0
Тактики - дело наживное. Меня больше волнует тот факт, что написать свой Gallina-интерпретатор (альтернативное доверенное ядро проверки питушни) - нихуя не просто, какие-то неподвижные точки прямо в сам язык встроены. Зачем? Зачем? Почему это не теоремы-аксиомы? Почему не сделать максимально простое доверенное ядро, а там уж на него навешивать всякие неподвижные точки, кванторы-шманторы, типы и прочую такую питулю?
> Как-то на HN (когда ещё туда ходил срать) мне один мета-математик доказывал, что теория типов — "хуйня, ибо из-за неё медленно!"
"Теория типов хуйня потому что медленно" - хуёвая доебка, согласен. Я до теорий типов могу доебаться намного лучше.
CHayT 29.04.2021 01:21 # 0
Ты путаешь куритсу с яйтсом. Ключевое слово Theorem в Coq — синоним определения функции. Axiom — примерно тоже, но без определеления. В Coq довольно много заумных ключевых слов, которые зачастую несут чисто декоративную функцию, но ядро языка при этом весьма простое.
bormand 28.04.2021 18:32 # +1
Ещё бы не застревать на задачах со звёздочками... Сраный перфекционизм почему-то не даёт забить на них и идти дальше, а решить ума не хватает.
JloJle4Ka 28.04.2021 18:35 # +1
OCETuHCKuu_nemyx 28.04.2021 19:13 # +1
CHayT 28.04.2021 20:14 # 0
j123123 28.04.2021 16:29 # 0
j123123 28.04.2021 16:59 # 0
вот вроде бы пофиксил немного...
j123123 29.04.2021 05:16 # +3
Доказательство там конечно совершенно нечитаемый пиздец, выглядит оно вот так:
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)...
j123123 29.04.2021 05:19 # +3
bormand 29.04.2021 12:50 # +2
> не осиливают
А как тогда вообще эти авто-пруверы юзать, если они на такой тривиальной теореме сливаются?
j123123 29.04.2021 13:11 # 0
Я думаю что авто-пруверы под такую питушню не затачивались, никто не придумывал специальных эвристик под ситуации когда там реализовывали через ассерты систему Гильберта и через эту внутреннюю систему Гильберта доказывали хуиту описанную через эту систему Гильберта. Быть может, если как-нибудь переформулировать эту хуиту в более удобоваримую форму, всякие другие SMT-решатели тоже будут что-то там доказывать.
j123123 29.04.2021 13:13 # +1
CHayT 29.04.2021 14:10 # +2
Разворачивается в... барабанная дробь...
SMT солверы нужны для байтоёбства, зачем их юзать для абстрактной питушни?
bormand 29.04.2021 14:14 # +3
А если я ему какое-нибудь sha в виде системы уравнений запишу, он найдёт что было на входе у хеша?
PolinaAksenova 29.04.2021 14:20 # +3
j123123 29.04.2021 15:08 # +1
> SMT солверы нужны для байтоёбства, зачем их юзать для абстрактной питушни?
Байтоебство изоморфно абстрактной питушне.
j123123 30.04.2021 06:48 # 0
(<=> a b) это значит что для доказывания можно свободно переписывать "b" на "a", и переписывать "a" на "b"
j123123 30.04.2021 06:52 # 0
не убирает ничего лишнего, а лишь нарашивает питушню в списке. И доказательство что из "x" выводимо "y" это когда из питушни "x" можно сконструировать "(& y ... некаяхуйня ... )" или когда из "(& y ... некаяхуйня ...)" можно сконструировать x
j123123 30.04.2021 07:06 # 0
Тут конечно надо заметить, что модус поненс от этого не становится неинвертируемым. Т.е. если есть (& a b) то из него можно синтезнуть (& a (-> a b), и из (& a (-> a b)) можно тоже обратно синтезнуть (& a b). Это я лишь к тому, что не было b, а теперь он появился.
j123123 30.04.2021 07:02 # +1
лучше так.
И да, такую вот переписывающую питушню реализовать достаточно просто. А сколько надо проебать времени, чтобы реализовать свою альтернативную Gallina из этого Coq, чтоб это был standalone executable компилирующийся из сишки?
bormand 30.04.2021 08:39 # +2
Это я к тому, что курица -- это всё-таки компроммисс между практичностью и минимальностью, чтобы и в кресты не скатиться и на голом переписывании термов не ебашить.
j123123 30.04.2021 14:43 # 0
j123123 30.04.2021 14:46 # 0
Любую хуитень можно назвать каким-то компромиссом. Для кого-то сишка -- "компромисс между практичностью и минимальностью", для кого-то кресты -- "компромисс между практичностью и минимальностью", для кого-то еще - ассемблер (а есть еще машинные коды, которые в HEX-редакторе можно руками вбивать). И как определить, чей компромисс более компромиссный?
MAuCKuu_nemyx 30.04.2021 21:06 # 0
DypHuu_niBEHb 30.04.2021 21:15 # +1
j123123 01.05.2021 12:38 # +3
https://www.youtube.com/watch?v=FtcQrFvnZxs
CHayT 28.04.2021 16:31 # +3
Понятно.
j123123 28.04.2021 17:00 # 0
bormand 28.04.2021 17:04 # +2
Настоящий сишник даже под "SMT" пишет как на няшной.
j123123 28.04.2021 17:17 # 0
bormand 28.04.2021 18:17 # 0
Но придётся принять ислам аксиому индукции?
j123123 28.04.2021 18:22 # +2
M_a2 это ж по сути хрень для выражений, которые являются истинными в данном контексте. См. https://en.wikipedia.org/wiki/Hilbert_system
PolinaAksenova 28.04.2021 21:57 # 0