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

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
  42. 42
  43. 43
Lemma mfun_equiv_commut f g g1 g2 :
  mfun_equiv g (g2 ∘ g1) ->
  commute f g1 ->
  commute f g2 ->
  commute f g.
Proof.
  intros Hg Hcomm_g1 Hcomm_g2 a z.
  split; intros H; unfold mfun_equiv in Hg.
  - destruct H as [b [Hb Hz]].
    rewrite Hg in Hz.
    destruct Hz as [d [Hd Hz]].
    destruct (Hcomm_g1 a d) as [Hg1f Hfg1]. clear Hfg1.
    destruct Hg1f as [d' [Had' Hcd']]. { sauto. }
    morph_shift g2 d'.
    destruct Had' as [c' Hc'].
    destruct (Hcomm_g2 c' z') as [Hg2f Hfg2].
    destruct Hg2f as [z'' [Hz'' Hz'z'']]. { sauto. }
    destruct Hz'' as [e'' He''].
    exists z''.
    split.
    + exists e''.
      split.
      * rewrite Hg. sauto.
      * easy.
    + now rewrite Hequiv_z_z', Hz'z''.
  - destruct H as [c [Hc Hz]].
    rewrite Hg in Hc.
    destruct Hc as [b [Hb Hc]].
    destruct (Hcomm_g2 b z) as [Hg2f Hfg2]. clear Hg2f.
    destruct Hfg2 as [z' [Hbz' Hzz']]. { sauto. }
    destruct Hbz' as [d [Hdz' Hbd']].
    destruct (Hcomm_g1 a d) as [Hg1f Hfg1]. clear Hg1f.
    destruct Hfg1 as [d' [Had' Hdd']]. { sauto. }
    destruct Had' as [b' [Hab' Hb'd']].
    morph_shift g2 d'.
    exists z''.
    split.
    + exists b'.
      split.
      * easy.
      * rewrite Hg. exists d'. sauto.
    + now rewrite Hzz', Hequiv_z'_z''.
Qed.

Why are we here, just to suffer?

Запостил: CHayT CHayT, (Updated )

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

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

    seo-пост: говно эти ваши комплюктеры. Вот с такой питушнёй приходится иметь дело, просто чтобы доказать, что если разбить инструкции некой абстрактной машины на некий ``микрокод'', то отсутствие гонок и конфликтов между последовательностью микроинструкций гарантирует отсутствие гонок между самими инструкциями с точностью до сетоида.
    Ответить

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

      Перевёл на Ltac2, там антиквотация переменных делается долларом. Думаю, можно засчитать.
      Ответить

  • ava guest # 0

    Даже Юникод используется: U+2218, RING OPERATOR.
    Ответить

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

    Вот вы всё гыгыкаете, а оказалось, что эта теорема нихуя не работает в общем случае, т.к. питух поймал corner case, где микроинструкция может пересечься с инструкцией из процесса с пидом, созданным в будущем. В итоге, хуй там, а не symmetry reduction для общего случая двух разных процессов. Ось времени им подавай. Тому, кто эту вашу многопоточность придумал, нужно гвоздь в голову забить, а за распределённые системы вообще нужно под килём протаскивать.
    Ответить

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

      ...Теперь таскай инвариант о валидности всех процессов, созданных в прошом, таскай его полностью, в каждый interleaving, в каждый сетоид. Багор просто неописуемый. Потоптал мою красивую ма-те-ма-тику питушок, ничего не скажешь.
      Ответить

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

        Здравствуй, бложик. В общем, идея с этим инвариантом проканала, но среднее доказательство занимает теперь 200 строк. И это при том, что все мои пруфы обмазаны огромным количеством тактик, т.е. большая кода часть автоматически доказывается. Очень-очень большой багор из-за одной мелкой детали.
        Но самое ужасное, что пришлось-таки при-нять аксиому proof_irrelevance, а до этого теория была чисто конструктивная, без всяких аксиом. Последнюю, вероятно, можно выкинуть, если ещё дальше всё усложнить.
        Ответить

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

Я, guest, находясь в здравом уме и твердой памяти, торжественно заявляю:

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

    ↑
    8
    ↓