blob: bf9f2d3471fad5813d859cda19deeede5eae92a6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
(** [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
| [ |- context[uproj' _ _ (construct _ _ _ _)] ]
=> cbv beta iota delta [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).
|
