From 42e3e6def1d2a4649e459d5c4dbae5e94e6fc91c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 19 Feb 2016 11:46:27 +0100
Subject: [PATCH] Improve and document split_and tactics.
---
theories/fin_maps.v | 2 +-
theories/finite.v | 6 +++---
theories/hashset.v | 6 +++---
theories/pretty.v | 2 +-
theories/tactics.v | 19 ++++++++++++++-----
theories/zmap.v | 2 +-
6 files changed, 23 insertions(+), 14 deletions(-)
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 7ac4cf42..a400ad49 100644
--- a/theories/fin_maps.v
+++ b/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.
diff --git a/theories/finite.v b/theories/finite.v
index ccb41220..c56dfcf8 100644
--- a/theories/finite.v
+++ b/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.
diff --git a/theories/hashset.v b/theories/hashset.v
index 30b42fa9..c18bdffe 100644
--- a/theories/hashset.v
+++ b/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|].
diff --git a/theories/pretty.v b/theories/pretty.v
index e7f0b645..2ca9129e 100644
--- a/theories/pretty.v
+++ b/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.
diff --git a/theories/tactics.v b/theories/tactics.v
index 939e9fab..544dc0a1 100644
--- a/theories/tactics.v
+++ b/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
diff --git a/theories/zmap.v b/theories/zmap.v
index 58a7059d..a0644bfa 100644
--- a/theories/zmap.v
+++ b/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. }
--
GitLab