diff options
author | Jason Gross <jgross@mit.edu> | 2017-04-02 23:04:04 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-04-02 23:04:04 -0400 |
commit | de02fe53f2a40cc4a2a57852f985a770925c2b06 (patch) | |
tree | 96887aa5ae05743370889f9f7476a70f6e10a787 /src | |
parent | e0f41c51fa4406389aa241f6e23b1af1a23aed0b (diff) |
Add Util.SigmaAssoc
Diffstat (limited to 'src')
-rw-r--r-- | src/Util/SigmaAssoc.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/Util/SigmaAssoc.v b/src/Util/SigmaAssoc.v new file mode 100644 index 000000000..fbebf2584 --- /dev/null +++ b/src/Util/SigmaAssoc.v @@ -0,0 +1,18 @@ +(** * 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 term := constr:(fun a : A => match P with + | P' => ltac:(let v := (eval cbv [P'] in P') in + lazymatch eval pattern (proj1_sig a) 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. |