sts.v 17.5 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 :
Ralf Jung's avatar
Ralf Jung committed
29
     (* TODO: This asks for ⊥ on sets: T1 ⊥ T2 := T1 ∩ T2 ⊆ ∅. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
30
     prim_step s1 s2  tok s1  T1    tok s2  T2   
Ralf Jung's avatar
Ralf Jung committed
31
     tok s1  T1  tok s2  T2  step (s1,T1) (s2,T2).
32
Definition steps := rtc step.
Robbert Krebbers's avatar
Robbert Krebbers committed
33
Inductive frame_step (T : tokens sts) (s1 s2 : state sts) : Prop :=
Robbert Krebbers's avatar
Robbert Krebbers committed
34
  | Frame_step T1 T2 :
35
     T1  (tok s1  T)    step (s1,T1) (s2,T2)  frame_step T s1 s2.
Robbert Krebbers's avatar
Robbert Krebbers committed
36 37 38

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

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

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

(** ** Properties of closure under frame steps *)
Lemma closed_disjoint' S T s : closed S T  s  S  tok s  T  .
88
Proof. intros [_ ? _]; set_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
89 90 91 92 93 94 95
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.
96
  intros [_ ? Hstep1] [_ ? Hstep2] ?; split; [done|set_solver|].
Robbert Krebbers's avatar
Robbert Krebbers committed
97
  intros s3 s4; rewrite !elem_of_intersection; intros [??] [T3 T4 ?]; split.
98 99
  - 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
100 101 102 103 104
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.
105
  inversion_clear 1 as [???? HR Hs1 Hs2]; intros [?? Hstep]??; split_and?; auto.
106
  - eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
107
  - set_solver -Hstep Hs1 Hs2.
Robbert Krebbers's avatar
Robbert Krebbers committed
108
Qed.
109 110 111 112 113 114 115 116 117 118
Lemma steps_closed s1 s2 T1 T2 S Tf :
  steps (s1,T1) (s2,T2)  closed S Tf  s1  S  T1  Tf   
  tok s1  T1    s2  S  T2  Tf    tok s2  T2  .
Proof.
  remember (s1,T1) as sT1. remember (s2,T2) as sT2. intros Hsteps.
  revert s1 T1 HeqsT1 s2 T2 HeqsT2.
  induction Hsteps as [?|? [s' T'] ? Hstep Hsteps IH]; intros; subst.
  - case: HeqsT2=>? ?. subst. done.
  - eapply step_closed in Hstep; [|done..]. destruct_conjs. eauto.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
119 120

(** ** Properties of the closure operators *)
121
Lemma elem_of_up s T : s  up s T.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
Proof. constructor. Qed.
123
Lemma subseteq_up_set S T : S  up_set S T.
Robbert Krebbers's avatar
Robbert Krebbers committed
124
Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
Ralf Jung's avatar
Ralf Jung committed
125 126
Lemma up_up_set s T : up s T  up_set {[ s ]} T.
Proof. by rewrite /up_set collection_bind_singleton. Qed.
127
Lemma closed_up_set S T :
128
  ( s, s  S  tok s  T  )  S    closed (up_set S T) T.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
Proof.
130
  intros HS Hne; unfold up_set; split.
131
  - assert ( s, s  up s T) by eauto using elem_of_up. set_solver.
132
  - intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
133
    specialize (HS s' Hs'); clear Hs' Hne S.
134
    induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
    inversion_clear Hstep; apply IH; clear IH; auto with sts.
136
  - intros s1 s2; rewrite !elem_of_bind; intros (s&?&?) ?; exists s.
Robbert Krebbers's avatar
Robbert Krebbers committed
137 138
    split; [eapply rtc_r|]; eauto.
Qed.
139
Lemma closed_up_set_empty S : S    closed (up_set S ) .
Robbert Krebbers's avatar
Robbert Krebbers committed
140
Proof. eauto using closed_up_set with sts. Qed.
141
Lemma closed_up s T : tok s  T    closed (up s T) T.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
Proof.
143
  intros; rewrite -(collection_bind_singleton (λ s, up s T) s).
144
  apply closed_up_set; set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
145
Qed.
146
Lemma closed_up_empty s : closed (up s ) .
Robbert Krebbers's avatar
Robbert Krebbers committed
147
Proof. eauto using closed_up with sts. Qed.
148
Lemma up_closed S T : closed S T  up_set S T  S.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
Proof.
150
  intros; split; auto using subseteq_up_set; intros s.
Robbert Krebbers's avatar
Robbert Krebbers committed
151 152 153
  unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).
  induction Hstep; eauto using closed_step.
Qed.
Ralf Jung's avatar
Ralf Jung committed
154 155 156 157 158 159
Lemma up_subseteq s T S :
  closed S T  s  S  sts.up s T  S.
Proof. move=>? ? s' ?. eapply closed_steps; done. Qed.
Lemma up_set_subseteq S1 T S2 :
  closed S2 T  S1  S2  sts.up_set S1 T  S2.
Proof. move=>? ? s [s' [? ?]]. eapply closed_steps; by eauto. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
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 204 205 206 207 208 209 210 211 212 213 214 215 216 217
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.

218 219 220 221
Hint Extern 10 (equiv (A:=set _) _ _) => set_solver : sts.
Hint Extern 10 (¬equiv (A:=set _) _ _) => set_solver : sts.
Hint Extern 10 (_  _) => set_solver : sts.
Hint Extern 10 (_  _) => set_solver : sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
222 223 224
Instance sts_equivalence: Equivalence (() : relation (car sts)).
Proof.
  split.
225 226 227
  - by intros []; constructor.
  - by destruct 1; constructor.
  - destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
228 229
Qed.
Global Instance sts_dra : DRA (car sts).
Robbert Krebbers's avatar
Robbert Krebbers committed
230 231
Proof.
  split.
232 233 234 235 236 237 238
  - 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,
239
      closed S T  s  S  tok s  T'    tok s  (T  T')  ).
240
    { intros S T T' s [??]; set_solver. }
Robbert Krebbers's avatar
Robbert Krebbers committed
241
    destruct 3; simpl in *; auto using closed_op with sts.
242 243
  - 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
244
      rewrite ?disjoint_union_difference; auto using closed_up with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
245
    eapply closed_up_set; eauto 2 using closed_disjoint with sts.
246 247 248 249 250 251
  - 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.
252
    assert (S  up_set S   S  ) by eauto using subseteq_up_set, closed_ne.
253
    set_solver.
254
  - intros [|S T]; constructor; auto with sts.
255
    assert (S  up_set S ); auto using subseteq_up_set with sts.
256
  - intros [s T|S T]; constructor; auto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
257 258 259
    + rewrite (up_closed (up _ _)); auto using closed_up with sts.
    + rewrite (up_closed (up_set _ _));
        eauto using closed_up_set, closed_ne with sts.
260
  - intros x y ?? (z&Hy&?&Hxz); exists (unit (x  y)); split_and?.
261
    + destruct Hxz;inversion_clear Hy;constructor;unfold up_set; set_solver.
262 263 264 265
    + 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
266 267 268 269
        | |- 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)
270
        end; auto with sts.
271
  - intros x y ?? (z&Hy&_&Hxz); destruct Hxz; inversion_clear Hy; constructor;
272
      repeat match goal with
273 274 275 276
      | |- 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)
277
      end; auto with sts.
278
  - intros x y ?? (z&Hy&?&Hxz); destruct Hxz as [S1 S2 T1 T2| |];
Robbert Krebbers's avatar
Robbert Krebbers committed
279
      inversion Hy; clear Hy; constructor; setoid_subst;
Robbert Krebbers's avatar
Robbert Krebbers committed
280
      rewrite ?disjoint_union_difference; auto.
281
    split; [|apply intersection_greatest; auto using subseteq_up_set with sts].
Robbert Krebbers's avatar
Robbert Krebbers committed
282 283 284 285
    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
286
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320
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
321
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
322 323
  intros S1 S2 ? T1 T2 HT; rewrite /sts_auth.
  by eapply to_validity_proper; try apply _; constructor.
Robbert Krebbers's avatar
Robbert Krebbers committed
324
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
325 326
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
327

Robbert Krebbers's avatar
Robbert Krebbers committed
328 329 330 331 332 333 334
(** 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
335

Robbert Krebbers's avatar
Robbert Krebbers committed
336 337 338
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
339

Robbert Krebbers's avatar
Robbert Krebbers committed
340 341 342 343
(** 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.
344
  intros; split; [split|constructor; set_solver]; simpl.
Robbert Krebbers's avatar
Robbert Krebbers committed
345
  - intros (?&?&?); by apply closed_disjoint' with S.
346 347 348 349
  - intros; split_and?.
    + set_solver+.
    + done.
    + constructor; set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
350 351
Qed.
Lemma sts_op_auth_frag_up s T :
352 353 354 355 356 357 358 359 360 361
  sts_auth s   sts_frag_up s T  sts_auth s T.
Proof.
  intros; split; [split|constructor; set_solver]; simpl.
  - intros (?&?&?). apply closed_disjoint' with (up s T); first done.
    apply elem_of_up.
  - intros; split_and?.
    + set_solver+.
    + by apply closed_up.
    + constructor; last set_solver. apply elem_of_up.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
362

Ralf Jung's avatar
Ralf Jung committed
363
Lemma sts_op_frag S1 S2 T1 T2 :
Ralf Jung's avatar
Ralf Jung committed
364
  T1  T2    sts.closed S1 T1  sts.closed S2 T2 
Ralf Jung's avatar
Ralf Jung committed
365 366
  sts_frag (S1  S2) (T1  T2)  sts_frag S1 T1  sts_frag S2 T2.
Proof.
367 368 369
  intros HT HS1 HS2. rewrite /sts_frag.
  (* FIXME why does rewrite not work?? *)
  etransitivity; last eapply to_validity_op; try done; [].
370
  intros Hval. constructor; last set_solver. eapply closed_ne, Hval.
Ralf Jung's avatar
Ralf Jung committed
371 372
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
373 374
(** Frame preserving updates *)
Lemma sts_update_auth s1 s2 T1 T2 :
375
  steps (s1,T1) (s2,T2)  sts_auth s1 T1 ~~> sts_auth s2 T2.
Robbert Krebbers's avatar
Robbert Krebbers committed
376
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
377
  intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst.
378
  destruct (steps_closed s1 s2 T1 T2 S Tf) as (?&?&?); auto; [].
379
  repeat (done || constructor).
Robbert Krebbers's avatar
Robbert Krebbers committed
380
Qed.
Ralf Jung's avatar
Ralf Jung committed
381

Robbert Krebbers's avatar
Robbert Krebbers committed
382 383
Lemma sts_update_frag S1 S2 T :
  closed S2 T  S1  S2  sts_frag S1 T ~~> sts_frag S2 T.
384
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
385
  rewrite /sts_frag=> HS Hcl. apply validity_update.
386
  inversion 3 as [|? S ? Tf|]; simplify_eq/=.
387 388
  - split; first done. constructor; [set_solver|done].
  - split; first done. constructor; set_solver.
389 390
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
391 392
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
393
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
394 395 396 397 398 399 400 401 402 403
  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 *)
404
  move=>Hcl2. split.
Robbert Krebbers's avatar
Robbert Krebbers committed
405
  - intros [[[Sf Tf|Sf Tf] vf Hvf] EQ].
406
    { exfalso. inversion_clear EQ as [Hv EQ']. apply EQ' in Hcl2. simpl in Hcl2.
407
      inversion Hcl2. }
408 409 410
    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]].
411
    apply Hvf in Hclf. simpl in Hclf. clear Hvf.
412
    inversion_clear Hdisj. split; last (exists Tf; split_and?); [done..|].
413
    apply (anti_symm ()).
414
    + move=>s HS2. apply elem_of_intersection. split; first by apply HS.
Robbert Krebbers's avatar
Robbert Krebbers committed
415
      by apply subseteq_up_set.
416
    + move=>s /elem_of_intersection [HS1 Hscl]. apply HS. split; first done.
417
      destruct Hscl as [s' [Hsup Hs']].
Robbert Krebbers's avatar
Robbert Krebbers committed
418
      eapply closed_steps; last (hnf in Hsup; eexact Hsup); first done.
419
      set_solver +HS Hs'.
Ralf Jung's avatar
Ralf Jung committed
420
  - intros (Hcl1 & Tf & Htk & Hf & Hs).
Robbert Krebbers's avatar
Robbert Krebbers committed
421
    exists (sts_frag (up_set S2 Tf) Tf).
422
    split; first split; simpl;[|done|].
423
    + intros _. split_and?; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
424 425
      * apply closed_up_set; last by eapply closed_ne.
        move=>s Hs2. move:(closed_disjoint _ _ Hcl2 _ Hs2).
426
        set_solver +Htk.
Robbert Krebbers's avatar
Robbert Krebbers committed
427
      * constructor; last done. rewrite -Hs. by eapply closed_ne.
428
    + intros _. constructor; [ set_solver +Htk | done].
429 430
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
431 432 433
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.
434
Proof.
435 436
  intros. apply sts_frag_included; split_and?; auto.
  exists ; split_and?; done || set_solver+.
437
Qed.
438
End stsRA.