Split off liftn_sig, add lift{3,4}_sig

6 files changed, 37 insertions, 22 deletions

diff --git a/_CoqProject b/_CoqProject
index ce12ad591..3bba84956 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -274,7 +274,6 @@ src/Util/PointedProp.v
 src/Util/Prod.v
 src/Util/Relations.v
 src/Util/Sigma.v
-src/Util/SigmaAssoc.v
 src/Util/Sum.v
 src/Util/Sumbool.v
 src/Util/Tactics.v
@@ -284,6 +283,8 @@ src/Util/Unit.v
 src/Util/WordUtil.v
 src/Util/ZRange.v
 src/Util/ZUtil.v
+src/Util/Sigma/Associativity.v
+src/Util/Sigma/Lift.v
 src/Util/Tactics/BreakMatch.v
 src/Util/Tactics/DestructHead.v
 src/Util/Tactics/DestructHyps.v
diff --git a/src/Reflection/Z/Bounds/Pipeline/Glue.v b/src/Reflection/Z/Bounds/Pipeline/Glue.v
index af6a5548b..f3a0d8ee5 100644
--- a/src/Reflection/Z/Bounds/Pipeline/Glue.v
+++ b/src/Reflection/Z/Bounds/Pipeline/Glue.v
@@ -12,7 +12,7 @@ Require Import Crypto.Util.Curry.
 Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Util.BoundedWord.
 Require Import Crypto.Util.Tuple.
-Require Import Crypto.Util.SigmaAssoc.
+Require Import Crypto.Util.Sigma.Associativity.
 Require Import Crypto.Util.Tactics.EvarExists.
 
 Module Export Exports.
diff --git a/src/Specific/IntegrationTest.v b/src/Specific/IntegrationTest.v
index fe2d49272..d6b178061 100644
--- a/src/Specific/IntegrationTest.v
+++ b/src/Specific/IntegrationTest.v
@@ -7,7 +7,7 @@ Require Import Crypto.NewBaseSystem.
 Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Specific.NewBaseSystemTest.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
-Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
+Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord.
 Require Import Crypto.Util.Tactics.Head.
 Import ListNotations.
 
diff --git a/src/Util/Sigma.v b/src/Util/Sigma.v
index 693b8ef00..1c30219b7 100644
--- a/src/Util/Sigma.v
+++ b/src/Util/Sigma.v
@@ -211,25 +211,6 @@ Section ex.
   Defined.
 End ex.
 
-(* 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))
-.
-
-(* Lift foralls out of sig proofs *)
-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 projT2_map {A P Q} (f : forall a, P a -> Q a) (x : @sigT A P) : @sigT A Q
   := let 'existT a p := x in existT Q a (f a p).
 Definition proj2_sig_map {A} {P Q : A -> Prop} (f : forall a, P a -> Q a) (x : @sig A P) : @sig A Q
diff --git a/src/Util/SigmaAssoc.v b/src/Util/Sigma/Associativity.v
index fbebf2584..fbebf2584 100644
--- a/src/Util/SigmaAssoc.v
+++ b/src/Util/Sigma/Associativity.v
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)).