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

    +2

    1. 01
    2. 02
    3. 03
    4. 04
    5. 05
    6. 06
    7. 07
    8. 08
    9. 09
    10. 10
    11. 11
    12. 12
    13. 13
    14. 14
    15. 15
    16. 16
    17. 17
    18. 18
    19. 19
    20. 20
    21. 21
    22. 22
    23. 23
    24. 24
    25. 25
    26. 26
    27. 27
    28. 28
    29. 29
    30. 30
    31. 31
    32. 32
    33. 33
    34. 34
    35. 35
    36. 36
    37. 37
    38. 38
    39. 39
    40. 40
    41. 41
    Definition uilv_add_trivial {N} te (t : list TE) (traces : Traces N)
             i j (Ht : MInt_ trace_elems_don't_commute j true traces t)
             s s' (Hls : LongStep s (te :: t) s')
             (Htriv : trivial_add i j traces) :
    MInt_ trace_elems_don't_commute i true (push_te traces i te) (te :: t).
  Proof with autorewrite with vector; eauto with vector; try vec_forall_eq_contradiction.
    unfold push_te.
    unfold trivial_add in Htriv.
    destruct (Fin.eq_dec i j) as [Hij|Hij].
    (* [i=j], solving by constructor: *)
    { subst.
      unfold trivial_add.
      eapply mint_keep with (rest := traces[@j])...
    }
    remember traces[@j] as t2_.
    destruct t2_ as [|te2 t2]; subst.
    { inversion Ht as [vec Hvec|? ? ? ? ? Hj Hcont|? ? ? ? ? ? Hjj0 Hswitch Hj Hcont];
        subst.
      - eapply mint_keep with (prog := true)...
        eapply mint_nil...
      - rewrite Hj in Heqt2_.
        discriminate.
    }
    remember traces[@i] as t1_.
    destruct t1_ as [|te1 t1]; subst.
    (* [te] is the last element in i-th trace: *)
    { eapply mint_keep with (rest := []) (prog := false)...
      inversion Ht as [vec Hvec|? ? ? ? ? Hj Hcont|? ? ? ? ? ? Hjj0 Hswitch Hj Hcont];
        subst...
      rewrite Heqt1_ in *.
      eapply mint_switch...
      rewrite <-Heqt1_...
    }
    destruct Htriv as [|[Hij' Hcomm]]; [contradiction Hij|idtac].
    eapply mint_keep with (rest := te1 :: t1) (prog := false)...
    rewrite Heqt1_, Vec.replace_id.
    inversion Ht as [vec Hvec|? ? ? ? ? Hj Hcont|? ? ? ? ? ? Hjj0 Hswitch Hj Hcont]; subst...
    replace te0 with te2 in * by congruence.
    eapply mint_switch...
    rewrite <-Heqt1_...
  Defined.

    Кто сказал, что хуже C++ темплейтов ничего уже нет? Вы ничего не понимаете в метушне. Это говно разворачивается в 12000 строк, например.

    Запостил: CHayT, 20 Августа 2020

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

    • ava CHayT 20.08.2020 00:20 # 0

      SEO post
      Ответить

    • ava Desktop 20.08.2020 00:24 # 0

      Это реально существующий язык?

      { Вы случайно не middle клингон? }
      Ответить

      • ava CHayT 20.08.2020 00:26 # 0

        Да, это Ltac, один из макроязыков Coq.
        Ответить

        • ava defecate-plusplus 20.08.2020 01:33 # +4

          Coq (фр. coq — петух) — интерактивное программное средство доказательства теорем из средний азий.
          Ответить

    • ava bootcamp_dropout 20.08.2020 00:28 # 0

      Я пытался понять что это делает минут пять и мне вспомнилось что я где-то про какие-то term rewriting слышал
      rewrite Heqt1_, Vec.replace_id.

      это оно?
      Ответить

      • ava CHayT 20.08.2020 00:32 # 0

        Что-то вроде того. Тактика "rewrite" берёт гипотезу типа (a = b) и заменяет в текущей цели все a на b, или наоборот.
        Ответить

        • ava bootcamp_dropout 20.08.2020 00:42 # 0

          А для чего это нужно?
          Ответить

          • ava CHayT 20.08.2020 00:54 # 0

            Так можно символьными вычислениями что-то доказать.
            Ответить

            • ava bootcamp_dropout 20.08.2020 01:10 # 0

              Я имею в виду, в индустрии что-то так доказывают? Или это для академии?
              Ответить

              • ava CHayT 20.08.2020 01:17 # 0

                В индустрии довольно это редко, но используют. К примеру: https://github.com/mit-plv/fiat-crypto
                Ответить

                • ava bootcamp_dropout 20.08.2020 01:33 # 0

                  Я думал, это можно как-то для тестирования использовать, например нагенерировать много кейсов, прогнать по ним программу и смотреть, не опровергает ли что-то гипотезу
                  Ответить

                  • ava CHayT 20.08.2020 01:41 # 0

                    Зачем генерить тесты, если есть доказательство, что свойства верны для любого ввода?
                    Ответить

                    • ava bootcamp_dropout 20.08.2020 01:53 # 0

                      Ну вот у тебя есть программа, о структуре которой ничего не известно. Ты генеришь тесты чтобы определить ее свойства, на их основанияи строишь гипотезы и их символьно доказываешь
                      Ответить

                      • ava CHayT 20.08.2020 02:02 # 0

                        Нет, суть такова: с помощью зависимых типов ты описываешь желаемые свойства функции, и если функция проходит тайпчек, то ты заключаешь, что она удовлетворяет этим свойствам всегда. Тесты не нужны. (Ну, кроме интеграционных).
                        Ответить

                        • ava bootcamp_dropout 20.08.2020 11:17 # 0

                          Жаль, тогда это не так круто если нельзя запруфать произвольную хуйню
                          Ответить

                        • ava j123123 22.08.2020 18:54 # 0

                          А теорема Гудстейна в Coq доказывается? Что там за аксиоматика вообще?
                          Ответить

                          • ava CHayT 22.08.2020 21:55 # 0

                            Хз про теорему. Без дополнительных аксиом, насколько я понимаю, там конструктивистская логика a la Martin-Löf, но при желании можно обмазаться классической логикой из стандартной библиотеки. Впрочем, для задач верификации мне это ровно один раз понадобилось. Я никакой интересной математикой не занимаюсь, увы.
                            Ответить

                            • ava gost 22.08.2020 22:00 # 0

                              А почему у тебя на аватарке аниме-девочка хочет застрелиться?
                              Ответить

                    • ava gostinho 20.08.2020 09:30 # 0

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

                      • ava XYPO3BO3 20.08.2020 12:39 # 0

                        Т. е. все работающие сейчас программы скорее всего правильные?
                        Ответить

                        • ava bormand 20.08.2020 12:42 # 0

                          В какой-то степени да.

                          В общем-то даже языки с формальными пруфами не гарантируют "правильности" кода, т.к. они проверяют только какой-то набор свойств, которые ты посчитал важными.
                          Ответить

                          • ava j123123 20.08.2020 23:36 # 0

                            Правильности кода не гарантирует вообще ничто, т.к. заказчик мог написать хуйню в ТЗ, и даже если б был мегакрутой ИИ, который любое ТЗ правильно и без багов превращает в код, получилась бы хуйня
                            Ответить

                      • ava 6a6yuH 20.08.2020 18:36 # 0

                        Странное утверждение для императивных языков.
                        Впрочем, шансы на корректность у них выше, чем у скриптоговна.
                        Скриптоговно не факт, что работает верно. Даже если запустилось
                        Ответить

    • ava gost 20.08.2020 07:04 # 0

      > ? ? ? ? ? ?
      ???????

      Доброе утро.
      Ответить

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