Improve and document split_and tactics.

theories/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.

theories/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.

theories/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|].

theories/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.

theories/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

theories/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. }