Add related_sigT_by_eq

3 files changed, 18 insertions, 16 deletions

diff --git a/_CoqProject b/_CoqProject
index b6ab62707..e37159754 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6561,6 +6561,7 @@ src/Util/SideConditions/RingPackage.v
 src/Util/Sigma/Associativity.v
 src/Util/Sigma/Lift.v
 src/Util/Sigma/MapProjections.v
+src/Util/Sigma/Related.v
 src/Util/Strings/Ascii.v
 src/Util/Strings/BinaryString.v
 src/Util/Strings/Decimal.v
diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v
index 2dd3decc4..659fb018c 100644
--- a/src/Experiments/NewPipeline/RewriterWf1.v
+++ b/src/Experiments/NewPipeline/RewriterWf1.v
@@ -24,6 +24,7 @@ Require Import Crypto.Util.FMapPositive.Equality.
 Require Import Crypto.Util.MSetPositive.Equality.
 Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.Sigma.
+Require Import Crypto.Util.Sigma.Related.
 Require Import Crypto.Util.ListUtil.SetoidList.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.Option.
@@ -1326,22 +1327,6 @@ Module Compilers.
             : @unification_resultT'1 t p evm -> @unification_resultT'2 t p evm -> Prop
             := @related_unification_resultT' (fun _ => wf_value G) t p evm.
 
-          (** TODO: MOVE ME? *)
-          Definition related_sigT_by_eq {A P1 P2} (R : forall x : A, P1 x -> P2 x -> Prop)
-                     (x : @sigT A P1) (y : @sigT A P2)
-            : Prop
-            := { pf : projT1 x = projT1 y
-               | R _ (rew pf in projT2 x) (projT2 y) }.
-
-          Definition map_related_sigT_by_eq {A P1 P2} {R1 R2 : forall x : A, P1 x -> P2 x -> Prop}
-                     (HR : forall x v1 v2, R1 x v1 v2 -> R2 x v1 v2)
-                     (x : @sigT A P1) (y : @sigT A P2)
-            : @related_sigT_by_eq A P1 P2 R1 x y -> @related_sigT_by_eq A P1 P2 R2 x y.
-          Proof using Type.
-            destruct x, y; cbv [related_sigT_by_eq projT1 projT2].
-            intro H; exists (proj1_sig H); apply HR, (proj2_sig H).
-          Qed.
-
           Definition related_unification_resultT (R : forall t, @value var1 t -> @value var2 t -> Prop) {t p}
             : @unification_resultT1 t p -> @unification_resultT2 t p -> Prop
             := related_sigT_by_eq (@related_unification_resultT' R t p).
diff --git a/src/Util/Sigma/Related.v b/src/Util/Sigma/Related.v
new file mode 100644
index 000000000..ac98f7629
--- /dev/null
+++ b/src/Util/Sigma/Related.v
@@ -0,0 +1,16 @@
+Import EqNotations.
+
+Definition related_sigT_by_eq {A P1 P2} (R : forall x : A, P1 x -> P2 x -> Prop)
+           (x : @sigT A P1) (y : @sigT A P2)
+  : Prop
+  := { pf : projT1 x = projT1 y
+     | R _ (rew pf in projT2 x) (projT2 y) }.
+
+Definition map_related_sigT_by_eq {A P1 P2} {R1 R2 : forall x : A, P1 x -> P2 x -> Prop}
+           (HR : forall x v1 v2, R1 x v1 v2 -> R2 x v1 v2)
+           (x : @sigT A P1) (y : @sigT A P2)
+  : @related_sigT_by_eq A P1 P2 R1 x y -> @related_sigT_by_eq A P1 P2 R2 x y.
+Proof using Type.
+  destruct x, y; cbv [related_sigT_by_eq projT1 projT2].
+  intro H; exists (proj1_sig H); apply HR, (proj2_sig H).
+Qed.