diff options
Diffstat (limited to 'src/Util/Sigma/Associativity.v')
-rw-r--r-- | src/Util/Sigma/Associativity.v | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/src/Util/Sigma/Associativity.v b/src/Util/Sigma/Associativity.v new file mode 100644 index 000000000..fbebf2584 --- /dev/null +++ b/src/Util/Sigma/Associativity.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. |