sts.v 9.84 KB
 Robbert Krebbers committed Nov 16, 2015 1 ``````Require Export iris.ra. `````` Robbert Krebbers committed Nov 17, 2015 2 ``````Require Import prelude.sets prelude.bsets iris.dra. `````` Robbert Krebbers committed Nov 11, 2015 3 4 5 6 7 ``````Local Arguments valid _ _ !_ /. Local Arguments op _ _ !_ !_ /. Local Arguments unit _ _ !_ /. Module sts. `````` Robbert Krebbers committed Nov 17, 2015 8 9 10 ``````Inductive t {A B} (R : relation A) (tok : A → bset B) := | auth : A → bset B → t R tok | frag : set A → bset B → t R tok. `````` Robbert Krebbers committed Nov 16, 2015 11 12 ``````Arguments auth {_ _ _ _} _ _. Arguments frag {_ _ _ _} _ _. `````` Robbert Krebbers committed Nov 11, 2015 13 14 `````` Section sts_core. `````` Robbert Krebbers committed Nov 16, 2015 15 ``````Context {A B : Type} `{∀ x y : B, Decision (x = y)}. `````` Robbert Krebbers committed Nov 17, 2015 16 ``````Context (R : relation A) (tok : A → bset B). `````` Robbert Krebbers committed Nov 11, 2015 17 18 `````` Inductive sts_equiv : Equiv (t R tok) := `````` Robbert Krebbers committed Nov 16, 2015 19 20 `````` | 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 committed Nov 11, 2015 21 ``````Global Existing Instance sts_equiv. `````` Robbert Krebbers committed Nov 17, 2015 22 ``````Inductive step : relation (A * bset B) := `````` Robbert Krebbers committed Nov 11, 2015 23 `````` | Step s1 s2 T1 T2 : `````` Robbert Krebbers committed Nov 16, 2015 24 `````` R s1 s2 → tok s1 ∩ T1 ≡ ∅ → tok s2 ∩ T2 ≡ ∅ → tok s1 ∪ T1 ≡ tok s2 ∪ T2 → `````` Robbert Krebbers committed Nov 11, 2015 25 26 `````` step (s1,T1) (s2,T2). Hint Resolve Step. `````` Robbert Krebbers committed Nov 17, 2015 27 ``````Inductive frame_step (T : bset B) (s1 s2 : A) : Prop := `````` Robbert Krebbers committed Nov 11, 2015 28 `````` | Frame_step T1 T2 : `````` Robbert Krebbers committed Nov 16, 2015 29 `````` T1 ∩ (tok s1 ∪ T) ≡ ∅ → step (s1,T1) (s2,T2) → frame_step T s1 s2. `````` Robbert Krebbers committed Nov 11, 2015 30 ``````Hint Resolve Frame_step. `````` Robbert Krebbers committed Nov 17, 2015 31 ``````Record closed (T : bset B) (S : set A) : Prop := Closed { `````` Robbert Krebbers committed Nov 16, 2015 32 `````` closed_disjoint s : s ∈ S → tok s ∩ T ≡ ∅; `````` Robbert Krebbers committed Nov 11, 2015 33 34 35 36 37 38 `````` 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. Global Instance sts_valid : Valid (t R tok) := λ x, `````` Robbert Krebbers committed Nov 16, 2015 39 `````` match x with auth s T => tok s ∩ T ≡ ∅ | frag S' T => closed T S' end. `````` Robbert Krebbers committed Nov 17, 2015 40 41 ``````Definition up (T : bset B) (s : A) : set A := mkSet (rtc (frame_step T) s). Definition up_set (T : bset B) (S : set A) : set A := S ≫= up T. `````` Robbert Krebbers committed Nov 11, 2015 42 43 44 45 46 ``````Global Instance sts_unit : Unit (t R tok) := λ x, match x with | frag S' _ => frag (up_set ∅ S') ∅ | auth s _ => frag (up ∅ s) ∅ end. Inductive sts_disjoint : Disjoint (t R tok) := `````` Robbert Krebbers committed Nov 16, 2015 47 48 49 `````` | frag_frag_disjoint S1 S2 T1 T2 : 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. `````` Robbert Krebbers committed Nov 11, 2015 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 ``````Global Existing Instance sts_disjoint. Global Instance sts_op : Op (t R tok) := λ 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. Inductive sts_included : Included (t R tok) := | frag_frag_included S1 S2 T1 T2 S' : T1 ⊆ T2 → S2 ≡ S1 ∩ S' → closed (T2 ∖ T1) S' → frag S1 T1 ≼ frag S2 T2 | frag_auth_included s S T1 T2 : s ∈ S → T1 ⊆ T2 → frag S T1 ≼ auth s T2 | auth_auth_included s T1 T2 : T1 ⊆ T2 → auth s T1 ≼ auth s T2. Global Existing Instance sts_included. Global Instance sts_minus : Minus (t R tok) := λ x1 x2, 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. `````` Robbert Krebbers committed Nov 16, 2015 72 ``````Hint Extern 5 (equiv (A:=set _) _ _) => esolve_elem_of : sts. `````` Robbert Krebbers committed Nov 17, 2015 73 ``````Hint Extern 5 (equiv (A:=bset _) _ _) => esolve_elem_of : sts. `````` Robbert Krebbers committed Nov 11, 2015 74 75 76 77 78 79 80 81 82 ``````Hint Extern 5 (_ ∈ _) => esolve_elem_of : sts. Hint Extern 5 (_ ⊆ _) => esolve_elem_of : sts. Instance: Equivalence ((≡) : relation (t R tok)). Proof. split. * by intros []; constructor. * by destruct 1; constructor. * destruct 1; inversion_clear 1; constructor; etransitivity; eauto. Qed. `````` Robbert Krebbers committed Nov 16, 2015 83 84 85 ``````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 committed Nov 11, 2015 86 ``````Proof. `````` Robbert Krebbers committed Nov 16, 2015 87 88 `````` intros ?? HT ?? HS; destruct 1; constructor; intros until 0; rewrite <-?HS, <-?HT; eauto. `````` Robbert Krebbers committed Nov 11, 2015 89 ``````Qed. `````` Robbert Krebbers committed Nov 16, 2015 90 91 ``````Instance closed_proper : Proper ((≡) ==> (≡) ==> iff) closed. Proof. by split; apply closed_proper'. Qed. `````` Robbert Krebbers committed Nov 11, 2015 92 ``````Lemma closed_op T1 T2 S1 S2 : `````` Robbert Krebbers committed Nov 16, 2015 93 `````` closed T1 S1 → closed T2 S2 → T1 ∩ T2 ≡ ∅ → closed (T1 ∪ T2) (S1 ∩ S2). `````` Robbert Krebbers committed Nov 11, 2015 94 95 96 97 98 99 100 101 102 ``````Proof. intros [? Hstep1] [? Hstep2] ?; split; [esolve_elem_of|]. intros s3 s4; rewrite !elem_of_intersection; intros [??] [T ??]; split. * apply Hstep1 with s3; eauto with sts. * apply Hstep2 with s3; eauto with sts. Qed. Lemma closed_all : closed ∅ set_all. Proof. split; auto with sts. Qed. Hint Resolve closed_all : sts. `````` Robbert Krebbers committed Nov 16, 2015 103 ``````Instance up_preserving : Proper (flip (⊆) ==> (=) ==> (⊆)) up. `````` Robbert Krebbers committed Nov 11, 2015 104 105 106 107 108 ``````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. `````` Robbert Krebbers committed Nov 16, 2015 109 110 111 112 ``````Instance up_proper : Proper ((≡) ==> (=) ==> (≡)) up. Proof. by intros ?? [??] ???; split; apply up_preserving. Qed. Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set. Proof. by intros T1 T2 HT S1 S2 HS; unfold up_set; rewrite HS, HT. Qed. `````` Robbert Krebbers committed Nov 11, 2015 113 114 115 116 ``````Lemma elem_of_up s T : s ∈ up T s. Proof. constructor. Qed. Lemma subseteq_up_set S T : S ⊆ up_set T S. Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed. `````` Robbert Krebbers committed Nov 16, 2015 117 ``````Lemma closed_up_set S T : (∀ s, s ∈ S → tok s ∩ T ≡ ∅) → closed T (up_set T S). `````` Robbert Krebbers committed Nov 11, 2015 118 119 120 121 122 123 124 125 126 127 128 ``````Proof. intros HS; unfold up_set; split. * intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs'). specialize (HS s' Hs'); clear Hs' S. 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. Lemma closed_up_set_empty S : closed ∅ (up_set ∅ S). Proof. eauto using closed_up_set with sts. Qed. `````` Robbert Krebbers committed Nov 16, 2015 129 ``````Lemma closed_up s T : tok s ∩ T ≡ ∅ → closed T (up T s). `````` Robbert Krebbers committed Nov 11, 2015 130 ``````Proof. `````` Robbert Krebbers committed Nov 16, 2015 131 `````` intros; rewrite <-(collection_bind_singleton (up T) s). `````` Robbert Krebbers committed Nov 11, 2015 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 `````` apply closed_up_set; auto with sts. 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. intros; split; auto using subseteq_up_set; intros s. unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?). induction Hstep; eauto using closed_step. Qed. Lemma up_set_subseteq T1 T2 S1 S2 : closed (T2 ∖ T1) S2 → up_set (T2 ∖ T1) (S1 ∩ S2) ⊆ S2. Proof. intros ? s2; unfold up_set; rewrite elem_of_bind; intros (s1&?&?). apply closed_steps with (T2 ∖ T1) s1; auto with sts. Qed. Global Instance sts_dra : DRA (t R tok). 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. * by do 2 destruct 1; inversion_clear 1; econstructor; setoid_subst. * assert (∀ T T' S s, `````` Robbert Krebbers committed Nov 16, 2015 158 `````` closed T S → s ∈ S → tok s ∩ T' ≡ ∅ → tok s ∩ (T ∪ T') ≡ ∅). `````` Robbert Krebbers committed Nov 11, 2015 159 160 161 162 163 `````` { intros S T T' s [??]; esolve_elem_of. } destruct 3; simpl in *; auto using closed_op with sts. * intros []; simpl; eauto using closed_up, closed_up_set with sts. * destruct 3; simpl in *; setoid_subst; eauto using closed_up with sts. eapply closed_up_set; eauto 2 using closed_disjoint with sts. `````` Robbert Krebbers committed Nov 16, 2015 164 `````` * intros [] [] []; constructor; rewrite ?(associative _); auto with sts. `````` Robbert Krebbers committed Nov 11, 2015 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 `````` * 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 []; constructor; auto using elem_of_up with sts. * intros [|S T]; constructor; auto with sts. assert (S ⊆ up_set ∅ S); auto using subseteq_up_set with sts. * intros [s T|S T]; constructor; auto with sts. + by rewrite (up_closed (up _ _)) by auto using closed_up with sts. + by rewrite (up_closed (up_set _ _)) by auto using closed_up_set with sts. * destruct 3 as [S1 S2| |]; simpl; match goal with |- _ ≼ frag ?S _ => apply frag_frag_included with S end; eauto using closed_up_empty, closed_up_set_empty; unfold up_set; esolve_elem_of. * destruct 3 as [S1 S2 T1 T2| |]; econstructor; eauto with sts. `````` Robbert Krebbers committed Nov 16, 2015 180 `````` by setoid_replace ((T1 ∪ T2) ∖ T1) with T2 by esolve_elem_of. `````` Robbert Krebbers committed Nov 11, 2015 181 182 `````` * destruct 3; constructor; eauto using elem_of_up with sts. * destruct 3 as [S1 S2 T1 T2 S'| |]; constructor; `````` Robbert Krebbers committed Nov 16, 2015 183 `````` rewrite ?(commutative _ (_ ∖ _)), <-?union_difference; auto with sts. `````` Robbert Krebbers committed Nov 11, 2015 184 185 186 187 188 `````` assert (S2 ⊆ up_set (T2 ∖ T1) S2) by eauto using subseteq_up_set. assert (up_set (T2 ∖ T1) (S1 ∩ S') ⊆ S') by eauto using up_set_subseteq. esolve_elem_of. Qed. Lemma step_closed s1 s2 T1 T2 S Tf : `````` Robbert Krebbers committed Nov 16, 2015 189 190 `````` step (s1,T1) (s2,T2) → closed Tf S → s1 ∈ S → T1 ∩ Tf ≡ ∅ → s2 ∈ S ∧ T2 ∩ Tf ≡ ∅ ∧ tok s2 ∩ T2 ≡ ∅. `````` Robbert Krebbers committed Nov 11, 2015 191 192 193 194 195 196 197 198 199 ``````Proof. inversion_clear 1 as [???? HR Hs1 Hs2]; intros [? Hstep] ??; split_ands; auto. * eapply Hstep with s1, Frame_step with T1 T2; auto with sts. * clear Hstep Hs1 Hs2; esolve_elem_of. Qed. End sts_core. End sts. Section sts_ra. `````` Robbert Krebbers committed Nov 16, 2015 200 ``````Context {A B : Type} `{∀ x y : B, Decision (x = y)}. `````` Robbert Krebbers committed Nov 17, 2015 201 ``````Context (R : relation A) (tok : A → bset B). `````` Robbert Krebbers committed Nov 11, 2015 202 203 204 205 206 207 208 `````` Definition sts := validity (valid : sts.t R tok → Prop). Global Instance sts_unit : Unit sts := validity_unit _. Global Instance sts_op : Op sts := validity_op _. Global Instance sts_included : Included sts := validity_included _. Global Instance sts_minus : Minus sts := validity_minus _. Global Instance sts_ra : RA sts := validity_ra _. `````` Robbert Krebbers committed Nov 17, 2015 209 210 ``````Definition sts_auth (s : A) (T : bset B) : sts := to_validity (sts.auth s T). Definition sts_frag (S : set A) (T : bset B) : sts := `````` Robbert Krebbers committed Nov 11, 2015 211 212 213 214 215 216 `````` to_validity (sts.frag S T). Lemma sts_update s1 s2 T1 T2 : sts.step R tok (s1,T1) (s2,T2) → sts_auth s1 T1 ⇝ sts_auth s2 T2. Proof. intros ?; apply dra_update; inversion 3 as [|? S ? Tf|]; subst. destruct (sts.step_closed R tok s1 s2 T1 T2 S Tf) as (?&?&?); auto. `````` Robbert Krebbers committed Nov 16, 2015 217 `````` repeat (done || constructor). `````` Robbert Krebbers committed Nov 11, 2015 218 219 ``````Qed. End sts_ra.``````