change STS construction: non-emptiness of the state set is now part of validity, not of closedness.

This strengthens some lemmas that are written using the notion of closednes, shortening some proofs all the way up to barrier.v

algebra/dra.v

@@ -142,12 +142,12 @@ Lemma to_validity_valid (x : A) :
   ✓ to_validity x → ✓ x.
 Proof. intros. done. Qed.
 Lemma to_validity_op (x y : A) :
-  ✓ x → ✓ y → (✓ (x ⋅ y) → x ⊥ y) →
+  (✓ (x ⋅ y) → ✓ x ∧ ✓ y ∧ x ⊥ y) →
   to_validity (x ⋅ y) ≡ to_validity x ⋅ to_validity y.
 Proof.
-  intros Hvalx Hvaly Hdisj. split; [split | done].
+  intros Hvd. split; [split | done].
   - simpl. auto.
-  - simpl. intros (_ & _ & ?).
+  - clear Hvd. simpl. intros (? & ? & ?).
     auto using dra_op_valid, to_validity_valid.
 Qed.
 

algebra/sts.v

@@ -36,8 +36,7 @@ Inductive frame_step (T : tokens sts) (s1 s2 : state sts) : Prop :=
 
 (** ** Closure under frame steps *)
 Record closed (S : states sts) (T : tokens sts) : Prop := Closed {
-  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
 }.
 Definition up (s : state sts) (T : tokens sts) : states sts :=
@@ -47,10 +46,10 @@ Definition up_set (S : states sts) (T : tokens sts) : states sts :=
 
 (** Tactic setup *)
 Hint Resolve Step.
-Hint Extern 10 (equiv (A:=set _) _ _) => set_solver : sts.
-Hint Extern 10 (¬equiv (A:=set _) _ _) => set_solver : sts.
-Hint Extern 10 (_ ∈ _) => set_solver : sts.
-Hint Extern 10 (_ ⊆ _) => set_solver : sts.
+Hint Extern 50 (equiv (A:=set _) _ _) => set_solver : sts.
+Hint Extern 50 (¬equiv (A:=set _) _ _) => set_solver : sts.
+Hint Extern 50 (_ ∈ _) => set_solver : sts.
+Hint Extern 50 (_ ⊆ _) => set_solver : sts.
 
 (** ** Setoids *)
 Instance framestep_mono : Proper (flip (⊆) ==> (=) ==> (=) ==> impl) frame_step.
@@ -84,16 +83,13 @@ Global Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set.
 Proof. by intros S1 S2 [??] T1 T2 [??]; split; apply up_set_preserving. Qed.
 
 (** ** Properties of closure under frame steps *)
-Lemma closed_disjoint' S T s : closed S T → s ∈ S → tok s ∩ T ≡ ∅.
-Proof. intros [_ ? _]; set_solver. Qed.
 Lemma closed_steps S T s1 s2 :
   closed S T → s1 ∈ S → rtc (frame_step T) s1 s2 → s2 ∈ S.
 Proof. induction 3; eauto using closed_step. Qed.
 Lemma closed_op T1 T2 S1 S2 :
-  closed S1 T1 → closed S2 T2 →
-  T1 ∩ T2 ≡ ∅ → S1 ∩ S2 ≢ ∅ → closed (S1 ∩ S2) (T1 ∪ T2).
+  closed S1 T1 → closed S2 T2 → closed (S1 ∩ S2) (T1 ∪ T2).
 Proof.
-  intros [_ ? Hstep1] [_ ? Hstep2] ?; split; [done|set_solver|].
+  intros [? Hstep1] [? Hstep2]; split; [set_solver|].
   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.
@@ -102,7 +98,7 @@ Lemma step_closed s1 s2 T1 T2 S Tf :
   step (s1,T1) (s2,T2) → closed S Tf → s1 ∈ S → T1 ∩ Tf ≡ ∅ →
   s2 ∈ S ∧ T2 ∩ Tf ≡ ∅ ∧ tok s2 ∩ T2 ≡ ∅.
 Proof.
-  inversion_clear 1 as [???? HR Hs1 Hs2]; intros [?? Hstep]??; split_and?; auto.
+  inversion_clear 1 as [???? HR Hs1 Hs2]; intros [? Hstep]??; split_and?; auto.
   - eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
   - set_solver -Hstep Hs1 Hs2.
 Qed.
@@ -125,26 +121,35 @@ 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.
 Proof. by rewrite /up_set collection_bind_singleton. Qed.
 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 ≡ ∅) → closed (up_set S T) T.
 Proof.
-  intros HS Hne; unfold up_set; split.
-  - assert (∀ s, s ∈ up s T) by eauto using elem_of_up. set_solver.
+  intros HS; unfold up_set; split.
   - intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
-    specialize (HS s' Hs'); clear Hs' Hne S.
+    specialize (HS s' Hs'); clear Hs' S.
     induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; first done.
     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 : S ≢ ∅ → closed (up_set S ∅) ∅.
-Proof. eauto using closed_up_set with sts. Qed.
 Lemma closed_up s T : tok s ∩ T ≡ ∅ → closed (up s T) T.
 Proof.
   intros; rewrite -(collection_bind_singleton (λ s, up s T) s).
   apply closed_up_set; set_solver.
 Qed.
+Lemma closed_up_set_empty S : closed (up_set S ∅) ∅.
+Proof. eauto using closed_up_set with sts. Qed.
 Lemma closed_up_empty s : closed (up s ∅) ∅.
 Proof. eauto using closed_up with sts. Qed.
+Lemma up_set_empty S T : up_set S T ≡ ∅ → S ≡ ∅.
+Proof.
+  move:(subseteq_up_set S T). set_solver.
+Qed.
+Lemma up_set_nonempty S T : S ≢ ∅ → up_set S T ≢ ∅.
+Proof. by move=>? /up_set_empty. Qed.
+Lemma up_nonempty s T : up s T ≢ ∅.
+Proof.
+  move:(elem_of_up s T). set_solver.
+Qed.
 Lemma up_closed S T : closed S T → up_set S T ≡ S.
 Proof.
   intros; split; auto using subseteq_up_set; intros s.
@@ -186,7 +191,9 @@ Inductive sts_equiv : Equiv (car sts) :=
   | frag_equiv S1 S2 T1 T2 : T1 ≡ T2 → S1 ≡ S2 → frag S1 T1 ≡ frag S2 T2.
 Existing Instance sts_equiv.
 Instance sts_valid : Valid (car sts) := λ x,
-  match x with auth s T => tok s ∩ T ≡ ∅ | frag S' T => closed S' T end.
+  match x with
+  | auth s T => tok s ∩ T ≡ ∅
+  | frag S' T => closed S' T ∧ S' ≢ ∅ end.
 Instance sts_unit : Unit (car sts) := λ x,
   match x with
   | frag S' _ => frag (up_set S' ∅ ) ∅
@@ -238,29 +245,36 @@ Proof.
   - assert (∀ T T' S s,
       closed S T → s ∈ S → tok s ∩ T' ≡ ∅ → tok s ∩ (T ∪ T') ≡ ∅).
     { intros S T T' s [??]; set_solver. }
-    destruct 3; simpl in *; auto using closed_op with sts.
-  - intros []; simpl; eauto using closed_up, closed_up_set, closed_ne with sts.
-  - intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy;clear Hy; setoid_subst;
-      rewrite ?disjoint_union_difference; auto using closed_up with sts.
-    eapply closed_up_set; eauto 2 using closed_disjoint with sts.
+    destruct 3; simpl in *; destruct_conjs; auto using closed_op with sts.
+  - intros []; simpl; intros; destruct_conjs; split;
+      eauto using closed_up, up_nonempty, closed_up_set, up_set_empty with sts.
+  - intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy; clear Hy;
+      setoid_subst; destruct_conjs; split_and?;
+      (* TODO improve this. *)
+      eauto using up_set_nonempty, up_nonempty;
+      assert ((T1 ∪ T2) ∖ T1 ≡ T2) as -> by set_solver;
+      eauto using closed_up, closed_disjoint; [].
+    eapply closed_up_set. intros.
+    eapply closed_disjoint; first done. set_solver.
   - intros [] [] []; constructor; rewrite ?assoc; auto with sts.
   - 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 [|S T]; constructor; auto using elem_of_up with sts.
-    assert (S ⊆ up_set S ∅ ∧ S ≢ ∅) by eauto using subseteq_up_set, closed_ne.
+    simpl in *. assert (S ⊆ up_set S ∅) by eauto using subseteq_up_set.
     set_solver.
   - 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.
     + rewrite (up_closed (up _ _)); auto using closed_up with sts.
     + rewrite (up_closed (up_set _ _));
-        eauto using closed_up_set, closed_ne with sts.
+        eauto using closed_up_set with sts.
   - intros x y ?? (z&Hy&?&Hxz); exists (unit (x ⋅ y)); split_and?.
     + destruct Hxz;inversion_clear Hy;constructor;unfold up_set; set_solver.
-    + destruct Hxz; inversion_clear Hy; simpl;
-        auto using closed_up_set_empty, closed_up_empty with sts.
+    + destruct Hxz; inversion_clear Hy; simpl; split_and?;
+        auto using closed_up_set_empty, closed_up_empty, up_nonempty; [].
+      eapply up_set_nonempty. set_solver.
     + destruct Hxz; inversion_clear Hy; constructor;
         repeat match goal with
         | |- context [ up_set ?S ?T ] =>
@@ -280,7 +294,7 @@ Proof.
       rewrite ?disjoint_union_difference; auto.
     split; [|apply intersection_greatest; auto using subseteq_up_set with sts].
     apply intersection_greatest; [auto with sts|].
-    intros s2; rewrite elem_of_intersection.
+    intros s2; rewrite elem_of_intersection. destruct_conjs.
     unfold up_set; rewrite elem_of_bind; intros (?&s1&?&?&?).
     apply closed_steps with T2 s1; auto with sts.
 Qed.
@@ -328,10 +342,10 @@ Proof. intros T1 T2 HT. by rewrite /sts_frag_up HT. Qed.
 (** Validity *)
 Lemma sts_auth_valid s T : ✓ sts_auth s T ↔ tok s ∩ T ≡ ∅.
 Proof. split. by move=> /(_ 0). by intros ??. Qed.
-Lemma sts_frag_valid S T : ✓ sts_frag S T ↔ closed S T.
+Lemma sts_frag_valid S T : ✓ sts_frag S T ↔ closed S T ∧ S ≢ ∅.
 Proof. split. by move=> /(_ 0). by intros ??. Qed.
 Lemma sts_frag_up_valid s T : tok s ∩ T ≡ ∅ → ✓ sts_frag_up s T.
-Proof. intros; by apply sts_frag_valid, closed_up. Qed.
+Proof. intros. by apply sts_frag_valid; auto using closed_up, up_nonempty. Qed.
 
 Lemma sts_auth_frag_valid_inv s S T1 T2 :
   ✓ (sts_auth s T1 ⋅ sts_frag S T2) → s ∈ S.
@@ -342,32 +356,36 @@ Lemma sts_op_auth_frag s S T :
   s ∈ S → closed S T → sts_auth s ∅ ⋅ sts_frag S T ≡ sts_auth s T.
 Proof.
   intros; split; [split|constructor; set_solver]; simpl.
-  - intros (?&?&?); by apply closed_disjoint' with S.
+  - intros (?&?&?); by apply closed_disjoint with S.
   - intros; split_and?.
     + set_solver+.
     + done.
+    + set_solver.
     + constructor; set_solver.
 Qed.
 Lemma sts_op_auth_frag_up s T :
   sts_auth s ∅ ⋅ sts_frag_up s T ≡ sts_auth s T.
 Proof.
   intros; split; [split|constructor; set_solver]; simpl.
-  - intros (?&?&?). apply closed_disjoint' with (up s T); first done.
+  - intros (?&?&?). destruct_conjs.
+    apply closed_disjoint with (up s T); first done.
     apply elem_of_up.
   - intros; split_and?.
     + set_solver+.
     + by apply closed_up.
+    + apply up_nonempty.
     + constructor; last set_solver. apply elem_of_up.
 Qed.
 
 Lemma sts_op_frag S1 S2 T1 T2 :
-  T1 ∩ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 →
+  T1 ∩ T2 ≡ ∅ → sts.closed S1 T1 → sts.closed S2 T2 →
   sts_frag (S1 ∩ S2) (T1 ∪ T2) ≡ sts_frag S1 T1 ⋅ sts_frag S2 T2.
 Proof.
   intros HT HS1 HS2. rewrite /sts_frag.
   (* FIXME why does rewrite not work?? *)
-  etrans; last eapply to_validity_op; try done; [].
-  intros Hval. constructor; last set_solver. eapply closed_ne, Hval.
+  etrans; last eapply to_validity_op; first done; [].
+  move=>/=[??]. split_and!; [auto; set_solver..|].
+  constructor; done.
 Qed.
 
 (** Frame preserving updates *)
@@ -375,28 +393,31 @@ Lemma sts_update_auth s1 s2 T1 T2 :
   steps (s1,T1) (s2,T2) → sts_auth s1 T1 ~~> sts_auth s2 T2.
 Proof.
   intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst.
+  simpl in *. destruct_conjs.
   destruct (steps_closed s1 s2 T1 T2 S Tf) as (?&?&?); auto; [].
   repeat (done || constructor).
 Qed.
 
-Lemma sts_update_frag S1 S2 T :
-  closed S2 T → S1 ⊆ S2 → sts_frag S1 T ~~> sts_frag S2 T.
+Lemma sts_update_frag S1 S2 T1 T2 :
+  closed S2 T2 → S1 ⊆ S2 → T2 ⊆ T1 → sts_frag S1 T1 ~~> sts_frag S2 T2.
 Proof.
-  rewrite /sts_frag=> HS Hcl. apply validity_update.
+  rewrite /sts_frag=> ? HS HT. apply validity_update.
   inversion 3 as [|? S ? Tf|]; simplify_eq/=.
-  - split; first done. constructor; [set_solver|done].
-  - split; first done. constructor; set_solver.
+  - split_and!; first done; first set_solver. constructor; set_solver.
+  - split_and!; first done; first set_solver. constructor; set_solver.
 Qed.
 
-Lemma sts_update_frag_up s1 S2 T :
-  closed S2 T → s1 ∈ S2 → sts_frag_up s1 T ~~> sts_frag S2 T.
+Lemma sts_update_frag_up s1 S2 T1 T2 :
+  closed S2 T2 → s1 ∈ S2 → T2 ⊆ T1 → sts_frag_up s1 T1 ~~> sts_frag S2 T2.
 Proof.
-  intros; by apply sts_update_frag; [|intros ?; eauto using closed_steps].
+  intros ? ? HT; apply sts_update_frag; [intros; eauto using closed_steps..].
+  rewrite <-HT. eapply up_subseteq; done.
 Qed.
 
 (** Inclusion *)
+(*
 Lemma sts_frag_included S1 S2 T1 T2 :
-  closed S2 T2 →
+  closed S2 T2 → S2 ≢ ∅
   sts_frag S1 T1 ≼ sts_frag S2 T2 ↔
   (closed S1 T1 ∧ ∃ Tf, T2 ≡ T1 ∪ Tf ∧ T1 ∩ Tf ≡ ∅ ∧ S2 ≡ S1 ∩ up_set S2 Tf).
 Proof. (* This should use some general properties of DRAs. To be improved
@@ -435,4 +456,5 @@ Proof.
   intros. apply sts_frag_included; split_and?; auto.
   exists ∅; split_and?; done || set_solver+.
 Qed.
+*)
 End stsRA.

barrier/barrier.v

@@ -41,22 +41,18 @@ Module barrier_proto.
     sts.closed (i_states i) {[ Change i ]}.
   Proof.
     split.
-    - apply (non_empty_inhabited(State Low {[ i ]})). rewrite !mkSet_elem_of /=.
-      apply lookup_singleton.
     - move=>[p I]. rewrite /= /tok !mkSet_elem_of /= =>HI.
-      move=>s' /elem_of_intersection. rewrite !mkSet_elem_of /=.
-      move=>[[Htok|Htok] ? ]; subst s'; first done.
-      destruct p; done.
+      destruct p; set_solver.
     - (* If we do the destruct of the states early, and then inversion
          on the proof of a transition, it doesn't work - we do not obtain
          the equalities we need. So we destruct the states late, because this
          means we can use "destruct" instead of "inversion". *)
       move=>s1 s2. rewrite !mkSet_elem_of /==> Hs1 Hstep.
-      (* We probably want some helper lemmas for this... *)
       inversion_clear Hstep as [T1 T2 Hdisj Hstep'].
       inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
       destruct Htrans; last done; move:Hs1 Hdisj Htok.
-      rewrite /= /tok /=.
+      rewrite /= /tok /=. 
+      (* TODO: Can this be done better? *)
       intros. apply dec_stable. 
       assert (Change i ∉ change_tokens I1) as HI1
         by (rewrite mkSet_not_elem_of; set_solver +Hs1).
@@ -74,9 +70,8 @@ Module barrier_proto.
   Lemma low_states_closed : sts.closed low_states {[ Send ]}.
   Proof.
     split.
-    - apply (non_empty_inhabited(State Low ∅)). by rewrite !mkSet_elem_of /=.
     - move=>[p I]. rewrite /= /tok !mkSet_elem_of /= =>HI.
-      destruct p; last done. set_solver.
+      destruct p; set_solver.
     - move=>s1 s2. rewrite !mkSet_elem_of /==> Hs1 Hstep.
       inversion_clear Hstep as [T1 T2 Hdisj Hstep'].
       inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
@@ -101,9 +96,9 @@ Module barrier_proto.
     (* TODO this proof is rather annoying. *)
     apply elem_of_equiv=>t. rewrite !elem_of_union.
     rewrite !mkSet_elem_of /change_tokens /=.
-    destruct t as [j|]; last naive_solver.
+    destruct t as [j|]; last set_solver.
     rewrite elem_of_difference elem_of_singleton.
-    destruct (decide (i = j)); naive_solver.
+    destruct (decide (i = j)); set_solver.
   Qed.
     
   Lemma split_step p i i1 i2 I :
@@ -115,15 +110,12 @@ Module barrier_proto.
     constructor; first constructor; rewrite /= /tok /=; first (destruct p; set_solver).
     (* This gets annoying... and I think I can see a pattern with all these proofs. Automatable? *)
     - apply elem_of_equiv=>t. destruct t; last set_solver.
-      rewrite !mkSet_elem_of /change_tokens /=.
-      rewrite !elem_of_union !elem_of_difference !elem_of_singleton.
-      destruct p; naive_solver.
+      rewrite !mkSet_elem_of. destruct p; set_solver.
     - apply elem_of_equiv=>t. destruct t as [j|]; last set_solver.
-      rewrite !mkSet_elem_of /change_tokens /=.
-      rewrite !elem_of_union !elem_of_difference !elem_of_singleton.
-      destruct (decide (i1 = j)); first naive_solver. 
-      destruct (decide (i2 = j)); first naive_solver.
-      destruct (decide (i = j)); naive_solver.
+      rewrite !mkSet_elem_of.
+      destruct (decide (i1 = j)); first set_solver. 
+      destruct (decide (i2 = j)); first set_solver.
+      destruct (decide (i = j)); set_solver.
   Qed.
 
 End barrier_proto.
@@ -145,9 +137,9 @@ Section proof.
   Local Hint Resolve signal_step wait_step split_step : sts.
   Local Hint Resolve sts.closed_op : sts.
 
-  Hint Extern 50 (_ ∈ _) => set_solver : sts.
-  Hint Extern 50 (_ ⊆ _) => set_solver : sts.
-  Hint Extern 50 (_ ≡ _) => set_solver : sts.
+  Hint Extern 50 (_ ∈ _) => try rewrite !mkSet_elem_of; set_solver : sts.
+  Hint Extern 50 (_ ⊆ _) => try rewrite !mkSet_elem_of; set_solver : sts.
+  Hint Extern 50 (_ ≡ _) => try rewrite !mkSet_elem_of; set_solver : sts.
 
   Local Notation iProp := (iPropG heap_lang Σ).
 
@@ -293,20 +285,10 @@ Section proof.
       rewrite (sts_own_weaken ⊤ _ _ (i_states i ∩ low_states) _ 
                               ({[ Change i ]} ∪ {[ Send ]})).
       + apply pvs_mono. rewrite sts_ownS_op; eauto with sts.
-      (* TODO the rest of this proof is rather annoying. *)
-      + rewrite /= /tok /=. apply elem_of_equiv=>t.
-        rewrite elem_of_difference elem_of_union.
-        rewrite !mkSet_elem_of /change_tokens.
-        (* TODO: destruct t; set_solver does not work. What is the best way to do on? *)
-        destruct t as [i'|]; last by naive_solver. split.
-        * move=>[_ Hn]. left. destruct (decide (i = i')); first by subst i.
-          exfalso. apply Hn. left. set_solver.
-        * move=>[[EQ]|?]; last discriminate. set_solver. 
-      + apply elem_of_intersection. rewrite !mkSet_elem_of /=. set_solver.
-      + apply sts.closed_op; eauto with sts; [].
-        apply (non_empty_inhabited (State Low {[ i ]})).
-        apply elem_of_intersection.
-        rewrite !mkSet_elem_of /=. set_solver.
+      + rewrite /= /tok /=  =>t. rewrite !mkSet_elem_of.
+        move=>[[?]|?]; set_solver. 
+      + eauto with sts.
+      + eauto with sts.
   Qed.
 
   Lemma signal_spec l P (Φ : val → iProp) :
@@ -441,12 +423,7 @@ Section proof.
         do 2 rewrite !(assoc (★)%I) [(_ ★ sts_ownS _ _ _)%I]comm.
         rewrite -!assoc. rewrite [(sts_ownS _ _ _ ★ _ ★ _)%I]assoc -pvs_frame_r.
         apply sep_mono.
-        * rewrite -sts_ownS_op; [|by eauto with sts..].
-          apply sts_own_weaken; first done.
-          { rewrite !mkSet_elem_of /=. set_solver+. }
-          apply sts.closed_op; [by eauto with sts..|].
-          apply (non_empty_inhabited (State Low ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]}))))).
-          rewrite !mkSet_elem_of /=. set_solver+.
+        * rewrite -sts_ownS_op; by eauto using sts_own_weaken with sts.
         * rewrite {1}[heap_ctx _]always_sep_dup !assoc [(_ ★ heap_ctx _)%I]comm -!assoc. apply sep_mono_r.
           rewrite !assoc ![(_ ★ heap_ctx _)%I]comm -!assoc. apply sep_mono_r.
           rewrite {1}[sts_ctx _ _ _]always_sep_dup !assoc [(_ ★ sts_ctx _ _ _)%I]comm -!assoc. apply sep_mono_r.
@@ -485,12 +462,7 @@ Section proof.
         do 2 rewrite !(assoc (★)%I) [(_ ★ sts_ownS _ _ _)%I]comm.
         rewrite -!assoc. rewrite [(sts_ownS _ _ _ ★ _ ★ _)%I]assoc -pvs_frame_r.
         apply sep_mono.
-        * rewrite -sts_ownS_op; [|by eauto with sts..].
-          apply sts_own_weaken; first done.
-          { rewrite !mkSet_elem_of /=. set_solver+. }
-          apply sts.closed_op; [by eauto with sts..|].
-          apply (non_empty_inhabited (State High ({[i1]} ∪ ({[i2]} ∪ (I ∖ {[i]}))))).
-          rewrite !mkSet_elem_of /=. set_solver+.
+        * rewrite -sts_ownS_op; by eauto using sts_own_weaken with sts.
         * rewrite {1}[heap_ctx _]always_sep_dup !assoc [(_ ★ heap_ctx _)%I]comm -!assoc. apply sep_mono_r.
           rewrite !assoc ![(_ ★ heap_ctx _)%I]comm -!assoc. apply sep_mono_r.
           rewrite {1}[sts_ctx _ _ _]always_sep_dup !assoc [(_ ★ sts_ctx _ _ _)%I]comm -!assoc. apply sep_mono_r.

program_logic/sts.v

@@ -53,23 +53,15 @@ Section sts.
 
   (* The same rule as implication does *not* hold, as could be shown using
      sts_frag_included. *)
-  (* TODO: sts.closed forces the user to prove that S2 is inhabited. This is
-     silly, we know that S1 is inhabited since we own it, and hence S2 is
-     inhabited, too. Probably, sts.closed should really just be about closedness.
-     I think keeping disjointnes of the token stuff in there is fine, since it
-     does not incur any unnecessary side-conditions.
-     Then we additionally demand for validity that S is nonempty, rather than
-     making that part of "closed".
-   *)
   Lemma sts_ownS_weaken E γ S1 S2 T1 T2 :
-    T1 ≡ T2 → S1 ⊆ S2 → sts.closed S2 T2 →
+    T2 ⊆ T1 → S1 ⊆ S2 → sts.closed S2 T2 →
     sts_ownS γ S1 T1 ⊑ (|={E}=> sts_ownS γ S2 T2).
-  Proof. intros -> ? ?. by apply own_update, sts_update_frag. Qed.
+  Proof. intros ? ? ?. by apply own_update, sts_update_frag. Qed.
 
   Lemma sts_own_weaken E γ s S T1 T2 :
-    T1 ≡ T2 → s ∈ S → sts.closed S T2 →
+    T2 ⊆ T1 → s ∈ S → sts.closed S T2 →
     sts_own γ s T1 ⊑ (|={E}=> sts_ownS γ S T2).
-  Proof. intros -> ??. by apply own_update, sts_update_frag_up. Qed.
+  Proof. intros ???. by apply own_update, sts_update_frag_up. Qed.
 
   Lemma sts_ownS_op γ S1 S2 T1 T2 :
     T1 ∩ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 →
@@ -106,8 +98,9 @@ Section sts.
     rewrite -!assoc. apply const_elim_sep_l=> Hvalid.
     assert (s ∈ S) by (by eapply sts_auth_frag_valid_inv, discrete_valid).
     rewrite const_equiv // left_id comm sts_op_auth_frag //.
-    (* this is horrible, but will be fixed whenever we have RAs back *)
-    by rewrite -sts_frag_valid; eapply cmra_valid_op_r, discrete_valid.
+    assert (✓ sts_frag S T) as Hv by
+          by eapply cmra_valid_op_r, discrete_valid.
+    apply (Hv 0).
   Qed.
 
   Lemma sts_closing E γ s T s' T' :