Куча говна / Говнокод #26883 Ссылка на оригинал

0

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
  7. 7
  8. 8
  9. 9
  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 CHayT, (Updated )

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

  • ava Desktop # Ссылка на оригинал 0

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

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

  • ava bootcamp_dropout # Ссылка на оригинал 0

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

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

    • ava CHayT # Ссылка на оригинал 0 ⇈

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

        • ava CHayT # Ссылка на оригинал 0 ⇈

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

              • ava bootcamp_dropout # Ссылка на оригинал 0 ⇈

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

                • ava CHayT # Ссылка на оригинал 0 ⇈

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

                  • ava bootcamp_dropout # Ссылка на оригинал 0 ⇈

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

                    • ava CHayT # Ссылка на оригинал 0 ⇈

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

                  • admin admin # 0 ⇈

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

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

Где здесь C++, guest?!

    А не использовать ли нам bbcode?

    ↑
    8
    ↓