From 2ad847c3276518b9b848b853d77f7261bcff5c04 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Thu, 3 Mar 2016 14:31:27 +0100
Subject: [PATCH] New destruct_and tactic that also deals with Boolean ands.
Contrary to destruct_conj from Program.
---
theories/tactics.v | 15 ++++++++++++++-
1 file changed, 14 insertions(+), 1 deletion(-)
diff --git a/theories/tactics.v b/theories/tactics.v
index 6ba160c..dd3f60c 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -69,10 +69,23 @@ Tactic Notation "etrans" := etransitivity.
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" :=
+ match goal with
+ | |- _ ∧ _ => split
+ | |- Is_true (_ && _) => apply andb_True; split
+ end.
Tactic Notation "split_and" "?" := repeat split_and.
Tactic Notation "split_and" "!" := hnf; split_and; split_and?.
+Tactic Notation "destruct_and" "?" :=
+ repeat match goal with
+ | H : False |- _ => destruct H
+ | H : _ ∧ _ |- _ => destruct H
+ | H : Is_true (bool_decide _) |- _ => apply (bool_decide_unpack _) in H
+ | H : Is_true (_ && _) |- _ => apply andb_True in H; destruct H
+ end.
+Tactic Notation "destruct_and" "!" := progress (destruct_and?).
+
(** The tactic [case_match] destructs an arbitrary match in the conclusion or
assumptions, and generates a corresponding equality. This tactic is best used
together with the [repeat] tactical. *)
--
GitLab