1. Куча / Говнокод #27028

    −1

    1. 01
    2. 02
    3. 03
    4. 04
    5. 05
    6. 06
    7. 07
    8. 08
    9. 09
    10. 10
    11. 11
    Lemma mint_head_eq CR1 CR2 (te : TE) l m r (t t' : list TE) :
        MInt CR1 (l, m, r) (te :: t) ->
        MInt CR2 (l, m, r) t' ->
        exists t'', t' = te :: t''.
      Proof.
        intros H1 H2.
        inversion_ H1; inversion_ H2; (* generates 25 goals *)
        match goal with
          |- (exists _, te :: ?T = te :: _) => now exists T
        end.
      Qed.

    Против метушни нет приёма.

    Запостил: CHayT, 14 Октября 2020

    Комментарии (33) RSS

    • seo: очередные кукареции
      Ответить
      • P.S. Говно в том, что вместо поиска изящного решения этот код сначала делает комбинаторный взрыв, а потом копипастит примерно одно и то же много раз для каждого кейза.
        Ответить
        • спасибо кэп
          Ответить
          • Можно было сразу догадаться по комментарию (* generates 25 goals *).
            Ответить
          • Не знаешь Ltac'а — по ебалу на-ка.
            Ответить
            • кстати, как правильно — «сюрстрёмминг» или «лютефиск»?
              Ответить
              • Разные блюда, лютефиск вроде вообще норвежское. Здесь на юге сюрстрёмминг — это мем, который пробуют однажды в жизни на спор.
                Ответить
              • Погуглим...

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

                Оказывается, шведы эту дрянь у финно-угров переняли... Я думал, это говно давно засыпало песками истории.
                Ответить
                • там ещё есть шняга вроде, когда убивают лося, вынимают внутренности и заваливают внутрь рыбу. лося после зарывают.

                  типа нычка на чёрный день

                  если конечно это не байка
                  Ответить
        • шутка, которую приходится объяснять
          Ответить
    • Какой-то язык для ма-те-ма-ти-ков.
      Ответить
    • показать все, что скрытоНу?
      Ответить
      • // код работает, вчера проверял
        Ответить
        • То есть код нихуя не делает? Нахуй тогда он нужен?
          Ответить
          • https://habr.com/ru/post/463957/

            Снаут пришел на собеседование к гесту8
            Ответить
            • полная хуита
              разве не надо в начале каждой программы писать «<?php» ?
              Ответить
            • Помнится, Снаут говорил что хаскелеговно непригодно для доказательств из-за полноты по тьюрингу.
              Ответить
              • Это Idris вроде
                Ответить
                • Понаделают языков с похожим синтаксисом... Вот «PHP» сразу видно.
                  Ответить
            • > тесты не нужны

              Вчера как раз в соседнем треде пришли к выводу, что несколько тестов-примеров таки стоит написать, чтобы убедиться, что мы доказываем что-то более-менее относящееся к задуманному, а не тупо мусор.
              Ответить
              • – Ромэн Снаутович, ты сделал задачу?
                – Я формально доказал её на кокоидрисе!
                – Хорошо, теперь перепиши как чистую любовь на С++ и покрой тестами
                – Это не лучший язык для! (хватает тросточку и цилиндр и хохоча убегает)
                Ответить
                • А эти системы сами умеют переписывать на что-то более прозаичное. Иногда даже с пруфом, что переписывание не испортило прогу.
                  Ответить
              • По моей практике обычно во время доказательства понимаешь, что что-то не так. Другое дело, что можно вымучить сто строк доказательства и наткнуться на дурацкий баг, а можно запилить тесты и найти его сразу, и не будить соседей скорбным завыванием.
                Ответить

    Добавить комментарий