-
Notifications
You must be signed in to change notification settings - Fork 1
/
separation.v
67 lines (56 loc) · 1.4 KB
/
separation.v
1
2
3
4
5
6
7
8
9
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
Load basics.
Axiom ParAssociativity :
forall p q r : D,
(p | q) | r = p | (q | r).
Hint Resolve ParAssociativity.
Definition ExchangeLaw :=
forall p p' q q' : D,
(p | p') ; (q | q') ref (p ; q) | (p' ; q').
Definition ParallelForHoare :=
forall p p' q q' r r': D,
[p]q[r] /\ [p']q'[r'] -> [p|p']q|q'[r|r'].
Definition ParallelForMilner :=
forall p p' q q' r r': D,
MilnerTransition p q r /\ MilnerTransition p' q' r' -> MilnerTransition (p|p') (q|q') (r|r').
Theorem ExchangeImpliesParallelForHoare: ExchangeLaw -> ParallelForHoare.
Proof.
intros EL.
unfold ParallelForHoare.
unfold HoareTriple.
intuition.
assert (TMP: (p | p') ; (q | q') ref (p ; q) | (p' ; q')).
apply EL.
apply Transitivity with (y := (p ; q) | (p' ; q')).
intuition.
Qed.
Theorem ExchangeImpliesParallelForMilner: ExchangeLaw -> ParallelForMilner.
Proof.
intros EL.
unfold ParallelForMilner.
unfold MilnerTransition.
intuition.
assert (TMP: (q | q') ; (r | r') ref (q ; r) | (q' ; r')).
apply EL.
apply Transitivity with (y := q; r | q'; r').
auto.
Qed.
Theorem ParallelForHoareImpliesExchange: ParallelForHoare -> ExchangeLaw.
Proof.
intros PH.
unfold ParallelForHoare.
unfold HoareTriple.
unfold ExchangeLaw.
intuition.
apply PH.
auto.
Qed.
Theorem ParallelForMilnerImpliesExchange: ParallelForMilner -> ExchangeLaw.
Proof.
intros PM.
unfold ParallelForMilner.
unfold MilnerTransition.
unfold ExchangeLaw.
intuition.
apply PM.
auto.
Qed.