From 614de6adad919e7601cb0f2ff03696e09ebc3dc6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 17 Aug 2016 12:58:30 -0700 Subject: Add simplify_projections to Util.Tactics --- src/Util/Tactics.v | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) (limited to 'src/Util/Tactics.v') 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). -- cgit v1.2.3