sts.v 18.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_disjoint s : s  S  tok s  T  ;
Robbert Krebbers's avatar
Robbert Krebbers committed
40 41
  closed_step s1 s2 : s1  S  frame_step T s1 s2  s2  S
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
42
Definition up (s : state sts) (T : tokens sts) : states sts :=
Ralf Jung's avatar
Ralf Jung committed
43
  mkSet (rtc (frame_step T) s).
Robbert Krebbers's avatar
Robbert Krebbers committed
44
Definition up_set (S : states sts) (T : tokens sts) : states sts :=
Robbert Krebbers's avatar
Robbert Krebbers committed
45
  S = λ s, up s T.
Robbert Krebbers's avatar
Robbert Krebbers committed
46

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

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

(** ** Properties of closure under frame steps *)
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 :
90
  closed S1 T1  closed S2 T2  closed (S1  S2) (T1  T2).
Robbert Krebbers's avatar
Robbert Krebbers committed
91
Proof.
92
  intros [? Hstep1] [? Hstep2]; split; [set_solver|].
Robbert Krebbers's avatar
Robbert Krebbers committed
93
  intros s3 s4; rewrite !elem_of_intersection; intros [??] [T3 T4 ?]; split.
94 95
  - 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 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.
101
  inversion_clear 1 as [???? HR Hs1 Hs2]; intros [? Hstep]??; split_and?; auto.
102
  - eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
103
  - set_solver -Hstep Hs1 Hs2.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
Qed.
105 106 107 108 109 110 111 112 113 114
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
115 116

(** ** Properties of the closure operators *)
117
Lemma elem_of_up s T : s  up s T.
Robbert Krebbers's avatar
Robbert Krebbers committed
118
Proof. constructor. Qed.
119
Lemma subseteq_up_set S T : S  up_set S T.
Robbert Krebbers's avatar
Robbert Krebbers committed
120
Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
Ralf Jung's avatar
Ralf Jung committed
121 122
Lemma up_up_set s T : up s T  up_set {[ s ]} T.
Proof. by rewrite /up_set collection_bind_singleton. Qed.
123
Lemma closed_up_set S T :
124
  ( s, s  S  tok s  T  )  closed (up_set S T) T.
Robbert Krebbers's avatar
Robbert Krebbers committed
125
Proof.
126
  intros HS; unfold up_set; split.
127
  - intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
128
    specialize (HS s' Hs'); clear Hs' S.
129
    induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
130
    inversion_clear Hstep; apply IH; clear IH; auto with sts.
131
  - intros s1 s2; rewrite !elem_of_bind; intros (s&?&?) ?; exists s.
Robbert Krebbers's avatar
Robbert Krebbers committed
132 133
    split; [eapply rtc_r|]; eauto.
Qed.
134
Lemma closed_up s T : tok s  T    closed (up s T) T.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
Proof.
136
  intros; rewrite -(collection_bind_singleton (λ s, up s T) s).
137
  apply closed_up_set; set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
138
Qed.
139 140
Lemma closed_up_set_empty S : closed (up_set S ) .
Proof. eauto using closed_up_set with sts. Qed.
141
Lemma closed_up_empty s : closed (up s ) .
Robbert Krebbers's avatar
Robbert Krebbers committed
142
Proof. eauto using closed_up with sts. Qed.
143 144 145 146 147 148 149 150 151 152
Lemma up_set_empty S T : up_set S T    S  .
Proof.
  move:(subseteq_up_set S T). set_solver.
Qed.
Lemma up_set_nonempty S T : S    up_set S T  .
Proof. by move=>? /up_set_empty. Qed.
Lemma up_nonempty s T : up s T  .
Proof.
  move:(elem_of_up s T). set_solver.
Qed.
153
Lemma up_closed S T : closed S T  up_set S T  S.
Robbert Krebbers's avatar
Robbert Krebbers committed
154
Proof.
155
  intros; split; auto using subseteq_up_set; intros s.
Robbert Krebbers's avatar
Robbert Krebbers committed
156 157 158
  unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).
  induction Hstep; eauto using closed_step.
Qed.
Ralf Jung's avatar
Ralf Jung committed
159 160 161 162 163 164
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
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
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.
192 193
Global Existing Instance sts_equiv.
Global Instance sts_valid : Valid (car sts) := λ x,
194 195 196
  match x with
  | auth s T => tok s  T  
  | frag S' T => closed S' T  S'   end.
197
Global Instance sts_unit : Unit (car sts) := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
198 199 200 201 202 203 204 205 206 207 208
  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.
209 210
Global Existing Instance sts_disjoint.
Global Instance sts_op : Op (car sts) := λ x1 x2,
Robbert Krebbers's avatar
Robbert Krebbers committed
211 212 213 214 215 216
  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.
217
Global Instance sts_minus : Minus (car sts) := λ x1 x2,
Robbert Krebbers's avatar
Robbert Krebbers committed
218 219 220 221 222 223 224
  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.

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

Robbert Krebbers's avatar
Robbert Krebbers committed
342 343 344
(** Validity *)
Lemma sts_auth_valid s T :  sts_auth s T  tok s  T  .
Proof. split. by move=> /(_ 0). by intros ??. Qed.
345
Lemma sts_frag_valid S T :  sts_frag S T  closed S T  S  .
Robbert Krebbers's avatar
Robbert Krebbers committed
346 347
Proof. split. by move=> /(_ 0). by intros ??. Qed.
Lemma sts_frag_up_valid s T : tok s  T     sts_frag_up s T.
348
Proof. intros. by apply sts_frag_valid; auto using closed_up, up_nonempty. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
349

Robbert Krebbers's avatar
Robbert Krebbers committed
350 351 352
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
353

Robbert Krebbers's avatar
Robbert Krebbers committed
354 355 356 357
(** 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.
358
  intros; split; [split|constructor; set_solver]; simpl.
359
  - intros (?&?&?); by apply closed_disjoint with S.
360 361 362
  - intros; split_and?.
    + set_solver+.
    + done.
363
    + set_solver.
364
    + constructor; set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
365 366
Qed.
Lemma sts_op_auth_frag_up s T :
367 368 369
  sts_auth s   sts_frag_up s T  sts_auth s T.
Proof.
  intros; split; [split|constructor; set_solver]; simpl.
370 371
  - intros (?&?&?). destruct_conjs.
    apply closed_disjoint with (up s T); first done.
372 373 374 375
    apply elem_of_up.
  - intros; split_and?.
    + set_solver+.
    + by apply closed_up.
376
    + apply up_nonempty.
377 378
    + constructor; last set_solver. apply elem_of_up.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
379

Ralf Jung's avatar
Ralf Jung committed
380
Lemma sts_op_frag S1 S2 T1 T2 :
381
  T1  T2    sts.closed S1 T1  sts.closed S2 T2 
Ralf Jung's avatar
Ralf Jung committed
382 383
  sts_frag (S1  S2) (T1  T2)  sts_frag S1 T1  sts_frag S2 T2.
Proof.
384 385
  intros HT HS1 HS2. rewrite /sts_frag.
  (* FIXME why does rewrite not work?? *)
386 387 388
  etrans; last eapply to_validity_op; first done; [].
  move=>/=[??]. split_and!; [auto; set_solver..|].
  constructor; done.
Ralf Jung's avatar
Ralf Jung committed
389 390
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
391 392
(** Frame preserving updates *)
Lemma sts_update_auth s1 s2 T1 T2 :
393
  steps (s1,T1) (s2,T2)  sts_auth s1 T1 ~~> sts_auth s2 T2.
Robbert Krebbers's avatar
Robbert Krebbers committed
394
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
395
  intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst.
396
  simpl in *. destruct_conjs.
397
  destruct (steps_closed s1 s2 T1 T2 S Tf) as (?&?&?); auto; [].
398
  repeat (done || constructor).
Robbert Krebbers's avatar
Robbert Krebbers committed
399
Qed.
Ralf Jung's avatar
Ralf Jung committed
400

401 402
Lemma sts_update_frag S1 S2 T1 T2 :
  closed S2 T2  S1  S2  T2  T1  sts_frag S1 T1 ~~> sts_frag S2 T2.
403
Proof.
404
  rewrite /sts_frag=> ? HS HT. apply validity_update.
405
  inversion 3 as [|? S ? Tf|]; simplify_eq/=.
406 407
  - split_and!; first done; first set_solver. constructor; set_solver.
  - split_and!; first done; first set_solver. constructor; set_solver.
408 409
Qed.

410 411
Lemma sts_update_frag_up s1 S2 T1 T2 :
  closed S2 T2  s1  S2  T2  T1  sts_frag_up s1 T1 ~~> sts_frag S2 T2.
Ralf Jung's avatar
Ralf Jung committed
412
Proof.
413 414
  intros ? ? HT; apply sts_update_frag; [intros; eauto using closed_steps..].
  rewrite <-HT. eapply up_subseteq; done.
Robbert Krebbers's avatar
Robbert Krebbers committed
415 416
Qed.

417 418 419 420 421 422 423 424 425 426 427 428 429
Lemma up_set_intersection S1 Sf Tf :
  closed Sf Tf  
  S1  Sf  S1  up_set (S1  Sf) Tf.
Proof.
  intros Hclf. apply (anti_symm ()).
  + move=>s [HS1 HSf]. split; first by apply HS1.
    by apply subseteq_up_set.
  + move=>s [HS1 Hscl]. split; first done.
    destruct Hscl as [s' [Hsup Hs']].
    eapply closed_steps; last (hnf in Hsup; eexact Hsup); first done.
    set_solver +Hs'.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
430
(** Inclusion *)
431 432 433
(* This is surprisingly different from to_validity_included. I am not sure
   whether this is because to_validity_included is non-canonical, or this
   one here is non-canonical - but I suspect both. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
434
Lemma sts_frag_included S1 S2 T1 T2 :
435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458
  closed S2 T2  S2   
  (sts_frag S1 T1  sts_frag S2 T2) 
  (closed S1 T1  S1     Tf, T2  T1  Tf  T1  Tf   
                                 S2  S1  up_set S2 Tf).
Proof.
  destruct (to_validity_included (sts_dra.car sts) (sts_dra.frag S1 T1) (sts_dra.frag S2 T2)) as [Hfincl Htoincl].
  intros Hcl2 HS2ne. split.
  - intros Hincl. destruct Hfincl as ((Hcl1 & ?) & (z & EQ & Hval & Hdisj)).
    { split; last done. split; done. }
    clear Htoincl. split_and!; try done; [].
    destruct z as [sf Tf|Sf Tf].
    { exfalso. inversion_clear EQ. }
    exists Tf. inversion_clear EQ as [|? ? ? ? HT2 HS2].
    inversion_clear Hdisj as [? ? ? ? _ HTdisj | |]. split_and!; [done..|].
    rewrite HS2. apply up_set_intersection. apply Hval.
  - intros (Hcl & Hne & (Tf & HT & HTdisj & HS)). destruct Htoincl as ((Hcl' & ?) & (z & EQ)); last first.
    { exists z. exact EQ. } clear Hfincl.
    split; first (split; done). exists (sts_dra.frag (up_set S2 Tf) Tf). split_and!.
    + constructor; done.
    + simpl. split.
      * apply closed_up_set. move=>s Hs2. move:(closed_disjoint _ _ Hcl2 _ Hs2).
        set_solver +HT.
      * by apply up_set_nonempty.
    + constructor; last done. by rewrite -HS.
459 460
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
461
Lemma sts_frag_included' S1 S2 T :
462
  closed S2 T  closed S1 T  S2    S1    S2  S1  up_set S2  
Robbert Krebbers's avatar
Robbert Krebbers committed
463
  sts_frag S1 T  sts_frag S2 T.
464
Proof.
465 466
  intros. apply sts_frag_included; split_and?; auto.
  exists ; split_and?; done || set_solver+.
467
Qed.
468

469
End stsRA.