diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-13 10:57:53 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-13 11:29:58 -0400 |
| commit | 1c58502d0556f56943e9e29f14c119d5b74c8d74 (patch) | |
| tree | 693d5eddd002dd6c42853b18f1626727dc60544e /src | |
| parent | 86215f5f2d1c3fc4296b454fb8236111d50aea5b (diff) | |
Add lift4_sig_sig
Diffstat (limited to 'src')
| -rw-r--r-- | src/Specific/IntegrationTestDisplayCommon.v | 2 | ||||
| -rw-r--r-- | src/Util/Sigma/Lift.v | 11 |
2 files changed, 12 insertions, 1 deletions
diff --git a/src/Specific/IntegrationTestDisplayCommon.v b/src/Specific/IntegrationTestDisplayCommon.v index c0ad77b78..d288d9075 100644 --- a/src/Specific/IntegrationTestDisplayCommon.v +++ b/src/Specific/IntegrationTestDisplayCommon.v @@ -38,7 +38,7 @@ Tactic Notation "display" open_constr(f) := let do_red F := (eval cbv [f proj1_sig fst snd Tuple.map Tuple.map' - Lift.lift2_sig Lift.lift4_sig + Lift.lift2_sig Lift.lift4_sig Lift.lift4_sig_sig MapProjections.proj2_sig_map Associativity.sig_sig_assoc sig_eq_trans_exist1 sig_R_trans_exist1 sig_eq_trans_rewrite_fun_exist1 adjust_tuple2_tuple2_sig diff --git a/src/Util/Sigma/Lift.v b/src/Util/Sigma/Lift.v index c57172029..22f966d09 100644 --- a/src/Util/Sigma/Lift.v +++ b/src/Util/Sigma/Lift.v @@ -31,3 +31,14 @@ Definition lift4_sig {A B C D E} (P:A->B->C->D->E->Prop) (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)). + +Definition lift4_sig_sig {A B C D E} {E' : A -> B -> C -> D -> E -> Prop} + (P:forall (a:A) (b:B) (c:C) (d:D) (e:E), E' a b c d e -> Prop) + (op_sig : forall (a:A) (b:B) (c:C) (d:D), {e : {e : E | E' a b c d e } | P a b c d (proj1_sig e) (proj2_sig e) }) + (opTP := fun op : A -> B -> C -> D -> E => forall a b c d, E' a b c d (op a b c d)) + : { op : sig opTP + | forall (a:A) (b:B) (c:C) (d:D), P a b c d (proj1_sig op a b c d) (proj2_sig op a b c d) } + := exist + (fun op : sig opTP => forall a b c d, P a b c d (proj1_sig op a b c d) (proj2_sig op a b c d)) + (exist opTP (fun a b c d => proj1_sig (proj1_sig (op_sig a b c d))) (fun a b c d => proj2_sig (proj1_sig (op_sig a b c d)))) + (fun a b c d => proj2_sig (op_sig a b c d)). |