forked from achlipala/frap
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Invariant.v
100 lines (83 loc) · 3.22 KB
/
Invariant.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
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
Require Import Relations.
Set Implicit Arguments.
Record trsys state := {
Initial : state -> Prop;
Step : state -> state -> Prop
}.
Definition invariantFor {state} (sys : trsys state) (invariant : state -> Prop) :=
forall s, sys.(Initial) s
-> forall s', sys.(Step)^* s s'
-> invariant s'.
Theorem use_invariant : forall {state} (sys : trsys state) (invariant : state -> Prop) s s',
invariantFor sys invariant
-> sys.(Step)^* s s'
-> sys.(Initial) s
-> invariant s'.
Proof.
firstorder.
Qed.
Theorem invariant_weaken : forall {state} (sys : trsys state)
(invariant1 invariant2 : state -> Prop),
invariantFor sys invariant1
-> (forall s, invariant1 s -> invariant2 s)
-> invariantFor sys invariant2.
Proof.
unfold invariantFor; intuition eauto.
Qed.
Theorem invariant_induction : forall {state} (sys : trsys state)
(invariant : state -> Prop),
(forall s, sys.(Initial) s -> invariant s)
-> (forall s, invariant s -> forall s', sys.(Step) s s' -> invariant s')
-> invariantFor sys invariant.
Proof.
unfold invariantFor; intros.
assert (invariant s) by eauto.
clear H1.
induction H2; eauto.
Qed.
(** * General parallel composition *)
Record threaded_state shared private := {
Shared : shared;
Private : private
}.
Inductive parallel1 shared private1 private2
(init1 : threaded_state shared private1 -> Prop)
(init2 : threaded_state shared private2 -> Prop)
: threaded_state shared (private1 * private2) -> Prop :=
| Pinit : forall sh pr1 pr2,
init1 {| Shared := sh; Private := pr1 |}
-> init2 {| Shared := sh; Private := pr2 |}
-> parallel1 init1 init2 {| Shared := sh; Private := (pr1, pr2) |}.
Inductive parallel2 shared private1 private2
(step1 : threaded_state shared private1 -> threaded_state shared private1 -> Prop)
(step2 : threaded_state shared private2 -> threaded_state shared private2 -> Prop)
: threaded_state shared (private1 * private2)
-> threaded_state shared (private1 * private2) -> Prop :=
| Pstep1 : forall sh pr1 pr2 sh' pr1',
step1 {| Shared := sh; Private := pr1 |} {| Shared := sh'; Private := pr1' |}
-> parallel2 step1 step2 {| Shared := sh; Private := (pr1, pr2) |}
{| Shared := sh'; Private := (pr1', pr2) |}
| Pstep2 : forall sh pr1 pr2 sh' pr2',
step2 {| Shared := sh; Private := pr2 |} {| Shared := sh'; Private := pr2' |}
-> parallel2 step1 step2 {| Shared := sh; Private := (pr1, pr2) |}
{| Shared := sh'; Private := (pr1, pr2') |}.
Definition parallel shared private1 private2
(sys1 : trsys (threaded_state shared private1))
(sys2 : trsys (threaded_state shared private2)) := {|
Initial := parallel1 sys1.(Initial) sys2.(Initial);
Step := parallel2 sys1.(Step) sys2.(Step)
|}.
(** * Switching to multistep versions of systems *)
Lemma trc_idem : forall A (R : A -> A -> Prop) x1 x2,
R^*^* x1 x2
-> R^* x1 x2.
Proof.
induction 1; eauto using trc_trans.
Qed.
Theorem invariant_multistepify : forall {state} (sys : trsys state)
(invariant : state -> Prop),
invariantFor sys invariant
-> invariantFor {| Initial := Initial sys; Step := (Step sys)^* |} invariant.
Proof.
unfold invariantFor; simpl; intuition eauto using trc_idem.
Qed.