Add split_andb tactic

1 files changed, 12 insertions, 0 deletions

diff --git a/src/Util/Bool.v b/src/Util/Bool.v
index a59cf53f0..948e87417 100644
--- a/src/Util/Bool.v
+++ b/src/Util/Bool.v
@@ -57,3 +57,15 @@ Proof.
   intros H; apply reflect_iff in H; intro b'; destruct b, b';
     intuition congruence.
 Qed.
+
+Definition andb_prop : forall a b : bool, a && b = true -> a = true /\ b = true. (* transparent version *)
+Proof. destruct a, b; simpl; split; try reflexivity; assumption. Defined.
+
+Ltac split_andb :=
+  repeat match goal with
+         | [ H : andb _ _ = true |- _ ] => apply andb_prop in H; destruct H
+         | [ H : is_true (andb ?x ?y) |- _ ]
+           => apply andb_prop in H;
+              change (is_true x /\ is_true y) in H;
+              destruct H
+         end.