Separate out tactics into a new file, add some lemmas

lemmas.v

@@ -3,15 +3,7 @@ Require Export Coq.Lists.List.
 Require Export Arith.EqNat.
 Require Export Program.Equality.
 Require Export Coq.Logic.ProofIrrelevance.
-
-Ltac inverts n :=
-  match n with
-  | S ?n' => match goal with
-            | [ H : _ |- _ ] => try (inversion H; subst; inverts n')
-            | _ => idtac
-            end
-  | _ => idtac
-  end.
+Require Export tactics.
 
 Module E.
   Require Coq.Sets.Ensembles.
@@ -542,4 +534,4 @@ Proof.
 Qed.
 Hint Resolve In_set_from_list_In_list.
 
-Hint Resolve nth_error_In.
+Hint Resolve nth_error_In. Hint Resolve in_map_iff.

tactics.v

@@ -0,0 +1,31 @@
+Ltac decomp :=
+  repeat match goal with
+         | [ H : _ /\ _ |- _ ] => destruct H
+         | [ H : exists _, _ |- _ ] => destruct H
+         end.
+
+Ltac inverts n :=
+  match n with
+  | S ?n' => match goal with
+            | [ H : _ |- _ ] => try (inversion H; subst; inverts n')
+            | _ => idtac
+            end
+  | _ => idtac
+  end.
+
+Ltac split_rec n :=
+  match n with
+  | S ?n' => match goal with
+            |[ |- exists _, _ ] => eexists; split_rec n'
+            |[ |- _ /\ _] => split; split_rec n'
+            | _ => idtac
+            end
+  | 0 => idtac
+  end.
+
+Ltac subst_some :=
+  repeat match goal with
+         | [ G : ?x = Some ?y,
+                 H : ?x = Some ?z |- _ ] => rewrite G in H
+         | [ H : Some ?x = Some ?y |- _ ] => inversion H; subst; clear H
+         end.