Improve and document split_and tactics.

algebra/cmra.v

@@ -476,7 +476,7 @@ Section discrete.
   Qed.
   Definition discrete_extend_mixin : CMRAExtendMixin A.
   Proof.
-    intros n x y1 y2 ??; exists (y1,y2); split_ands; auto.
+    intros n x y1 y2 ??; exists (y1,y2); split_and?; auto.
     apply (timeless _), dist_le with n; auto with lia.
   Qed.
   Definition discreteRA : cmraT :=

algebra/dra.v

@@ -104,13 +104,13 @@ Definition validity_ra : RA (discreteC T).
 Proof.
   split.
   - intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
-    split; intros (?&?&?); split_ands';
+    split; intros (?&?&?); split_and!;
       first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
   - by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq.
   - intros ?? [??]; naive_solver.
   - intros x1 x2 [? Hx] y1 y2 [? Hy];
       split; simpl; [|by intros (?&?&?); rewrite Hx // Hy].
-    split; intros (?&?&z&?&?); split_ands'; try tauto.
+    split; intros (?&?&z&?&?); split_and!; try tauto.
     + exists z. by rewrite -Hy // -Hx.
     + exists z. by rewrite Hx ?Hy; tauto.
   - intros [x px ?] [y py ?] [z pz ?]; split; simpl;
@@ -135,7 +135,7 @@ Lemma validity_update (x y : validityRA) :
   (∀ z, ✓ x → ✓ z → validity_car x ⊥ z → ✓ y ∧ validity_car y ⊥ z) → x ~~> y.
 Proof.
   intros Hxy. apply discrete_update.
-  intros z (?&?&?); split_ands'; try eapply Hxy; eauto.
+  intros z (?&?&?); split_and!; try eapply Hxy; eauto.
 Qed.
 
 Lemma to_validity_valid (x : A) :

algebra/iprod.v

@@ -156,7 +156,7 @@ Section iprod_cmra.
     intros n f f1 f2 Hf Hf12.
     set (g x := cmra_extend_op n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)).
     exists ((λ x, (proj1_sig (g x)).1), (λ x, (proj1_sig (g x)).2)).
-    split_ands; intros x; apply (proj2_sig (g x)).
+    split_and?; intros x; apply (proj2_sig (g x)).
   Qed.
   Canonical Structure iprodRA : cmraT :=
     CMRAT iprod_cofe_mixin iprod_cmra_mixin iprod_cmra_extend_mixin.

algebra/option.v

@@ -75,7 +75,7 @@ Proof.
   - intros [mz Hmz].
     destruct mx as [x|]; [right|by left].
     destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
-    destruct mz as [z|]; inversion_clear Hmz; split_ands; auto;
+    destruct mz as [z|]; inversion_clear Hmz; split_and?; auto;
       cofe_subst; eauto using cmra_includedN_l.
   - intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
     by exists (Some z); constructor.

algebra/sts.v

@@ -101,7 +101,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_ands; 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.
@@ -240,7 +240,7 @@ Proof.
     + rewrite (up_closed (up _ _)); auto using closed_up with sts.
     + 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.
+  - 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.
@@ -326,7 +326,7 @@ Lemma sts_op_auth_frag s S T :
 Proof.
   intros; split; [split|constructor; set_solver]; simpl.
   - intros (?&?&?); by apply closed_disjoint' with S.
-  - intros; split_ands. set_solver+. done. constructor; set_solver.
+  - intros; split_and?. 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.
@@ -381,7 +381,7 @@ when we have RAs back *)
     move:(EQ' Hcl2)=>{EQ'} EQ. inversion_clear EQ as [|? ? ? ? HT HS].
     destruct Hv as [Hv _]. move:(Hv Hcl2)=>{Hv} [/= Hcl1  [Hclf Hdisj]].
     apply Hvf in Hclf. simpl in Hclf. clear Hvf.
-    inversion_clear Hdisj. split; last (exists Tf; split_ands); [done..|].
+    inversion_clear Hdisj. split; last (exists Tf; split_and?); [done..|].
     apply (anti_symm (⊆)).
     + move=>s HS2. apply elem_of_intersection. split; first by apply HS.
       by apply subseteq_up_set.
@@ -392,7 +392,7 @@ when we have RAs back *)
   - intros (Hcl1 & Tf & Htk & Hf & Hs).
     exists (sts_frag (up_set S2 Tf) Tf).
     split; first split; simpl;[|done|].
-    + intros _. split_ands; first done.
+    + intros _. split_and?; first done.
       * apply closed_up_set; last by eapply closed_ne.
         move=>s Hs2. move:(closed_disjoint _ _ Hcl2 _ Hs2).
         set_solver +Htk.
@@ -404,7 +404,7 @@ 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 sts_frag_included; split_ands; auto.
-  exists ∅; split_ands; done || set_solver+.
+  intros. apply sts_frag_included; split_and?; auto.
+  exists ∅; split_and?; done || set_solver+.
 Qed.
 End stsRA.

algebra/upred.v

@@ -143,7 +143,7 @@ Next Obligation.
   assert (∃ x2', y ≡{n2}≡ x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?).
   { destruct Hxy as [z Hy]; exists (x2 ⋅ z); split; eauto using cmra_included_l.
     apply dist_le with n1; auto. by rewrite (assoc op) -Hx Hy. }
-  clear Hxy; cofe_subst y; exists x1, x2'; split_ands; [done| |].
+  clear Hxy; cofe_subst y; exists x1, x2'; split_and?; [done| |].
   - apply uPred_weaken with n1 x1; eauto using cmra_validN_op_l.
   - apply uPred_weaken with n1 x2; eauto using cmra_validN_op_r.
 Qed.
@@ -273,7 +273,7 @@ Global Instance impl_proper :
 Global Instance sep_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_sep M).
 Proof.
   intros P P' HP Q Q' HQ n' x ??; split; intros (x1&x2&?&?&?); cofe_subst x;
-    exists x1, x2; split_ands; try (apply HP || apply HQ);
+    exists x1, x2; split_and?; try (apply HP || apply HQ);
     eauto using cmra_validN_op_l, cmra_validN_op_r.
 Qed.
 Global Instance sep_proper :
@@ -564,17 +564,17 @@ Qed.
 Global Instance sep_assoc : Assoc (≡) (@uPred_sep M).
 Proof.
   intros P Q R n x ?; split.
-  - intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1 ⋅ y1), y2; split_ands; auto.
+  - intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1 ⋅ y1), y2; split_and?; auto.
     + by rewrite -(assoc op) -Hy -Hx.
     + by exists x1, y1.
-  - intros (x1&x2&Hx&(y1&y2&Hy&?&?)&?); exists y1, (y2 ⋅ x2); split_ands; auto.
+  - intros (x1&x2&Hx&(y1&y2&Hy&?&?)&?); exists y1, (y2 ⋅ x2); split_and?; auto.
     + by rewrite (assoc op) -Hy -Hx.
     + by exists y2, x2.
 Qed.
 Lemma wand_intro_r P Q R : (P ★ Q) ⊑ R → P ⊑ (Q -★ R).
 Proof.
   intros HPQR n x ?? n' x' ???; apply HPQR; auto.
-  exists x, x'; split_ands; auto.
+  exists x, x'; split_and?; auto.
   eapply uPred_weaken with n x; eauto using cmra_validN_op_l.
 Qed.
 Lemma wand_elim_l P Q : ((P -★ Q) ★ P) ⊑ Q.

barrier/barrier.v

@@ -267,7 +267,7 @@ Section spec.
       (∀ l P Q, (P -★ Q) ⊑ (recv l P -★ recv l Q)).
   Proof.
     intros HN. exists (λ l, CofeMor (recv N heapN l)). exists (λ l, CofeMor (send N heapN l)).
-    split_ands; cbn.
+    split_and?; cbn.
     - intros. apply: always_intro. apply impl_intro_l. rewrite -newchan_spec.
       rewrite comm always_and_sep_r. apply sep_mono_r. apply forall_intro=>l.
       apply wand_intro_l. rewrite right_id -(exist_intro l) const_equiv // left_id.

prelude/fin_maps.v

@@ -476,7 +476,7 @@ Lemma insert_subset_inv {A} (m1 m2 : M A) i x :
   m1 !! i = None → <[i:=x]> m1 ⊂ m2 →
   ∃ m2', m2 = <[i:=x]>m2' ∧ m1 ⊂ m2' ∧ m2' !! i = None.
 Proof.
-  intros Hi Hm1m2. exists (delete i m2). split_ands.
+  intros Hi Hm1m2. exists (delete i m2). split_and?.
   - rewrite insert_delete. done. eapply lookup_weaken, strict_include; eauto.
     by rewrite lookup_insert.
   - eauto using insert_delete_subset.

prelude/finite.v

@@ -220,7 +220,7 @@ Proof. done. Qed.
 Program Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type :=
   {| enum := (inl <$> enum A) ++ (inr <$> enum B) |}.
 Next Obligation.
-  intros. apply NoDup_app; split_ands.
+  intros. apply NoDup_app; split_and?.
   - apply (NoDup_fmap_2 _). by apply NoDup_enum.
   - intro. rewrite !elem_of_list_fmap. intros (?&?&?) (?&?&?); congruence.
   - apply (NoDup_fmap_2 _). by apply NoDup_enum.
@@ -237,7 +237,7 @@ Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
 Next Obligation.
   intros ??????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
   { constructor. }
-  apply NoDup_app; split_ands.
+  apply NoDup_app; split_and?.
   - by apply (NoDup_fmap_2 _), NoDup_enum.
   - intros [? y]. rewrite elem_of_list_fmap. intros (?&?&?); simplify_eq.
     clear IH. induction Hxs as [|x' xs ?? IH]; simpl.
@@ -271,7 +271,7 @@ Next Obligation.
   intros ????. induction n as [|n IH]; simpl; [apply NoDup_singleton |].
   revert IH. generalize (list_enum (enum A) n). intros l Hl.
   induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl; auto; [constructor |].
-  apply NoDup_app; split_ands.
+  apply NoDup_app; split_and?.
   - by apply (NoDup_fmap_2 _).
   - intros [k1 Hk1]. clear Hxs IH. rewrite elem_of_list_fmap.
     intros ([k2 Hk2]&?&?) Hxk2; simplify_eq/=. destruct Hx. revert Hxk2.

prelude/hashset.v

@@ -85,7 +85,7 @@ Proof.
       rewrite elem_of_list_intersection in Hx; naive_solver. }
     intros [(l&?&?) (k&?&?)]. assert (x ∈ list_intersection l k)
       by (by rewrite elem_of_list_intersection).
-    exists (list_intersection l k); split; [exists l, k|]; split_ands; auto.
+    exists (list_intersection l k); split; [exists l, k|]; split_and?; auto.
     by rewrite option_guard_True by eauto using elem_of_not_nil.
   - unfold elem_of, hashset_elem_of, intersection, hashset_intersection.
     intros [m1 ?] [m2 ?] x; simpl.
@@ -95,7 +95,7 @@ Proof.
     intros [(l&?&?) Hm2]; destruct (m2 !! hash x) as [k|] eqn:?; eauto.
     destruct (decide (x ∈ k)); [destruct Hm2; eauto|].
     assert (x ∈ list_difference l k) by (by rewrite elem_of_list_difference).
-    exists (list_difference l k); split; [right; exists l,k|]; split_ands; auto.
+    exists (list_difference l k); split; [right; exists l,k|]; split_and?; auto.
     by rewrite option_guard_True by eauto using elem_of_not_nil.
   - unfold elem_of at 2, hashset_elem_of, elements, hashset_elems.
     intros [m Hm] x; simpl. setoid_rewrite elem_of_list_bind. split.
@@ -107,7 +107,7 @@ Proof.
     rewrite map_Forall_to_list in Hm. generalize (NoDup_fst_map_to_list m).
     induction Hm as [|[n l] m' [??]];
       csimpl; inversion_clear 1 as [|?? Hn]; [constructor|].
-    apply NoDup_app; split_ands; eauto.
+    apply NoDup_app; split_and?; eauto.
     setoid_rewrite elem_of_list_bind; intros x ? ([n' l']&?&?); simpl in *.
     assert (hash x = n ∧ hash x = n') as [??]; subst.
     { split; [eapply (Forall_forall (λ x, hash x = n) l); eauto|].

prelude/pretty.v

@@ -57,7 +57,7 @@ Proof.
   { intros -> Hlen; edestruct help; rewrite Hlen; simpl; lia. }
   { intros <- Hlen; edestruct help; rewrite <-Hlen; simpl; lia. }
   intros Hs Hlen; apply IH in Hs; destruct Hs;
-    simplify_eq/=; split_ands'; auto using N.div_lt_upper_bound with lia.
+    simplify_eq/=; split_and?; auto using N.div_lt_upper_bound with lia.
   rewrite (N.div_mod x 10), (N.div_mod y 10) by done.
   auto using N.mod_lt with f_equal.
 Qed.

prelude/tactics.v

@@ -54,11 +54,20 @@ Ltac done :=
 Tactic Notation "by" tactic(tac) :=
   tac; done.
 
-(** Whereas the [split] tactic splits any inductive with one constructor, the
-tactic [split_and] only splits a conjunction. *)
-Ltac split_and := match goal with |- _ ∧ _ => split end.
-Ltac split_ands := repeat split_and.
-Ltac split_ands' := repeat (hnf; split_and).
+(** Tactics for splitting conjunctions:
+
+- [split_and] : split the goal if is syntactically of the shape [_ ∧ _]
+- [split_ands?] : split the goal repeatedly (perhaps zero times) while it is
+  of the shape [_ ∧ _].
+- [split_ands!] : works similarly, but at least one split should succeed. In
+  order to do so, it will head normalize the goal first to possibly expose a
+  conjunction.
+
+Note that [split_and] differs from [split] by only splitting conjunctions. The
+[split] tactic splits any inductive with one constructor. *)
+Tactic Notation "split_and" := match goal with |- _ ∧ _ => split end.
+Tactic Notation "split_and" "?" := repeat split_and.
+Tactic Notation "split_and" "!" := hnf; split_and; split_and?.
 
 (** The tactic [case_match] destructs an arbitrary match in the conclusion or
 assumptions, and generates a corresponding equality. This tactic is best used

prelude/zmap.v

@@ -64,7 +64,7 @@ Proof.
   - intros ? [o t t']; unfold map_to_list; simpl.
     assert (NoDup ((prod_map Z.pos id <$> map_to_list t) ++
       prod_map Z.neg id <$> map_to_list t')).
-    { apply NoDup_app; split_ands.
+    { apply NoDup_app; split_and?.
       - apply (NoDup_fmap_2 _), NoDup_map_to_list.
       - intro. rewrite !elem_of_list_fmap. naive_solver.
       - apply (NoDup_fmap_2 _), NoDup_map_to_list. }

program_logic/adequacy.v

@@ -74,7 +74,7 @@ Proof.
   intros Hv ? [k ?]%rtc_nsteps.
   eapply ht_adequacy_steps with (r1 := (Res ∅ (Excl σ1) (Some m))); eauto; [|].
   { by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN. }
-  exists (Res ∅ (Excl σ1) ∅), (Res ∅ ∅ (Some m)); split_ands.
+  exists (Res ∅ (Excl σ1) ∅), (Res ∅ ∅ (Some m)); split_and?.
   - by rewrite Res_op ?left_id ?right_id.
   - by rewrite /uPred_holds /=.
   - by apply ownG_spec.

program_logic/lifting.v

@@ -38,7 +38,7 @@ Proof.
     as (r'&(r1'&r2'&?&?&?)&?); auto; cofe_subst r'.
   { split. destruct k; try eapply Hstep; eauto. apply ownP_spec; auto. }
   { rewrite (comm _ r2) -assoc; eauto using wsat_le. }
-  by exists r1', r2'; split_ands; [| |by intros ? ->].
+  by exists r1', r2'; split_and?; [| |by intros ? ->].
 Qed.
 
 Lemma wp_lift_pure_step E (φ : expr Λ → option (expr Λ) → Prop) Φ e1 :
@@ -51,7 +51,7 @@ Proof.
   intros rf k Ef σ1 ???; split; [done|]. destruct n as [|n]; first lia.
   intros e2 σ2 ef ?; destruct (Hstep σ1 e2 σ2 ef); auto; subst.
   destruct (Hwp e2 ef k r) as (r1&r2&Hr&?&?); auto.
-  exists r1,r2; split_ands; [rewrite -Hr| |by intros ? ->]; eauto using wsat_le.
+  exists r1,r2; split_and?; [rewrite -Hr| |by intros ? ->]; eauto using wsat_le.
 Qed.
 
 (** Derived lifting lemmas. *)

program_logic/namespaces.v

@@ -39,7 +39,7 @@ Section ndisjoint.
   Lemma ndot_preserve_disjoint_l N1 N2 x : N1 ⊥ N2 → ndot N1 x ⊥ N2.
   Proof.
     intros (N1' & N2' & Hpr1 & Hpr2 & Hl & Hne). exists N1', N2'.
-    split_ands; try done; []. by apply suffix_of_cons_r.
+    split_and?; try done; []. by apply suffix_of_cons_r.
   Qed.
 
   Lemma ndot_preserve_disjoint_r N1 N2 x : N1 ⊥ N2 → N1 ⊥ ndot N2 x .

program_logic/ownership.v

@@ -79,7 +79,7 @@ Proof.
   - intros [(P'&Hi&HP) _]; rewrite Hi.
     by apply Some_dist, symmetry, agree_valid_includedN,
       (cmra_included_includedN _ P'),HP; apply map_lookup_validN with (wld r) i.
-  - intros ?; split_ands; try apply cmra_empty_leastN; eauto.
+  - intros ?; split_and?; try apply cmra_empty_leastN; eauto.
 Qed.
 Lemma ownP_spec r n σ : ✓{n} r → (ownP σ) n r ↔ pst r ≡{n}≡ Excl σ.
 Proof.

program_logic/pviewshifts.v

@@ -44,7 +44,7 @@ Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Λ Σ E1 E2).
 Proof.
   intros P Q HPQ r1 n' ??; simpl; split; intros HP rf k Ef σ ???;
     destruct (HP rf k Ef σ) as (r2&?&?); auto;
-    exists r2; split_ands; auto; apply HPQ; eauto.
+    exists r2; split_and?; auto; apply HPQ; eauto.
 Qed.
 Global Instance pvs_proper E1 E2 : Proper ((≡) ==> (≡)) (@pvs Λ Σ E1 E2).
 Proof. apply ne_proper, _. Qed.
@@ -84,7 +84,7 @@ Proof.
   destruct (HP (r2 ⋅ rf) k Ef σ) as (r'&?&?); eauto.
   { by rewrite assoc -(dist_le _ _ _ _ Hr); last lia. }
   exists (r' ⋅ r2); split; last by rewrite -assoc.
-  exists r', r2; split_ands; auto; apply uPred_weaken with n r2; auto.
+  exists r', r2; split_and?; auto; apply uPred_weaken with n r2; auto.
 Qed.
 Lemma pvs_openI i P : ownI i P ⊑ (|={{[i]},∅}=> ▷ P).
 Proof.

program_logic/resources.v

@@ -84,14 +84,14 @@ Lemma res_included (r1 r2 : res Λ Σ A) :
   r1 ≼ r2 ↔ wld r1 ≼ wld r2 ∧ pst r1 ≼ pst r2 ∧ gst r1 ≼ gst r2.
 Proof.
   split; [|by intros ([w ?]&[σ ?]&[m ?]); exists (Res w σ m)].
-  intros [r Hr]; split_ands;
+  intros [r Hr]; split_and?;
     [exists (wld r)|exists (pst r)|exists (gst r)]; apply Hr.
 Qed.
 Lemma res_includedN (r1 r2 : res Λ Σ A) n :
   r1 ≼{n} r2 ↔ wld r1 ≼{n} wld r2 ∧ pst r1 ≼{n} pst r2 ∧ gst r1 ≼{n} gst r2.
 Proof.
   split; [|by intros ([w ?]&[σ ?]&[m ?]); exists (Res w σ m)].
-  intros [r Hr]; split_ands;
+  intros [r Hr]; split_and?;
     [exists (wld r)|exists (pst r)|exists (gst r)]; apply Hr.
 Qed.
 Definition res_cmra_mixin : CMRAMixin (res Λ Σ A).
@@ -99,18 +99,18 @@ Proof.
   split.
   - by intros n x [???] ? [???]; constructor; simpl in *; cofe_subst.
   - by intros n [???] ? [???]; constructor; simpl in *; cofe_subst.
-  - by intros n [???] ? [???] (?&?&?); split_ands'; simpl in *; cofe_subst.
+  - by intros n [???] ? [???] (?&?&?); split_and!; simpl in *; cofe_subst.
   - by intros n [???] ? [???] [???] ? [???];
       constructor; simpl in *; cofe_subst.
-  - by intros n ? (?&?&?); split_ands'; apply cmra_validN_S.
+  - by intros n ? (?&?&?); split_and!; apply cmra_validN_S.
   - by intros ???; constructor; rewrite /= assoc.
   - by intros ??; constructor; rewrite /= comm.
   - by intros ?; constructor; rewrite /= cmra_unit_l.
   - by intros ?; constructor; rewrite /= cmra_unit_idemp.
   - intros n r1 r2; rewrite !res_includedN.
-    by intros (?&?&?); split_ands'; apply cmra_unit_preservingN.
+    by intros (?&?&?); split_and!; apply cmra_unit_preservingN.
   - intros n r1 r2 (?&?&?);
-      split_ands'; simpl in *; eapply cmra_validN_op_l; eauto.
+      split_and!; simpl in *; eapply cmra_validN_op_l; eauto.
   - intros n r1 r2; rewrite res_includedN; intros (?&?&?).
     by constructor; apply cmra_op_minus.
 Qed.
@@ -127,7 +127,7 @@ Canonical Structure resRA : cmraT :=
 Global Instance res_cmra_identity : CMRAIdentity resRA.
 Proof.
   split.
-  - intros n; split_ands'; apply cmra_empty_valid.
+  - intros n; split_and!; apply cmra_empty_valid.
   - by split; rewrite /= left_id.
   - apply _.
 Qed.
@@ -205,8 +205,8 @@ Instance res_map_cmra_monotone {Λ Σ} {A B : cofeT} (f : A -n> B) :
 Proof.
   split.
   - by intros n r1 r2; rewrite !res_includedN;
-      intros (?&?&?); split_ands'; simpl; try apply includedN_preserving.
-  - by intros n r (?&?&?); split_ands'; simpl; try apply validN_preserving.
+      intros (?&?&?); split_and!; simpl; try apply includedN_preserving.
+  - by intros n r (?&?&?); split_and!; simpl; try apply validN_preserving.
 Qed.
 Definition resC_map {Λ Σ A B} (f : A -n> B) : resC Λ Σ A -n> resC Λ Σ B :=
   CofeMor (res_map f : resRA Λ Σ A → resRA Λ Σ B).

program_logic/weakestpre.v

@@ -46,7 +46,7 @@ Next Obligation.
     destruct (Hgo (rf' ⋅ rf) k Ef σ1) as [Hsafe Hstep];
       rewrite ?assoc -?Hr; auto; constructor; [done|].
     intros e2 σ2 ef ?; destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
-    exists r2, (r2' ⋅ rf'); split_ands; eauto 10 using (IH k), cmra_included_l.
+    exists r2, (r2' ⋅ rf'); split_and?; eauto 10 using (IH k), cmra_included_l.
     by rewrite -!assoc (assoc _ r2).
 Qed.
 Instance: Params (@wp) 4.
@@ -73,7 +73,7 @@ Proof.
   destruct (Hgo rf k Ef σ1) as [Hsafe Hstep]; auto.
   split; [done|intros e2 σ2 ef ?].
   destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
-  exists r2, r2'; split_ands; [|eapply IH|]; eauto.
+  exists r2, r2'; split_and?; [|eapply IH|]; eauto.
 Qed.
 Global Instance wp_proper E e :
   Proper (pointwise_relation _ (≡) ==> (≡)) (@wp Λ Σ E e).
@@ -92,7 +92,7 @@ Proof.
   destruct (Hgo rf k ((E2 ∖ E1) ∪ Ef) σ1) as [Hsafe Hstep]; rewrite -?HE'; auto.
   split; [done|intros e2 σ2 ef ?].
   destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
-  exists r2, r2'; split_ands; [rewrite HE'|eapply IH|]; eauto.
+  exists r2, r2'; split_and?; [rewrite HE'|eapply IH|]; eauto.
 Qed.
 
 Lemma wp_value_inv E Φ v n r : wp E (of_val v) Φ n r → (|={E}=> Φ v)%I n r.
@@ -126,7 +126,7 @@ Proof.
   destruct (wp_step_inv E Ef (pvs E E ∘ Φ) e k n σ1 r rf) as [? Hstep]; auto.
   split; [done|intros e2 σ2 ef ?].
   destruct (Hstep e2 σ2 ef) as (r2&r2'&?&Hwp'&?); auto.
-  exists r2, r2'; split_ands; [|apply (IH k)|]; auto.
+  exists r2, r2'; split_and?; [|apply (IH k)|]; auto.
 Qed.
 Lemma wp_atomic E1 E2 e Φ :
   E2 ⊆ E1 → atomic e → (|={E1,E2}=> wp E2 e (λ v, |={E2,E1}=> Φ v)) ⊑ wp E1 e Φ.
@@ -142,7 +142,7 @@ Proof.
     [|destruct (atomic_step e σ1 e2 σ2 ef); naive_solver].
   apply pvs_trans in Hvs'; auto.
   destruct (Hvs' (r2' ⋅ rf) k Ef σ2) as (r3&[]); rewrite ?assoc; auto.
-  exists r3, r2'; split_ands; last done.
+  exists r3, r2'; split_and?; last done.
   - by rewrite -assoc.
   - constructor; apply pvs_intro; auto.
 Qed.
@@ -158,7 +158,7 @@ Proof.
   { by rewrite assoc. }
   split; [done|intros e2 σ2 ef ?].
   destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
-  exists (r2 ⋅ rR), r2'; split_ands; auto.
+  exists (r2 ⋅ rR), r2'; split_and?; auto.
   - by rewrite -(assoc _ r2)
       (comm _ rR) !assoc -(assoc _ _ rR).
   - apply IH; eauto using uPred_weaken.
@@ -172,9 +172,9 @@ Proof.
   destruct (Hgo (rR⋅rf) k Ef σ1) as [Hsafe Hstep];rewrite ?assoc;auto.
   split; [done|intros e2 σ2 ef ?].
   destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto.
-  exists (r2 ⋅ rR), r2'; split_ands; auto.
+  exists (r2 ⋅ rR), r2'; split_and?; auto.
   - by rewrite -(assoc _ r2) (comm _ rR) !assoc -(assoc _ _ rR).
-  - apply wp_frame_r; [auto|exists r2, rR; split_ands; auto].
+  - apply wp_frame_r; [auto|exists r2, rR; split_and?; auto].
     eapply uPred_weaken with n rR; eauto.
 Qed.
 Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
@@ -190,7 +190,7 @@ Proof.
   intros e2 σ2 ef ?.
   destruct (fill_step_inv e σ1 e2 σ2 ef) as (e2'&->&?); auto.
   destruct (Hstep e2' σ2 ef) as (r2&r2'&?&?&?); auto.
-  exists r2, r2'; split_ands; try eapply IH; eauto.
+  exists r2, r2'; split_and?; try eapply IH; eauto.
 Qed.
 
 (** * Derived rules *)

program_logic/wsat.v

@@ -72,7 +72,7 @@ Lemma wsat_init k E σ mm : ✓{S k} mm → wsat (S k) E σ (Res ∅ (Excl σ) m
 Proof.
   intros Hv. exists ∅; constructor; auto.
   - rewrite big_opM_empty right_id.
-    split_ands'; try (apply cmra_valid_validN, ra_empty_valid);
+    split_and!; try (apply cmra_valid_validN, ra_empty_valid);
       constructor || apply Hv.
   - by intros i; rewrite lookup_empty=>-[??].
   - intros i P ?; rewrite /= left_id lookup_empty; inversion_clear 1.
@@ -123,7 +123,7 @@ Proof.
     apply (inj Excl).
     by rewrite -Hpst_r -Hpst -assoc Hpst' right_id. }
   split; [done|exists rs].
-  by constructor; split_ands'; try (rewrite /= -assoc Hpst').
+  by constructor; first split_and!; try rewrite /= -assoc Hpst'.
 Qed.
 Lemma wsat_update_gst n E σ r rf mm1 (P : iGst Λ Σ → Prop) :
   mm1 ≼{S n} gst r → mm1 ~~>: (λ mm2, default False mm2 P) →
@@ -132,7 +132,8 @@ Proof.
   intros [mf Hr] Hup [rs [(?&?&?) Hσ HE Hwld]].
   destruct (Hup (S n) (mf ⋅ gst (rf ⋅ big_opM rs))) as ([m2|]&?&Hval'); try done.
   { by rewrite /= (assoc _ mm1) -Hr assoc. }
-  exists m2; split; [exists rs; split; split_ands'; auto|done].
+  exists m2; split; [exists rs|done].
+  by constructor; first split_and!; auto.
 Qed.
 Lemma wsat_alloc n E1 E2 σ r P rP :
   ¬set_finite E1 → P n rP → wsat (S n) (E1 ∪ E2) σ (rP ⋅ r) →
@@ -153,9 +154,9 @@ Proof.
     rewrite /= !lookup_op !op_is_Some -!not_eq_None_Some; tauto. }
   assert (r ⋅ big_opM (<[i:=rP]> rs) ≡ rP ⋅ r ⋅ big_opM rs) as Hr.
   { by rewrite (comm _ rP) -assoc big_opM_insert. }
-  exists i; split_ands; [exists (<[i:=rP]>rs); constructor| |]; auto.
+  exists i; split_and?; [exists (<[i:=rP]>rs); constructor| |]; auto.
   - destruct Hval as (?&?&?);  rewrite -assoc Hr.
-    split_ands'; rewrite /= ?left_id; [|eauto|eauto].
+    split_and!; rewrite /= ?left_id; [|eauto|eauto].
     intros j; destruct (decide (j = i)) as [->|].
     + by rewrite !lookup_op Hri HrPi Hrsi !right_id lookup_singleton.
     + by rewrite lookup_op lookup_singleton_ne // left_id.