blob: 005e7ab2d3b30e09171c11bdc02717febb78d2a2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
(** * Reassociation of [sig] *)
Definition sig_sig_assoc {A} {P : A -> Prop} {Q}
: { a : A | P a /\ Q a } -> { ap : { a : A | P a } | Q (proj1_sig ap) }
:= fun apq => exist _ (exist _ (proj1_sig apq) (proj1 (proj2_sig apq))) (proj2 (proj2_sig apq)).
Ltac sig_sig_assoc :=
lazymatch goal with
| [ |- { a : ?A | ?P } ]
=> let P'' := fresh a in
let P' := fresh P'' in
let P' := fresh P' in
let term := constr:(fun a : A => match P with
| P' => ltac:(let v := (eval cbv [P'] in P') in
let proj := lazymatch v with context[@proj1_sig ?A ?P a] => constr:(@proj1_sig A P a) end in
lazymatch eval pattern proj in v with
| ?P _ => exact P
end)
end) in
let Q := lazymatch (eval cbv beta in term) with fun _ => ?term => term end in
apply (@sig_sig_assoc _ _ Q)
end.
|
