rename STS lemmas to make _op a suffix

theories/algebra/sts.v

@@ -327,14 +327,14 @@ Lemma sts_auth_frag_valid_inv s S T1 T2 :
 Proof. by intros (?&?&Hdisj); inversion Hdisj. Qed.
 
 (** Op *)
-Lemma sts_op_auth_frag s S T :
+Lemma sts_auth_frag_op 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; split_and?; last constructor; set_solver.
 Qed.
-Lemma sts_op_auth_frag_up s T :
+Lemma sts_auth_frag_up_op s T :
   sts_auth s ∅ ⋅ sts_frag_up s T ≡ sts_auth s T.
 Proof.
   intros; split; [split|constructor; set_solver]; simpl.
@@ -346,7 +346,7 @@ Proof.
     + constructor; last set_solver. apply elem_of_up.
 Qed.
 
-Lemma sts_op_frag S1 S2 T1 T2 :
+Lemma sts_frag_op S1 S2 T1 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.
@@ -357,7 +357,7 @@ Qed.
 (* Notice that the following does *not* hold -- the composition of the
    two closures is weaker than the closure with the itnersected token
    set.  Also see up_op.
-Lemma sts_op_frag_up s T1 T2 :
+Lemma sts_frag_up_op s T1 T2 :
   T1 ## T2 → sts_frag_up s (T1 ∪ T2) ≡ sts_frag_up s T1 ⋅ sts_frag_up s T2.
 *)
 

theories/base_logic/lib/sts.v

@@ -96,7 +96,7 @@ Section sts.
   Lemma sts_ownS_op γ S1 S2 T1 T2 :
     T1 ## T2 → sts.closed S1 T1 → sts.closed S2 T2 →
     sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ⊣⊢ (sts_ownS γ S1 T1 ∗ sts_ownS γ S2 T2).
-  Proof. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed.
+  Proof. intros. by rewrite /sts_ownS -own_op sts_frag_op. Qed.
 
   Lemma sts_own_op γ s T1 T2 :
     T1 ## T2 → sts_own γ s (T1 ∪ T2) ==∗ sts_own γ s T1 ∗ sts_own γ s T2.
@@ -104,7 +104,7 @@ Section sts.
   Proof.
     intros. rewrite /sts_own -own_op. iIntros "Hown".
     iDestruct (own_valid with "Hown") as %Hval%sts_frag_up_valid.
-    rewrite -sts_op_frag.
+    rewrite -sts_frag_op.
     - iApply (sts_own_weaken with "Hown"); first done.
       + split; apply sts.elem_of_up.
       + eapply sts.closed_op; apply sts.closed_up; set_solver.
@@ -121,7 +121,7 @@ Section sts.
     iIntros "Hφ". rewrite /sts_ctx /sts_own.
     iMod (own_alloc (sts_auth s (⊤ ∖ sts.tok s))) as (γ) "Hγ".
     { apply sts_auth_valid; set_solver. }
-    iExists γ; iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ $]".
+    iExists γ; iRevert "Hγ"; rewrite -sts_auth_frag_up_op; iIntros "[Hγ $]".
     iMod (inv_alloc N _ (sts_inv γ φ) with "[Hφ Hγ]") as "#?"; auto.
     rewrite /sts_inv. iNext. iExists s. by iFrame.
   Qed.
@@ -139,8 +139,8 @@ Section sts.
     iModIntro; iExists s; iSplit; [done|]; iFrame "Hφ".
     iIntros (s' T') "[% Hφ]".
     iMod (own_update_2 with "Hγ Hγf") as "Hγ".
-    { rewrite sts_op_auth_frag; [|done..]. by apply sts_update_auth. }
-    iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ $]".
+    { rewrite sts_auth_frag_op; [|done..]. by apply sts_update_auth. }
+    iRevert "Hγ"; rewrite -sts_auth_frag_up_op; iIntros "[Hγ $]".
     iModIntro. iNext. iExists s'; by iFrame.
   Qed.