Add under_with_unification_resultT_relation_hetero

Might not be the best name...

2 files changed, 30 insertions, 38 deletions

diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v
index 93fa108d6..666b0cc21 100644
--- a/src/Experiments/NewPipeline/Rewriter.v
+++ b/src/Experiments/NewPipeline/Rewriter.v
@@ -520,6 +520,16 @@ Module Compilers.
                   => fun f (x : value' _ _) => @reflect _ d (f @ (@reify _ s x))
                 end%expr%under_lets.
 
+        Fixpoint reify_expr {t} (e : @expr.expr base.type ident value t)
+          : @expr.expr base.type ident var t
+          := match e in expr.expr t return expr.expr t with
+             | expr.Ident t idc => expr.Ident idc
+             | expr.Var t v => reify v
+             | expr.Abs s d f => expr.Abs (fun x => @reify_expr _ (f (reflect (expr.Var x))))
+             | expr.App s d f x => expr.App (@reify_expr _ f) (@reify_expr _ x)
+             | expr.LetIn A B x f => expr.LetIn (@reify_expr _ x) (fun xv => @reify_expr _ (f (reflect (expr.Var xv))))
+             end.
+
         Definition reify_and_let_binds_cps {with_lets} {t} : value' with_lets t -> forall T, (expr t -> UnderLets T) -> UnderLets T
           := match t, with_lets return value' with_lets t -> forall T, (expr t -> UnderLets T) -> UnderLets T with
              | type.base _, false => reify_and_let_binds_base_cps _
@@ -605,19 +615,26 @@ Module Compilers.
                     (@under_with_unification_resultT' _ x evm _ _ F)
              end.
 
-        Fixpoint under_with_unification_resultT'_relation {t p evm K1 K2}
+        Fixpoint under_with_unification_resultT'_relation_hetero {t p evm K1 K2}
+                 (FH : forall t, value t -> value t -> Prop)
                  (F : K1 -> K2 -> Prop)
                  {struct p}
           : @with_unification_resultT' t p evm K1 -> @with_unification_resultT' t p evm K2 -> Prop
           := match p return with_unification_resultT' p evm K1 -> with_unification_resultT' p evm K2 -> Prop with
-             | pattern.Wildcard t => fun f1 f2 => forall v, F (f1 v) (f2 v)
+             | pattern.Wildcard t => fun f1 f2 => forall v1 v2, FH _ v1 v2 -> F (f1 v1) (f2 v2)
              | pattern.Ident t idc => under_type_of_list_relation_cps F
              | pattern.App s d f x
-               => @under_with_unification_resultT'_relation
+               => @under_with_unification_resultT'_relation_hetero
                     _ f evm _ _
-                    (@under_with_unification_resultT'_relation _ x evm _ _ F)
+                    FH
+                    (@under_with_unification_resultT'_relation_hetero _ x evm _ _ FH F)
              end.
 
+        Definition under_with_unification_resultT'_relation {t p evm K1 K2}
+                 (F : K1 -> K2 -> Prop)
+          : @with_unification_resultT' t p evm K1 -> @with_unification_resultT' t p evm K2 -> Prop
+          := @under_with_unification_resultT'_relation_hetero t p evm K1 K2 (fun _ => eq) F.
+
         Definition ident_collect_vars := (fun t idc => fold_right PositiveSet.union PositiveSet.empty (List.map pattern.type.collect_vars (type_vars_of_pident t idc))).
 
         Definition with_unification_resultT {t} (p : pattern t) (K : type -> Type) : Type
@@ -633,8 +650,15 @@ Module Compilers.
           := pattern.type.under_forall_vars
                (fun evm => under_with_unification_resultT' (F evm)).
 
+        Definition under_with_unification_resultT_relation_hetero {t p K1 K2}
+                   (FH : forall t, value t -> value t -> Prop)
+                   (F : forall evm, K1 (pattern.type.subst_default t evm) -> K2 (pattern.type.subst_default t evm) -> Prop)
+          : @with_unification_resultT t p K1 -> @with_unification_resultT t p K2 -> Prop
+          := pattern.type.under_forall_vars_relation
+               (fun evm => under_with_unification_resultT'_relation_hetero FH (F evm)).
+
         Definition under_with_unification_resultT_relation {t p K1 K2}
-                 (F : forall evm, K1 (pattern.type.subst_default t evm) -> K2 (pattern.type.subst_default t evm) -> Prop)
+                   (F : forall evm, K1 (pattern.type.subst_default t evm) -> K2 (pattern.type.subst_default t evm) -> Prop)
           : @with_unification_resultT t p K1 -> @with_unification_resultT t p K2 -> Prop
           := pattern.type.under_forall_vars_relation
                (fun evm => under_with_unification_resultT'_relation (F evm)).
diff --git a/src/Experiments/NewPipeline/RewriterRulesGood.v b/src/Experiments/NewPipeline/RewriterRulesGood.v
index 4e5c79cae..978c49189 100644
--- a/src/Experiments/NewPipeline/RewriterRulesGood.v
+++ b/src/Experiments/NewPipeline/RewriterRulesGood.v
@@ -19,6 +19,7 @@ Require Import Crypto.Util.Tactics.RewriteHyp.
 Require Import Crypto.Util.Tactics.Head.
 Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.ListUtil.ForallIn.
 Require Import Crypto.Util.Option.
 Require Import Crypto.Util.CPSNotations.
 Require Import Crypto.Util.HProp.
@@ -190,39 +191,6 @@ Module Compilers.
             (nat_rect (fun _ => @Compile.value base.type ident var2 (type.base A -> type.base B)) O2 S2 n).
       Proof. induction n; cbn [nat_rect]; auto. Qed.
 
-      (** TODO: MOVE ME? *)
-      Lemma fold_right_impl_Proper {A} {P Q : A -> Prop} ls (concl1 concl2 : Prop)
-            (Hconcl : concl1 -> concl2)
-            (HPQ : forall a, In a ls -> Q a -> P a)
-        : fold_right (fun a (concl : Prop) => P a -> concl) concl1 ls
-          -> fold_right (fun a (concl : Prop) => Q a -> concl) concl2 ls.
-      Proof. induction ls as [|x xs IHxs]; cbn [fold_right In] in *; intuition. Qed.
-
-      Lemma forall_In_existT {A P} {Q : forall a : A, P a -> Prop} ls
-        : fold_right
-            (fun xp (concl : Prop)
-             => Q (projT1 xp) (projT2 xp) -> concl)
-            (forall x p, In (@existT A P x p) ls -> Q x p)
-            ls.
-      Proof.
-        induction ls as [|x xs IHxs]; cbn [fold_right In]; intros;
-          destruct_head' False; destruct_head'_or.
-        eapply fold_right_impl_Proper; [ | | refine IHxs ]; intuition (subst; eauto).
-      Qed.
-
-      (** TODO: MOVE ME? *)
-      Lemma forall_In_pair_existT {A A' P P'} {Q : forall (a : A) (a' : A'), P a -> P' a' -> Prop} ls
-        : fold_right
-            (fun xp_x'p' (concl : Prop)
-             => Q (projT1 (fst xp_x'p')) (projT1 (snd xp_x'p')) (projT2 (fst xp_x'p')) (projT2 (snd xp_x'p')) -> concl)
-            (forall x p x' p', In (@existT A P x p, @existT A' P' x' p') ls -> Q x x' p p')
-            ls.
-      Proof.
-        induction ls as [|x xs IHxs]; cbn [fold_right In]; intros;
-          destruct_head' False; destruct_head'_prod; destruct_head'_or; intros.
-        eapply fold_right_impl_Proper; [ | | refine IHxs ]; intuition (inversion_prod; subst; eauto).
-      Qed.
-
       Local Ltac start_good :=
         split; [ reflexivity | ];
         lazymatch goal with