Нашли или выдавили из себя код, который нельзя назвать нормальным,
на который без улыбки не взглянешь?
Не торопитесь его удалять или рефакторить, — запостите его на
говнокод.ру, посмеёмся вместе!
(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_list)
(declare-fun m_node (M_list M_list) M_list)
; один хер какой порядок, можно переписать (a, b) на (b, a)
(assert
(forall ( (a M_list) (b M_list) )
(=
(m_node a b)
(m_node b a)
)
)
)
; если есть (a (b c)) то можно переписать на (с (a b))
(assert
(forall ( (a M_list) (b M_list) (c M_list) )
(=
(m_node a (m_node b c) )
(m_node c (m_node a b) )
)
)
)
; Можно создавать или удалять повторы, (a a) <=> a
(assert
(forall ( (a M_list))
(=
(m_node a a)
a
)
)
)
; Чтоб узнать, выводима ли такая-то хернь
(declare-fun m_node_select (M_list M_list) Bool)
(assert
(forall ( (a M_list) (b M_list) )
(m_node_select
a (m_node a b)
)
)
)
; проверяем, можно ли сконструировать (a a) из (c ((b d) a))
(assert
(not (forall ( (a M_list) (b M_list) (c M_list) (d M_list) )
(m_node_select
(m_node a a)
(m_node c (m_node (m_node b d) a) )
)
))
)
(check-sat)
(get-proof)
Вот вам немного гомоикон SMT-солвера. Эта вот хренотень сама доказывает, не то что какой-то там Coq.
Понятно что по тем вот говноправилам можно чтоб всплыло 'a' и потом его удвоить "(a a) <=> a"
потом через m_node_select вытащить этот дубликат
На этой хуите с uninterpreted functions кстати можно попробовать свой гильберт-стайл прувер написать, и чтоб оно там само всякие вореции доказательств перебирало.
Конкретно в этом случае может быть какие-то автоматические тактики Coq и осилят (пусть снаут проверит, если не лень), но в общем случае эти SMT-решатели сами по себе доказывают намного лучше (т.к. специально под это затачивались) чем какая-то auto-хрень в Coq (в котором же еще надо понимать, какие тактики в каком порядке к какой питушне и как применять)
Variable M_list: Set.
Variable m_node: M_list -> M_list -> M_list.
Hypothesis H1: forall a b: M_list, m_node a b = m_node b a.
Hypothesis H2: forall a b c: M_list, m_node a (m_node b c) = m_node c (m_node a b).
Hypothesis H3: forall a: M_list, m_node a a = a.
Variable m_node_select: M_list -> M_list -> Prop.
Hyphotesis H4: forall a b: M_list, m_node_select a (m_node a b).
Theorem T: forall a b c d: M_list,
m_node_select (m_node a a) (m_node c (m_node (m_node b d) a)).
'Prop' - proposition - высказывание. Ну и тут делаются преобразования над какими-то высказываниями. А что такое 'Set' - некие вычислимые множества или че вообще такое? https://cs.stackexchange.com/a/80737
> Prop is meant for propositions. It is impredicative, meaning that you can instantiate polymorphic functions with polymorphic types. It also has proof irrelevance, meaning that if p1,p2:P then p1=p2. This allows terms that are only used for proof to be erased in any code generated by Coq.
> Set is meant for computation. It's predicative, and doesn't have proof irrelevance, which lets you do nice things like not assuming 1=2. The Set parts remain during code extraction.
Зачем тут нужна какая-то предикативность для этой питушни? Если непредикативно, то можно еще кодогенерировать это как-то там, убрав термы для доказательств.
Я вообще ненастоящий сварщик(пусть снаут прокомментирует).
Там рассуждалось о том, что такую-то хуитень можно на такую-то хуитень заменить в обе стороны, т.е. вполне себе некие операции над высказываниями. Если "Set" понимать как множества в математическом смысле (ZFC там, или еще чего), то тут тоже мимо.
Ну я представлял, что m_node -- это какая-то функция над множествами, обладающая определёнными свойствами. И вот мы можем воспользоваться этими свойствами чтобы трансформировать выражение не меняя его смысл.
Т.е., к примеру, мы взяли какое-то множество, определили на нём операцию сложения, пруфнули что она обладает вот этими вот описанными в твоём коде свойствами. И теперь мы можем юзать это для оптимизации кода, в котором юзается сложение.
И вот эта фраза "The Set parts remain during code extraction" становится очень полезной.
> Yes. https://arxiv.org/abs/1412.8091 details a translation from OpenTheory to Metamath, and https://arxiv.org/abs/1910.10703 has a translation from Metamath -> MM0 -> Lean + HOL. You have to map every axiom and inference rule of the source system to a theorem of the target system, and since most of these systems have a similar idea about what math is this is usually possible, modulo some axiomatic strength mismatches, which can usually be addressed by adding (reasonable, idiomatic) axioms to the target system to make up the difference.
вангую, было так: в 2001-м году гугл купил deja news, который питухи вообще на коленке написали в 1995-м. Потом какой-то питух чото там подмандил чутка, и с тех пор так оно и работает. Внутри там ад, израиль, черти ебуца и код 2001-го года
SMT-солверы работают в логике первого порядка, её Coq сожрёт, думаю даже без дополнительных аксиом. Хотя, как именно доказательство адаптируется, вопрос интересный.
Лол что. У миди Клавы есть фидбек и скорость нажатия. Если бы этого небыло - нахуй они нужны. Погугли про взвешенные и не взвешенные клавиши + у каждой невзвншеноц клавиши разрабатывается свой фидбек у разных фирм под своим потентом. Если бы силы нажатия небыло - нахуй тогда вообще миди клава нужна - это был бы наверное прекрасный подарок для ребенка который любит музыцировать - но ты как родитель ненавидишь всеми нервами его музыцирования. По этому для программной части именно - миди клава будет лучше, для анал-огово пианина, синты, и другая аналоговая громкая хуйня
Не совсем так. Даже у невзвешеных клавиш есть фидбек, но он конечно не молоточковый так как у разных фирм - своя технология. Да и в чем от этого плюс даёт? Только у самой дешёвой пали китайской за 3к рубасов нет фидбека, а силы нажатия ну это вообще пиздец детское сломанное пианино или самопал на ардуики от китайского долбоеба
Это не лисп, этот язык называется SMT-LIB http://smtlib.cs.uiowa.edu/language.shtml
Если некий язык в качестве синтаксиса испольует S-expression, это не делает его лиспом.
А что делать, если они не осиливают? Какой-то способ вручную пнуть в нужном направлении есть?
Блин, я вот кстати х.з. как в петухе записать a и b -- неведомая хуйня одного сорта. Походу тут совсем другая логика юзается.
https://cs.stackexchange.com/a/80737
> Prop is meant for propositions. It is impredicative, meaning that you can instantiate polymorphic functions with polymorphic types. It also has proof irrelevance, meaning that if p1,p2:P then p1=p2. This allows terms that are only used for proof to be erased in any code generated by Coq.
> Set is meant for computation. It's predicative, and doesn't have proof irrelevance, which lets you do nice things like not assuming 1=2. The Set parts remain during code extraction.
Зачем тут нужна какая-то предикативность для этой питушни? Если непредикативно, то можно еще кодогенерировать это как-то там, убрав термы для доказательств.
Я вообще ненастоящий сварщик(пусть снаут прокомментирует).
И вот эта фраза "The Set parts remain during code extraction" становится очень полезной.
Будто я настоящий, лол. Set к ZFC и вычислимым множествам отношения не имеет, это просто название
самого низкого уровня в иерархии вселенных.
Питух умеет юзать что Z3, что CVC4 через coqhammer. Шах и мат, аметисты.
Там вот https://groups.google.com/g/metamath/c/b9k2nWOWJ-A напимер пишут
> Yes. https://arxiv.org/abs/1412.8091 details a translation from OpenTheory to Metamath, and https://arxiv.org/abs/1910.10703 has a translation from Metamath -> MM0 -> Lean + HOL. You have to map every axiom and inference rule of the source system to a theorem of the target system, and since most of these systems have a similar idea about what math is this is usually possible, modulo some axiomatic strength mismatches, which can usually be addressed by adding (reasonable, idiomatic) axioms to the target system to make up the difference.
Вы все ещё хотите работать в гугле?
У красноглазых они во все поля и грузятся из архивов мгновенно
Pozor
Понятное дело, что в 2021 нужно грузить все сообщения сразу, да еще и загзипованные (или за бротлинные даже)
Фидо
https://groups.google.com/g/fido7.ru.fidonet.today
Юзнет
https://groups.google.com/g/alt.unix
устали поди за двадцать пять лет-то
па рэстаранам
Всё-таки цели у этих инструментов немного разные.
А у пианино кусок механики от настоящего пианино.
Да ну... Медленно и неудобно же. А народ в реалтайме эти крутилки вертит, чтобы из потока не выходить.
Это как тебя заставить хоткеи мышкой прожимать.
http://smtlib.cs.uiowa.edu/language.shtml
Если некий язык в качестве синтаксиса испольует S-expression, это не делает его лиспом.