Category: здоровье

Category was added automatically. Read all entries about "здоровье".

(no subject)

Господа, я решил признаться в собственной ментальной импотенции.
Несмотря на то, что задача из предыдущего поста решается просто, хотя бы даже индукцией по AST, состоящему из значений, более общая задачка, которую я решил поковырять, строго, в coq, не решается. Я хотел доказать, что для любой операции "@", про которую известно _только_ такое: a@b = b@a, a@(b@c) = (a@b)@c, верно утверждение, что выражение a@b@c@...@z зависит только от значений входящих в него переменных, и не зависит от расстановки скобок в выражении. В терминах Coq я бы сформулировал это через multiset'ы: если multiset'ы, состоящие из значений переменных, равны, то равны и значения любых выражений, составленных из этих переменных. Но не так-то просто это доказать, как оказалось.
Даже с помощью могучего beroal, рассказавшего мне про Coq очень много интересного, у меня не получилось доказать всё строго, в Coq.

А пишу я всё это только потому, что вопрос надо закрыть, каменты раскрыть, непричастных наказать, виновных наградить, детям цветы, бабам мороженое. Иногда были вещи, о чём написать (буквально насрать на ваши мониторы посредством вашей же уютненкой жежешечной фиенд-ленты), но это было неприемлемо из-за такого висящего вопроса.

Теперь же — берегитесь.