From a9be1e26a165b391aee5380e06215044c0844505 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 17 Feb 2016 16:26:12 +0100
Subject: [PATCH] Rename solve_elem_of into set_solver.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

It is doing much more than just dealing with ∈, it solves all kinds
of goals involving set operations (including ≡ and ⊆).
---
 algebra/sts.v               |  52 +++++++-------
 algebra/upred_big_op.v      |   4 +-
 barrier/barrier.v           |  26 +++----
 prelude/collections.v       | 132 ++++++++++++++++++------------------
 prelude/fin_collections.v   |  24 +++----
 prelude/fin_map_dom.v       |  12 ++--
 prelude/hashset.v           |   2 +-
 program_logic/adequacy.v    |   2 +-
 program_logic/invariants.v  |  16 ++---
 program_logic/lifting.v     |   2 +-
 program_logic/namespaces.v  |   8 +--
 program_logic/pviewshifts.v |  12 ++--
 program_logic/sts.v         |   4 +-
 program_logic/viewshifts.v  |   4 +-
 program_logic/weakestpre.v  |   6 +-
 program_logic/wsat.v        |  14 ++--
 16 files changed, 160 insertions(+), 160 deletions(-)

diff --git a/algebra/sts.v b/algebra/sts.v
index 8790c3092..6868c3187 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -46,16 +46,16 @@ Definition up_set (S : states sts) (T : tokens sts) : states 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.
+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.
 
 (** ** Setoids *)
 Instance framestep_mono : Proper (flip (⊆) ==> (=) ==> (=) ==> impl) frame_step.
 Proof.
   intros ?? HT ?? <- ?? <-; destruct 1; econstructor;
-    eauto with sts; solve_elem_of.
+    eauto with sts; set_solver.
 Qed.
 Global Instance framestep_proper : Proper ((≡) ==> (=) ==> (=) ==> iff) frame_step.
 Proof. by intros ?? [??] ??????; split; apply framestep_mono. Qed.
@@ -84,7 +84,7 @@ 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.
+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.
@@ -92,7 +92,7 @@ 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 [_ ? Hstep1] [_ ? Hstep2] ?; split; [done|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.
@@ -103,7 +103,7 @@ Lemma step_closed s1 s2 T1 T2 S Tf :
 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.
+  - set_solver -Hstep Hs1 Hs2.
 Qed.
 
 (** ** Properties of the closure operators *)
@@ -117,7 +117,7 @@ Lemma closed_up_set S T :
   (∀ s, s ∈ S → tok s ∩ T ⊆ ∅) → S ≢ ∅ → 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. solve_elem_of.
+  - assert (∀ s, s ∈ up s T) by eauto using elem_of_up. set_solver.
   - intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
     specialize (HS s' Hs'); clear Hs' Hne S.
     induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; first done.
@@ -130,7 +130,7 @@ 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; solve_elem_of.
+  apply closed_up_set; set_solver.
 Qed.
 Lemma closed_up_empty s : closed (up s ∅) ∅.
 Proof. eauto using closed_up with sts. Qed.
@@ -198,10 +198,10 @@ Instance sts_minus : Minus (car sts) := λ x1 x2,
   | 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.
+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.
 Instance sts_equivalence: Equivalence ((≡) : relation (car sts)).
 Proof.
   split.
@@ -220,7 +220,7 @@ Proof.
   - by do 2 destruct 1; constructor; setoid_subst.
   - assert (∀ T T' S s,
       closed S T → s ∈ S → tok s ∩ T' ≡ ∅ → tok s ∩ (T ∪ T') ≡ ∅).
-    { intros S T T' s [??]; solve_elem_of. }
+    { 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;
@@ -233,7 +233,7 @@ Proof.
   - 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.
-    solve_elem_of.
+    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.
@@ -241,7 +241,7 @@ Proof.
     + rewrite (up_closed (up_set _ _));
         eauto using closed_up_set, closed_ne with sts.
   - intros x y ?? (z&Hy&?&Hxz); exists (unit (x â‹… y)); split_ands.
-    + destruct Hxz;inversion_clear Hy;constructor;unfold up_set; solve_elem_of.
+    + 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; constructor;
@@ -324,9 +324,9 @@ Proof. by move=> /(_ 0) [? [? Hdisj]]; inversion Hdisj. Qed.
 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; split; [split|constructor; set_solver]; simpl.
   - intros (?&?&?); by apply closed_disjoint' with S.
-  - intros; split_ands. solve_elem_of+. done. constructor; solve_elem_of.
+  - intros; split_ands. set_solver+. done. constructor; set_solver.
 Qed.
 Lemma sts_op_auth_frag_up s T :
   tok s ∩ T ≡ ∅ → sts_auth s ∅ ⋅ sts_frag_up s T ≡ sts_auth s T.
@@ -339,7 +339,7 @@ Proof.
   intros HT HS1 HS2. rewrite /sts_frag.
   (* FIXME why does rewrite not work?? *)
   etransitivity; last eapply to_validity_op; try done; [].
-  intros Hval. constructor; last solve_elem_of. eapply closed_ne, Hval.
+  intros Hval. constructor; last set_solver. eapply closed_ne, Hval.
 Qed.
 
 (** Frame preserving updates *)
@@ -356,8 +356,8 @@ Lemma sts_update_frag S1 S2 T :
 Proof.
   rewrite /sts_frag=> HS Hcl. apply validity_update.
   inversion 3 as [|? S ? Tf|]; simplify_eq/=.
-  - split; first done. constructor; [solve_elem_of|done].
-  - split; first done. constructor; solve_elem_of.
+  - split; first done. constructor; [set_solver|done].
+  - split; first done. constructor; set_solver.
 Qed.
 
 Lemma sts_update_frag_up s1 S2 T :
@@ -388,16 +388,16 @@ when we have RAs back *)
     + move=>s /elem_of_intersection [HS1 Hscl]. apply HS. split; first done.
       destruct Hscl as [s' [Hsup Hs']].
       eapply closed_steps; last (hnf in Hsup; eexact Hsup); first done.
-      solve_elem_of +HS Hs'.
+      set_solver +HS Hs'.
   - intros (Hcl1 & Tf & Htk & Hf & Hs).
     exists (sts_frag (up_set S2 Tf) Tf).
     split; first split; simpl;[|done|].
     + intros _. split_ands; first done.
       * apply closed_up_set; last by eapply closed_ne.
         move=>s Hs2. move:(closed_disjoint _ _ Hcl2 _ Hs2).
-        solve_elem_of +Htk.
+        set_solver +Htk.
       * constructor; last done. rewrite -Hs. by eapply closed_ne.
-    + intros _. constructor; [ solve_elem_of +Htk | done].
+    + intros _. constructor; [ set_solver +Htk | done].
 Qed.
 
 Lemma sts_frag_included' S1 S2 T :
@@ -405,6 +405,6 @@ Lemma sts_frag_included' S1 S2 T :
   sts_frag S1 T ≼ sts_frag S2 T.
 Proof.
   intros. apply sts_frag_included; split_ands; auto.
-  exists ∅; split_ands; done || solve_elem_of+.
+  exists ∅; split_ands; done || set_solver+.
 Qed.
 End stsRA.
diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index 9eeeb17b2..7c45252ce 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -178,8 +178,8 @@ Section gset.
   Lemma big_sepS_delete P X x :
     x ∈ X → (Π★{set X} P)%I ≡ (P x ★ Π★{set X ∖ {[ x ]}} P)%I.
   Proof.
-    intros. rewrite -big_sepS_insert; last solve_elem_of.
-    by rewrite -union_difference_L; last solve_elem_of.
+    intros. rewrite -big_sepS_insert; last set_solver.
+    by rewrite -union_difference_L; last set_solver.
   Qed.
   Lemma big_sepS_singleton P x : (Π★{set {[ x ]}} P)%I ≡ (P x)%I.
   Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed.
diff --git a/barrier/barrier.v b/barrier/barrier.v
index 03386f134..8a6c48c6c 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -57,11 +57,11 @@ Module barrier_proto.
       rewrite /= /tok /=.
       intros. apply dec_stable. 
       assert (Change i ∉ change_tokens I1) as HI1
-        by (rewrite mkSet_not_elem_of; solve_elem_of +Hs1).
+        by (rewrite mkSet_not_elem_of; set_solver +Hs1).
       assert (Change i ∉ change_tokens I2) as HI2.
       { destruct p.
-        - solve_elem_of +Htok Hdisj HI1.
-        - solve_elem_of +Htok Hdisj HI1 / discriminate. }
+        - set_solver +Htok Hdisj HI1.
+        - set_solver +Htok Hdisj HI1 / discriminate. }
       done.
   Qed.
 
@@ -74,13 +74,13 @@ Module barrier_proto.
     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. solve_elem_of.
+      destruct p; last done. 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].
       destruct Htrans; move:Hs1 Hdisj Htok =>/=;
                                 first by destruct p.
-      rewrite /= /tok /=. intros. solve_elem_of +Hdisj Htok.
+      rewrite /= /tok /=. intros. set_solver +Hdisj Htok.
   Qed.
 
 End barrier_proto.
@@ -162,23 +162,23 @@ Section proof.
       { rewrite -later_intro. apply wand_intro_l. by rewrite right_id. }
       rewrite (sts_own_weaken ⊤ _ _ (i_states i ∩ low_states) _ ({[ Change i ]} ∪ {[ Send ]})).
       + apply pvs_mono. rewrite sts_ownS_op; first done.
-        * solve_elem_of.
+        * set_solver.
         * apply i_states_closed.
         * apply low_states_closed.
       + rewrite /= /tok /=. apply elem_of_equiv=>t. rewrite elem_of_difference elem_of_union.
         rewrite !mkSet_elem_of /change_tokens.
-        (* TODO: destruct t; solve_elem_of does not work. What is the best way to do on? *)
+        (* 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. solve_elem_of.
-        * move=>[[EQ]|?]; last discriminate. solve_elem_of. 
-      + apply elem_of_intersection. rewrite !mkSet_elem_of /=. solve_elem_of.
+          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.
         * apply i_states_closed.
         * apply low_states_closed.
-        * solve_elem_of.
+        * set_solver.
         * apply (non_empty_inhabited (State Low {[ i ]})). apply elem_of_intersection.
-          rewrite !mkSet_elem_of /=. solve_elem_of.
+          rewrite !mkSet_elem_of /=. set_solver.
   Qed.
 
   Lemma signal_spec l P (Q : val → iProp) :
@@ -199,7 +199,7 @@ Section proof.
       erewrite later_sep. apply sep_mono_r. apply later_intro. }
     apply wand_intro_l. rewrite -(exist_intro (State High I)).
     rewrite -(exist_intro ∅). rewrite const_equiv /=; last first.
-    { constructor; first constructor; rewrite /= /tok /=; solve_elem_of. }
+    { constructor; first constructor; rewrite /= /tok /=; set_solver. }
     rewrite left_id -later_intro {2}/barrier_inv -!assoc. apply sep_mono_r.
     rewrite !assoc [(_ ★ P)%I]comm !assoc -2!assoc.
     apply sep_mono; last first.
diff --git a/prelude/collections.v b/prelude/collections.v
index d51ab7cc3..a9ff16465 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -207,7 +207,7 @@ Ltac decompose_empty := repeat
 occurrences of [(∪)], [(∩)], [(∖)], [(<$>)], [∅], [{[_]}], [(≡)], and [(⊆)],
 by rewriting these into logically equivalent propositions. For example we
 rewrite [A → x ∈ X ∪ ∅] into [A → x ∈ X ∨ False]. *)
-Ltac unfold_elem_of :=
+Ltac set_unfold :=
   repeat_on_hyps (fun H =>
     repeat match type of H with
     | context [ _ ⊆ _ ] => setoid_rewrite elem_of_subseteq in H
@@ -251,21 +251,21 @@ Ltac unfold_elem_of :=
   end.
 
 (** Since [firstorder] fails or loops on very small goals generated by
-[solve_elem_of] already. We use the [naive_solver] tactic as a substitute.
+[set_solver] already. We use the [naive_solver] tactic as a substitute.
 This tactic either fails or proves the goal. *)
-Tactic Notation "solve_elem_of" tactic3(tac) :=
+Tactic Notation "set_solver" tactic3(tac) :=
   setoid_subst;
   decompose_empty;
-  unfold_elem_of;
+  set_unfold;
   naive_solver tac.
-Tactic Notation "solve_elem_of" "-" hyp_list(Hs) "/" tactic3(tac) :=
-  clear Hs; solve_elem_of tac.
-Tactic Notation "solve_elem_of" "+" hyp_list(Hs) "/" tactic3(tac) :=
-  revert Hs; clear; solve_elem_of tac.
-Tactic Notation "solve_elem_of" := solve_elem_of eauto.
-Tactic Notation "solve_elem_of" "-" hyp_list(Hs) := clear Hs; solve_elem_of.
-Tactic Notation "solve_elem_of" "+" hyp_list(Hs) :=
-  revert Hs; clear; solve_elem_of.
+Tactic Notation "set_solver" "-" hyp_list(Hs) "/" tactic3(tac) :=
+  clear Hs; set_solver tac.
+Tactic Notation "set_solver" "+" hyp_list(Hs) "/" tactic3(tac) :=
+  revert Hs; clear; set_solver tac.
+Tactic Notation "set_solver" := set_solver eauto.
+Tactic Notation "set_solver" "-" hyp_list(Hs) := clear Hs; set_solver.
+Tactic Notation "set_solver" "+" hyp_list(Hs) :=
+  revert Hs; clear; set_solver.
 
 (** * More theorems *)
 Section collection.
@@ -273,7 +273,7 @@ Section collection.
   Implicit Types X Y : C.
 
   Global Instance: Lattice C.
-  Proof. split. apply _. firstorder auto. solve_elem_of. Qed.
+  Proof. split. apply _. firstorder auto. set_solver. Qed.
   Global Instance difference_proper :
      Proper ((≡) ==> (≡) ==> (≡)) (@difference C _).
   Proof.
@@ -281,23 +281,23 @@ Section collection.
     by rewrite !elem_of_difference, HX, HY.
   Qed.
   Lemma non_empty_inhabited x X : x ∈ X → X ≢ ∅.
-  Proof. solve_elem_of. Qed.
+  Proof. set_solver. Qed.
   Lemma intersection_singletons x : ({[x]} : C) ∩ {[x]} ≡ {[x]}.
-  Proof. solve_elem_of. Qed.
+  Proof. set_solver. Qed.
   Lemma difference_twice X Y : (X ∖ Y) ∖ Y ≡ X ∖ Y.
-  Proof. solve_elem_of. Qed.
+  Proof. set_solver. Qed.
   Lemma subseteq_empty_difference X Y : X ⊆ Y → X ∖ Y ≡ ∅.
-  Proof. solve_elem_of. Qed.
+  Proof. set_solver. Qed.
   Lemma difference_diag X : X ∖ X ≡ ∅.
-  Proof. solve_elem_of. Qed.
+  Proof. set_solver. Qed.
   Lemma difference_union_distr_l X Y Z : (X ∪ Y) ∖ Z ≡ X ∖ Z ∪ Y ∖ Z.
-  Proof. solve_elem_of. Qed.
+  Proof. set_solver. Qed.
   Lemma difference_union_distr_r X Y Z : Z ∖ (X ∪ Y) ≡ (Z ∖ X) ∩ (Z ∖ Y).
-  Proof. solve_elem_of. Qed.
+  Proof. set_solver. Qed.
   Lemma difference_intersection_distr_l X Y Z : (X ∩ Y) ∖ Z ≡ X ∖ Z ∩ Y ∖ Z.
-  Proof. solve_elem_of. Qed.
+  Proof. set_solver. Qed.
   Lemma disjoint_union_difference X Y : X ∩ Y ≡ ∅ → (X ∪ Y) ∖ X ≡ Y.
-  Proof. solve_elem_of. Qed.
+  Proof. set_solver. Qed.
 
   Section leibniz.
     Context `{!LeibnizEquiv C}.
@@ -334,10 +334,10 @@ Section collection.
     Lemma non_empty_difference X Y : X ⊂ Y → Y ∖ X ≢ ∅.
     Proof.
       intros [HXY1 HXY2] Hdiff. destruct HXY2. intros x.
-      destruct (decide (x ∈ X)); solve_elem_of.
+      destruct (decide (x ∈ X)); set_solver.
     Qed.
     Lemma empty_difference_subseteq X Y : X ∖ Y ≡ ∅ → X ⊆ Y.
-    Proof. intros ? x ?; apply dec_stable; solve_elem_of. Qed.
+    Proof. intros ? x ?; apply dec_stable; set_solver. Qed.
     Context `{!LeibnizEquiv C}.
     Lemma union_difference_L X Y : X ⊆ Y → Y = X ∪ Y ∖ X.
     Proof. unfold_leibniz. apply union_difference. Qed.
@@ -396,33 +396,33 @@ Section NoDup.
   Proof. firstorder. Qed.
 
   Lemma elem_of_upto_elem_of x X : x ∈ X → elem_of_upto x X.
-  Proof. unfold elem_of_upto. solve_elem_of. Qed.
+  Proof. unfold elem_of_upto. set_solver. Qed.
   Lemma elem_of_upto_empty x : ¬elem_of_upto x ∅.
-  Proof. unfold elem_of_upto. solve_elem_of. Qed.
+  Proof. unfold elem_of_upto. set_solver. Qed.
   Lemma elem_of_upto_singleton x y : elem_of_upto x {[ y ]} ↔ R x y.
-  Proof. unfold elem_of_upto. solve_elem_of. Qed.
+  Proof. unfold elem_of_upto. set_solver. Qed.
 
   Lemma elem_of_upto_union X Y x :
     elem_of_upto x (X ∪ Y) ↔ elem_of_upto x X ∨ elem_of_upto x Y.
-  Proof. unfold elem_of_upto. solve_elem_of. Qed.
+  Proof. unfold elem_of_upto. set_solver. Qed.
   Lemma not_elem_of_upto x X : ¬elem_of_upto x X → ∀ y, y ∈ X → ¬R x y.
-  Proof. unfold elem_of_upto. solve_elem_of. Qed.
+  Proof. unfold elem_of_upto. set_solver. Qed.
 
   Lemma set_NoDup_empty: set_NoDup ∅.
-  Proof. unfold set_NoDup. solve_elem_of. Qed.
+  Proof. unfold set_NoDup. set_solver. Qed.
   Lemma set_NoDup_add x X :
     ¬elem_of_upto x X → set_NoDup X → set_NoDup ({[ x ]} ∪ X).
-  Proof. unfold set_NoDup, elem_of_upto. solve_elem_of. Qed.
+  Proof. unfold set_NoDup, elem_of_upto. set_solver. Qed.
   Lemma set_NoDup_inv_add x X :
     x ∉ X → set_NoDup ({[ x ]} ∪ X) → ¬elem_of_upto x X.
   Proof.
     intros Hin Hnodup [y [??]].
-    rewrite (Hnodup x y) in Hin; solve_elem_of.
+    rewrite (Hnodup x y) in Hin; set_solver.
   Qed.
   Lemma set_NoDup_inv_union_l X Y : set_NoDup (X ∪ Y) → set_NoDup X.
-  Proof. unfold set_NoDup. solve_elem_of. Qed.
+  Proof. unfold set_NoDup. set_solver. Qed.
   Lemma set_NoDup_inv_union_r X Y : set_NoDup (X ∪ Y) → set_NoDup Y.
-  Proof. unfold set_NoDup. solve_elem_of. Qed.
+  Proof. unfold set_NoDup. set_solver. Qed.
 End NoDup.
 
 (** * Quantifiers *)
@@ -433,27 +433,27 @@ Section quantifiers.
   Definition set_Exists X := ∃ x, x ∈ X ∧ P x.
 
   Lemma set_Forall_empty : set_Forall ∅.
-  Proof. unfold set_Forall. solve_elem_of. Qed.
+  Proof. unfold set_Forall. set_solver. Qed.
   Lemma set_Forall_singleton x : set_Forall {[ x ]} ↔ P x.
-  Proof. unfold set_Forall. solve_elem_of. Qed.
+  Proof. unfold set_Forall. set_solver. Qed.
   Lemma set_Forall_union X Y : set_Forall X → set_Forall Y → set_Forall (X ∪ Y).
-  Proof. unfold set_Forall. solve_elem_of. Qed.
+  Proof. unfold set_Forall. set_solver. Qed.
   Lemma set_Forall_union_inv_1 X Y : set_Forall (X ∪ Y) → set_Forall X.
-  Proof. unfold set_Forall. solve_elem_of. Qed.
+  Proof. unfold set_Forall. set_solver. Qed.
   Lemma set_Forall_union_inv_2 X Y : set_Forall (X ∪ Y) → set_Forall Y.
-  Proof. unfold set_Forall. solve_elem_of. Qed.
+  Proof. unfold set_Forall. set_solver. Qed.
 
   Lemma set_Exists_empty : ¬set_Exists ∅.
-  Proof. unfold set_Exists. solve_elem_of. Qed.
+  Proof. unfold set_Exists. set_solver. Qed.
   Lemma set_Exists_singleton x : set_Exists {[ x ]} ↔ P x.
-  Proof. unfold set_Exists. solve_elem_of. Qed.
+  Proof. unfold set_Exists. set_solver. Qed.
   Lemma set_Exists_union_1 X Y : set_Exists X → set_Exists (X ∪ Y).
-  Proof. unfold set_Exists. solve_elem_of. Qed.
+  Proof. unfold set_Exists. set_solver. Qed.
   Lemma set_Exists_union_2 X Y : set_Exists Y → set_Exists (X ∪ Y).
-  Proof. unfold set_Exists. solve_elem_of. Qed.
+  Proof. unfold set_Exists. set_solver. Qed.
   Lemma set_Exists_union_inv X Y :
     set_Exists (X ∪ Y) → set_Exists X ∨ set_Exists Y.
-  Proof. unfold set_Exists. solve_elem_of. Qed.
+  Proof. unfold set_Exists. set_solver. Qed.
 End quantifiers.
 
 Section more_quantifiers.
@@ -510,7 +510,7 @@ Section fresh.
   Qed.
   Lemma Forall_fresh_subseteq X Y xs :
     Forall_fresh X xs → Y ⊆ X → Forall_fresh Y xs.
-  Proof. rewrite !Forall_fresh_alt; solve_elem_of. Qed.
+  Proof. rewrite !Forall_fresh_alt; set_solver. Qed.
 
   Lemma fresh_list_length n X : length (fresh_list n X) = n.
   Proof. revert X. induction n; simpl; auto. Qed.
@@ -518,12 +518,12 @@ Section fresh.
   Proof.
     revert X. induction n as [|n IH]; intros X; simpl;[by rewrite elem_of_nil|].
     rewrite elem_of_cons; intros [->| Hin]; [apply is_fresh|].
-    apply IH in Hin; solve_elem_of.
+    apply IH in Hin; set_solver.
   Qed.
   Lemma NoDup_fresh_list n X : NoDup (fresh_list n X).
   Proof.
     revert X. induction n; simpl; constructor; auto.
-    intros Hin; apply fresh_list_is_fresh in Hin; solve_elem_of.
+    intros Hin; apply fresh_list_is_fresh in Hin; set_solver.
   Qed.
   Lemma Forall_fresh_list X n : Forall_fresh X (fresh_list n X).
   Proof.
@@ -537,50 +537,50 @@ Section collection_monad.
 
   Global Instance collection_fmap_mono {A B} :
     Proper (pointwise_relation _ (=) ==> (⊆) ==> (⊆)) (@fmap M _ A B).
-  Proof. intros f g ? X Y ?; solve_elem_of. Qed.
+  Proof. intros f g ? X Y ?; set_solver. Qed.
   Global Instance collection_fmap_proper {A B} :
     Proper (pointwise_relation _ (=) ==> (≡) ==> (≡)) (@fmap M _ A B).
-  Proof. intros f g ? X Y [??]; split; solve_elem_of. Qed.
+  Proof. intros f g ? X Y [??]; split; set_solver. Qed.
   Global Instance collection_bind_mono {A B} :
     Proper (((=) ==> (⊆)) ==> (⊆) ==> (⊆)) (@mbind M _ A B).
-  Proof. unfold respectful; intros f g Hfg X Y ?; solve_elem_of. Qed.
+  Proof. unfold respectful; intros f g Hfg X Y ?; set_solver. Qed.
   Global Instance collection_bind_proper {A B} :
     Proper (((=) ==> (≡)) ==> (≡) ==> (≡)) (@mbind M _ A B).
-  Proof. unfold respectful; intros f g Hfg X Y [??]; split; solve_elem_of. Qed.
+  Proof. unfold respectful; intros f g Hfg X Y [??]; split; set_solver. Qed.
   Global Instance collection_join_mono {A} :
     Proper ((⊆) ==> (⊆)) (@mjoin M _ A).
-  Proof. intros X Y ?; solve_elem_of. Qed.
+  Proof. intros X Y ?; set_solver. Qed.
   Global Instance collection_join_proper {A} :
     Proper ((≡) ==> (≡)) (@mjoin M _ A).
-  Proof. intros X Y [??]; split; solve_elem_of. Qed.
+  Proof. intros X Y [??]; split; set_solver. Qed.
 
   Lemma collection_bind_singleton {A B} (f : A → M B) x : {[ x ]} ≫= f ≡ f x.
-  Proof. solve_elem_of. Qed.
+  Proof. set_solver. Qed.
   Lemma collection_guard_True {A} `{Decision P} (X : M A) : P → guard P; X ≡ X.
-  Proof. solve_elem_of. Qed.
+  Proof. set_solver. Qed.
   Lemma collection_fmap_compose {A B C} (f : A → B) (g : B → C) (X : M A) :
     g ∘ f <$> X ≡ g <$> (f <$> X).
-  Proof. solve_elem_of. Qed.
+  Proof. set_solver. Qed.
   Lemma elem_of_fmap_1 {A B} (f : A → B) (X : M A) (y : B) :
     y ∈ f <$> X → ∃ x, y = f x ∧ x ∈ X.
-  Proof. solve_elem_of. Qed.
+  Proof. set_solver. Qed.
   Lemma elem_of_fmap_2 {A B} (f : A → B) (X : M A) (x : A) :
     x ∈ X → f x ∈ f <$> X.
-  Proof. solve_elem_of. Qed.
+  Proof. set_solver. Qed.
   Lemma elem_of_fmap_2_alt {A B} (f : A → B) (X : M A) (x : A) (y : B) :
     x ∈ X → y = f x → y ∈ f <$> X.
-  Proof. solve_elem_of. Qed.
+  Proof. set_solver. Qed.
 
   Lemma elem_of_mapM {A B} (f : A → M B) l k :
     l ∈ mapM f k ↔ Forall2 (λ x y, x ∈ f y) l k.
   Proof.
     split.
-    - revert l. induction k; solve_elem_of.
-    - induction 1; solve_elem_of.
+    - revert l. induction k; set_solver.
+    - induction 1; set_solver.
   Qed.
   Lemma collection_mapM_length {A B} (f : A → M B) l k :
     l ∈ mapM f k → length l = length k.
-  Proof. revert l; induction k; solve_elem_of. Qed.
+  Proof. revert l; induction k; set_solver. Qed.
   Lemma elem_of_mapM_fmap {A B} (f : A → B) (g : B → M A) l k :
     Forall (λ x, ∀ y, y ∈ g x → f y = x) l → k ∈ mapM g l → fmap f k = l.
   Proof.
@@ -606,7 +606,7 @@ Section finite.
   Context `{SimpleCollection A B}.
   Global Instance set_finite_subseteq :
      Proper (flip (⊆) ==> impl) (@set_finite A B _).
-  Proof. intros X Y HX [l Hl]; exists l; solve_elem_of. Qed.
+  Proof. intros X Y HX [l Hl]; exists l; set_solver. Qed.
   Global Instance set_finite_proper : Proper ((≡) ==> iff) (@set_finite A B _).
   Proof. by intros X Y [??]; split; apply set_finite_subseteq. Qed.
   Lemma empty_finite : set_finite ∅.
@@ -619,9 +619,9 @@ Section finite.
     rewrite elem_of_union, elem_of_app; naive_solver.
   Qed.
   Lemma union_finite_inv_l X Y : set_finite (X ∪ Y) → set_finite X.
-  Proof. intros [l ?]; exists l; solve_elem_of. Qed.
+  Proof. intros [l ?]; exists l; set_solver. Qed.
   Lemma union_finite_inv_r X Y : set_finite (X ∪ Y) → set_finite Y.
-  Proof. intros [l ?]; exists l; solve_elem_of. Qed.
+  Proof. intros [l ?]; exists l; set_solver. Qed.
 End finite.
 
 Section more_finite.
@@ -636,6 +636,6 @@ Section more_finite.
     set_finite Y → set_finite (X ∖ Y) → set_finite X.
   Proof.
     intros [l ?] [k ?]; exists (l ++ k).
-    intros x ?; destruct (decide (x ∈ Y)); rewrite elem_of_app; solve_elem_of.
+    intros x ?; destruct (decide (x ∈ Y)); rewrite elem_of_app; set_solver.
   Qed.
 End more_finite.
diff --git a/prelude/fin_collections.v b/prelude/fin_collections.v
index 7726f9682..65850cbf1 100644
--- a/prelude/fin_collections.v
+++ b/prelude/fin_collections.v
@@ -41,7 +41,7 @@ Qed.
 Lemma elements_singleton x : elements {[ x ]} = [x].
 Proof.
   apply Permutation_singleton. by rewrite <-(right_id ∅ (∪) {[x]}),
-    elements_union_singleton, elements_empty by solve_elem_of.
+    elements_union_singleton, elements_empty by set_solver.
 Qed.
 Lemma elements_contains X Y : X ⊆ Y → elements X `contains` elements Y.
 Proof.
@@ -90,7 +90,7 @@ Proof.
   intros E. destruct (size_pos_elem_of X); auto with lia.
   exists x. apply elem_of_equiv. split.
   - rewrite elem_of_singleton. eauto using size_singleton_inv.
-  - solve_elem_of.
+  - set_solver.
 Qed.
 Lemma size_union X Y : X ∩ Y ≡ ∅ → size (X ∪ Y) = size X + size Y.
 Proof.
@@ -98,7 +98,7 @@ Proof.
   apply Permutation_length, NoDup_Permutation.
   - apply NoDup_elements.
   - apply NoDup_app; repeat split; try apply NoDup_elements.
-    intros x; rewrite !elem_of_elements; solve_elem_of.
+    intros x; rewrite !elem_of_elements; set_solver.
   - intros. by rewrite elem_of_app, !elem_of_elements, elem_of_union.
 Qed.
 Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100.
@@ -121,15 +121,15 @@ Next Obligation.
 Qed.
 Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X).
 Proof.
-  rewrite <-size_union by solve_elem_of.
-  setoid_replace (Y ∖ X) with ((Y ∪ X) ∖ X) by solve_elem_of.
-  rewrite <-union_difference, (comm (∪)); solve_elem_of.
+  rewrite <-size_union by set_solver.
+  setoid_replace (Y ∖ X) with ((Y ∪ X) ∖ X) by set_solver.
+  rewrite <-union_difference, (comm (∪)); set_solver.
 Qed.
 Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
 Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
 Lemma subset_size X Y : X ⊂ Y → size X < size Y.
 Proof.
-  intros. rewrite (union_difference X Y) by solve_elem_of.
+  intros. rewrite (union_difference X Y) by set_solver.
   rewrite size_union_alt, difference_twice.
   cut (size (Y ∖ X) ≠ 0); [lia |].
   by apply size_non_empty_iff, non_empty_difference.
@@ -143,8 +143,8 @@ Proof.
   intros ? Hemp Hadd. apply well_founded_induction with (⊂).
   { apply collection_wf. }
   intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX].
-  - rewrite (union_difference {[ x ]} X) by solve_elem_of.
-    apply Hadd. solve_elem_of. apply IH; solve_elem_of.
+  - rewrite (union_difference {[ x ]} X) by set_solver.
+    apply Hadd. set_solver. apply IH; set_solver.
   - by rewrite HX.
 Qed.
 Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
@@ -158,10 +158,10 @@ Proof.
     symmetry. apply elem_of_elements. }
   induction 1 as [|x l ?? IH]; simpl.
   - intros X HX. setoid_rewrite elem_of_nil in HX.
-    rewrite equiv_empty. done. solve_elem_of.
+    rewrite equiv_empty. done. set_solver.
   - intros X HX. setoid_rewrite elem_of_cons in HX.
-    rewrite (union_difference {[ x ]} X) by solve_elem_of.
-    apply Hadd. solve_elem_of. apply IH. solve_elem_of.
+    rewrite (union_difference {[ x ]} X) by set_solver.
+    apply Hadd. set_solver. apply IH. set_solver.
 Qed.
 Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R}
     (f : A → B → B) (b : B) `{!Proper ((=) ==> R ==> R) f}
diff --git a/prelude/fin_map_dom.v b/prelude/fin_map_dom.v
index b29fe3691..55e575f61 100644
--- a/prelude/fin_map_dom.v
+++ b/prelude/fin_map_dom.v
@@ -36,13 +36,13 @@ Proof.
 Qed.
 Lemma dom_empty {A} : dom D (@empty (M A) _) ≡ ∅.
 Proof.
-  split; intro; [|solve_elem_of].
+  split; intro; [|set_solver].
   rewrite elem_of_dom, lookup_empty. by inversion 1.
 Qed.
 Lemma dom_empty_inv {A} (m : M A) : dom D m ≡ ∅ → m = ∅.
 Proof.
   intros E. apply map_empty. intros. apply not_elem_of_dom.
-  rewrite E. solve_elem_of.
+  rewrite E. set_solver.
 Qed.
 Lemma dom_alter {A} f (m : M A) i : dom D (alter f i m) ≡ dom D m.
 Proof.
@@ -54,19 +54,19 @@ Lemma dom_insert {A} (m : M A) i x : dom D (<[i:=x]>m) ≡ {[ i ]} ∪ dom D m.
 Proof.
   apply elem_of_equiv. intros j. rewrite elem_of_union, !elem_of_dom.
   unfold is_Some. setoid_rewrite lookup_insert_Some.
-  destruct (decide (i = j)); solve_elem_of.
+  destruct (decide (i = j)); set_solver.
 Qed.
 Lemma dom_insert_subseteq {A} (m : M A) i x : dom D m ⊆ dom D (<[i:=x]>m).
-Proof. rewrite (dom_insert _). solve_elem_of. Qed.
+Proof. rewrite (dom_insert _). set_solver. Qed.
 Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X :
   X ⊆ dom D m → X ⊆ dom D (<[i:=x]>m).
 Proof. intros. transitivity (dom D m); eauto using dom_insert_subseteq. Qed.
 Lemma dom_singleton {A} (i : K) (x : A) : dom D {[i := x]} ≡ {[ i ]}.
-Proof. rewrite <-insert_empty, dom_insert, dom_empty; solve_elem_of. Qed.
+Proof. rewrite <-insert_empty, dom_insert, dom_empty; set_solver. Qed.
 Lemma dom_delete {A} (m : M A) i : dom D (delete i m) ≡ dom D m ∖ {[ i ]}.
 Proof.
   apply elem_of_equiv. intros j. rewrite elem_of_difference, !elem_of_dom.
-  unfold is_Some. setoid_rewrite lookup_delete_Some. solve_elem_of.
+  unfold is_Some. setoid_rewrite lookup_delete_Some. set_solver.
 Qed.
 Lemma delete_partial_alter_dom {A} (m : M A) i f :
   i ∉ dom D m → delete i (partial_alter f i m) = m.
diff --git a/prelude/hashset.v b/prelude/hashset.v
index c7282ec66..f71425666 100644
--- a/prelude/hashset.v
+++ b/prelude/hashset.v
@@ -155,7 +155,7 @@ Proof.
   - revert x. induction l as [|y l IH]; intros x; simpl.
     { by rewrite elem_of_empty. }
     rewrite elem_of_union, elem_of_singleton. intros [->|]; [left|right]; eauto.
-  - induction 1; solve_elem_of.
+  - induction 1; set_solver.
 Qed.
 Lemma NoDup_remove_dups_fast l : NoDup (remove_dups_fast l).
 Proof.
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 81782e266..4453110f5 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -1,7 +1,7 @@
 From program_logic Require Export hoare.
 From program_logic Require Import wsat ownership.
 Local Hint Extern 10 (_ ≤ _) => omega.
-Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of.
+Local Hint Extern 100 (@eq coPset _ _) => eassumption || set_solver.
 Local Hint Extern 10 (✓{_} _) =>
   repeat match goal with
   | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
diff --git a/program_logic/invariants.v b/program_logic/invariants.v
index 698827e6b..0ea33451f 100644
--- a/program_logic/invariants.v
+++ b/program_logic/invariants.v
@@ -2,9 +2,9 @@ From algebra Require Export base.
 From program_logic Require Import ownership.
 From program_logic Require Export namespaces pviewshifts weakestpre.
 Import uPred.
-Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
-Local Hint Extern 100 (@subseteq coPset _ _) => solve_elem_of.
-Local Hint Extern 100 (_ ∉ _) => solve_elem_of.
+Local Hint Extern 100 (@eq coPset _ _) => set_solver.
+Local Hint Extern 100 (@subseteq coPset _ _) => set_solver.
+Local Hint Extern 100 (_ ∉ _) => set_solver.
 Local Hint Extern 99 ({[ _ ]} ⊆ _) => apply elem_of_subseteq_singleton.
 
 (** Derived forms and lemmas about them. *)
@@ -41,16 +41,16 @@ Proof.
   rewrite -[R](idemp (∧)%I) {1}Hinv Hinner =>{Hinv Hinner R}.
   rewrite always_and_sep_l /inv sep_exist_r. apply exist_elim=>i.
   rewrite always_and_sep_l -assoc. apply const_elim_sep_l=>HiN.
-  rewrite -(fsa_open_close E (E ∖ {[encode i]})) //; last by solve_elem_of+.
-  (* Add this to the local context, so that solve_elem_of finds it. *)
+  rewrite -(fsa_open_close E (E ∖ {[encode i]})) //; last by set_solver+.
+  (* Add this to the local context, so that set_solver finds it. *)
   assert ({[encode i]} ⊆ nclose N) by eauto.
   rewrite (always_sep_dup (ownI _ _)).
   rewrite {1}pvs_openI !pvs_frame_r.
-  apply pvs_mask_frame_mono; [solve_elem_of..|].
+  apply pvs_mask_frame_mono; [set_solver..|].
   rewrite (comm _ (â–·_)%I) -assoc wand_elim_r fsa_frame_l.
-  apply fsa_mask_frame_mono; [solve_elem_of..|]. intros a.
+  apply fsa_mask_frame_mono; [set_solver..|]. intros a.
   rewrite assoc -always_and_sep_l pvs_closeI pvs_frame_r left_id.
-  apply pvs_mask_frame'; solve_elem_of.
+  apply pvs_mask_frame'; set_solver.
 Qed.
 
 (* Derive the concrete forms for pvs and wp, because they are useful. *)
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 51ea687ac..bd00e8cd4 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -1,7 +1,7 @@
 From program_logic Require Export weakestpre.
 From program_logic Require Import wsat ownership.
 Local Hint Extern 10 (_ ≤ _) => omega.
-Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
+Local Hint Extern 100 (@eq coPset _ _) => set_solver.
 Local Hint Extern 10 (✓{_} _) =>
   repeat match goal with
   | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
diff --git a/program_logic/namespaces.v b/program_logic/namespaces.v
index 34a457b8d..997197b21 100644
--- a/program_logic/namespaces.v
+++ b/program_logic/namespaces.v
@@ -56,21 +56,21 @@ Section ndisjoint.
 End ndisjoint.
 
 (* This tactic solves goals about inclusion and disjointness
-   of masks (i.e., coPsets) with solve_elem_of, taking
+   of masks (i.e., coPsets) with set_solver, taking
    disjointness of namespaces into account. *)
 (* TODO: This tactic is by far now yet as powerful as it should be.
    For example, given N1 ⊥ N2, it should be able to solve
    nclose (ndot N1 x) ∩ N2 ≡ ∅. It should also solve
    (ndot N x) ∩ (ndot N y) ≡ ∅ if x ≠ y is in the context or
    follows from [discriminate]. *)
-Ltac solve_elem_of_ndisj :=
+Ltac set_solver_ndisj :=
   repeat match goal with
          (* TODO: Restrict these to have type namespace *)
          | [ H : (?N1 ⊥ ?N2) |-_ ] => apply ndisj_disjoint in H
          end;
-  solve_elem_of.
+  set_solver.
 (* TODO: restrict this to match only if this is ⊆ of coPset *)
-Hint Extern 500 (_ ⊆ _) => solve_elem_of_ndisj : ndisj.
+Hint Extern 500 (_ ⊆ _) => set_solver_ndisj : ndisj.
 (* The hope is that registering these will suffice to solve most goals
    of the form N1 ⊥ N2.
    TODO: Can this prove x ≠ y if discriminate can? *)
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index d27181d85..b309e564f 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -2,8 +2,8 @@ From prelude Require Export co_pset.
 From program_logic Require Export model.
 From program_logic Require Import ownership wsat.
 Local Hint Extern 10 (_ ≤ _) => omega.
-Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
-Local Hint Extern 100 (_ ∉ _) => solve_elem_of.
+Local Hint Extern 100 (@eq coPset _ _) => set_solver.
+Local Hint Extern 100 (_ ∉ _) => set_solver.
 Local Hint Extern 10 (✓{_} _) =>
   repeat match goal with
   | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
@@ -93,7 +93,7 @@ Proof.
   intros r [|n] ? [? HP] rf [|k] Ef σ ? HE ?; try lia; exists ∅; split; [done|].
   rewrite left_id; apply wsat_close with P r.
   - apply ownI_spec, uPred_weaken with r (S n); auto.
-  - solve_elem_of +HE.
+  - set_solver +HE.
   - by rewrite -(left_id_L ∅ (∪) Ef).
   - apply uPred_weaken with r n; auto.
 Qed.
@@ -131,7 +131,7 @@ Import uPred.
 Global Instance pvs_mono' E1 E2 : Proper ((⊑) ==> (⊑)) (@pvs Λ Σ E1 E2).
 Proof. intros P Q; apply pvs_mono. Qed.
 Lemma pvs_trans' E P : pvs E E (pvs E E P) ⊑ pvs E E P.
-Proof. apply pvs_trans; solve_elem_of. Qed.
+Proof. apply pvs_trans; set_solver. Qed.
 Lemma pvs_strip_pvs E P Q : P ⊑ pvs E E Q → pvs E E P ⊑ pvs E E Q.
 Proof. move=>->. by rewrite pvs_trans'. Qed.
 Lemma pvs_frame_l E1 E2 P Q : (P ★ pvs E1 E2 Q) ⊑ pvs E1 E2 (P ★ Q).
@@ -159,7 +159,7 @@ Lemma pvs_mask_frame' E1 E1' E2 E2' P :
   E1' ⊆ E1 → E2' ⊆ E2 → E1 ∖ E1' = E2 ∖ E2' → pvs E1' E2' P ⊑ pvs E1 E2 P.
 Proof.
   intros HE1 HE2 HEE.
-  rewrite (pvs_mask_frame _ _ (E1 ∖ E1')); last solve_elem_of.
+  rewrite (pvs_mask_frame _ _ (E1 ∖ E1')); last set_solver.
   by rewrite {2}HEE -!union_difference_L.
 Qed. 
 
@@ -175,7 +175,7 @@ Proof. intros HE1 HE2 HEE ->. by apply pvs_mask_frame'. Qed.
    where that would be useful. *)
 Lemma pvs_trans3 E1 E2 Q :
   E2 ⊆ E1 → pvs E1 E2 (pvs E2 E2 (pvs E2 E1 Q)) ⊑ pvs E1 E1 Q.
-Proof. intros HE. rewrite !pvs_trans; solve_elem_of. Qed.
+Proof. intros HE. rewrite !pvs_trans; set_solver. Qed.
 
 Lemma pvs_mask_weaken E1 E2 P : E1 ⊆ E2 → pvs E1 E1 P ⊑ pvs E2 E2 P.
 Proof. auto using pvs_mask_frame'. Qed.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 6dab4f8bb..eff7bea2f 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -75,14 +75,14 @@ Section sts.
   Proof.
     intros HN. eapply sep_elim_True_r.
     { apply (own_alloc (sts_auth s (⊤ ∖ sts.tok s)) N).
-      apply sts_auth_valid; solve_elem_of. }
+      apply sts_auth_valid; set_solver. }
     rewrite pvs_frame_l. rewrite -(pvs_mask_weaken N E) //.
     apply pvs_strip_pvs.
     rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
     transitivity (▷ sts_inv γ φ ★ sts_own γ s (⊤ ∖ sts.tok s))%I.
     { rewrite /sts_inv -(exist_intro s) later_sep.
       rewrite [(_ ★ ▷ φ _)%I]comm -assoc. apply sep_mono_r.
-      by rewrite -later_intro -own_op sts_op_auth_frag_up; last solve_elem_of. }
+      by rewrite -later_intro -own_op sts_op_auth_frag_up; last set_solver. }
     rewrite (inv_alloc N) /sts_ctx pvs_frame_r.
     by rewrite always_and_sep_l.
   Qed.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index a268e20f4..1e8faf212 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -57,7 +57,7 @@ Proof.
 Qed.
 
 Lemma vs_transitive' E P Q R : ((P ={E}=> Q) ∧ (Q ={E}=> R)) ⊑ (P ={E}=> R).
-Proof. apply vs_transitive; solve_elem_of. Qed.
+Proof. apply vs_transitive; set_solver. Qed.
 Lemma vs_reflexive E P : P ={E}=> P.
 Proof. apply vs_alt, pvs_intro. Qed.
 
@@ -85,7 +85,7 @@ Proof.
 Qed.
 
 Lemma vs_mask_frame' E Ef P Q : Ef ∩ E = ∅ → (P ={E}=> Q) ⊑ (P ={E ∪ Ef}=> Q).
-Proof. intros; apply vs_mask_frame; solve_elem_of. Qed.
+Proof. intros; apply vs_mask_frame; set_solver. Qed.
 
 Lemma vs_open_close N E P Q R :
   nclose N ⊆ E →
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 1aa695b03..995154be8 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -1,9 +1,9 @@
 From program_logic Require Export pviewshifts.
 From program_logic Require Import wsat.
 Local Hint Extern 10 (_ ≤ _) => omega.
-Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of.
-Local Hint Extern 100 (_ ∉ _) => solve_elem_of.
-Local Hint Extern 100 (@subseteq coPset _ _ _) => solve_elem_of.
+Local Hint Extern 100 (@eq coPset _ _) => eassumption || set_solver.
+Local Hint Extern 100 (_ ∉ _) => set_solver.
+Local Hint Extern 100 (@subseteq coPset _ _ _) => set_solver.
 Local Hint Extern 10 (✓{_} _) =>
   repeat match goal with
   | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
diff --git a/program_logic/wsat.v b/program_logic/wsat.v
index 7fa49e5cd..91ec36a58 100644
--- a/program_logic/wsat.v
+++ b/program_logic/wsat.v
@@ -82,15 +82,15 @@ Lemma wsat_open n E σ r i P :
   wsat (S n) ({[i]} ∪ E) σ r → ∃ rP, wsat (S n) E σ (rP ⋅ r) ∧ P n rP.
 Proof.
   intros HiP Hi [rs [Hval Hσ HE Hwld]].
-  destruct (Hwld i P) as (rP&?&?); [solve_elem_of +|by apply lookup_wld_op_l|].
+  destruct (Hwld i P) as (rP&?&?); [set_solver +|by apply lookup_wld_op_l|].
   assert (rP ⋅ r ⋅ big_opM (delete i rs) ≡ r ⋅ big_opM rs) as Hr.
   { by rewrite (comm _ rP) -assoc big_opM_delete. }
   exists rP; split; [exists (delete i rs); constructor; rewrite ?Hr|]; auto.
   - intros j; rewrite lookup_delete_is_Some Hr.
-    generalize (HE j); solve_elem_of +Hi.
+    generalize (HE j); set_solver +Hi.
   - intros j P'; rewrite Hr=> Hj ?.
-    setoid_rewrite lookup_delete_ne; last (solve_elem_of +Hi Hj).
-    apply Hwld; [solve_elem_of +Hj|done].
+    setoid_rewrite lookup_delete_ne; last (set_solver +Hi Hj).
+    apply Hwld; [set_solver +Hj|done].
 Qed.
 Lemma wsat_close n E σ r i P rP :
   wld rP !! i ≡{S n}≡ Some (to_agree (Next (iProp_unfold P))) → i ∉ E →
@@ -102,8 +102,8 @@ Proof.
   { by rewrite (comm _ rP) -assoc big_opM_insert. }
   exists (<[i:=rP]>rs); constructor; rewrite ?Hr; auto.
   - intros j; rewrite Hr lookup_insert_is_Some=>-[?|[??]]; subst.
-    + rewrite !lookup_op HiP !op_is_Some; solve_elem_of +.
-    + destruct (HE j) as [Hj Hj']; auto; solve_elem_of +Hj Hj'.
+    + rewrite !lookup_op HiP !op_is_Some; set_solver +.
+    + destruct (HE j) as [Hj Hj']; auto; set_solver +Hj Hj'.
   - intros j P'; rewrite Hr elem_of_union elem_of_singleton=>-[?|?]; subst.
     + rewrite !lookup_wld_op_l ?HiP; auto=> HP.
       apply (inj Some), (inj to_agree), (inj Next), (inj iProp_unfold) in HP.
@@ -161,7 +161,7 @@ Proof.
     + by rewrite lookup_op lookup_singleton_ne // left_id.
   - by rewrite -assoc Hr /= left_id.
   - intros j; rewrite -assoc Hr; destruct (decide (j = i)) as [->|].
-    + rewrite /= !lookup_op lookup_singleton !op_is_Some; solve_elem_of +Hi.
+    + rewrite /= !lookup_op lookup_singleton !op_is_Some; set_solver +Hi.
     + rewrite lookup_insert_ne //.
       rewrite lookup_op lookup_singleton_ne // left_id; eauto.
   - intros j P'; rewrite -assoc Hr; destruct (decide (j=i)) as [->|].
-- 
GitLab