diff options
Diffstat (limited to 'src/Util/Sigma')
-rw-r--r-- | src/Util/Sigma/Associativity.v | 18 | ||||
-rw-r--r-- | src/Util/Sigma/Lift.v | 33 |
2 files changed, 51 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. diff --git a/src/Util/Sigma/Lift.v b/src/Util/Sigma/Lift.v new file mode 100644 index 000000000..c57172029 --- /dev/null +++ b/src/Util/Sigma/Lift.v @@ -0,0 +1,33 @@ +(** * Lift foralls out of sig proofs *) + +Definition lift1_sig {A C} (P:A->C->Prop) + (op_sig : forall (a:A), {c | P a c}) +: { op : A -> C | forall (a:A), P a (op a) } +:= exist + (fun op => forall a, P a (op a)) + (fun a => proj1_sig (op_sig a)) + (fun a => proj2_sig (op_sig a)). + +Definition lift2_sig {A B C} (P:A->B->C->Prop) + (op_sig : forall (a:A) (b:B), {c | P a b c}) + : { op : A -> B -> C | forall (a:A) (b:B), P a b (op a b) } + := exist + (fun op => forall a b, P a b (op a b)) + (fun a b => proj1_sig (op_sig a b)) + (fun a b => proj2_sig (op_sig a b)). + +Definition lift3_sig {A B C D} (P:A->B->C->D->Prop) + (op_sig : forall (a:A) (b:B) (c:C), {d | P a b c d}) + : { op : A -> B -> C -> D | forall (a:A) (b:B) (c:C), P a b c (op a b c) } + := exist + (fun op => forall a b c, P a b c (op a b c)) + (fun a b c => proj1_sig (op_sig a b c)) + (fun a b c => proj2_sig (op_sig a b c)). + +Definition lift4_sig {A B C D E} (P:A->B->C->D->E->Prop) + (op_sig : forall (a:A) (b:B) (c:C) (d:D), {e | P a b c d e}) + : { op : A -> B -> C -> D -> E | forall (a:A) (b:B) (c:C) (d:D), P a b c d (op a b c d) } + := exist + (fun op => forall a b c d, P a b c d (op a b c d)) + (fun a b c d => proj1_sig (op_sig a b c d)) + (fun a b c d => proj2_sig (op_sig a b c d)). |