diff options
Diffstat (limited to 'src/Util/Tactics.v')
-rw-r--r-- | src/Util/Tactics.v | 33 |
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). |