sts.v 13.1 KB
 1 ``````From prelude Require Export sets. `````` Robbert Krebbers committed Feb 13, 2016 2 3 ``````From algebra Require Export cmra. From algebra Require Import dra. `````` Robbert Krebbers committed Nov 11, 2015 4 5 6 7 ``````Local Arguments valid _ _ !_ /. Local Arguments op _ _ !_ !_ /. Local Arguments unit _ _ !_ /. `````` Robbert Krebbers committed Feb 01, 2016 8 ``````Module sts. `````` Ralf Jung committed Feb 15, 2016 9 `````` `````` Robbert Krebbers committed Feb 16, 2016 10 ``````Record stsT := STS { `````` Ralf Jung committed Feb 15, 2016 11 12 13 14 15 `````` state : Type; token : Type; trans : relation state; tok : state → set token; }. `````` Ralf Jung committed Feb 16, 2016 16 ``````Arguments STS {_ _} _ _. `````` Ralf Jung committed Feb 15, 2016 17 18 19 `````` (* The type of bounds we can give to the state of an STS. This is the type that we equip with an RA structure. *) `````` Robbert Krebbers committed Feb 16, 2016 20 ``````Inductive bound (sts : stsT) := `````` Ralf Jung committed Feb 15, 2016 21 22 23 24 25 `````` | bound_auth : state sts → set (token sts) → bound sts | bound_frag : set (state sts) → set (token sts )→ bound sts. Arguments bound_auth {_} _ _. Arguments bound_frag {_} _ _. `````` Robbert Krebbers committed Nov 11, 2015 26 ``````Section sts_core. `````` Robbert Krebbers committed Feb 16, 2016 27 ``````Context (sts : stsT). `````` Robbert Krebbers committed Nov 20, 2015 28 ``````Infix "≼" := dra_included. `````` Robbert Krebbers committed Nov 11, 2015 29 `````` `````` Ralf Jung committed Feb 15, 2016 30 31 32 33 34 35 36 37 38 39 40 ``````Notation state := (state sts). Notation token := (token sts). Notation trans := (trans sts). Notation tok := (tok sts). Inductive equiv : Equiv (bound sts) := | auth_equiv s T1 T2 : T1 ≡ T2 → bound_auth s T1 ≡ bound_auth s T2 | frag_equiv S1 S2 T1 T2 : T1 ≡ T2 → S1 ≡ S2 → bound_frag S1 T1 ≡ bound_frag S2 T2. Global Existing Instance equiv. Inductive step : relation (state * set token) := `````` Robbert Krebbers committed Nov 11, 2015 41 `````` | Step s1 s2 T1 T2 : `````` Ralf Jung committed Feb 15, 2016 42 43 `````` trans s1 s2 → tok s1 ∩ T1 ≡ ∅ → tok s2 ∩ T2 ≡ ∅ → tok s1 ∪ T1 ≡ tok s2 ∪ T2 → step (s1,T1) (s2,T2). `````` Robbert Krebbers committed Nov 11, 2015 44 ``````Hint Resolve Step. `````` Ralf Jung committed Feb 15, 2016 45 ``````Inductive frame_step (T : set token) (s1 s2 : state) : Prop := `````` Robbert Krebbers committed Nov 11, 2015 46 `````` | Frame_step T1 T2 : `````` Robbert Krebbers committed Nov 16, 2015 47 `````` T1 ∩ (tok s1 ∪ T) ≡ ∅ → step (s1,T1) (s2,T2) → frame_step T s1 s2. `````` Robbert Krebbers committed Nov 11, 2015 48 ``````Hint Resolve Frame_step. `````` Ralf Jung committed Feb 15, 2016 49 ``````Record closed (S : set state) (T : set token) : Prop := Closed { `````` Robbert Krebbers committed Dec 08, 2015 50 `````` closed_ne : S ≢ ∅; `````` Robbert Krebbers committed Nov 16, 2015 51 `````` closed_disjoint s : s ∈ S → tok s ∩ T ≡ ∅; `````` Robbert Krebbers committed Nov 11, 2015 52 53 54 `````` closed_step s1 s2 : s1 ∈ S → frame_step T s1 s2 → s2 ∈ S }. Lemma closed_steps S T s1 s2 : `````` 55 `````` closed S T → s1 ∈ S → rtc (frame_step T) s1 s2 → s2 ∈ S. `````` Robbert Krebbers committed Nov 11, 2015 56 ``````Proof. induction 3; eauto using closed_step. Qed. `````` Ralf Jung committed Feb 15, 2016 57 ``````Global Instance valid : Valid (bound sts) := λ x, `````` Robbert Krebbers committed Nov 11, 2015 58 `````` match x with `````` Ralf Jung committed Feb 15, 2016 59 `````` | bound_auth s T => tok s ∩ T ≡ ∅ | bound_frag S' T => closed S' T `````` Robbert Krebbers committed Nov 11, 2015 60 `````` end. `````` Ralf Jung committed Feb 15, 2016 61 62 ``````Definition up (s : state) (T : set token) : set state := mkSet (rtc (frame_step T) s). `````` Robbert Krebbers committed Feb 16, 2016 63 64 ``````Definition up_set (S : set state) (T : set token) : set state := S ≫= λ s, up s T. `````` Ralf Jung committed Feb 15, 2016 65 66 67 68 69 70 ``````Global Instance unit : Unit (bound sts) := λ x, match x with | bound_frag S' _ => bound_frag (up_set S' ∅ ) ∅ | bound_auth s _ => bound_frag (up s ∅) ∅ end. Inductive disjoint : Disjoint (bound sts) := `````` Robbert Krebbers committed Dec 08, 2015 71 `````` | frag_frag_disjoint S1 S2 T1 T2 : `````` Ralf Jung committed Feb 15, 2016 72 73 74 75 76 77 78 `````` S1 ∩ S2 ≢ ∅ → T1 ∩ T2 ≡ ∅ → bound_frag S1 T1 ⊥ bound_frag S2 T2 | auth_frag_disjoint s S T1 T2 : s ∈ S → T1 ∩ T2 ≡ ∅ → bound_auth s T1 ⊥ bound_frag S T2 | frag_auth_disjoint s S T1 T2 : s ∈ S → T1 ∩ T2 ≡ ∅ → bound_frag S T1 ⊥ bound_auth s T2. Global Existing Instance disjoint. Global Instance op : Op (bound sts) := λ x1 x2, `````` Robbert Krebbers committed Nov 11, 2015 79 `````` match x1, x2 with `````` Ralf Jung committed Feb 15, 2016 80 81 82 83 84 `````` | bound_frag S1 T1, bound_frag S2 T2 => bound_frag (S1 ∩ S2) (T1 ∪ T2) | bound_auth s T1, bound_frag _ T2 => bound_auth s (T1 ∪ T2) | bound_frag _ T1, bound_auth s T2 => bound_auth s (T1 ∪ T2) | bound_auth s T1, bound_auth _ T2 => bound_auth s (T1 ∪ T2)(* never happens *) `````` Robbert Krebbers committed Nov 11, 2015 85 `````` end. `````` Ralf Jung committed Feb 15, 2016 86 ``````Global Instance minus : Minus (bound sts) := λ x1 x2, `````` Robbert Krebbers committed Nov 11, 2015 87 `````` match x1, x2 with `````` Ralf Jung committed Feb 15, 2016 88 89 90 91 92 93 `````` | bound_frag S1 T1, bound_frag S2 T2 => bound_frag (up_set S1 (T1 ∖ T2)) (T1 ∖ T2) | bound_auth s T1, bound_frag _ T2 => bound_auth s (T1 ∖ T2) | bound_frag _ T2, bound_auth s T1 => bound_auth s (T1 ∖ T2) (* never happens *) | bound_auth s T1, bound_auth _ T2 => bound_frag (up s (T1 ∖ T2)) (T1 ∖ T2) `````` Robbert Krebbers committed Nov 11, 2015 94 95 `````` end. `````` Ralf Jung committed Feb 15, 2016 96 97 ``````Hint Extern 10 (base.equiv (A:=set _) _ _) => solve_elem_of : sts. Hint Extern 10 (¬(base.equiv (A:=set _) _ _)) => solve_elem_of : sts. `````` Robbert Krebbers committed Jan 16, 2016 98 99 ``````Hint Extern 10 (_ ∈ _) => solve_elem_of : sts. Hint Extern 10 (_ ⊆ _) => solve_elem_of : sts. `````` Ralf Jung committed Feb 15, 2016 100 ``````Instance: Equivalence ((≡) : relation (bound sts)). `````` Robbert Krebbers committed Nov 11, 2015 101 102 103 104 105 106 ``````Proof. split. * by intros []; constructor. * by destruct 1; constructor. * destruct 1; inversion_clear 1; constructor; etransitivity; eauto. Qed. `````` Robbert Krebbers committed Nov 16, 2015 107 108 109 ``````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 110 ``````Proof. `````` Robbert Krebbers committed Nov 16, 2015 111 `````` intros ?? HT ?? HS; destruct 1; `````` Robbert Krebbers committed Jan 13, 2016 112 `````` constructor; intros until 0; rewrite -?HS -?HT; eauto. `````` Robbert Krebbers committed Nov 11, 2015 113 ``````Qed. `````` Robbert Krebbers committed Nov 16, 2015 114 115 ``````Instance closed_proper : Proper ((≡) ==> (≡) ==> iff) closed. Proof. by split; apply closed_proper'. Qed. `````` Robbert Krebbers committed Nov 11, 2015 116 ``````Lemma closed_op T1 T2 S1 S2 : `````` 117 118 `````` closed S1 T1 → closed S2 T2 → T1 ∩ T2 ≡ ∅ → S1 ∩ S2 ≢ ∅ → closed (S1 ∩ S2) (T1 ∪ T2). `````` Robbert Krebbers committed Nov 11, 2015 119 ``````Proof. `````` Robbert Krebbers committed Jan 16, 2016 120 `````` intros [_ ? Hstep1] [_ ? Hstep2] ?; split; [done|solve_elem_of|]. `````` Robbert Krebbers committed Dec 08, 2015 121 122 123 `````` 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 124 ``````Qed. `````` 125 ``````Instance up_preserving : Proper ((=) ==> flip (⊆) ==> (⊆)) up. `````` Robbert Krebbers committed Nov 11, 2015 126 ``````Proof. `````` 127 `````` intros s ? <- T T' HT ; apply elem_of_subseteq. `````` Robbert Krebbers committed Nov 11, 2015 128 129 130 `````` induction 1 as [|s1 s2 s3 [T1 T2]]; [constructor|]. eapply rtc_l; [eapply Frame_step with T1 T2|]; eauto with sts. Qed. `````` 131 132 ``````Instance up_proper : Proper ((=) ==> (≡) ==> (≡)) up. Proof. by intros ??? ?? [??]; split; apply up_preserving. Qed. `````` Ralf Jung committed Feb 15, 2016 133 134 135 136 137 ``````Instance up_set_preserving : Proper ((⊆) ==> flip (⊆) ==> (⊆)) up_set. 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 committed Nov 16, 2015 138 ``````Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set. `````` Robbert Krebbers committed Feb 16, 2016 139 ``````Proof. by intros S1 S2 [??] T1 T2 [??]; split; apply up_set_preserving. Qed. `````` 140 ``````Lemma elem_of_up s T : s ∈ up s T. `````` Robbert Krebbers committed Nov 11, 2015 141 ``````Proof. constructor. Qed. `````` 142 ``````Lemma subseteq_up_set S T : S ⊆ up_set S T. `````` Robbert Krebbers committed Nov 11, 2015 143 ``````Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed. `````` Ralf Jung committed Feb 15, 2016 144 145 ``````Lemma up_up_set s T : up s T ≡ up_set {[ s ]} T. Proof. by rewrite /up_set collection_bind_singleton. Qed. `````` Robbert Krebbers committed Dec 08, 2015 146 ``````Lemma closed_up_set S T : `````` 147 `````` (∀ s, s ∈ S → tok s ∩ T ≡ ∅) → S ≢ ∅ → closed (up_set S T) T. `````` Robbert Krebbers committed Nov 11, 2015 148 ``````Proof. `````` Robbert Krebbers committed Dec 08, 2015 149 `````` intros HS Hne; unfold up_set; split. `````` 150 `````` * assert (∀ s, s ∈ up s T) by eauto using elem_of_up. solve_elem_of. `````` Robbert Krebbers committed Nov 11, 2015 151 `````` * intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs'). `````` Robbert Krebbers committed Dec 08, 2015 152 `````` specialize (HS s' Hs'); clear Hs' Hne S. `````` Robbert Krebbers committed Nov 11, 2015 153 154 155 156 157 `````` 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. `````` 158 ``````Lemma closed_up_set_empty S : S ≢ ∅ → closed (up_set S ∅) ∅. `````` Robbert Krebbers committed Nov 11, 2015 159 ``````Proof. eauto using closed_up_set with sts. Qed. `````` 160 ``````Lemma closed_up s T : tok s ∩ T ≡ ∅ → closed (up s T) T. `````` Robbert Krebbers committed Nov 11, 2015 161 ``````Proof. `````` 162 `````` intros; rewrite -(collection_bind_singleton (λ s, up s T) s). `````` Robbert Krebbers committed Jan 16, 2016 163 `````` apply closed_up_set; solve_elem_of. `````` Robbert Krebbers committed Nov 11, 2015 164 ``````Qed. `````` 165 ``````Lemma closed_up_empty s : closed (up s ∅) ∅. `````` Robbert Krebbers committed Nov 11, 2015 166 ``````Proof. eauto using closed_up with sts. Qed. `````` 167 ``````Lemma up_closed S T : closed S T → up_set S T ≡ S. `````` Robbert Krebbers committed Nov 11, 2015 168 ``````Proof. `````` Robbert Krebbers committed Dec 08, 2015 169 `````` intros; split; auto using subseteq_up_set; intros s. `````` Robbert Krebbers committed Nov 11, 2015 170 171 172 `````` unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?). induction Hstep; eauto using closed_step. Qed. `````` Ralf Jung committed Feb 15, 2016 173 ``````Global Instance dra : DRA (bound sts). `````` Robbert Krebbers committed Nov 11, 2015 174 175 176 177 178 179 180 181 ``````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, `````` 182 `````` closed S T → s ∈ S → tok s ∩ T' ≡ ∅ → tok s ∩ (T ∪ T') ≡ ∅). `````` Robbert Krebbers committed Jan 16, 2016 183 `````` { intros S T T' s [??]; solve_elem_of. } `````` Robbert Krebbers committed Nov 11, 2015 184 `````` destruct 3; simpl in *; auto using closed_op with sts. `````` Robbert Krebbers committed Dec 08, 2015 185 `````` * intros []; simpl; eauto using closed_up, closed_up_set, closed_ne with sts. `````` Robbert Krebbers committed Nov 20, 2015 186 187 `````` * 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 188 `````` eapply closed_up_set; eauto 2 using closed_disjoint with sts. `````` Robbert Krebbers committed Feb 11, 2016 189 `````` * intros [] [] []; constructor; rewrite ?assoc; auto with sts. `````` Robbert Krebbers committed Nov 11, 2015 190 191 192 193 `````` * 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 194 `````` * intros [|S T]; constructor; auto using elem_of_up with sts. `````` 195 `````` assert (S ⊆ up_set S ∅ ∧ S ≢ ∅) by eauto using subseteq_up_set, closed_ne. `````` Robbert Krebbers committed Jan 16, 2016 196 `````` solve_elem_of. `````` Robbert Krebbers committed Nov 11, 2015 197 `````` * intros [|S T]; constructor; auto with sts. `````` 198 `````` assert (S ⊆ up_set S ∅); auto using subseteq_up_set with sts. `````` Robbert Krebbers committed Nov 11, 2015 199 `````` * intros [s T|S T]; constructor; auto with sts. `````` Robbert Krebbers committed Jan 13, 2016 200 201 202 `````` + 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 203 `````` * intros x y ?? (z&Hy&?&Hxz); exists (unit (x ⋅ y)); split_ands. `````` Robbert Krebbers committed Jan 16, 2016 204 `````` + destruct Hxz;inversion_clear Hy;constructor;unfold up_set; solve_elem_of. `````` Robbert Krebbers committed Dec 08, 2015 205 206 207 208 `````` + 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 `````` 209 210 211 212 `````` | |- 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) `````` Robbert Krebbers committed Dec 08, 2015 213 214 215 `````` end; auto with sts. * intros x y ?? (z&Hy&_&Hxz); destruct Hxz; inversion_clear Hy; constructor; repeat match goal with `````` 216 217 218 219 `````` | |- 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) `````` Robbert Krebbers committed Dec 08, 2015 220 `````` end; auto with sts. `````` Robbert Krebbers committed Nov 20, 2015 221 222 `````` * 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 223 `````` rewrite ?disjoint_union_difference; auto. `````` Robbert Krebbers committed Dec 08, 2015 224 `````` split; [|apply intersection_greatest; auto using subseteq_up_set with sts]. `````` Robbert Krebbers committed Nov 20, 2015 225 226 227 228 `````` 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 229 230 ``````Qed. Lemma step_closed s1 s2 T1 T2 S Tf : `````` 231 `````` step (s1,T1) (s2,T2) → closed S Tf → s1 ∈ S → T1 ∩ Tf ≡ ∅ → `````` Robbert Krebbers committed Nov 16, 2015 232 `````` s2 ∈ S ∧ T2 ∩ Tf ≡ ∅ ∧ tok s2 ∩ T2 ≡ ∅. `````` Robbert Krebbers committed Nov 11, 2015 233 ``````Proof. `````` Robbert Krebbers committed Dec 08, 2015 234 `````` inversion_clear 1 as [???? HR Hs1 Hs2]; intros [?? Hstep]??; split_ands; auto. `````` Robbert Krebbers committed Nov 11, 2015 235 `````` * eapply Hstep with s1, Frame_step with T1 T2; auto with sts. `````` Robbert Krebbers committed Jan 16, 2016 236 `````` * solve_elem_of -Hstep Hs1 Hs2. `````` Robbert Krebbers committed Nov 11, 2015 237 238 239 ``````Qed. End sts_core. `````` Robbert Krebbers committed Feb 01, 2016 240 ``````Section stsRA. `````` Robbert Krebbers committed Feb 16, 2016 241 ``````Context (sts : stsT). `````` Robbert Krebbers committed Nov 11, 2015 242 `````` `````` Ralf Jung committed Feb 15, 2016 243 244 245 246 247 ``````Canonical Structure RA := validityRA (bound sts). Definition auth (s : state sts) (T : set (token sts)) : RA := to_validity (bound_auth s T). Definition frag (S : set (state sts)) (T : set (token sts)) : RA := to_validity (bound_frag S T). `````` Ralf Jung committed Feb 15, 2016 248 `````` `````` Ralf Jung committed Feb 15, 2016 249 250 ``````Lemma update_auth s1 s2 T1 T2 : step sts (s1,T1) (s2,T2) → auth s1 T1 ~~> auth s2 T2. `````` Robbert Krebbers committed Nov 11, 2015 251 ``````Proof. `````` Robbert Krebbers committed Nov 22, 2015 252 `````` intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst. `````` Ralf Jung committed Feb 15, 2016 253 `````` destruct (step_closed sts s1 s2 T1 T2 S Tf) as (?&?&?); auto. `````` Robbert Krebbers committed Nov 16, 2015 254 `````` repeat (done || constructor). `````` Robbert Krebbers committed Nov 11, 2015 255 ``````Qed. `````` Ralf Jung committed Feb 15, 2016 256 `````` `````` Ralf Jung committed Feb 15, 2016 257 258 259 ``````Lemma sts_update_frag S1 S2 (T : set (token sts)) : S1 ⊆ S2 → closed sts S2 T → frag S1 T ~~> frag S2 T. `````` Ralf Jung committed Feb 15, 2016 260 261 262 263 264 265 ``````Proof. move=>HS Hcl. eapply validity_update; inversion 3 as [|? S ? Tf|]; subst. - split; first done. constructor; last done. solve_elem_of. - split; first done. constructor; solve_elem_of. Qed. `````` Ralf Jung committed Feb 15, 2016 266 267 268 269 270 ``````Lemma frag_included S1 S2 T1 T2 : closed sts S2 T2 → frag S1 T1 ≼ frag S2 T2 ↔ (closed sts S1 T1 ∧ ∃ Tf, T2 ≡ T1 ∪ Tf ∧ T1 ∩ Tf ≡ ∅ ∧ S2 ≡ (S1 ∩ up_set sts S2 Tf)). `````` Ralf Jung committed Feb 15, 2016 271 ``````Proof. `````` 272 273 `````` move=>Hcl2. split. - intros [xf EQ]. destruct xf as [xf vf Hvf]. destruct xf as [Sf Tf|Sf Tf]. `````` Ralf Jung committed Feb 15, 2016 274 `````` { exfalso. inversion_clear EQ as [Hv EQ']. apply EQ' in Hcl2. simpl in Hcl2. `````` 275 `````` inversion Hcl2. } `````` Ralf Jung committed Feb 15, 2016 276 277 278 `````` 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]]. `````` 279 280 281 `````` apply Hvf in Hclf. simpl in Hclf. clear Hvf. inversion_clear Hdisj. split; last (exists Tf; split_ands); [done..|]. apply (anti_symm (⊆)). `````` Ralf Jung committed Feb 15, 2016 282 `````` + move=>s HS2. apply elem_of_intersection. split; first by apply HS. `````` 283 `````` by apply sts.subseteq_up_set. `````` Ralf Jung committed Feb 15, 2016 284 `````` + move=>s /elem_of_intersection [HS1 Hscl]. apply HS. split; first done. `````` 285 286 `````` destruct Hscl as [s' [Hsup Hs']]. eapply sts.closed_steps; last (hnf in Hsup; eexact Hsup); first done. `````` Ralf Jung committed Feb 15, 2016 287 `````` solve_elem_of +HS Hs'. `````` Ralf Jung committed Feb 15, 2016 288 289 `````` - intros (Hcl1 & Tf & Htk & Hf & Hs). exists (frag (up_set sts S2 Tf) Tf). `````` 290 291 292 `````` split; first split; simpl;[|done|]. + intros _. split_ands; first done. * apply sts.closed_up_set; last by eapply sts.closed_ne. `````` Ralf Jung committed Feb 15, 2016 293 `````` move=>s Hs2. move:(closed_disjoint sts _ _ Hcl2 _ Hs2). `````` Ralf Jung committed Feb 15, 2016 294 `````` solve_elem_of +Htk. `````` 295 296 297 298 `````` * constructor; last done. rewrite -Hs. by eapply sts.closed_ne. + intros _. constructor; [ solve_elem_of +Htk | done]. Qed. `````` Ralf Jung committed Feb 15, 2016 299 300 ``````Lemma frag_included' S1 S2 T : closed sts S2 T → closed sts S1 T → `````` Robbert Krebbers committed Feb 16, 2016 301 `````` S2 ≡ S1 ∩ sts.up_set sts S2 ∅ → `````` Ralf Jung committed Feb 15, 2016 302 `````` frag S1 T ≼ frag S2 T. `````` 303 ``````Proof. `````` Ralf Jung committed Feb 15, 2016 304 `````` intros. apply frag_included; first done. `````` 305 306 `````` split; first done. exists ∅. split_ands; done || solve_elem_of+. Qed. `````` Ralf Jung committed Feb 15, 2016 307 `````` `````` Robbert Krebbers committed Feb 01, 2016 308 ``````End stsRA. `````` Ralf Jung committed Feb 15, 2016 309 310 `````` End sts.``````