- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
- 12
- 13
- 14
- 15
- 16
- 17
- 18
- 19
- 20
- 21
- 22
- 23
- 24
- 25
- 26
- 27
- 28
- 29
- 30
- 31
- 32
- 33
- 34
- 35
- 36
- 37
- 38
- 39
- 40
- 41
- 42
- 43
- 44
- 45
- 46
- 47
- 48
- 49
- 50
- 51
- 52
- 53
- 54
- 55
- 56
- 57
- 58
- 59
- 60
- 61
- 62
- 63
- 64
- 65
- 66
- 67
- 68
- 69
- 70
- 71
- 72
- 73
- 74
- 75
- 76
- 77
- 78
- 79
- 80
- 81
- 82
- 83
- 84
- 85
- 86
- 87
- 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. Часть доказательства про выкидывание из рассмотрения коммутирующих системных вызовов.
Follow us!
Ну тебе не надо это на доске студентам объяснять, а coq всё стерпит.
Теорему про раскраску графа вообще чуть ли не брутфорсом доказывали...
З.Ы. Ня, привет.
Что интересно, это не потому, что мне было лень эту функцию на леммы разбивать, а именно чтобы получить в итоге нужный тип. Такая вот злая лемма. Всё-то криво в этом вашем программировании, никаких красивых симметрий.