Add simplify_projections to Util.Tactics

1 files changed, 33 insertions, 0 deletions

diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index a318f469b..be777512c 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -398,3 +398,36 @@ Ltac eforward_step H :=
   end.
 Ltac forward H := try (forward_step H; [ forward H | .. ]).
 Ltac eforward H := try (eforward_step H; [ eforward H | .. ]).
+
+(** [simplify_projections] reduces terms of the form [fst (_, _)] (for
+    any projection from [prod], [sig], [sigT], or [and]) *)
+Ltac pre_simplify_projection proj proj' uproj' :=
+  pose proj as proj';
+  pose proj as uproj';
+  unfold proj in uproj';
+  change proj with proj'.
+Ltac do_simplify_projection_2Targ_4carg_step proj proj' uproj' construct :=
+  change proj' with uproj' at 1;
+  lazymatch goal with
+  | [ |- appcontext[uproj' _ _ (construct _ _ _ _)] ]
+    => unfold uproj'
+  | _ => change uproj' with proj
+  end.
+Ltac do_simplify_projection_2Targ_4carg proj proj' uproj' construct :=
+  repeat do_simplify_projection_2Targ_4carg_step proj proj' uproj' construct.
+Ltac simplify_projection_2Targ_4carg proj construct :=
+  let proj' := fresh "proj" in
+  let uproj' := fresh "proj" in
+  pre_simplify_projection proj proj' uproj';
+  do_simplify_projection_2Targ_4carg proj proj' uproj' construct;
+  clear proj' uproj'.
+
+Ltac simplify_projections :=
+  repeat (simplify_projection_2Targ_4carg @fst @pair
+          || simplify_projection_2Targ_4carg @snd @pair
+          || simplify_projection_2Targ_4carg @proj1_sig @exist
+          || simplify_projection_2Targ_4carg @proj2_sig @exist
+          || simplify_projection_2Targ_4carg @projT1 @existT
+          || simplify_projection_2Targ_4carg @projT2 @existT
+          || simplify_projection_2Targ_4carg @proj1 @conj
+          || simplify_projection_2Targ_4carg @proj2 @conj).