sts.v 10.2 KB
Newer Older
1
2
Require Export modures.ra.
Require Import prelude.sets modures.dra.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
4
5
6
7
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Local Arguments unit _ _ !_ /.

Module sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
8
9
10
Inductive t {A B} (R : relation A) (tok : A  set B) :=
  | auth : A  set B  t R tok
  | frag : set A  set B  t R tok.
11
12
Arguments auth {_ _ _ _} _ _.
Arguments frag {_ _ _ _} _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
13
14

Section sts_core.
Robbert Krebbers's avatar
Robbert Krebbers committed
15
16
Context {A B : Type} (R : relation A) (tok : A  set B).
Infix "≼" := dra_included.
Robbert Krebbers's avatar
Robbert Krebbers committed
17
18

Inductive sts_equiv : Equiv (t R tok) :=
19
20
  | auth_equiv s T1 T2 : T1  T2  auth s T1  auth s T2
  | frag_equiv S1 S2 T1 T2 : T1  T2  S1  S2  frag S1 T1  frag S2 T2.
Robbert Krebbers's avatar
Robbert Krebbers committed
21
Global Existing Instance sts_equiv.
Robbert Krebbers's avatar
Robbert Krebbers committed
22
Inductive step : relation (A * set B) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
23
  | Step s1 s2 T1 T2 :
24
     R s1 s2  tok s1  T1    tok s2  T2    tok s1  T1  tok s2  T2 
Robbert Krebbers's avatar
Robbert Krebbers committed
25
26
     step (s1,T1) (s2,T2).
Hint Resolve Step.
Robbert Krebbers's avatar
Robbert Krebbers committed
27
Inductive frame_step (T : set B) (s1 s2 : A) : Prop :=
Robbert Krebbers's avatar
Robbert Krebbers committed
28
  | Frame_step T1 T2 :
29
     T1  (tok s1  T)    step (s1,T1) (s2,T2)  frame_step T s1 s2.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
Hint Resolve Frame_step.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
Record closed (T : set B) (S : set A) : Prop := Closed {
32
  closed_ne : S  ;
33
  closed_disjoint s : s  S  tok s  T  ;
Robbert Krebbers's avatar
Robbert Krebbers committed
34
35
36
37
38
39
  closed_step s1 s2 : s1  S  frame_step T s1 s2  s2  S
}.
Lemma closed_steps S T s1 s2 :
  closed T S  s1  S  rtc (frame_step T) s1 s2  s2  S.
Proof. induction 3; eauto using closed_step. Qed.
Global Instance sts_valid : Valid (t R tok) := λ x,
40
  match x with auth s T => tok s  T   | frag S' T => closed T S' end.
Robbert Krebbers's avatar
Robbert Krebbers committed
41
42
Definition up (T : set B) (s : A) : set A := mkSet (rtc (frame_step T) s).
Definition up_set (T : set B) (S : set A) : set A := S = up T.
Robbert Krebbers's avatar
Robbert Krebbers committed
43
44
45
46
47
Global Instance sts_unit : Unit (t R tok) := λ x,
  match x with
  | frag S' _ => frag (up_set  S')  | auth s _ => frag (up  s) 
  end.
Inductive sts_disjoint : Disjoint (t R tok) :=
48
49
  | frag_frag_disjoint S1 S2 T1 T2 :
     S1  S2    T1  T2    frag S1 T1  frag S2 T2
50
51
  | auth_frag_disjoint s S T1 T2 : s  S  T1  T2    auth s T1  frag S T2
  | frag_auth_disjoint s S T1 T2 : s  S  T1  T2    frag S T1  auth s T2.
Robbert Krebbers's avatar
Robbert Krebbers committed
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
Global Existing Instance sts_disjoint.
Global Instance sts_op : Op (t R tok) := λ x1 x2,
  match x1, x2 with
  | frag S1 T1, frag S2 T2 => frag (S1  S2) (T1  T2)
  | auth s T1, frag _ T2 => auth s (T1  T2)
  | frag _ T1, auth s T2 => auth s (T1  T2)
  | auth s T1, auth _ T2 => auth s (T1  T2) (* never happens *)
  end.
Global Instance sts_minus : Minus (t R tok) := λ x1 x2,
  match x1, x2 with
  | frag S1 T1, frag S2 T2 => frag (up_set (T1  T2) S1) (T1  T2)
  | auth s T1, frag _ T2 => auth s (T1  T2)
  | frag _ T2, auth s T1 => auth s (T1  T2) (* never happens *)
  | auth s T1, auth _ T2 => frag (up (T1  T2) s) (T1  T2)
  end.

68
69
70
71
Hint Extern 10 (equiv (A:=set _) _ _) => solve_elem_of : sts.
Hint Extern 10 (¬(equiv (A:=set _) _ _)) => solve_elem_of : sts.
Hint Extern 10 (_  _) => solve_elem_of : sts.
Hint Extern 10 (_  _) => solve_elem_of : sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
73
74
75
76
77
78
Instance: Equivalence (() : relation (t R tok)).
Proof.
  split.
  * by intros []; constructor.
  * by destruct 1; constructor.
  * destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
Qed.
79
80
81
Instance framestep_proper : Proper (() ==> (=) ==> (=) ==> impl) frame_step.
Proof. intros ?? HT ?? <- ?? <-; destruct 1; econstructor; eauto with sts. Qed.
Instance closed_proper' : Proper (() ==> () ==> impl) closed.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
Proof.
83
  intros ?? HT ?? HS; destruct 1;
Robbert Krebbers's avatar
Robbert Krebbers committed
84
    constructor; intros until 0; rewrite -?HS -?HT; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
Qed.
86
87
Instance closed_proper : Proper (() ==> () ==> iff) closed.
Proof. by split; apply closed_proper'. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
88
Lemma closed_op T1 T2 S1 S2 :
89
90
  closed T1 S1  closed T2 S2 
  T1  T2    S1  S2    closed (T1  T2) (S1  S2).
Robbert Krebbers's avatar
Robbert Krebbers committed
91
Proof.
92
  intros [_ ? Hstep1] [_ ? Hstep2] ?; split; [done|solve_elem_of|].
93
94
95
  intros s3 s4; rewrite !elem_of_intersection; intros [??] [T3 T4 ?]; split.
  * apply Hstep1 with s3, Frame_step with T3 T4; auto with sts.
  * apply Hstep2 with s3, Frame_step with T3 T4; auto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
96
Qed.
97
Instance up_preserving : Proper (flip () ==> (=) ==> ()) up.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
99
100
101
102
Proof.
  intros T T' HT s ? <-; apply elem_of_subseteq.
  induction 1 as [|s1 s2 s3 [T1 T2]]; [constructor|].
  eapply rtc_l; [eapply Frame_step with T1 T2|]; eauto with sts.
Qed.
103
104
105
Instance up_proper : Proper (() ==> (=) ==> ()) up.
Proof. by intros ?? [??] ???; split; apply up_preserving. Qed.
Instance up_set_proper : Proper (() ==> () ==> ()) up_set.
Robbert Krebbers's avatar
Robbert Krebbers committed
106
Proof. by intros T1 T2 HT S1 S2 HS; rewrite /up_set HS HT. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
108
Lemma elem_of_up s T : s  up T s.
Proof. constructor. Qed.
109
Lemma subseteq_up_set S T : S  up_set T S.
Robbert Krebbers's avatar
Robbert Krebbers committed
110
Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
111
112
Lemma closed_up_set S T :
  ( s, s  S  tok s  T  )  S    closed T (up_set T S).
Robbert Krebbers's avatar
Robbert Krebbers committed
113
Proof.
114
  intros HS Hne; unfold up_set; split.
115
  * assert ( s, s  up T s) by eauto using elem_of_up. solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
116
  * intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
117
    specialize (HS s' Hs'); clear Hs' Hne S.
Robbert Krebbers's avatar
Robbert Krebbers committed
118
119
120
121
122
    induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; auto.
    inversion_clear Hstep; apply IH; clear IH; auto with sts.
  * intros s1 s2; rewrite !elem_of_bind; intros (s&?&?) ?; exists s.
    split; [eapply rtc_r|]; eauto.
Qed.
123
Lemma closed_up_set_empty S : S    closed  (up_set  S).
Robbert Krebbers's avatar
Robbert Krebbers committed
124
Proof. eauto using closed_up_set with sts. Qed.
125
Lemma closed_up s T : tok s  T    closed T (up T s).
Robbert Krebbers's avatar
Robbert Krebbers committed
126
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
  intros; rewrite -(collection_bind_singleton (up T) s).
128
  apply closed_up_set; solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
130
131
132
133
Qed.
Lemma closed_up_empty s : closed  (up  s).
Proof. eauto using closed_up with sts. Qed.
Lemma up_closed S T : closed T S  up_set T S  S.
Proof.
134
  intros; split; auto using subseteq_up_set; intros s.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
136
137
138
139
140
141
142
143
144
145
146
  unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).
  induction Hstep; eauto using closed_step.
Qed.
Global Instance sts_dra : DRA (t R tok).
Proof.
  split.
  * apply _.
  * by do 2 destruct 1; constructor; setoid_subst.
  * by destruct 1; constructor; setoid_subst.
  * by intros ? [|]; destruct 1; inversion_clear 1; constructor; setoid_subst.
  * by do 2 destruct 1; constructor; setoid_subst.
  * assert ( T T' S s,
147
      closed T S  s  S  tok s  T'    tok s  (T  T')  ).
148
    { intros S T T' s [??]; solve_elem_of. }
Robbert Krebbers's avatar
Robbert Krebbers committed
149
    destruct 3; simpl in *; auto using closed_op with sts.
150
  * intros []; simpl; eauto using closed_up, closed_up_set, closed_ne with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
151
152
  * intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy;clear Hy; setoid_subst;
      rewrite ?disjoint_union_difference; auto using closed_up with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
153
    eapply closed_up_set; eauto 2 using closed_disjoint with sts.
154
  * intros [] [] []; constructor; rewrite ?(associative _); auto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
155
156
157
158
  * destruct 4; inversion_clear 1; constructor; auto with sts.
  * destruct 4; inversion_clear 1; constructor; auto with sts.
  * destruct 1; constructor; auto with sts.
  * destruct 3; constructor; auto with sts.
159
160
  * intros [|S T]; constructor; auto using elem_of_up with sts.
    assert (S  up_set  S  S  ) by eauto using subseteq_up_set, closed_ne.
161
    solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
162
  * intros [|S T]; constructor; auto with sts.
163
    assert (S  up_set  S); auto using subseteq_up_set with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
  * intros [s T|S T]; constructor; auto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
166
167
    + rewrite (up_closed (up _ _)); auto using closed_up with sts.
    + rewrite (up_closed (up_set _ _));
        eauto using closed_up_set, closed_ne with sts.
168
  * intros x y ?? (z&Hy&?&Hxz); exists (unit (x  y)); split_ands.
169
    + destruct Hxz;inversion_clear Hy;constructor;unfold up_set; solve_elem_of.
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
    + destruct Hxz; inversion_clear Hy; simpl;
        auto using closed_up_set_empty, closed_up_empty with sts.
    + destruct Hxz; inversion_clear Hy; constructor;
        repeat match goal with
        | |- context [ up_set ?T ?S ] =>
           unless (S  up_set T S) by done; pose proof (subseteq_up_set S T)
        | |- context [ up ?T ?s ] =>
           unless (s  up T s) by done; pose proof (elem_of_up s T)
        end; auto with sts.
  * intros x y ?? (z&Hy&_&Hxz); destruct Hxz; inversion_clear Hy; constructor;
      repeat match goal with
      | |- context [ up_set ?T ?S ] =>
         unless (S  up_set T S) by done; pose proof (subseteq_up_set S T)
      | |- context [ up ?T ?s ] =>
           unless (s  up T s) by done; pose proof (elem_of_up s T)
      end; auto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
186
187
  * intros x y ?? (z&Hy&?&Hxz); destruct Hxz as [S1 S2 T1 T2| |];
      inversion Hy; clear Hy; constructor; setoid_subst;
Robbert Krebbers's avatar
Robbert Krebbers committed
188
      rewrite ?disjoint_union_difference; auto.
189
    split; [|apply intersection_greatest; auto using subseteq_up_set with sts].
Robbert Krebbers's avatar
Robbert Krebbers committed
190
191
192
193
    apply intersection_greatest; [auto with sts|].
    intros s2; rewrite elem_of_intersection.
    unfold up_set; rewrite elem_of_bind; intros (?&s1&?&?&?).
    apply closed_steps with T2 s1; auto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
194
195
Qed.
Lemma step_closed s1 s2 T1 T2 S Tf :
196
197
  step (s1,T1) (s2,T2)  closed Tf S  s1  S  T1  Tf   
  s2  S  T2  Tf    tok s2  T2  .
Robbert Krebbers's avatar
Robbert Krebbers committed
198
Proof.
199
  inversion_clear 1 as [???? HR Hs1 Hs2]; intros [?? Hstep]??; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
200
  * eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
201
  * solve_elem_of -Hstep Hs1 Hs2.
Robbert Krebbers's avatar
Robbert Krebbers committed
202
203
204
205
206
Qed.
End sts_core.
End sts.

Section sts_ra.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
Context {A B : Type} (R : relation A) (tok : A  set B).
Robbert Krebbers's avatar
Robbert Krebbers committed
208

Robbert Krebbers's avatar
Robbert Krebbers committed
209
Definition sts := validity ( : sts.t R tok  Prop).
Robbert Krebbers's avatar
Robbert Krebbers committed
210
Global Instance sts_equiv : Equiv sts := validity_equiv _.
Robbert Krebbers's avatar
Robbert Krebbers committed
211
212
213
214
Global Instance sts_unit : Unit sts := validity_unit _.
Global Instance sts_op : Op sts := validity_op _.
Global Instance sts_minus : Minus sts := validity_minus _.
Global Instance sts_ra : RA sts := validity_ra _.
Robbert Krebbers's avatar
Robbert Krebbers committed
215
Definition sts_auth (s : A) (T : set B) : sts := to_validity (sts.auth s T).
Robbert Krebbers's avatar
Robbert Krebbers committed
216
217
Definition sts_frag (S : set A) (T : set B) : sts := to_validity (sts.frag S T).
Canonical Structure stsRA := validityRA (sts.t R tok).
Robbert Krebbers's avatar
Robbert Krebbers committed
218
219
220
Lemma sts_update s1 s2 T1 T2 :
  sts.step R tok (s1,T1) (s2,T2)  sts_auth s1 T1  sts_auth s2 T2.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
221
  intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
222
  destruct (sts.step_closed R tok s1 s2 T1 T2 S Tf) as (?&?&?); auto.
223
  repeat (done || constructor).
Robbert Krebbers's avatar
Robbert Krebbers committed
224
225
Qed.
End sts_ra.