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

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

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

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

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

216
Section stsRA.
Robbert Krebbers's avatar
Robbert Krebbers committed
217
Context {A B : Type} (R : relation A) (tok : A  set B).
Robbert Krebbers's avatar
Robbert Krebbers committed
218

219
220
221
Canonical Structure stsRA := validityRA (sts R tok).
Definition sts_auth (s : A) (T : set B) : stsRA := to_validity (auth s T).
Definition sts_frag (S : set A) (T : set B) : stsRA := to_validity (frag S T).
Ralf Jung's avatar
Ralf Jung committed
222

223
Lemma sts_update_auth s1 s2 T1 T2 :
224
  sts.step R tok (s1,T1) (s2,T2)  sts_auth s1 T1 ~~> sts_auth s2 T2.
Robbert Krebbers's avatar
Robbert Krebbers committed
225
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
226
  intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
227
  destruct (sts.step_closed R tok s1 s2 T1 T2 S Tf) as (?&?&?); auto.
228
  repeat (done || constructor).
Robbert Krebbers's avatar
Robbert Krebbers committed
229
Qed.
Ralf Jung's avatar
Ralf Jung committed
230

231
232
233
234
235
236
237
238
239
Lemma sts_update_frag S1 S2 (T : set B) :
  S1  S2  sts.closed R tok S2 T 
  sts_frag S1 T ~~> sts_frag S2 T.
Proof.
  move=>HS Hcl. eapply validity_update; inversion 3 as [|? S ? Tf|]; subst.
  - split; first done. constructor; last done. solve_elem_of.
  - split; first done. constructor; solve_elem_of.
Qed.

240
241
242
243
Lemma sts_frag_included S1 S2 T1 T2 :
  sts.closed R tok S2 T2 
  sts_frag S1 T1  sts_frag S2 T2  
  (sts.closed R tok S1 T1   Tf, T2  T1  Tf  T1  Tf    S2  (S1  sts.up_set R tok S2 Tf)).
Ralf Jung's avatar
Ralf Jung committed
244
Proof.
245
246
  move=>Hcl2. split.
  - intros [xf EQ]. destruct xf as [xf vf Hvf]. destruct xf as [Sf Tf|Sf Tf].
247
    { exfalso. inversion_clear EQ as [Hv EQ']. apply EQ' in Hcl2. simpl in Hcl2.
248
      inversion Hcl2. }
249
250
251
    inversion_clear EQ as [Hv EQ'].
    move:(EQ' Hcl2)=>{EQ'} EQ. inversion_clear EQ as [|? ? ? ? HT HS].
    destruct Hv as [Hv _]. move:(Hv Hcl2)=>{Hv} [/= Hcl1  [Hclf Hdisj]].
252
253
254
    apply Hvf in Hclf. simpl in Hclf. clear Hvf.
    inversion_clear Hdisj. split; last (exists Tf; split_ands); [done..|].
    apply (anti_symm ()).
255
    + move=>s HS2. apply elem_of_intersection. split; first by apply HS.
256
      by apply sts.subseteq_up_set.
257
    + move=>s /elem_of_intersection [HS1 Hscl]. apply HS. split; first done.
258
259
      destruct Hscl as [s' [Hsup Hs']].
      eapply sts.closed_steps; last (hnf in Hsup; eexact Hsup); first done.
260
      solve_elem_of +HS Hs'.
261
262
263
264
265
  - intros (Hcl1 & Tf & Htk & Hf & Hs). exists (sts_frag (sts.up_set R tok S2 Tf) Tf).
    split; first split; simpl;[|done|].
    + intros _. split_ands; first done.
      * apply sts.closed_up_set; last by eapply sts.closed_ne.
        move=>s Hs2. move:(sts.closed_disjoint _ _ _ _ Hcl2 _ Hs2).
Ralf Jung's avatar
Ralf Jung committed
266
        solve_elem_of +Htk.
267
268
269
270
271
272
273
274
275
276
277
278
      * constructor; last done. rewrite -Hs. by eapply sts.closed_ne.
    + intros _. constructor; [ solve_elem_of +Htk | done].
Qed.

Lemma sts_frag_included' S1 S2 T :
  sts.closed R tok S2 T  sts.closed R tok S1 T 
  S2  (S1  sts.up_set R tok S2 ) 
  sts_frag S1 T  sts_frag S2 T.
Proof.
  intros. apply sts_frag_included; first done.
  split; first done. exists . split_ands; done || solve_elem_of+.
Qed.
Ralf Jung's avatar
Ralf Jung committed
279

280
End stsRA.