Add related_iff_app_curried

3 files changed, 25 insertions, 0 deletions

diff --git a/_CoqProject b/_CoqProject
index 30aab707b..afb75162c 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -6530,6 +6530,7 @@ src/Util/Decidable/Decidable2Bool.v
 src/Util/ListUtil/FoldBool.v
 src/Util/ListUtil/Forall.v
 src/Util/Logic/ImplAnd.v
+src/Util/Logic/ProdForall.v
 src/Util/SideConditions/AdmitPackage.v
 src/Util/SideConditions/Autosolve.v
 src/Util/SideConditions/CorePackages.v
diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v
index cb0a222f6..73ead2ae0 100644
--- a/src/Experiments/NewPipeline/LanguageWf.v
+++ b/src/Experiments/NewPipeline/LanguageWf.v
@@ -16,6 +16,7 @@ Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.ListUtil.
 Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.Prod.
+Require Import Crypto.Util.Logic.ProdForall.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.HProp.
 Require Import Crypto.Util.CPSNotations.
@@ -79,6 +80,24 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
         : Transitive (@type.and_for_each_lhs_of_arrow base_type f f R t).
       Proof. cbv [Transitive] in *; induction t; cbn; repeat split; intuition eauto. Qed.
     End app_curried_instances.
+
+    Lemma related_iff_app_curried {base_type base_interp R} t F G
+      : (@type.related base_type base_interp R t F G)
+        <-> (forall x y, type.and_for_each_lhs_of_arrow (@type.related base_type base_interp R) x y -> R (type.final_codomain t) (type.app_curried F x) (type.app_curried G y)).
+    Proof using Type.
+      induction t as [t|s IHs d IHd]; cbn; [ tauto | ].
+      cbv [respectful].
+      rewrite pull_prod_forall.
+      lazymatch goal with
+      | [ |- (forall x y, @?P x y) <-> (forall z w, @?Q z w) ]
+        => cut (forall x y, (P x y <-> Q x y)); [ intro H'; setoid_rewrite H'; reflexivity | intros ??; cbn [fst snd] ]
+      end.
+      lazymatch goal with
+      | [ |- (?P -> ?Q) <-> (forall z w, ?P' /\ @?R z w -> @?S z w) ]
+        => unify P P'; cut (P' -> (Q <-> (forall z w, R z w -> S z w))); [ change P with P'; solve [ intuition ] | intro; cbn [fst snd] ]
+      end.
+      eauto.
+    Qed.
   End type.
 
   Module ident.
diff --git a/src/Util/Logic/ProdForall.v b/src/Util/Logic/ProdForall.v
new file mode 100644
index 000000000..f194b442b
--- /dev/null
+++ b/src/Util/Logic/ProdForall.v
@@ -0,0 +1,5 @@
+Require Export Crypto.Util.FixCoqMistakes.
+
+Lemma pull_prod_forall A A' B B' (Q : A * A' -> B * B' -> Prop)
+: (forall x y, Q x y) <-> (forall x0 y0 x1 y1, Q (x0, x1) (y0, y1)).
+Proof. intuition. Qed.