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

    0

    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
    42. 42
    43. 43
    44. 44
    45. 45
    46. 46
    47. 47
    48. 48
    49. 49
    50. 50
    51. 51
    52. 52
    53. 53
    54. 54
    55. 55
    56. 56
    57. 57
    58. 58
    59. 59
    60. 60
    61. 61
    62. 62
    63. 63
    64. 64
    65. 65
    66. 66
    67. 67
    68. 68
    69. 69
    70. 70
    71. 71
    72. 72
    73. 73
    74. 74
    75. 75
    76. 76
    77. 77
    78. 78
    79. 79
    80. 80
    81. 81
    82. 82
    83. 83
    84. 84
    85. 85
    86. 86
    87. 87
    88. 88
    Fixpoint mint_add0 {N} (i k : Fin.t N) te_i te' t0 vec
                 (Ht : MInt nonCommRel N k vec (te' :: t0))
                 (Hik : k < i)
                 (Hcomm0 : trace_elems_commute te_i te')
                 {struct Ht} :
          exists t' : list TE,
              MInt nonCommRel N k (vec_append i te_i vec) (te' :: t') /\
              Permutation trace_elems_commute (te_i :: te' :: t0) (te' :: t').
        Proof with eauto.
          (* Welcome to the hell proof! *)
          remember (te' :: t0) as t_.
          destruct Ht as [k
                         |k j vec te_k t Hij Ht
                         |k j vec te_k te_j t Hij Hcomm Ht
                         ];
            [discriminate
            |replace te' with te_k in * by congruence; clear Heqt_..
            ].
          2:{ destruct (trace_elems_commute_dec te_i te_j).
              - apply mint_add0 with (te_i := te_i) (i := i) in Ht; [|lia|assumption].
                destruct Ht as [t' [Ht' Hperm']].
                exists (te_j :: t'). split.
                + swap_vec_append.
                  eapply mint_cons2...
                + apply permut_cons with (a := te_k) in Hperm'.
                  eapply permut_trans...
                  now apply permut_head'.
              - exists (te_i :: te_j :: t). split.
                + swap_vec_append.
                  apply mint_cons1 with (j0 := i); [lia|].
                  apply mint_cons2 with (j0 := j); [lia|auto..].
                + now apply permut_head'.
          }
          { inversion_ Ht.
            - exists [te_i]. split.
              + swap_vec_append.
                apply mint_cons1 with (j0 := i); [lia|].
                apply mint_cons1 with (j0 := i); [lia|].
                constructor.
              + now apply permut_head'.
            - rename te into te_j.
              destruct (PeanoNat.Nat.lt_ge_cases j i).
              2:{ exists (te_i :: te_j :: t1). split.
                  - swap_vec_append.
                    apply mint_cons1 with (j1 := i); [lia|].
                    apply mint_cons1 with (j1 := j); [lia|assumption].
                  - now apply permut_head'.
              }
              { destruct (trace_elems_commute_dec te_i te_j) as [Hte_ij|Hte_ij].
                - apply mint_add0 with (i := i) (te_i := te_i) in Ht; [|lia|assumption].
                  destruct Ht as [t' [Ht' Hperm']].
                  exists (te_j :: t'). split.
                  + swap_vec_append.
                    eapply mint_cons1...
                  + apply permut_cons with (a := te_k) in Hperm'.
                    now apply permut_head.
                - exists (te_i :: te_j :: t1). split.
                  + swap_vec_append.
                    apply mint_cons1 with (j1 := i); [lia|].
                    apply mint_cons2 with (j1 := j); [lia|assumption..].
                  + apply permut_head; [assumption|constructor].
              }
            - rename j0 into i0. cbn in H0.
              destruct (PeanoNat.Nat.lt_ge_cases j i).
              2:{ exists (te_i :: te_i0 :: te_j :: t1). split.
                  + swap_vec_append.
                    apply mint_cons1 with (j0 := i); [lia|].
                    apply mint_cons1 with (j0 := j); [lia|assumption].
                  + now apply permut_head'.
              }
              { destruct (trace_elems_commute_dec te_i te_i0).
                - apply mint_add0 with (i := i) (te_i := te_i) in Ht; [|lia|assumption].
                  destruct Ht as [t' [Ht' Hperm']].
                  exists (te_i0 :: t'). split.
                  + swap_vec_append.
                    eapply mint_cons1...
                  + apply permut_cons with (a := te_k) in Hperm'.
                    now apply permut_head.
                - exists (te_i :: te_i0 :: te_j :: t1). split.
                  + swap_vec_append.
                    apply mint_cons1 with (j0 := i); [lia|].
                    apply mint_cons2 with (j0 := j); [lia|assumption..].
                  + apply permut_head.
                    * assumption.
                    * constructor.
              }
          }
        Qed.

    Мой magnum opus. Часть доказательства про выкидывание из рассмотрения коммутирующих системных вызовов.

    Запостил: CHayT, 17 Ноября 2020

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

    • Разворецивается всего в 600 строк Gallina. Тут прекрасно всё: и копипаста, и автоматическое именование переменных с последующим переименовыванием, и сама идея хуйнуть троекратно вложенный кейз-анализ.
      Ответить
      • Ня, привет.
        Ответить
      • > троекратно вложенный кейз-анализ

        Ну тебе не надо это на доске студентам объяснять, а coq всё стерпит.

        Теорему про раскраску графа вообще чуть ли не брутфорсом доказывали...

        З.Ы. Ня, привет.
        Ответить
        • > Ну тебе не надо это на доске студентам объяснять, а coq всё стерпит.

          Что интересно, это не потому, что мне было лень эту функцию на леммы разбивать, а именно чтобы получить в итоге нужный тип. Такая вот злая лемма. Всё-то криво в этом вашем программировании, никаких красивых симметрий.
          Ответить
    • Это на каком язычке?
      Ответить
    • Давно вуз окончил?
      Ответить
    • А были ли успешные попытки прикручивания к Coq нейросетей, чтоб оно само там применяло стратегии и как-нибудь доказывалось?
      Ответить
      • Попытки были (coqhammer, gamepad), насколько успешные не знаю, мне они не помогли. +Я знаю, что сейчас несколько исследовательских групп что-то новое ковыряет.
        Ответить
        • Вообще, на мой взгляд, самое трудное — это правильные определения. Если в них есть баг или они недостаточно специфичны, то нейросеть просто в какой-то момент встанет или натворит непонятной херни. И потом фиг поймёшь, то ли искуственный идиот что-то напутал, то ли твои определения говно. Ручное доказательство это конечно долго, но зато когда приходишь к какой-то неразрешимой херне, понимаешь, что к чему. Поэтому в данном случае я даже тактику induction не использовал, чтобы она какой-нибудь ненужной херни в гипотезу индукции не подхватила, и запилил индукцию вручную.
          Ответить
          • Но ты ведь тоже нейросеть.
            Ответить
            • Да, но я та же нейросеть, которая ставит задачу и которая будет это дебажить.
              Ответить
              • Ну так разреши нейросети формулировать задачу и оценивать результат.
                Ответить
    • Ебать поехавший.
      Ответить

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