sts.v 9.84 KB
 Robbert Krebbers committed Feb 04, 2016 1 2 ``````Require Export algebra.cmra. Require Import prelude.sets algebra.dra. `````` Robbert Krebbers committed Nov 11, 2015 3 4 5 6 ``````Local Arguments valid _ _ !_ /. Local Arguments op _ _ !_ !_ /. Local Arguments unit _ _ !_ /. `````` Robbert Krebbers committed Feb 01, 2016 7 8 9 ``````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. `````` Robbert Krebbers committed Nov 16, 2015 10 11 ``````Arguments auth {_ _ _ _} _ _. Arguments frag {_ _ _ _} _ _. `````` Robbert Krebbers committed Nov 11, 2015 12 `````` `````` Robbert Krebbers committed Feb 01, 2016 13 ``````Module sts. `````` Robbert Krebbers committed Nov 11, 2015 14 ``````Section sts_core. `````` Robbert Krebbers committed Nov 20, 2015 15 16 ``````Context {A B : Type} (R : relation A) (tok : A → set B). Infix "≼" := dra_included. `````` Robbert Krebbers committed Nov 11, 2015 17 `````` `````` Robbert Krebbers committed Feb 01, 2016 18 ``````Inductive sts_equiv : Equiv (sts 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 20, 2015 22 ``````Inductive step : relation (A * set 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 20, 2015 27 ``````Inductive frame_step (T : set 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 20, 2015 31 ``````Record closed (T : set B) (S : set A) : Prop := Closed { `````` Robbert Krebbers committed Dec 08, 2015 32 `````` closed_ne : S ≢ ∅; `````` Robbert Krebbers committed Nov 16, 2015 33 `````` closed_disjoint s : s ∈ S → tok s ∩ T ≡ ∅; `````` Robbert Krebbers committed Nov 11, 2015 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. `````` Robbert Krebbers committed Feb 01, 2016 39 ``````Global Instance sts_valid : Valid (sts R tok) := λ x, `````` Robbert Krebbers committed Nov 16, 2015 40 `````` match x with auth s T => tok s ∩ T ≡ ∅ | frag S' T => closed T S' end. `````` Robbert Krebbers committed Nov 20, 2015 41 42 ``````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. `````` Robbert Krebbers committed Feb 01, 2016 43 ``````Global Instance sts_unit : Unit (sts R tok) := λ x, `````` Robbert Krebbers committed Nov 11, 2015 44 45 46 `````` match x with | frag S' _ => frag (up_set ∅ S') ∅ | auth s _ => frag (up ∅ s) ∅ end. `````` Robbert Krebbers committed Feb 01, 2016 47 ``````Inductive sts_disjoint : Disjoint (sts R tok) := `````` Robbert Krebbers committed Dec 08, 2015 48 49 `````` | frag_frag_disjoint S1 S2 T1 T2 : S1 ∩ S2 ≢ ∅ → T1 ∩ T2 ≡ ∅ → frag S1 T1 ⊥ frag S2 T2 `````` Robbert Krebbers committed Nov 16, 2015 50 51 `````` | 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 52 ``````Global Existing Instance sts_disjoint. `````` Robbert Krebbers committed Feb 01, 2016 53 ``````Global Instance sts_op : Op (sts R tok) := λ x1 x2, `````` Robbert Krebbers committed Nov 11, 2015 54 55 56 57 58 59 `````` 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. `````` Robbert Krebbers committed Feb 01, 2016 60 ``````Global Instance sts_minus : Minus (sts R tok) := λ x1 x2, `````` Robbert Krebbers committed Nov 11, 2015 61 62 63 64 65 66 67 `````` 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 Jan 16, 2016 68 69 70 71 ``````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. `````` Robbert Krebbers committed Feb 01, 2016 72 ``````Instance: Equivalence ((≡) : relation (sts R tok)). `````` Robbert Krebbers committed Nov 11, 2015 73 74 75 76 77 78 ``````Proof. split. * by intros []; constructor. * by destruct 1; constructor. * destruct 1; inversion_clear 1; constructor; etransitivity; eauto. Qed. `````` Robbert Krebbers committed Nov 16, 2015 79 80 81 ``````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 82 ``````Proof. `````` Robbert Krebbers committed Nov 16, 2015 83 `````` intros ?? HT ?? HS; destruct 1; `````` Robbert Krebbers committed Jan 13, 2016 84 `````` constructor; intros until 0; rewrite -?HS -?HT; eauto. `````` Robbert Krebbers committed Nov 11, 2015 85 ``````Qed. `````` Robbert Krebbers committed Nov 16, 2015 86 87 ``````Instance closed_proper : Proper ((≡) ==> (≡) ==> iff) closed. Proof. by split; apply closed_proper'. Qed. `````` Robbert Krebbers committed Nov 11, 2015 88 ``````Lemma closed_op T1 T2 S1 S2 : `````` Robbert Krebbers committed Dec 08, 2015 89 90 `````` closed T1 S1 → closed T2 S2 → T1 ∩ T2 ≡ ∅ → S1 ∩ S2 ≢ ∅ → closed (T1 ∪ T2) (S1 ∩ S2). `````` Robbert Krebbers committed Nov 11, 2015 91 ``````Proof. `````` Robbert Krebbers committed Jan 16, 2016 92 `````` intros [_ ? Hstep1] [_ ? Hstep2] ?; split; [done|solve_elem_of|]. `````` Robbert Krebbers committed Dec 08, 2015 93 94 95 `````` 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 committed Nov 11, 2015 96 ``````Qed. `````` Robbert Krebbers committed Nov 16, 2015 97 ``````Instance up_preserving : Proper (flip (⊆) ==> (=) ==> (⊆)) up. `````` Robbert Krebbers committed Nov 11, 2015 98 99 100 101 102 ``````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 103 104 105 ``````Instance up_proper : Proper ((≡) ==> (=) ==> (≡)) up. Proof. by intros ?? [??] ???; split; apply up_preserving. Qed. Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set. `````` Robbert Krebbers committed Jan 13, 2016 106 ``````Proof. by intros T1 T2 HT S1 S2 HS; rewrite /up_set HS HT. Qed. `````` Robbert Krebbers committed Nov 11, 2015 107 108 ``````Lemma elem_of_up s T : s ∈ up T s. Proof. constructor. Qed. `````` Robbert Krebbers committed Dec 08, 2015 109 ``````Lemma subseteq_up_set S T : S ⊆ up_set T S. `````` Robbert Krebbers committed Nov 11, 2015 110 ``````Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed. `````` Robbert Krebbers committed Dec 08, 2015 111 112 ``````Lemma closed_up_set S T : (∀ s, s ∈ S → tok s ∩ T ≡ ∅) → S ≢ ∅ → closed T (up_set T S). `````` Robbert Krebbers committed Nov 11, 2015 113 ``````Proof. `````` Robbert Krebbers committed Dec 08, 2015 114 `````` intros HS Hne; unfold up_set; split. `````` Robbert Krebbers committed Jan 16, 2016 115 `````` * assert (∀ s, s ∈ up T s) by eauto using elem_of_up. solve_elem_of. `````` Robbert Krebbers committed Nov 11, 2015 116 `````` * intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs'). `````` Robbert Krebbers committed Dec 08, 2015 117 `````` specialize (HS s' Hs'); clear Hs' Hne S. `````` Robbert Krebbers committed Nov 11, 2015 118 119 120 121 122 `````` 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. `````` Robbert Krebbers committed Dec 08, 2015 123 ``````Lemma closed_up_set_empty S : S ≢ ∅ → closed ∅ (up_set ∅ S). `````` Robbert Krebbers committed Nov 11, 2015 124 ``````Proof. eauto using closed_up_set with sts. Qed. `````` Robbert Krebbers committed Nov 16, 2015 125 ``````Lemma closed_up s T : tok s ∩ T ≡ ∅ → closed T (up T s). `````` Robbert Krebbers committed Nov 11, 2015 126 ``````Proof. `````` Robbert Krebbers committed Jan 13, 2016 127 `````` intros; rewrite -(collection_bind_singleton (up T) s). `````` Robbert Krebbers committed Jan 16, 2016 128 `````` apply closed_up_set; solve_elem_of. `````` Robbert Krebbers committed Nov 11, 2015 129 130 131 132 133 ``````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. `````` Robbert Krebbers committed Dec 08, 2015 134 `````` intros; split; auto using subseteq_up_set; intros s. `````` Robbert Krebbers committed Nov 11, 2015 135 136 137 `````` unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?). induction Hstep; eauto using closed_step. Qed. `````` Robbert Krebbers committed Feb 01, 2016 138 ``````Global Instance sts_dra : DRA (sts R tok). `````` Robbert Krebbers committed Nov 11, 2015 139 140 141 142 143 144 145 146 ``````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, `````` Robbert Krebbers committed Nov 16, 2015 147 `````` closed T S → s ∈ S → tok s ∩ T' ≡ ∅ → tok s ∩ (T ∪ T') ≡ ∅). `````` Robbert Krebbers committed Jan 16, 2016 148 `````` { intros S T T' s [??]; solve_elem_of. } `````` Robbert Krebbers committed Nov 11, 2015 149 `````` destruct 3; simpl in *; auto using closed_op with sts. `````` Robbert Krebbers committed Dec 08, 2015 150 `````` * intros []; simpl; eauto using closed_up, closed_up_set, closed_ne with sts. `````` Robbert Krebbers committed Nov 20, 2015 151 152 `````` * intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy;clear Hy; setoid_subst; rewrite ?disjoint_union_difference; auto using closed_up with sts. `````` Robbert Krebbers committed Nov 11, 2015 153 `````` eapply closed_up_set; eauto 2 using closed_disjoint with sts. `````` Robbert Krebbers committed Nov 16, 2015 154 `````` * intros [] [] []; constructor; rewrite ?(associative _); auto with sts. `````` Robbert Krebbers committed Nov 11, 2015 155 156 157 158 `````` * 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. `````` Robbert Krebbers committed Dec 08, 2015 159 160 `````` * 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. `````` Robbert Krebbers committed Jan 16, 2016 161 `````` solve_elem_of. `````` Robbert Krebbers committed Nov 11, 2015 162 `````` * intros [|S T]; constructor; auto with sts. `````` Robbert Krebbers committed Dec 08, 2015 163 `````` assert (S ⊆ up_set ∅ S); auto using subseteq_up_set with sts. `````` Robbert Krebbers committed Nov 11, 2015 164 `````` * intros [s T|S T]; constructor; auto with sts. `````` Robbert Krebbers committed Jan 13, 2016 165 166 167 `````` + rewrite (up_closed (up _ _)); auto using closed_up with sts. + rewrite (up_closed (up_set _ _)); eauto using closed_up_set, closed_ne with sts. `````` Robbert Krebbers committed Dec 08, 2015 168 `````` * intros x y ?? (z&Hy&?&Hxz); exists (unit (x ⋅ y)); split_ands. `````` Robbert Krebbers committed Jan 16, 2016 169 `````` + destruct Hxz;inversion_clear Hy;constructor;unfold up_set; solve_elem_of. `````` Robbert Krebbers committed Dec 08, 2015 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 `````` + 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 committed Nov 20, 2015 186 187 `````` * intros x y ?? (z&Hy&?&Hxz); destruct Hxz as [S1 S2 T1 T2| |]; inversion Hy; clear Hy; constructor; setoid_subst; `````` Robbert Krebbers committed Jan 13, 2016 188 `````` rewrite ?disjoint_union_difference; auto. `````` Robbert Krebbers committed Dec 08, 2015 189 `````` split; [|apply intersection_greatest; auto using subseteq_up_set with sts]. `````` Robbert Krebbers committed Nov 20, 2015 190 191 192 193 `````` 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 committed Nov 11, 2015 194 195 ``````Qed. Lemma step_closed s1 s2 T1 T2 S Tf : `````` Robbert Krebbers committed Nov 16, 2015 196 197 `````` 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 198 ``````Proof. `````` Robbert Krebbers committed Dec 08, 2015 199 `````` inversion_clear 1 as [???? HR Hs1 Hs2]; intros [?? Hstep]??; split_ands; auto. `````` Robbert Krebbers committed Nov 11, 2015 200 `````` * eapply Hstep with s1, Frame_step with T1 T2; auto with sts. `````` Robbert Krebbers committed Jan 16, 2016 201 `````` * solve_elem_of -Hstep Hs1 Hs2. `````` Robbert Krebbers committed Nov 11, 2015 202 203 204 205 ``````Qed. End sts_core. End sts. `````` Robbert Krebbers committed Feb 01, 2016 206 ``````Section stsRA. `````` Robbert Krebbers committed Nov 22, 2015 207 ``````Context {A B : Type} (R : relation A) (tok : A → set B). `````` Robbert Krebbers committed Nov 11, 2015 208 `````` `````` Robbert Krebbers committed Feb 01, 2016 209 210 211 ``````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 committed Nov 11, 2015 212 ``````Lemma sts_update s1 s2 T1 T2 : `````` Ralf Jung committed Feb 03, 2016 213 `````` sts.step R tok (s1,T1) (s2,T2) → sts_auth s1 T1 ~~> sts_auth s2 T2. `````` Robbert Krebbers committed Nov 11, 2015 214 ``````Proof. `````` Robbert Krebbers committed Nov 22, 2015 215 `````` intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst. `````` Robbert Krebbers committed Nov 11, 2015 216 `````` 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 ``````Qed. `````` Robbert Krebbers committed Feb 01, 2016 219 ``End stsRA.``