sts.v 16.1 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 _ _ !_ /.

Robbert Krebbers's avatar
Robbert Krebbers committed
8
(** * Definition of STSs *)
9
Module sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
Structure stsT := STS {
Ralf Jung's avatar
Ralf Jung committed
11
12
  state : Type;
  token : Type;
Robbert Krebbers's avatar
Robbert Krebbers committed
13
14
  prim_step : relation state;
  tok : state  set token;
Ralf Jung's avatar
Ralf Jung committed
15
}.
16
Arguments STS {_ _} _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
17
18
19
20
Arguments prim_step {_} _ _.
Arguments tok {_} _.
Notation states sts := (set (state sts)).
Notation tokens sts := (set (token sts)).
Ralf Jung's avatar
Ralf Jung committed
21

Robbert Krebbers's avatar
Robbert Krebbers committed
22
23
24
(** * Theory and definitions *)
Section sts.
Context {sts : stsT}.
Ralf Jung's avatar
Ralf Jung committed
25

Robbert Krebbers's avatar
Robbert Krebbers committed
26
27
(** ** Step relations *)
Inductive step : relation (state sts * tokens sts) :=
Robbert Krebbers's avatar
Robbert Krebbers committed
28
  | Step s1 s2 T1 T2 :
Robbert Krebbers's avatar
Robbert Krebbers committed
29
     prim_step s1 s2  tok s1  T1    tok s2  T2   
Ralf Jung's avatar
Ralf Jung committed
30
     tok s1  T1  tok s2  T2  step (s1,T1) (s2,T2).
Robbert Krebbers's avatar
Robbert Krebbers committed
31
Inductive frame_step (T : tokens sts) (s1 s2 : state sts) : Prop :=
Robbert Krebbers's avatar
Robbert Krebbers committed
32
  | Frame_step T1 T2 :
33
     T1  (tok s1  T)    step (s1,T1) (s2,T2)  frame_step T s1 s2.
Robbert Krebbers's avatar
Robbert Krebbers committed
34
35
36

(** ** Closure under frame steps *)
Record closed (S : states sts) (T : tokens sts) : Prop := Closed {
37
  closed_ne : S  ;
38
  closed_disjoint s : s  S  tok s  T  ;
Robbert Krebbers's avatar
Robbert Krebbers committed
39
40
  closed_step s1 s2 : s1  S  frame_step T s1 s2  s2  S
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
41
Definition up (s : state sts) (T : tokens sts) : states sts :=
Ralf Jung's avatar
Ralf Jung committed
42
  mkSet (rtc (frame_step T) s).
Robbert Krebbers's avatar
Robbert Krebbers committed
43
Definition up_set (S : states sts) (T : tokens sts) : states sts :=
Robbert Krebbers's avatar
Robbert Krebbers committed
44
  S = λ s, up s T.
Robbert Krebbers's avatar
Robbert Krebbers committed
45

Robbert Krebbers's avatar
Robbert Krebbers committed
46
47
48
49
(** Tactic setup *)
Hint Resolve Step.
Hint Extern 10 (equiv (A:=set _) _ _) => solve_elem_of : sts.
Hint Extern 10 (¬equiv (A:=set _) _ _) => solve_elem_of : sts.
50
51
Hint Extern 10 (_  _) => solve_elem_of : sts.
Hint Extern 10 (_  _) => solve_elem_of : sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
52
53
54

(** ** Setoids *)
Instance framestep_proper' : Proper (() ==> (=) ==> (=) ==> impl) frame_step.
55
Proof. intros ?? HT ?? <- ?? <-; destruct 1; econstructor; eauto with sts. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
57
Global Instance framestep_proper : Proper (() ==> (=) ==> (=) ==> iff) frame_step.
Proof. by intros ?? [??] ??????; split; apply framestep_proper'. Qed.
58
Instance closed_proper' : Proper (() ==> () ==> impl) closed.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
Proof.
60
  intros ?? HT ?? HS; destruct 1;
Robbert Krebbers's avatar
Robbert Krebbers committed
61
    constructor; intros until 0; rewrite -?HS -?HT; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
63
Global Instance closed_proper : Proper (() ==> () ==> iff) closed.
64
Proof. by split; apply closed_proper'. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
Global Instance up_preserving : Proper ((=) ==> flip () ==> ()) up.
Robbert Krebbers's avatar
Robbert Krebbers committed
66
Proof.
67
  intros s ? <- T T' HT ; apply elem_of_subseteq.
Robbert Krebbers's avatar
Robbert Krebbers committed
68
69
70
  induction 1 as [|s1 s2 s3 [T1 T2]]; [constructor|].
  eapply rtc_l; [eapply Frame_step with T1 T2|]; eauto with sts.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
Global Instance up_proper : Proper ((=) ==> () ==> ()) up.
72
Proof. by intros ??? ?? [??]; split; apply up_preserving. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
73
Global Instance up_set_preserving : Proper (() ==> flip () ==> ()) up_set.
Ralf Jung's avatar
Ralf Jung committed
74
75
76
77
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
78
Global Instance up_set_proper : Proper (() ==> () ==> ()) up_set.
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Proof. by intros S1 S2 [??] T1 T2 [??]; split; apply up_set_preserving. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
80
81
82
83
84
85
86
87
88
89
90
91
92

(** ** Properties of closure under frame steps *)
Lemma closed_disjoint' S T s : closed S T  s  S  tok s  T  .
Proof. intros [_ ? _]; solve_elem_of. Qed.
Lemma closed_steps S T s1 s2 :
  closed S T  s1  S  rtc (frame_step T) s1 s2  s2  S.
Proof. induction 3; eauto using closed_step. Qed.
Lemma closed_op T1 T2 S1 S2 :
  closed S1 T1  closed S2 T2 
  T1  T2    S1  S2    closed (S1  S2) (T1  T2).
Proof.
  intros [_ ? Hstep1] [_ ? Hstep2] ?; split; [done|solve_elem_of|].
  intros s3 s4; rewrite !elem_of_intersection; intros [??] [T3 T4 ?]; split.
93
94
  - 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
95
96
97
98
99
100
Qed.
Lemma step_closed s1 s2 T1 T2 S Tf :
  step (s1,T1) (s2,T2)  closed S Tf  s1  S  T1  Tf   
  s2  S  T2  Tf    tok s2  T2  .
Proof.
  inversion_clear 1 as [???? HR Hs1 Hs2]; intros [?? Hstep]??; split_ands; auto.
101
102
  - eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
  - solve_elem_of -Hstep Hs1 Hs2.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
104
105
Qed.

(** ** Properties of the closure operators *)
106
Lemma elem_of_up s T : s  up s T.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
Proof. constructor. Qed.
108
Lemma subseteq_up_set S T : S  up_set S T.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
Ralf Jung's avatar
Ralf Jung committed
110
111
Lemma up_up_set s T : up s T  up_set {[ s ]} T.
Proof. by rewrite /up_set collection_bind_singleton. Qed.
112
Lemma closed_up_set S T :
113
  ( s, s  S  tok s  T  )  S    closed (up_set S T) T.
Robbert Krebbers's avatar
Robbert Krebbers committed
114
Proof.
115
  intros HS Hne; unfold up_set; split.
116
117
  - assert ( s, s  up s T) by eauto using elem_of_up. solve_elem_of.
  - intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
118
    specialize (HS s' Hs'); clear Hs' Hne S.
119
    induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
120
    inversion_clear Hstep; apply IH; clear IH; auto with sts.
121
  - intros s1 s2; rewrite !elem_of_bind; intros (s&?&?) ?; exists s.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
123
    split; [eapply rtc_r|]; eauto.
Qed.
124
Lemma closed_up_set_empty S : S    closed (up_set S ) .
Robbert Krebbers's avatar
Robbert Krebbers committed
125
Proof. eauto using closed_up_set with sts. Qed.
126
Lemma closed_up s T : tok s  T    closed (up s T) T.
Robbert Krebbers's avatar
Robbert Krebbers committed
127
Proof.
128
  intros; rewrite -(collection_bind_singleton (λ s, up s T) s).
129
  apply closed_up_set; solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
Qed.
131
Lemma closed_up_empty s : closed (up s ) .
Robbert Krebbers's avatar
Robbert Krebbers committed
132
Proof. eauto using closed_up with sts. Qed.
133
Lemma up_closed S T : closed S T  up_set S T  S.
Robbert Krebbers's avatar
Robbert Krebbers committed
134
Proof.
135
  intros; split; auto using subseteq_up_set; intros s.
Robbert Krebbers's avatar
Robbert Krebbers committed
136
137
138
  unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).
  induction Hstep; eauto using closed_step.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
End sts. End sts.

Notation stsT := sts.stsT.
Notation STS := sts.STS.

(** * STSs form a disjoint RA *)
(* This module should never be imported, uses the module [sts] below. *)
Module sts_dra.
Import sts.

(* The type of bounds we can give to the state of an STS. This is the type
   that we equip with an RA structure. *)
Inductive car (sts : stsT) :=
  | auth : state sts  set (token sts)  car sts
  | frag : set (state sts)  set (token sts )  car sts.
Arguments auth {_} _ _.
Arguments frag {_} _ _.

Section sts_dra.
Context {sts : stsT}.
Infix "≼" := dra_included.
Implicit Types S : states sts.
Implicit Types T : tokens sts.

Inductive sts_equiv : Equiv (car sts) :=
  | 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.
Existing Instance sts_equiv.
Instance sts_valid : Valid (car sts) := λ x,
  match x with auth s T => tok s  T   | frag S' T => closed S' T end.
Instance sts_unit : Unit (car sts) := λ x,
  match x with
  | frag S' _ => frag (up_set S'  ) 
  | auth s _  => frag (up s ) 
  end.
Inductive sts_disjoint : Disjoint (car sts) :=
  | frag_frag_disjoint S1 S2 T1 T2 :
     S1  S2    T1  T2    frag S1 T1  frag S2 T2
  | 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.
Existing Instance sts_disjoint.
Instance sts_op : Op (car sts) := λ 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.
Instance sts_minus : Minus (car sts) := λ x1 x2,
  match x1, x2 with
  | frag S1 T1, frag S2 T2 => frag (up_set S1 (T1  T2)) (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 s (T1  T2)) (T1  T2)
  end.

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.
Instance sts_equivalence: Equivalence (() : relation (car sts)).
Proof.
  split.
204
205
206
  - by intros []; constructor.
  - by destruct 1; constructor.
  - destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
207
208
Qed.
Global Instance sts_dra : DRA (car sts).
Robbert Krebbers's avatar
Robbert Krebbers committed
209
210
Proof.
  split.
211
212
213
214
215
216
217
  - apply _.
  - by do 2 destruct 1; constructor; setoid_subst.
  - by destruct 1; constructor; setoid_subst.
  - by destruct 1; simpl; intros ?; 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,
218
      closed S T  s  S  tok s  T'    tok s  (T  T')  ).
219
    { intros S T T' s [??]; solve_elem_of. }
Robbert Krebbers's avatar
Robbert Krebbers committed
220
    destruct 3; simpl in *; auto using closed_op with sts.
221
222
  - intros []; simpl; eauto using closed_up, closed_up_set, closed_ne with sts.
  - intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy;clear Hy; setoid_subst;
Robbert Krebbers's avatar
Robbert Krebbers committed
223
      rewrite ?disjoint_union_difference; auto using closed_up with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
224
    eapply closed_up_set; eauto 2 using closed_disjoint with sts.
225
226
227
228
229
230
  - intros [] [] []; constructor; rewrite ?assoc; auto with sts.
  - 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.
  - intros [|S T]; constructor; auto using elem_of_up with sts.
231
    assert (S  up_set S   S  ) by eauto using subseteq_up_set, closed_ne.
232
    solve_elem_of.
233
  - intros [|S T]; constructor; auto with sts.
234
    assert (S  up_set S ); auto using subseteq_up_set with sts.
235
  - intros [s T|S T]; constructor; auto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
236
237
238
    + rewrite (up_closed (up _ _)); auto using closed_up with sts.
    + rewrite (up_closed (up_set _ _));
        eauto using closed_up_set, closed_ne with sts.
239
  - intros x y ?? (z&Hy&?&Hxz); exists (unit (x  y)); split_ands.
240
    + destruct Hxz;inversion_clear Hy;constructor;unfold up_set; solve_elem_of.
241
242
243
244
    + 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
245
246
247
248
        | |- 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)
249
        end; auto with sts.
250
  - intros x y ?? (z&Hy&_&Hxz); destruct Hxz; inversion_clear Hy; constructor;
251
      repeat match goal with
252
253
254
255
      | |- 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)
256
      end; auto with sts.
257
  - intros x y ?? (z&Hy&?&Hxz); destruct Hxz as [S1 S2 T1 T2| |];
Robbert Krebbers's avatar
Robbert Krebbers committed
258
      inversion Hy; clear Hy; constructor; setoid_subst;
Robbert Krebbers's avatar
Robbert Krebbers committed
259
      rewrite ?disjoint_union_difference; auto.
260
    split; [|apply intersection_greatest; auto using subseteq_up_set with sts].
Robbert Krebbers's avatar
Robbert Krebbers committed
261
262
263
264
    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
265
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
Canonical Structure RA : cmraT := validityRA (car sts).
End sts_dra. End sts_dra.

(** * The STS Resource Algebra *)
(** Finally, the general theory of STS that should be used by users *)
Notation stsRA := (@sts_dra.RA).

Section sts_definitions.
  Context {sts : stsT}.
  Definition sts_auth (s : sts.state sts) (T : sts.tokens sts) : stsRA sts :=
    to_validity (sts_dra.auth s T).
  Definition sts_frag (S : sts.states sts) (T : sts.tokens sts) : stsRA sts :=
    to_validity (sts_dra.frag S T).
  Definition sts_frag_up (s : sts.state sts) (T : sts.tokens sts) : stsRA sts :=
    sts_frag (sts.up s T) T.
End sts_definitions.
Instance: Params (@sts_auth) 2.
Instance: Params (@sts_frag) 1.
Instance: Params (@sts_frag_up) 2.

Section stsRA.
Import sts.
Context {sts : stsT}.
Implicit Types s : state sts.
Implicit Types S : states sts.
Implicit Types T : tokens sts.

(** Setoids *)
Global Instance sts_auth_proper s : Proper (() ==> ()) (sts_auth s).
Proof. (* this proof is horrible *)
  intros T1 T2 HT. rewrite /sts_auth.
  by eapply to_validity_proper; try apply _; constructor.
Qed.
Global Instance sts_frag_proper : Proper (() ==> () ==> ()) (@sts_frag sts).
Robbert Krebbers's avatar
Robbert Krebbers committed
300
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
301
302
  intros S1 S2 ? T1 T2 HT; rewrite /sts_auth.
  by eapply to_validity_proper; try apply _; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
303
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
304
305
Global Instance sts_frag_up_proper s : Proper (() ==> ()) (sts_frag_up s).
Proof. intros T1 T2 HT. by rewrite /sts_frag_up HT. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
306

Robbert Krebbers's avatar
Robbert Krebbers committed
307
308
309
310
311
312
313
(** Validity *)
Lemma sts_auth_valid s T :  sts_auth s T  tok s  T  .
Proof. split. by move=> /(_ 0). by intros ??. Qed.
Lemma sts_frag_valid S T :  sts_frag S T  closed S T.
Proof. split. by move=> /(_ 0). by intros ??. Qed.
Lemma sts_frag_up_valid s T : tok s  T     sts_frag_up s T.
Proof. intros; by apply sts_frag_valid, closed_up. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
314

Robbert Krebbers's avatar
Robbert Krebbers committed
315
316
317
Lemma sts_auth_frag_valid_inv s S T1 T2 :
   (sts_auth s T1  sts_frag S T2)  s  S.
Proof. by move=> /(_ 0) [? [? Hdisj]]; inversion Hdisj. Qed.
Ralf Jung's avatar
Ralf Jung committed
318

Robbert Krebbers's avatar
Robbert Krebbers committed
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
(** Op *)
Lemma sts_op_auth_frag s S T :
  s  S  closed S T  sts_auth s   sts_frag S T  sts_auth s T.
Proof.
  intros; split; [split|constructor; solve_elem_of]; simpl.
  - intros (?&?&?); by apply closed_disjoint' with S.
  - intros; split_ands. solve_elem_of+. done. constructor; solve_elem_of.
Qed.
Lemma sts_op_auth_frag_up s T :
  tok s  T    sts_auth s   sts_frag_up s T  sts_auth s T.
Proof. intros; apply sts_op_auth_frag; auto using elem_of_up, closed_up. Qed.

(** Frame preserving updates *)
Lemma sts_update_auth s1 s2 T1 T2 :
  step (s1,T1) (s2,T2)  sts_auth s1 T1 ~~> sts_auth s2 T2.
Robbert Krebbers's avatar
Robbert Krebbers committed
334
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
335
  intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
336
  destruct (step_closed s1 s2 T1 T2 S Tf) as (?&?&?); auto.
337
  repeat (done || constructor).
Robbert Krebbers's avatar
Robbert Krebbers committed
338
Qed.
Ralf Jung's avatar
Ralf Jung committed
339

Robbert Krebbers's avatar
Robbert Krebbers committed
340
341
Lemma sts_update_frag S1 S2 T :
  closed S2 T  S1  S2  sts_frag S1 T ~~> sts_frag S2 T.
342
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
343
344
345
  rewrite /sts_frag=> HS Hcl. apply validity_update.
  inversion 3 as [|? S ? Tf|]; simplify_equality'.
  - split; first done. constructor; [solve_elem_of|done].
346
347
348
  - split; first done. constructor; solve_elem_of.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
349
350
Lemma sts_update_frag_up s1 S2 T :
  closed S2 T  s1  S2  sts_frag_up s1 T ~~> sts_frag S2 T.
Ralf Jung's avatar
Ralf Jung committed
351
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
352
353
354
355
356
357
358
359
360
361
  intros; by apply sts_update_frag; [|intros ?; eauto using closed_steps].
Qed.

(** Inclusion *)
Lemma sts_frag_included S1 S2 T1 T2 :
  closed S2 T2 
  sts_frag S1 T1  sts_frag S2 T2 
  (closed S1 T1   Tf, T2  T1  Tf  T1  Tf    S2  S1  up_set S2 Tf).
Proof. (* This should use some general properties of DRAs. To be improved
when we have RAs back *)
362
  move=>Hcl2. split.
Robbert Krebbers's avatar
Robbert Krebbers committed
363
  - intros [[[Sf Tf|Sf Tf] vf Hvf] EQ].
364
    { exfalso. inversion_clear EQ as [Hv EQ']. apply EQ' in Hcl2. simpl in Hcl2.
365
      inversion Hcl2. }
366
367
368
    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]].
369
370
371
    apply Hvf in Hclf. simpl in Hclf. clear Hvf.
    inversion_clear Hdisj. split; last (exists Tf; split_ands); [done..|].
    apply (anti_symm ()).
372
    + move=>s HS2. apply elem_of_intersection. split; first by apply HS.
Robbert Krebbers's avatar
Robbert Krebbers committed
373
      by apply subseteq_up_set.
374
    + move=>s /elem_of_intersection [HS1 Hscl]. apply HS. split; first done.
375
      destruct Hscl as [s' [Hsup Hs']].
Robbert Krebbers's avatar
Robbert Krebbers committed
376
      eapply closed_steps; last (hnf in Hsup; eexact Hsup); first done.
377
      solve_elem_of +HS Hs'.
Ralf Jung's avatar
Ralf Jung committed
378
  - intros (Hcl1 & Tf & Htk & Hf & Hs).
Robbert Krebbers's avatar
Robbert Krebbers committed
379
    exists (sts_frag (up_set S2 Tf) Tf).
380
381
    split; first split; simpl;[|done|].
    + intros _. split_ands; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
382
383
      * apply closed_up_set; last by eapply closed_ne.
        move=>s Hs2. move:(closed_disjoint _ _ Hcl2 _ Hs2).
Ralf Jung's avatar
Ralf Jung committed
384
        solve_elem_of +Htk.
Robbert Krebbers's avatar
Robbert Krebbers committed
385
      * constructor; last done. rewrite -Hs. by eapply closed_ne.
386
387
388
    + intros _. constructor; [ solve_elem_of +Htk | done].
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
389
390
391
Lemma sts_frag_included' S1 S2 T :
  closed S2 T  closed S1 T  S2  S1  up_set S2  
  sts_frag S1 T  sts_frag S2 T.
392
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
393
394
  intros. apply sts_frag_included; split_ands; auto.
  exists ; split_ands; done || solve_elem_of+.
395
Qed.
396
End stsRA.