Commit 59f369c4 authored by Ralf Jung's avatar Ralf Jung
Browse files

sts: for disjointness, it is enough to demand being a subset of the empty set

parent c7995ce7
...@@ -48,9 +48,15 @@ Inductive frame_step (T : set token) (s1 s2 : state) : Prop := ...@@ -48,9 +48,15 @@ Inductive frame_step (T : set token) (s1 s2 : state) : Prop :=
Hint Resolve Frame_step. Hint Resolve Frame_step.
Record closed (S : set state) (T : set token) : Prop := Closed { Record closed (S : set state) (T : set token) : Prop := Closed {
closed_ne : S ; closed_ne : S ;
closed_disjoint s : s S tok s T ; closed_disjoint s : s S tok s T ;
closed_step s1 s2 : s1 S frame_step T s1 s2 s2 S closed_step s1 s2 : s1 S frame_step T s1 s2 s2 S
}. }.
Lemma closed_disjoint' S T s :
closed S T s S tok s T .
Proof.
move=>Hcl Hin. move:(closed_disjoint _ _ Hcl _ Hin).
solve_elem_of+.
Qed.
Lemma closed_steps S T s1 s2 : Lemma closed_steps S T s1 s2 :
closed S T s1 S rtc (frame_step T) s1 s2 s2 S. closed S T s1 S rtc (frame_step T) s1 s2 s2 S.
Proof. induction 3; eauto using closed_step. Qed. Proof. induction 3; eauto using closed_step. Qed.
...@@ -144,13 +150,13 @@ Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed. ...@@ -144,13 +150,13 @@ Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
Lemma up_up_set s T : up s T up_set {[ s ]} T. Lemma up_up_set s T : up s T up_set {[ s ]} T.
Proof. by rewrite /up_set collection_bind_singleton. Qed. Proof. by rewrite /up_set collection_bind_singleton. Qed.
Lemma closed_up_set S T : Lemma closed_up_set S T :
( s, s S tok s T ) S closed (up_set S T) T. ( s, s S tok s T ) S closed (up_set S T) T.
Proof. Proof.
intros HS Hne; unfold up_set; split. intros HS Hne; unfold up_set; split.
* assert ( s, s up s T) by eauto using elem_of_up. solve_elem_of. * assert ( s, s up s T) by eauto using elem_of_up. solve_elem_of.
* intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs'). * intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
specialize (HS s' Hs'); clear Hs' Hne S. specialize (HS s' Hs'); clear Hs' Hne S.
induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; auto. induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; first done.
inversion_clear Hstep; apply IH; clear IH; auto with sts. inversion_clear Hstep; apply IH; clear IH; auto with sts.
* intros s1 s2; rewrite !elem_of_bind; intros (s&?&?) ?; exists s. * intros s1 s2; rewrite !elem_of_bind; intros (s&?&?) ?; exists s.
split; [eapply rtc_r|]; eauto. split; [eapply rtc_r|]; eauto.
......
...@@ -18,9 +18,9 @@ Instance set_difference {A} : Difference (set A) := λ X1 X2, ...@@ -18,9 +18,9 @@ Instance set_difference {A} : Difference (set A) := λ X1 X2,
Instance set_collection : Collection A (set A). Instance set_collection : Collection A (set A).
Proof. by split; [split | |]; repeat intro. Qed. Proof. by split; [split | |]; repeat intro. Qed.
Lemma mkSet_elem_of {A} (f : A Prop) x : f x x mkSet f. Lemma mkSet_elem_of {A} (f : A Prop) x : (x mkSet f) = f x.
Proof. done. Qed. Proof. done. Qed.
Lemma mkSet_not_elem_of {A} (f : A Prop) x : ~f x x mkSet f. Lemma mkSet_not_elem_of {A} (f : A Prop) x : (x mkSet f) = (~f x).
Proof. done. Qed. Proof. done. Qed.
Instance set_ret : MRet set := λ A (x : A), {[ x ]}. Instance set_ret : MRet set := λ A (x : A), {[ x ]}.
......
...@@ -97,7 +97,7 @@ Section sts. ...@@ -97,7 +97,7 @@ Section sts.
- intros Hdisj. split_ands; first by solve_elem_of+. - intros Hdisj. split_ands; first by solve_elem_of+.
+ done. + done.
+ constructor; [done | solve_elem_of-]. + constructor; [done | solve_elem_of-].
- intros _. by eapply closed_disjoint. - intros _. by eapply closed_disjoint'.
- intros _. constructor. solve_elem_of+. - intros _. constructor. solve_elem_of+.
Qed. Qed.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment