sts.v 9.87 KB
Newer Older
1 2 3
From algebra Require Export cmra.
From prelude Require Import sets.
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.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
Record closed (T : set B) (S : set A) : 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 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.
40
Global Instance sts_valid : Valid (sts R tok) := λ x,
41
  match x with auth s T => tok s  T   | frag S' T => closed T S' end.
Robbert Krebbers's avatar
Robbert Krebbers committed
42 43
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.
44
Global Instance sts_unit : Unit (sts R tok) := λ x,
Robbert Krebbers's avatar
Robbert Krebbers committed
45 46 47
  match x with
  | frag S' _ => frag (up_set  S')  | auth s _ => frag (up  s) 
  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 63 64 65 66 67 68
  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.

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 T1 S1  closed T2 S2 
  T1  T2    S1  S2    closed (T1  T2) (S1  S2).
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 100 101 102 103
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.
104 105 106
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
107
Proof. by intros T1 T2 HT S1 S2 HS; rewrite /up_set HS HT. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
108 109
Lemma elem_of_up s T : s  up T s.
Proof. constructor. Qed.
110
Lemma subseteq_up_set S T : S  up_set T S.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
112 113
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
114
Proof.
115
  intros HS Hne; unfold up_set; split.
116
  * assert ( s, s  up T s) by eauto using elem_of_up. solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
  * intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
118
    specialize (HS s' Hs'); clear Hs' Hne S.
Robbert Krebbers's avatar
Robbert Krebbers committed
119 120 121 122 123
    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.
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 T (up T s).
Robbert Krebbers's avatar
Robbert Krebbers committed
127
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
  intros; rewrite -(collection_bind_singleton (up T) s).
129
  apply closed_up_set; solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
130 131 132 133 134
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.
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.
139
Global Instance sts_dra : DRA (sts R tok).
Robbert Krebbers's avatar
Robbert Krebbers committed
140 141 142 143 144 145 146 147
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,
148
      closed T S  s  S  tok s  T'    tok s  (T  T')  ).
149
    { intros S T T' s [??]; solve_elem_of. }
Robbert Krebbers's avatar
Robbert Krebbers committed
150
    destruct 3; simpl in *; auto using closed_op with sts.
151
  * intros []; simpl; eauto using closed_up, closed_up_set, closed_ne with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
152 153
  * 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
154
    eapply closed_up_set; eauto 2 using closed_disjoint with sts.
155
  * intros [] [] []; constructor; rewrite ?assoc; auto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
156 157 158 159
  * 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.
160 161
  * 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.
162
    solve_elem_of.
Robbert Krebbers's avatar
Robbert Krebbers committed
163
  * intros [|S T]; constructor; auto with sts.
164
    assert (S  up_set  S); auto using subseteq_up_set with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
165
  * intros [s T|S T]; constructor; auto with sts.
Robbert Krebbers's avatar
Robbert Krebbers committed
166 167 168
    + rewrite (up_closed (up _ _)); auto using closed_up with sts.
    + rewrite (up_closed (up_set _ _));
        eauto using closed_up_set, closed_ne with sts.
169
  * intros x y ?? (z&Hy&?&Hxz); exists (unit (x  y)); split_ands.
170
    + destruct Hxz;inversion_clear Hy;constructor;unfold up_set; solve_elem_of.
171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186
    + 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
187 188
  * 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
189
      rewrite ?disjoint_union_difference; auto.
190
    split; [|apply intersection_greatest; auto using subseteq_up_set with sts].
Robbert Krebbers's avatar
Robbert Krebbers committed
191 192 193 194
    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
195 196
Qed.
Lemma step_closed s1 s2 T1 T2 S Tf :
197 198
  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
199
Proof.
200
  inversion_clear 1 as [???? HR Hs1 Hs2]; intros [?? Hstep]??; split_ands; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
201
  * eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
202
  * solve_elem_of -Hstep Hs1 Hs2.
Robbert Krebbers's avatar
Robbert Krebbers committed
203 204 205 206
Qed.
End sts_core.
End sts.

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

210 211 212
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).
Robbert Krebbers's avatar
Robbert Krebbers committed
213
Lemma sts_update s1 s2 T1 T2 :
214
  sts.step R tok (s1,T1) (s2,T2)  sts_auth s1 T1 ~~> sts_auth s2 T2.
Robbert Krebbers's avatar
Robbert Krebbers committed
215
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
216
  intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
217
  destruct (sts.step_closed R tok s1 s2 T1 T2 S Tf) as (?&?&?); auto.
218
  repeat (done || constructor).
Robbert Krebbers's avatar
Robbert Krebbers committed
219
Qed.
220
End stsRA.