Many STS tweaks:

* Clearly separate the file algebra/sts in three parts:
  1.) The definition of an STS, step relations, and closure stuff
  2.) The construction as a disjoint RA (this module should never be used)
  3.) The construction as a CMRA with many derived properties
* Turn stsT into a canonical structure so that we can make more of its arguments
  implicit.
* Rename the underlying step relation of STSs to prim_step (similar naming as
  for languages, but here in a module to avoid ambiguity)
* Refactor program_logic/sts by moving general properties of the STS CMRA to
  algebra/sts.v
* Make naming and use of modules in program_logic/sts more consistent with
  program_logic/auth and program_logic/saved_prop
* Prove setoid properties of all definitions in program_logic/sts

algebra/dra.v

@@ -23,6 +23,7 @@ Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Minus A} := {
   dra_equivalence :> Equivalence ((≡) : relation A);
   dra_op_proper :> Proper ((≡) ==> (≡) ==> (≡)) (⋅);
   dra_unit_proper :> Proper ((≡) ==> (≡)) unit;
+  dra_valid_proper :> Proper ((≡) ==> impl) valid;
   dra_disjoint_proper :> ∀ x, Proper ((≡) ==> impl) (disjoint x);
   dra_minus_proper :> Proper ((≡) ==> (≡) ==> (≡)) minus;
   (* validity *)
@@ -61,7 +62,10 @@ Proof.
   * intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
     split; [|intros; transitivity y]; tauto.
 Qed.
-
+Instance dra_valid_proper' : Proper ((≡) ==> iff) (valid : A → Prop).
+Proof. by split; apply dra_valid_proper. Qed.
+Instance to_validity_proper : Proper ((≡) ==> (≡)) to_validity.
+Proof. by intros x1 x2 Hx; split; rewrite /= Hx. Qed.
 Instance: Proper ((≡) ==> (≡) ==> iff) (⊥).
 Proof.
   intros x1 x2 Hx y1 y2 Hy; split.

algebra/sts.v

@@ -5,144 +5,104 @@ Local Arguments valid _ _ !_ /.
 Local Arguments op _ _ !_ !_ /.
 Local Arguments unit _ _ !_ /.
 
+(** * Definition of STSs *)
 Module sts.
-
-Record stsT := STS {
+Structure stsT := STS {
   state : Type;
   token : Type;
-  trans : relation state;
-  tok   : state → set token;
+  prim_step : relation state;
+  tok : state → set token;
 }.
 Arguments STS {_ _} _ _.
+Arguments prim_step {_} _ _.
+Arguments tok {_} _.
+Notation states sts := (set (state sts)).
+Notation tokens sts := (set (token sts)).
 
-(* The type of bounds we can give to the state of an STS. This is the type
-   that we equip with an RA structure. *)
-Inductive bound (sts : stsT) :=
-  | 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 {_} _ _.
+(** * Theory and definitions *)
+Section sts.
+Context {sts : stsT}.
 
-Section sts_core.
-Context (sts : stsT).
-Infix "≼" := dra_included.
-
-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) :=
+(** ** Step relations *)
+Inductive step : relation (state sts * tokens sts) :=
   | Step s1 s2 T1 T2 :
-     trans s1 s2 → tok s1 ∩ T1 ≡ ∅ → tok s2 ∩ T2 ≡ ∅ →
+     prim_step s1 s2 → tok s1 ∩ T1 ≡ ∅ → tok s2 ∩ T2 ≡ ∅ →
      tok s1 ∪ T1 ≡ tok s2 ∪ T2 → step (s1,T1) (s2,T2).
-Hint Resolve Step.
-Inductive frame_step (T : set token) (s1 s2 : state) : Prop :=
+Inductive frame_step (T : tokens sts) (s1 s2 : state sts) : Prop :=
   | Frame_step T1 T2 :
      T1 ∩ (tok s1 ∪ T) ≡ ∅ → step (s1,T1) (s2,T2) → frame_step T s1 s2.
-Hint Resolve Frame_step.
-Record closed (S : set state) (T : set token) : Prop := Closed {
+
+(** ** 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_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 :
-  closed S T → s1 ∈ S → rtc (frame_step T) s1 s2 → s2 ∈ S.
-Proof. induction 3; eauto using closed_step. Qed.
-Global Instance valid : Valid (bound sts) := λ x,
-  match x with
-  | bound_auth s T => tok s ∩ T ≡ ∅ | bound_frag S' T => closed S' T
-  end.
-Definition up (s : state) (T : set token) : set state :=
+Definition up (s : state sts) (T : tokens sts) : states sts :=
   mkSet (rtc (frame_step T) s).
-Definition up_set (S : set state) (T : set token) : set state :=
+Definition up_set (S : states sts) (T : tokens sts) : states sts :=
   S ≫= λ s, up s T.
-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) :=
-  | frag_frag_disjoint S1 S2 T1 T2 :
-     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,
-  match x1, x2 with
-  | 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 *)
-  end.
-Global Instance minus : Minus (bound sts) := λ x1 x2,
-  match x1, x2 with
-  | 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)
-  end.
 
-Hint Extern 10 (base.equiv (A:=set _) _ _) => solve_elem_of : sts.
-Hint Extern 10 (¬(base.equiv (A:=set _) _ _)) => solve_elem_of : sts.
+(** Tactic setup *)
+Hint Resolve Step.
+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.
-Instance: Equivalence ((≡) : relation (bound sts)).
-Proof.
-  split.
-  * by intros []; constructor.
-  * by destruct 1; constructor.
-  * destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
-Qed.
-Instance framestep_proper : Proper ((≡) ==> (=) ==> (=) ==> impl) frame_step.
+
+(** ** Setoids *)
+Instance framestep_proper' : Proper ((≡) ==> (=) ==> (=) ==> impl) frame_step.
 Proof. intros ?? HT ?? <- ?? <-; destruct 1; econstructor; eauto with sts. Qed.
+Global Instance framestep_proper : Proper ((≡) ==> (=) ==> (=) ==> iff) frame_step.
+Proof. by intros ?? [??] ??????; split; apply framestep_proper'. Qed.
 Instance closed_proper' : Proper ((≡) ==> (≡) ==> impl) closed.
 Proof.
   intros ?? HT ?? HS; destruct 1;
     constructor; intros until 0; rewrite -?HS -?HT; eauto.
 Qed.
-Instance closed_proper : Proper ((≡) ==> (≡) ==> iff) closed.
+Global Instance closed_proper : Proper ((≡) ==> (≡) ==> iff) closed.
 Proof. by split; apply closed_proper'. Qed.
-Lemma closed_op T1 T2 S1 S2 :
-  closed S1 T1 → closed S2 T2 →
-  T1 ∩ T2 ≡ ∅ → S1 ∩ S2 ≢ ∅ → closed (S1 ∩ S2) (T1 ∪ T2).
-Proof.
-  intros [_ ? Hstep1] [_ ? Hstep2] ?; split; [done|solve_elem_of|].
-  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.
-Qed.
-Instance up_preserving : Proper ((=) ==> flip (⊆) ==> (⊆)) up.
+Global Instance up_preserving : Proper ((=) ==> flip (⊆) ==> (⊆)) up.
 Proof.
   intros s ? <- T T' HT ; 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.
-Instance up_proper : Proper ((=) ==> (≡) ==> (≡)) up.
+Global Instance up_proper : Proper ((=) ==> (≡) ==> (≡)) up.
 Proof. by intros ??? ?? [??]; split; apply up_preserving. Qed.
-Instance up_set_preserving : Proper ((⊆) ==> flip (⊆) ==> (⊆)) up_set.
+Global 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.
-Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set.
+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 [_ ? _]; solve_elem_of. 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).
+Proof.
+  intros [_ ? Hstep1] [_ ? Hstep2] ?; split; [done|solve_elem_of|].
+  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.
+Qed.
+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_ands; auto.
+  * eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
+  * solve_elem_of -Hstep Hs1 Hs2.
+Qed.
+
+(** ** Properties of the closure operators *)
 Lemma elem_of_up s T : s ∈ up s T.
 Proof. constructor. Qed.
 Lemma subseteq_up_set S T : S ⊆ up_set S T.
@@ -176,12 +136,82 @@ Proof.
   unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).
   induction Hstep; eauto using closed_step.
 Qed.
-Global Instance dra : DRA (bound sts).
+End sts. End sts.
+
+Notation stsT := sts.stsT.
+Notation STS := sts.STS.
+
+(** * STSs form a disjoint RA *)
+(* This module should never be imported, uses the module [sts] below. *)
+Module sts_dra.
+Import sts.
+
+(* The type of bounds we can give to the state of an STS. This is the type
+   that we equip with an RA structure. *)
+Inductive car (sts : stsT) :=
+  | auth : state sts → set (token sts) → car sts
+  | frag : set (state sts) → set (token sts ) → car sts.
+Arguments auth {_} _ _.
+Arguments frag {_} _ _.
+
+Section sts_dra.
+Context {sts : stsT}.
+Infix "≼" := dra_included.
+Implicit Types S : states sts.
+Implicit Types T : tokens sts.
+
+Inductive sts_equiv : Equiv (car sts) :=
+  | 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.
+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.
+Instance sts_unit : Unit (car sts) := λ x,
+  match x with
+  | frag S' _ => frag (up_set S' ∅ ) ∅
+  | auth s _  => frag (up s ∅) ∅
+  end.
+Inductive sts_disjoint : Disjoint (car sts) :=
+  | frag_frag_disjoint S1 S2 T1 T2 :
+     S1 ∩ S2 ≢ ∅ → 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.
+Existing Instance sts_disjoint.
+Instance sts_op : Op (car sts) := λ 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.
+Instance sts_minus : Minus (car sts) := λ x1 x2,
+  match x1, x2 with
+  | frag S1 T1, frag S2 T2 => frag (up_set S1 (T1 ∖ T2)) (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 s (T1 ∖ T2)) (T1 ∖ T2)
+  end.
+
+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.
+Instance sts_equivalence: Equivalence ((≡) : relation (car sts)).
+Proof.
+  split.
+  * by intros []; constructor.
+  * by destruct 1; constructor.
+  * destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
+Qed.
+Global Instance sts_dra : DRA (car sts).
 Proof.
   split.
   * apply _.
   * by do 2 destruct 1; constructor; setoid_subst.
   * by destruct 1; constructor; setoid_subst.
+  * by destruct 1; simpl; intros ?; 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,
@@ -233,50 +263,104 @@ Proof.
     unfold up_set; rewrite elem_of_bind; intros (?&s1&?&?&?).
     apply closed_steps with T2 s1; auto with sts.
 Qed.
-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 ≡ ∅.
+Canonical Structure RA : cmraT := validityRA (car sts).
+End sts_dra. End sts_dra.
+
+(** * The STS Resource Algebra *)
+(** Finally, the general theory of STS that should be used by users *)
+Notation stsRA := (@sts_dra.RA).
+
+Section sts_definitions.
+  Context {sts : stsT}.
+  Definition sts_auth (s : sts.state sts) (T : sts.tokens sts) : stsRA sts :=
+    to_validity (sts_dra.auth s T).
+  Definition sts_frag (S : sts.states sts) (T : sts.tokens sts) : stsRA sts :=
+    to_validity (sts_dra.frag S T).
+  Definition sts_frag_up (s : sts.state sts) (T : sts.tokens sts) : stsRA sts :=
+    sts_frag (sts.up s T) T.
+End sts_definitions.
+Instance: Params (@sts_auth) 2.
+Instance: Params (@sts_frag) 1.
+Instance: Params (@sts_frag_up) 2.
+
+Section stsRA.
+Import sts.
+Context {sts : stsT}.
+Implicit Types s : state sts.
+Implicit Types S : states sts.
+Implicit Types T : tokens sts.
+
+(** Setoids *)
+Global Instance sts_auth_proper s : Proper ((≡) ==> (≡)) (sts_auth s).
+Proof. (* this proof is horrible *)
+  intros T1 T2 HT. rewrite /sts_auth.
+  by eapply to_validity_proper; try apply _; constructor.
+Qed.
+Global Instance sts_frag_proper : Proper ((≡) ==> (≡) ==> (≡)) (@sts_frag sts).
 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.
-  * solve_elem_of -Hstep Hs1 Hs2.
+  intros S1 S2 ? T1 T2 HT; rewrite /sts_auth.
+  by eapply to_validity_proper; try apply _; constructor.
 Qed.
-End sts_core.
+Global Instance sts_frag_up_proper s : Proper ((≡) ==> (≡)) (sts_frag_up s).
+Proof. intros T1 T2 HT. by rewrite /sts_frag_up HT. Qed.
 
-Section stsRA.
-Context (sts : stsT).
+(** 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.
+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.
 
-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).
+Lemma sts_auth_frag_valid_inv s S T1 T2 :
+  ✓ (sts_auth s T1 ⋅ sts_frag S T2) → s ∈ S.
+Proof. by move=> /(_ 0) [? [? Hdisj]]; inversion Hdisj. Qed.
 
-Lemma update_auth s1 s2 T1 T2 :
-  step sts (s1,T1) (s2,T2) → auth s1 T1 ~~> auth s2 T2.
+(** Op *)
+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; solve_elem_of]; simpl.
+  - intros (?&?&?); by apply closed_disjoint' with S.
+  - intros; split_ands. solve_elem_of+. done. constructor; solve_elem_of.
+Qed.
+Lemma sts_op_auth_frag_up s T :
+  tok s ∩ T ≡ ∅ → sts_auth s ∅ ⋅ sts_frag_up s T ≡ sts_auth s T.
+Proof. intros; apply sts_op_auth_frag; auto using elem_of_up, closed_up. Qed.
+
+(** Frame preserving updates *)
+Lemma sts_update_auth s1 s2 T1 T2 :
+  step (s1,T1) (s2,T2) → sts_auth s1 T1 ~~> sts_auth s2 T2.
 Proof.
   intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst.
-  destruct (step_closed sts s1 s2 T1 T2 S Tf) as (?&?&?); auto.
+  destruct (step_closed s1 s2 T1 T2 S Tf) as (?&?&?); auto.
   repeat (done || constructor).
 Qed.
 
-Lemma sts_update_frag S1 S2 (T : set (token sts)) :
-  S1 ⊆ S2 → closed sts S2 T →
-  frag S1 T ~~> frag S2 T.
+Lemma sts_update_frag S1 S2 T :
+  closed S2 T → S1 ⊆ S2 → sts_frag S1 T ~~> sts_frag S2 T.
 Proof.
-  move=>HS Hcl. eapply validity_update; inversion 3 as [|? S ? Tf|]; subst.
-  - split; first done. constructor; last done. solve_elem_of.
+  rewrite /sts_frag=> HS Hcl. apply validity_update.
+  inversion 3 as [|? S ? Tf|]; simplify_equality'.
+  - split; first done. constructor; [solve_elem_of|done].
   - split; first done. constructor; solve_elem_of.
 Qed.
 
-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)).
+Lemma sts_update_frag_up s1 S2 T :
+  closed S2 T → s1 ∈ S2 → sts_frag_up s1 T ~~> sts_frag S2 T.
 Proof.
+  intros; by apply sts_update_frag; [|intros ?; eauto using closed_steps].
+Qed.
+
+(** Inclusion *)
+Lemma sts_frag_included S1 S2 T1 T2 :
+  closed S2 T2 →
+  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
+when we have RAs back *)
   move=>Hcl2. split.
-  - intros [xf EQ]. destruct xf as [xf vf Hvf]. destruct xf as [Sf Tf|Sf Tf].
+  - intros [[[Sf Tf|Sf Tf] vf Hvf] EQ].
     { exfalso. inversion_clear EQ as [Hv EQ']. apply EQ' in Hcl2. simpl in Hcl2.
       inversion Hcl2. }
     inversion_clear EQ as [Hv EQ'].
@@ -286,31 +370,27 @@ Proof.
     inversion_clear Hdisj. split; last (exists Tf; split_ands); [done..|].
     apply (anti_symm (⊆)).
     + move=>s HS2. apply elem_of_intersection. split; first by apply HS.
-      by apply sts.subseteq_up_set.
+      by apply subseteq_up_set.
     + move=>s /elem_of_intersection [HS1 Hscl]. apply HS. split; first done.
       destruct Hscl as [s' [Hsup Hs']].
-      eapply sts.closed_steps; last (hnf in Hsup; eexact Hsup); first done.
+      eapply closed_steps; last (hnf in Hsup; eexact Hsup); first done.
       solve_elem_of +HS Hs'.
   - intros (Hcl1 & Tf & Htk & Hf & Hs).
-    exists (frag (up_set sts S2 Tf) Tf).
+    exists (sts_frag (up_set S2 Tf) Tf).
     split; first split; simpl;[|done|].
     + intros _. split_ands; first done.
-      * apply sts.closed_up_set; last by eapply sts.closed_ne.
-        move=>s Hs2. move:(closed_disjoint sts _ _ Hcl2 _ Hs2).
+      * apply closed_up_set; last by eapply closed_ne.
+        move=>s Hs2. move:(closed_disjoint _ _ Hcl2 _ Hs2).
         solve_elem_of +Htk.
-      * constructor; last done. rewrite -Hs. by eapply sts.closed_ne.
+      * constructor; last done. rewrite -Hs. by eapply closed_ne.
     + intros _. constructor; [ solve_elem_of +Htk | done].
 Qed.
 
-Lemma frag_included' S1 S2 T :
-  closed sts S2 T → closed sts S1 T →
-  S2 ≡ S1 ∩ sts.up_set sts S2 ∅ →
-  frag S1 T ≼ frag S2 T.
+Lemma sts_frag_included' S1 S2 T :
+  closed S2 T → closed S1 T → S2 ≡ S1 ∩ up_set S2 ∅ →
+  sts_frag S1 T ≼ sts_frag S2 T.
 Proof.
-  intros. apply frag_included; first done.
-  split; first done. exists ∅. split_ands; done || solve_elem_of+.
+  intros. apply sts_frag_included; split_ands; auto.
+  exists ∅; split_ands; done || solve_elem_of+.
 Qed.
-
 End stsRA.
-
-End sts.

barrier/barrier.v

@@ -27,14 +27,14 @@ Module barrier_proto.
       change_tokens (state_I s)
     ∪ match state_phase s with Low => ∅ | High => {[ Send ]} end.
 
-  Definition sts := sts.STS trans tok.
+  Canonical Structure sts := sts.STS trans tok.
 
   (* The set of states containing some particular i *)
   Definition i_states (i : gname) : set stateT :=
     mkSet (λ s, i ∈ state_I s).
 
   Lemma i_states_closed i :
-    sts.closed sts (i_states i) {[ Change i ]}.
+    sts.closed (i_states i) {[ Change i ]}.
   Proof.
     split.
     - apply (non_empty_inhabited(State Low {[ i ]})). rewrite !mkSet_elem_of /=.
@@ -68,7 +68,7 @@ Module barrier_proto.
     mkSet (λ s, if state_phase s is Low then True else False).
   
   Lemma low_states_closed :
-    sts.closed sts low_states {[ Send ]}.
+    sts.closed low_states {[ Send ]}.
   Proof.
     split.
     - apply (non_empty_inhabited(State Low ∅)). by rewrite !mkSet_elem_of /=.
@@ -96,7 +96,7 @@ Section proof.
   (* TODO: Bundle HeapI and HeapG and have notation so that we can just write
      "l ↦ '0". *)
   Context (HeapI : gid) `{!HeapInG Σ HeapI} (HeapG : gname).
-  Context (StsI : gid) `{!sts.InG heap_lang Σ StsI sts}.
+  Context (StsI : gid) `{!STSInG heap_lang Σ StsI sts}.
   Context (SpI : gid) `{!SavedPropInG heap_lang Σ SpI}.
 
   Notation iProp := (iPropG heap_lang Σ).
@@ -114,13 +114,13 @@ Section proof.
     end.
 
   Definition barrier_ctx (γ : gname) (l : loc) (P : iProp) : iProp :=
-    (heap_ctx HeapI HeapG N ★ sts.ctx StsI sts γ N (barrier_inv l P))%I.
+    (heap_ctx HeapI HeapG N ★ sts_ctx StsI sts γ N (barrier_inv l P))%I.
 
   Definition send (l : loc) (P : iProp) : iProp :=
-    (∃ γ, barrier_ctx γ l P ★ sts.in_states StsI sts γ low_states {[ Send ]})%I.
+    (∃ γ, barrier_ctx γ l P ★ sts_ownS StsI sts γ low_states {[ Send ]})%I.
 
   Definition recv (l : loc) (R : iProp) : iProp :=
-    (∃ γ (P Q : iProp) i, barrier_ctx γ l P ★ sts.in_states StsI sts γ (i_states i) {[ Change i ]} ★
+    (∃ γ (P Q : iProp) i, barrier_ctx γ l P ★ sts_ownS StsI sts γ (i_states i) {[ Change i ]} ★
         saved_prop_own SpI i Q ★ ▷(Q -★ R))%I.
     
   Lemma newchan_spec (P : iProp) (Q : val → iProp) :

program_logic/sts.v

 From algebra Require Export sts.
-From algebra Require Import dra.
 From program_logic Require Export invariants ghost_ownership.
 Import uPred.
 
-Local Arguments valid _ _ !_ /.
-Local Arguments op _ _ !_ !_ /.
-Local Arguments unit _ _ !_ /.
-
-Module sts.
-(** This module is *not* meant to be imported. Instead, just use "sts.ctx" etc.
-    like you would use "auth_ctx" etc. *)
-Export algebra.sts.sts.
-
-Class InG Λ Σ (i : gid) (sts : stsT) := {
-  inG :> ghost_ownership.InG Λ Σ i (sts.RA sts);
-  inh :> Inhabited (state sts);
+Class STSInG Λ Σ (i : gid) (sts : stsT) := {
+  sts_inG :> ghost_ownership.InG Λ Σ i (stsRA sts);
+  sts_inhabited :> Inhabited (sts.state sts);
 }.
 
 Section definitions.
-  Context {Λ Σ} (i : gid) (sts : stsT) `{!InG Λ Σ i sts} (γ : gname).
-  Definition inv  (φ : state sts → iPropG Λ Σ) : iPropG Λ Σ :=
-    (∃ s, own i γ (auth sts s ∅) ★ φ s)%I.
-  Definition in_states (S : set (state sts)) (T: set (token sts)) : iPropG Λ Σ:=
-    own i γ (frag sts S T)%I.
-  Definition in_state (s : state sts) (T: set (token sts)) : iPropG Λ Σ :=
-    in_states (up sts s T) T.
-  Definition ctx (N : namespace) (φ : state sts → iPropG Λ Σ) : iPropG Λ Σ :=
-    invariants.inv N (inv φ).
+  Context {Λ Σ} (i : gid) (sts : stsT) `{!STSInG Λ Σ i sts} (γ : gname).
+  Import sts.
+  Definition sts_inv (φ : state sts → iPropG Λ Σ) : iPropG Λ Σ :=
+    (∃ s, own i γ (sts_auth s ∅) ★ φ s)%I.
+  Definition sts_ownS (S : states sts) (T : tokens sts) : iPropG Λ Σ:=
+    own i γ (sts_frag S T).
+  Definition sts_own (s : state sts) (T : tokens sts) : iPropG Λ Σ :=
+    own i γ (sts_frag_up s T).
+  Definition sts_ctx (N : namespace) (φ: state sts → iPropG Λ Σ) : iPropG Λ Σ :=
+    inv N (sts_inv φ).
 End definitions.
-Instance: Params (@inv) 6.
-Instance: Params (@in_states) 6.
-Instance: Params (@in_state) 6.
-Instance: Params (@ctx) 7.
+Instance: Params (@sts_inv) 6.
+Instance: Params (@sts_ownS) 6.
+Instance: Params (@sts_own) 7.
+Instance: Params (@sts_ctx) 7.
 
 Section sts.
-  Context {Λ Σ} (i : gid) (sts : stsT) `{!InG Λ Σ StsI sts}.
-  Context (φ : state sts → iPropG Λ Σ).
+  Context {Λ Σ} (i : gid) (sts : stsT) `{!STSInG Λ Σ StsI sts}.
+  Context (φ : sts.state sts → iPropG Λ Σ).
   Implicit Types N : namespace.
   Implicit Types P Q R : iPropG Λ Σ.
   Implicit Types γ : gname.
+  Implicit Types S : sts.states sts.
+  Implicit Types T : sts.tokens sts.
+
+  (** Setoids *)
+  Global Instance sts_inv_ne n γ :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_inv StsI sts γ).
+  Proof. by intros φ1 φ2 Hφ; rewrite /sts_inv; setoid_rewrite Hφ. Qed.
+  Global Instance sts_inv_proper γ :
+    Proper (pointwise_relation _ (≡) ==> (≡)) (sts_inv StsI sts γ).
+  Proof. by intros φ1 φ2 Hφ; rewrite /sts_inv; setoid_rewrite Hφ. Qed.
+  Global Instance sts_ownS_proper γ :
+    Proper ((≡) ==> (≡) ==> (≡)) (sts_ownS StsI sts γ).
+  Proof. intros S1 S2 HS T1 T2 HT. by rewrite /sts_ownS HS HT. Qed.
+  Global Instance sts_own_proper γ s :
+    Proper ((≡) ==> (≡)) (sts_ownS StsI sts γ s).
+  Proof. intros T1 T2 HT. by rewrite /sts_ownS HT. Qed.
+  Global Instance sts_ctx_ne n γ N :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx StsI sts γ N).
+  Proof. by intros φ1 φ2 Hφ; rewrite /sts_ctx Hφ. Qed.
+  Global Instance sts_ctx_proper γ N :
+    Proper (pointwise_relation _ (≡) ==> (≡)) (sts_ctx StsI sts γ N).
+  Proof. by intros φ1 φ2 Hφ; rewrite /sts_ctx Hφ. Qed.
 
   (* The same rule as implication does *not* hold, as could be shown using
      sts_frag_included. *)
-  Lemma in_states_weaken E γ S1 S2 T :
-    S1 ⊆ S2 → closed sts S2 T →
-    in_states StsI sts γ S1 T ⊑ pvs E E (in_states StsI sts γ S2 T).
-  Proof.
-    rewrite /in_states=>Hs Hcl. apply own_update, sts_update_frag; done.
-  Qed.
+  Lemma sts_ownS_weaken E γ S1 S2 T :
+    S1 ⊆ S2 → sts.closed S2 T →
+    sts_ownS StsI sts γ S1 T ⊑ pvs E E (sts_ownS StsI sts γ S2 T).
+  Proof. intros. by apply own_update, sts_update_frag. Qed.
 
-  Lemma in_state_states E γ s S T :
-    s ∈ S → closed sts S T →
-    in_state StsI sts γ s T ⊑ pvs E E (in_states StsI sts γ S T).
-  Proof.
-    move=>Hs Hcl. apply in_states_weaken; last done.
-    move=>s' Hup. eapply closed_steps in Hcl;last (hnf in Hup; eexact Hup);done.
-  Qed.
+  Lemma sts_own_weaken E γ s S T :
+    s ∈ S → sts.closed S T →
+    sts_own StsI sts γ s T ⊑ pvs E E (sts_ownS StsI sts γ S T).
+  Proof. intros. by apply own_update, sts_update_frag_up. Qed.
 
-  Lemma alloc N s :
-    φ s ⊑ pvs N N (∃ γ, ctx StsI sts γ N φ ∧
-                        in_state StsI sts γ s (set_all ∖ sts.(tok) s)).
+  Lemma sts_alloc N s :
+    φ s ⊑ pvs N N (∃ γ, sts_ctx StsI sts γ N φ ∧
+                        sts_own StsI sts γ s (set_all ∖ sts.tok s)).
   Proof.
     eapply sep_elim_True_r.
-    { eapply (own_alloc StsI (auth sts s (set_all ∖ sts.(tok) s)) N).
-      apply discrete_valid=>/=. solve_elem_of. }
+    { apply (own_alloc StsI (sts_auth s (set_all ∖ sts.tok s)) N).
+      apply sts_auth_valid; solve_elem_of. }
     rewrite pvs_frame_l. apply pvs_strip_pvs.
     rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
-    transitivity (▷ inv StsI sts γ φ ★
-                    in_state StsI sts γ s (set_all ∖ sts.(tok) s))%I.
-    { rewrite /inv -later_intro -(exist_intro s).
-      rewrite [(_ ★ φ _)%I]comm -assoc. apply sep_mono; first done.
-      rewrite -own_op. apply equiv_spec, own_proper.
-      split; first split; simpl.
-      - intros; solve_elem_of+.
-      - intros _. split_ands; first by solve_elem_of+.
-        + apply closed_up. solve_elem_of+.
-        + constructor; last solve_elem_of+. apply sts.elem_of_up. 
-      - intros _. constructor. solve_elem_of+. }
-    rewrite (inv_alloc N) /ctx pvs_frame_r. apply pvs_mono.
+    transitivity (▷ sts_inv StsI sts γ φ ★
+                    sts_own StsI sts γ s (set_all ∖ sts.tok s))%I.
+    { rewrite /sts_inv -later_intro -(exist_intro s).
+      rewrite [(_ ★ φ _)%I]comm -assoc. apply sep_mono_r.
+      by rewrite -own_op sts_op_auth_frag_up; last solve_elem_of+. }
+    rewrite (inv_alloc N) /sts_ctx pvs_frame_r.
     by rewrite always_and_sep_l.
   Qed.
 
-  Lemma opened E γ S T :
-    (▷ inv StsI sts γ φ ★ in_states StsI sts γ S T)
-      ⊑ pvs E E (∃ s, ■ (s ∈ S) ★ ▷ φ s ★ own StsI γ (auth sts s T)).
+  Lemma sts_opened E γ S T :
+    (▷ sts_inv StsI sts γ φ ★ sts_ownS StsI sts γ S T)
+    ⊑ pvs E E (∃ s, ■ (s ∈ S) ★ ▷ φ s ★ own StsI γ (sts_auth s T)).
   Proof.
-    rewrite /inv /in_states later_exist sep_exist_r. apply exist_elim=>s.
+    rewrite /sts_inv /sts_ownS later_exist sep_exist_r. apply exist_elim=>s.
     rewrite later_sep pvs_timeless !pvs_frame_r. apply pvs_mono.
     rewrite -(exist_intro s).
     rewrite [(_ ★ ▷φ _)%I]comm -!assoc -own_op -[(▷φ _ ★ _)%I]comm.
     rewrite own_valid_l discrete_validI.
-    rewrite -!assoc. apply const_elim_sep_l=>-[_ [Hcl Hdisj]].
-    simpl in Hdisj, Hcl. inversion_clear Hdisj. rewrite const_equiv // left_id.
-    rewrite comm. apply sep_mono; first done.
-    apply equiv_spec, own_proper. split; first split; simpl.
-    - intros Hdisj. split_ands; first by solve_elem_of+.
-      + done.
-      + constructor; [done | solve_elem_of-].
-    - intros _. by eapply closed_disjoint'.
-    - intros _. constructor. solve_elem_of+.
+    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.
   Qed.
 
-  Lemma closing E γ s T s' T' :
-    step sts (s, T) (s', T') →
-    (▷ φ s' ★ own StsI γ (auth sts s T))
-    ⊑ pvs E E (▷ inv StsI sts γ φ ★ in_state StsI sts γ s' T').
+  Lemma sts_closing E γ s T s' T' :
+    sts.step (s, T) (s', T') →
+    (▷ φ s' ★ own StsI γ (sts_auth s T))
+    ⊑ pvs E E (▷ sts_inv StsI sts γ φ ★ sts_own StsI sts γ s' T').
   Proof.
-    intros Hstep. rewrite /inv /in_states -(exist_intro s').
+    intros Hstep. rewrite /sts_inv /sts_own -(exist_intro s').
     rewrite later_sep [(_ ★ ▷φ _)%I]comm -assoc.
-    rewrite -pvs_frame_l. apply sep_mono; first done.
-    rewrite -later_intro.
+    rewrite -pvs_frame_l. apply sep_mono_r. rewrite -later_intro.
     rewrite own_valid_l discrete_validI. apply const_elim_sep_l=>Hval.
-    simpl in Hval. transitivity (pvs E E (own StsI γ (auth sts s' T'))).
-    { by apply own_update, sts.update_auth. }
-    apply pvs_mono. rewrite -own_op. apply equiv_spec, own_proper.
-    split; first split; simpl.
-    - intros _.
-      set Tf := set_all ∖ sts.(tok) s ∖ T.
-      assert (closed sts (up sts s Tf) Tf).
-      { apply closed_up. rewrite /Tf. solve_elem_of+. }
-      eapply step_closed; [done..| |].
-      + apply elem_of_up.
-      + rewrite /Tf. solve_elem_of+.
-    - intros ?. split_ands; first by solve_elem_of+.
-      + apply closed_up. done.
-      + constructor; last solve_elem_of+. apply elem_of_up.
-    - intros _. constructor. solve_elem_of+.
+    transitivity (pvs E E (own StsI γ (sts_auth s' T'))).
+    { by apply own_update, sts_update_auth. }
+    by rewrite -own_op sts_op_auth_frag_up; last by inversion_clear Hstep.
   Qed.
 
   Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}.
 
-  Lemma states_fsa E N P (Q : V → iPropG Λ Σ) γ S T :
+  Lemma sts_fsaS E N P (Q : V → iPropG Λ Σ) γ S T :
     fsaV → nclose N ⊆ E →
-    P ⊑ ctx StsI sts γ N φ →
-    P ⊑ (in_states StsI sts γ S T ★ ∀ s,
+    P ⊑ sts_ctx StsI sts γ N φ →
+    P ⊑ (sts_ownS StsI sts γ S T ★ ∀ s,
           ■ (s ∈ S) ★ ▷ φ s -★
           fsa (E ∖ nclose N) (λ x, ∃ s' T',
-            ■ (step sts (s, T) (s', T')) ★ ▷ φ s' ★
-            (in_state StsI sts γ s' T' -★ Q x))) →
+            ■ sts.step (s, T) (s', T') ★ ▷ φ s' ★
+            (sts_own StsI sts γ s' T' -★ Q x))) →
     P ⊑ fsa E Q.
   Proof.
-    rewrite /ctx=>? HN Hinv Hinner.
+    rewrite /sts_ctx=>? HN Hinv Hinner.
     eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
     apply wand_intro_l. rewrite assoc.
-    rewrite (opened (E ∖ N)) !pvs_frame_r !sep_exist_r.
+    rewrite (sts_opened (E ∖ N)) !pvs_frame_r !sep_exist_r.
     apply (fsa_strip_pvs fsa). apply exist_elim=>s.
     rewrite (forall_elim s). rewrite [(▷_ ★ _)%I]comm.
     (* Getting this wand eliminated is really annoying. *)
@@ -154,24 +139,19 @@ Section sts.
     rewrite sep_exist_l; apply exist_elim=>T'.
     rewrite comm -!assoc. apply const_elim_sep_l=>-Hstep.
     rewrite assoc [(_ ★ (_ -★ _))%I]comm -assoc.
-    rewrite (closing (E ∖ N)) //; [].
+    rewrite (sts_closing (E ∖ N)) //; [].
     rewrite pvs_frame_l. apply pvs_mono.
     by rewrite assoc [(_ ★ ▷_)%I]comm -assoc wand_elim_l.
   Qed.
 
-  Lemma state_fsa E N P (Q : V → iPropG Λ Σ) γ s0 T :
+  Lemma sts_fsa E N P (Q : V → iPropG Λ Σ) γ s0 T :
     fsaV → nclose N ⊆ E →
-    P ⊑ ctx StsI sts γ N φ →
-    P ⊑ (in_state StsI sts γ s0 T ★ ∀ s,
-          ■ (s ∈ up sts s0 T) ★ ▷ φ s -★
+    P ⊑ sts_ctx StsI sts γ N φ →
+    P ⊑ (sts_own StsI sts γ s0 T ★ ∀ s,
+          ■ (s ∈ sts.up s0 T) ★ ▷ φ s -★
           fsa (E ∖ nclose N) (λ x, ∃ s' T',
-            ■ (step sts (s, T) (s', T')) ★ ▷ φ s' ★
-            (in_state StsI sts γ s' T' -★ Q x))) →
+            ■ (sts.step (s, T) (s', T')) ★ ▷ φ s' ★
+            (sts_own StsI sts γ s' T' -★ Q x))) →
     P ⊑ fsa E Q.
-  Proof.
-    rewrite {1}/state. apply states_fsa.
-  Qed.
-
-End sts.
-
+  Proof. apply sts_fsaS. Qed.
 End sts.