Improvements in rewrite-rule-specific proofs

N.B. All that remains in the commented out bits is fixing the fact that
in [make_rewrite_step] rules, we need to permit value expressions to be
well-formed in any context where we add arbitrary well-formed things to
the context (like subterms of the arguments we get).

Note that the timing diff is off, because after a rebase, the previous
commit no longer builds.

After     | File Name                                                            | Before   || Change     | % Change
--------------------------------------------------------------------------------------------------------------------
19m33.61s | Total                                                                | 8m20.18s || +11m13.42s | +134.63%
--------------------------------------------------------------------------------------------------------------------
5m57.63s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples                   |   N/A    || +5m57.62s  | ∞
1m15.88s  | Experiments/NewPipeline/RewriterRulesGood                            | 7m12.00s || -5m56.12s  | -82.43%
4m33.68s  | Experiments/NewPipeline/Toplevel1                                    |   N/A    || +4m33.68s  | ∞
1m38.58s  | Experiments/NewPipeline/Toplevel2                                    |   N/A    || +1m38.57s  | ∞
0m39.26s  | p521_32.c                                                            |   N/A    || +0m39.25s  | ∞
0m37.08s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      |   N/A    || +0m37.07s  | ∞
0m34.84s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    |   N/A    || +0m34.84s  | ∞
0m32.82s  | p521_64.c                                                            |   N/A    || +0m32.82s  | ∞
0m23.70s  | p384_32.c                                                            |   N/A    || +0m23.69s  | ∞
0m20.49s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        |   N/A    || +0m20.48s  | ∞
0m18.70s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          |   N/A    || +0m18.69s  | ∞
0m13.47s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          |   N/A    || +0m13.47s  | ∞
0m10.38s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            |   N/A    || +0m10.38s  | ∞
0m08.56s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   |   N/A    || +0m08.56s  | ∞
0m08.50s  | p384_64.c                                                            |   N/A    || +0m08.50s  | ∞
1m11.05s  | Experiments/NewPipeline/RewriterWf2                                  | 1m03.76s || +0m07.28s  | +11.43%
0m05.49s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       |   N/A    || +0m05.49s  | ∞
0m05.36s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs |   N/A    || +0m05.36s  | ∞
0m04.07s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         |   N/A    || +0m04.07s  | ∞
0m03.89s  | p256_32.c                                                            |   N/A    || +0m03.89s  | ∞
0m03.82s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     |   N/A    || +0m03.81s  | ∞
0m03.74s  | secp256k1_32.c                                                       |   N/A    || +0m03.74s  | ∞
0m03.16s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       |   N/A    || +0m03.16s  | ∞
0m02.26s  | p224_32.c                                                            |   N/A    || +0m02.25s  | ∞
0m02.09s  | curve25519_32.c                                                      |   N/A    || +0m02.08s  | ∞
0m01.55s  | p224_64.c                                                            |   N/A    || +0m01.55s  | ∞
0m01.53s  | p256_64.c                                                            |   N/A    || +0m01.53s  | ∞
0m01.50s  | secp256k1_64.c                                                       |   N/A    || +0m01.50s  | ∞
0m01.44s  | curve25519_64.c                                                      |   N/A    || +0m01.43s  | ∞
0m01.41s  | Experiments/NewPipeline/CLI                                          |   N/A    || +0m01.40s  | ∞
0m01.21s  | Experiments/NewPipeline/StandaloneHaskellMain                        |   N/A    || +0m01.20s  | ∞
0m01.20s  | Experiments/NewPipeline/StandaloneOCamlMain                          |   N/A    || +0m01.19s  | ∞
0m04.36s  | Experiments/NewPipeline/RewriterWf1                                  | 0m04.43s || -0m00.06s  | -1.58%
0m00.92s  | Experiments/NewPipeline/RewriterProofs                               |   N/A    || +0m00.92s  | ∞

3 files changed, 429 insertions, 44 deletions

diff --git a/src/Experiments/NewPipeline/RewriterRulesGood.v b/src/Experiments/NewPipeline/RewriterRulesGood.v
index 03502fb9c..605cbf5ca 100644
--- a/src/Experiments/NewPipeline/RewriterRulesGood.v
+++ b/src/Experiments/NewPipeline/RewriterRulesGood.v
@@ -81,24 +81,275 @@ Module Compilers.
         apply rlist_rect_cps_id.
       Qed.
 
+      Lemma wf_rlist_rect {A P}
+            N1 N2 C1 C2 ls1 ls2 G
+            (Hwf : expr.wf G ls1 ls2)
+            (HN : UnderLets.wf (fun G' => expr.wf G') G N1 N2)
+            (HC : forall G' x xs y ys rec1 rec2,
+                (exists seg, G' = (seg ++ G)%list)
+                -> expr.wf G x y
+                -> expr.wf G (reify_list xs) (reify_list ys)
+                -> expr.wf G' rec1 rec2
+                -> UnderLets.wf (fun G'' => expr.wf G'') G' (C1 x xs rec1) (C2 y ys rec2))
+        : option_eq (UnderLets.wf (fun G' => Compile.wf_anyexpr G' (type.base P)) G)
+                    (@rlist_rect var1 A P var1 N1 C1 ls1 _ id)
+                    (@rlist_rect var2 A P var2 N2 C2 ls2 _ id).
+      Proof.
+        cbv [rlist_rect].
+        rewrite !expr.reflect_list_cps_id; cbv [id].
+        cbv [Compile.option_bind' Option.bind].
+        break_innermost_match.
+        all: repeat first [ match goal with
+                            | [ H : invert_expr.reflect_list ?v = Some _, H' : invert_expr.reflect_list ?v' = None |- _ ]
+                              => first [ erewrite <- expr.wf_reflect_list in H' by eassumption
+                                      | erewrite -> expr.wf_reflect_list in H' by eassumption ];
+                                exfalso; clear -H H'; congruence
+                            | [ |- UnderLets.wf _ _ _ _ ] => constructor
+                            | [ |- Compile.wf_anyexpr _ _ _ _ ] => constructor
+                            end
+                          | progress expr.invert_subst
+                          | progress cbn [sequence_return option_eq]
+                          | assumption
+                          | reflexivity
+                          | apply @UnderLets.wf_splice with (P:=fun G' => expr.wf G')
+                          | progress intros ].
+        lazymatch goal with
+        | [ H : expr.wf _ (reify_list ?l) (reify_list ?l') |- _ ]
+          => revert dependent l'; intro l2; revert dependent l; intro l1
+        end.
+        revert l2; induction l1 as [|l1 ls1 IHls1], l2; cbn [list_rect];
+          rewrite ?expr.reify_list_cons, ?expr.reify_list_nil;
+          intros; expr.inversion_wf_constr; [ assumption | ].
+        all: repeat first [ match goal with
+                            | [ H : invert_expr.reflect_list ?v = Some _, H' : invert_expr.reflect_list ?v' = None |- _ ]
+                              => first [ erewrite <- expr.wf_reflect_list in H' by eassumption
+                                      | erewrite -> expr.wf_reflect_list in H' by eassumption ];
+                                exfalso; clear -H H'; congruence
+                            | [ |- UnderLets.wf _ _ _ _ ] => constructor
+                            end
+                          | progress expr.invert_subst
+                          | progress cbn [sequence_return option_eq]
+                          | assumption
+                          | reflexivity
+                          | solve [ auto ]
+                          | progress subst
+                          | apply @UnderLets.wf_splice with (P:=fun G' => expr.wf G')
+                          | progress intros
+                          | wf_safe_t_step
+                          | progress type.inversion_type
+                          | progress expr.inversion_wf_constr ].
+      Qed.
+
+      Lemma wf_rlist_rect_cast {A A' P}
+            N1 N2 C1 C2 ls1 ls2 G
+            (Hwf : expr.wf G ls1 ls2)
+            (HN : UnderLets.wf (fun G' x1 x2 => Compile.wf_anyexpr G' (type.base P) (AnyExpr.wrap x1) (AnyExpr.wrap x2)) G N1 N2)
+            (HC : forall G' x xs y ys rec1 rec2,
+                (exists seg, G' = (seg ++ G)%list)
+                -> expr.wf G x y
+                -> expr.wf G (reify_list xs) (reify_list ys)
+                -> expr.wf G' rec1 rec2
+                -> UnderLets.wf (fun G'' => expr.wf G'') G' (C1 x xs rec1) (C2 y ys rec2))
+        : option_eq (UnderLets.wf (fun G' => Compile.wf_anyexpr G' (type.base P)) G)
+                    (@rlist_rect_cast var1 A A' P var1 N1 C1 ls1 _ id)
+                    (@rlist_rect_cast var2 A A' P var2 N2 C2 ls2 _ id).
+      Proof.
+        cbv [rlist_rect_cast].
+        cbv [Compile.castbe Compile.castb id Compile.option_bind' Option.bind sequence_return]; rewrite_type_transport_correct; break_innermost_match;
+          type_beq_to_eq; subst; [ | reflexivity ].
+        apply wf_rlist_rect; auto.
+        eapply UnderLets.wf_Proper_list_impl; [ | | eassumption ]; trivial; cbn; intros ? ? ? H.
+        inversion H; inversion_sigma; type.inversion_type; subst; assumption.
+      Qed.
+
+      Lemma wf_rlist_rectv {A P}
+            N1 N2 C1 C2 ls1 ls2 G
+            (Hwf : expr.wf G ls1 ls2)
+            (HN : UnderLets.wf (fun G' v1 v2
+                                => forall G'',
+                                    (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
+                                    -> expr.wf G'' v1 v2) G N1 N2)
+            (HC : forall G' x xs y ys rec1 rec2,
+                (exists seg, G' = (seg ++ G)%list)
+                -> expr.wf G x y
+                -> expr.wf G (reify_list xs) (reify_list ys)
+                -> (forall G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
+                          -> expr.wf G'' rec1 rec2)
+                -> UnderLets.wf (fun G' v1 v2
+                                => forall G'',
+                                    (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
+                                    -> expr.wf G'' v1 v2)
+                               G' (C1 x xs rec1) (C2 y ys rec2))
+        : option_eq (UnderLets.wf
+                       (fun G' v1 v2
+                        => exists (pf1 : AnyExpr.anyexpr_ty v1 = P) (pf2 : AnyExpr.anyexpr_ty v2 = P),
+                            forall G'',
+                              (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
+                              -> expr.wf G''
+                                        (rew [fun t : base.type => expr t] pf1 in AnyExpr.unwrap v1)
+                                        (rew [fun t : base.type => expr t] pf2 in AnyExpr.unwrap v2))
+                       G)
+                    (@rlist_rect var1 A P (@Compile.value _ ident var1) N1 C1 ls1 _ id)
+                    (@rlist_rect var2 A P (@Compile.value _ ident var2) N2 C2 ls2 _ id).
+      Proof.
+        cbv [rlist_rect].
+        rewrite !expr.reflect_list_cps_id; cbv [id].
+        cbv [Compile.option_bind' Option.bind].
+        break_innermost_match.
+        all: repeat first [ match goal with
+                            | [ H : invert_expr.reflect_list ?v = Some _, H' : invert_expr.reflect_list ?v' = None |- _ ]
+                              => first [ erewrite <- expr.wf_reflect_list in H' by eassumption
+                                      | erewrite -> expr.wf_reflect_list in H' by eassumption ];
+                                exfalso; clear -H H'; congruence
+                            | [ |- UnderLets.wf _ _ _ _ ] => constructor
+                            | [ |- Compile.wf_anyexpr _ _ _ _ ] => constructor
+                            end
+                          | progress expr.invert_subst
+                          | progress cbn [sequence_return option_eq]
+                          | assumption
+                          | reflexivity
+                          | apply @UnderLets.wf_splice with (P:=fun G' v1 v2
+                                                                => forall G'',
+                                                                    (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
+                                                                    -> expr.wf G'' v1 v2)
+                          | progress intros ].
+        lazymatch goal with
+        | [ H : expr.wf _ (reify_list ?l) (reify_list ?l') |- _ ]
+          => revert dependent l'; intro l2; revert dependent l; intro l1
+        end.
+        revert l2; induction l1 as [|l1 ls1 IHls1], l2; cbn [list_rect];
+          rewrite ?expr.reify_list_cons, ?expr.reify_list_nil;
+          intros; expr.inversion_wf_constr; [ assumption | ].
+        all: repeat first [ match goal with
+                            | [ H : invert_expr.reflect_list ?v = Some _, H' : invert_expr.reflect_list ?v' = None |- _ ]
+                              => first [ erewrite <- expr.wf_reflect_list in H' by eassumption
+                                      | erewrite -> expr.wf_reflect_list in H' by eassumption ];
+                                exfalso; clear -H H'; congruence
+                            | [ |- UnderLets.wf _ _ _ _ ] => constructor
+                            end
+                          | progress expr.invert_subst
+                          | progress cbn [sequence_return option_eq AnyExpr.anyexpr_ty eq_rect]
+                          | (exists eq_refl)
+                          | assumption
+                          | reflexivity
+                          | solve [ auto ]
+                          | progress subst
+                          | apply @UnderLets.wf_splice with (P:=fun G' v1 v2
+                                                                => forall G'',
+                                                                    (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
+                                                                    -> expr.wf G'' v1 v2)
+                          | progress intros
+                          | wf_safe_t_step
+                          | progress type.inversion_type
+                          | progress expr.inversion_wf_constr ].
+      Qed.
+
+      Lemma wf_rlist_rect_castv {A A' P}
+            N1 N2 C1 C2 ls1 ls2 G
+            (Hwf : expr.wf G ls1 ls2)
+            (HN : UnderLets.wf (fun G' x1 x2
+                                => forall G'',
+                                    (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
+                                    -> Compile.wf_anyexpr G'' (type.base P) (AnyExpr.wrap x1) (AnyExpr.wrap x2)) G N1 N2)
+            (HC : forall G' x xs y ys rec1 rec2,
+                (exists seg, G' = (seg ++ G)%list)
+                -> expr.wf G x y
+                -> expr.wf G (reify_list xs) (reify_list ys)
+                -> (forall G'', (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
+                          -> expr.wf G'' rec1 rec2)
+                -> UnderLets.wf (fun G' v1 v2
+                                => forall G'',
+                                    (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
+                                    -> expr.wf G'' v1 v2)
+                               G' (C1 x xs rec1) (C2 y ys rec2))
+        : option_eq (UnderLets.wf
+                       (fun G' v1 v2
+                        => exists (pf1 : AnyExpr.anyexpr_ty v1 = P) (pf2 : AnyExpr.anyexpr_ty v2 = P),
+                            forall G'',
+                              (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> Compile.wf_value G' v1' v2')
+                              -> expr.wf G''
+                                        (rew [fun t : base.type => expr t] pf1 in AnyExpr.unwrap v1)
+                                        (rew [fun t : base.type => expr t] pf2 in AnyExpr.unwrap v2))
+                       G)
+                    (@rlist_rect_cast var1 A A' P (@Compile.value _ ident var1) N1 C1 ls1 _ id)
+                    (@rlist_rect_cast var2 A A' P (@Compile.value _ ident var2) N2 C2 ls2 _ id).
+      Proof.
+        cbv [rlist_rect_cast].
+        cbv [Compile.castbe Compile.castb id Compile.option_bind' Option.bind sequence_return]; rewrite_type_transport_correct; break_innermost_match;
+          type_beq_to_eq; subst; [ | reflexivity ].
+        apply wf_rlist_rectv; auto.
+        eapply UnderLets.wf_Proper_list_impl; [ | | eassumption ]; trivial; cbn; intros ? ? ? H.
+        repeat let x := fresh in intro x; specialize (H x).
+        inversion H; inversion_sigma; type.inversion_type; subst; assumption.
+      Qed.
+
+
+      Lemma wf_nat_rect {A}
+            G O1 O2 S1 S2 n
+            (HO : UnderLets.wf (fun G' => expr.wf G') G O1 O2)
+            (HS : forall n rec1 rec2,
+                UnderLets.wf (fun G' => expr.wf G') G rec1 rec2
+                -> UnderLets.wf (fun G' => expr.wf G') G (S1 n rec1) (S2 n rec2))
+        : UnderLets.wf (fun G' => expr.wf G') G
+                       (nat_rect (fun _ => UnderLets.UnderLets base.type ident var1 (expr (type.base A))) O1 S1 n)
+                       (nat_rect (fun _ => UnderLets.UnderLets base.type ident var2 (expr (type.base A))) O2 S2 n).
+      Proof. induction n; cbn [nat_rect]; auto. Qed.
+
+      Lemma wf_nat_rect_arrow {A B}
+            G O1 O2 S1 S2 n
+            (HO : Compile.wf_value G O1 O2)
+            (HS : forall n rec1 rec2,
+                Compile.wf_value G rec1 rec2
+                -> Compile.wf_value G (S1 n rec1) (S2 n rec2))
+        : Compile.wf_value
+            G
+            (nat_rect (fun _ => @Compile.value base.type ident var1 (type.base A -> type.base B)) O1 S1 n)
+            (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.
+
       Local Ltac start_cps_id :=
         lazymatch goal with
-        | [ |- In _ ?rewr -> _ ] => let h := head rewr in cbv [h]
+        | [ |- forall x p, In (@existT ?A ?P x p) ?ls -> @?Q x p ]
+          => apply (@forall_In_existT A P Q ls); cbn [projT1 projT2]; cbv [id]
         end;
-        cbn [In combine]; intros; destruct_head'_or; inversion_sigma; subst; try reflexivity; destruct_head' False.
+        try reflexivity.
 
       Local Ltac cps_id_step :=
         first [ reflexivity
+              | progress intros
               | progress destruct_head' False
               | progress subst
               | progress inversion_option
-              | progress cbv [id Compile.binding_dataT pattern.ident.arg_types Compile.ptype_interp Compile.ptype_interp_cps Compile.pbase_type_interp_cps Compile.value Compile.value' Compile.app_binding_data Compile.app_ptype_interp_cps Compile.app_pbase_type_interp_cps Compile.lift_with_bindings Compile.lift_ptype_interp_cps Compile.lift_pbase_type_interp_cps cpsbind cpscall cpsreturn cps_option_bind type_base rwhen] in *
-              | progress cbn [UnderLets.splice eq_rect projT1 projT2 Option.bind Option.sequence Option.sequence_return] in *
+              | progress cbn [Compile.value' UnderLets.splice eq_rect projT1 projT2 Option.bind Option.sequence Option.sequence_return] in *
+              | progress destruct_head'_sigT
+              | progress destruct_head'_prod
+              | progress destruct_head'_unit
+              | progress cbv [id Compile.binding_dataT pattern.ident.arg_types Compile.ptype_interp Compile.ptype_interp_cps Compile.pbase_type_interp_cps Compile.value Compile.app_binding_data Compile.app_ptype_interp_cps Compile.app_pbase_type_interp_cps Compile.lift_with_bindings Compile.lift_ptype_interp_cps Compile.lift_pbase_type_interp_cps cpsbind cpscall cpsreturn cps_option_bind type_base rwhen] in *
               | progress type_beq_to_eq
               | progress rewrite_type_transport_correct
+              | break_match_step ltac:(fun v => match type of v with sumbool _ _ => idtac end)
               | progress cbv [Compile.option_bind' Compile.castbe Compile.castb Compile.castv] in *
               | progress break_innermost_match
-              | progress destruct_head'_sigT
               | rewrite !expr.reflect_list_cps_id
               | match goal with
                 | [ |- context[@rlist_rect_cast ?var ?A ?A' ?P ?ivar ?N_case ?C_case ?ls ?T ?k] ]
@@ -115,80 +366,213 @@ Module Compilers.
 
       Local Ltac cps_id_t := start_cps_id; repeat cps_id_step.
 
-      Lemma nbe_cps_id {var} p r
-        : In (existT _ p r) (@nbe_rewrite_rules var)
-          -> forall v T k, r v T k = k (r v _ id).
-      Proof. cps_id_t. Qed.
+      Lemma nbe_cps_id {var}
+        : forall p r, In (existT _ p r) (@nbe_rewrite_rules var)
+                      -> forall v T k, r v T k = k (r v _ id).
+      Proof. Time cps_id_t. Time Qed.
 
-      Lemma arith_cps_id max_const {var} p r
-        : In (existT _ p r) (@arith_rewrite_rules var max_const)
-          -> forall v T k, r v T k = k (r v _ id).
-      Proof. cps_id_t. Qed.
+      Lemma arith_cps_id max_const {var}
+        : forall p r, In (existT _ p r) (@arith_rewrite_rules var max_const)
+                 -> forall v T k, r v T k = k (r v _ id).
+      Proof. Time cps_id_t. Time Qed.
 
-      Lemma fancy_cps_id invert_low invert_high {var} p r
-        : In (existT _ p r) (@fancy_rewrite_rules var invert_low invert_high)
-          -> forall v T k, r v T k = k (r v _ id).
-      Proof. cps_id_t. Qed.
+      Lemma fancy_cps_id invert_low invert_high {var}
+        : forall p r, In (existT _ p r) (@fancy_rewrite_rules var invert_low invert_high)
+                 -> forall v T k, r v T k = k (r v _ id).
+      Proof. Time cps_id_t. Time 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.
+
+      (** TODO: MOVE ME *)
+      Lemma combine_repeat {A B} (a : A) (b : B) n : combine (repeat a n) (repeat b n) = repeat (a, b) n.
+      Proof. induction n; cbn; congruence. Qed.
+      Lemma combine_rev_rev_samelength {A B} ls1 ls2 : length ls1 = length ls2 -> @combine A B (rev ls1) (rev ls2) = rev (combine ls1 ls2).
+      Proof.
+        revert ls2; induction ls1 as [|? ? IHls1], ls2; cbn in *; try congruence; intros.
+        rewrite combine_app_samelength, IHls1 by (rewrite ?rev_length; congruence); cbn [combine].
+        reflexivity.
+      Qed.
 
       Local Ltac start_good cps_id rewrite_rules :=
         split; [ reflexivity | ];
-          repeat apply conj; try solve [ eapply cps_id ]; [];
-            cbv [rewrite_rules]; cbn [In combine];
-              intros; destruct_head'_or; inversion_prod; inversion_sigma; subst; destruct_head' False;
-              (split; [ reflexivity | ]).
+        repeat apply conj; try solve [ eapply cps_id ]; [];
+        lazymatch goal with
+        | [ |- forall x p x' p', In (@existT ?A ?P x p, @existT ?A' ?P' x' p') ?ls -> @?Q x x' p p' ]
+          => apply (@forall_In_pair_existT A A' P P' Q ls); cbn [projT1 projT2 fst snd]; cbv [id]
+        end;
+        intros; (split; [ reflexivity | ]).
 
       Local Ltac good_t_step :=
         first [ progress subst
-              | progress cbv [id Compile.binding_dataT pattern.ident.arg_types Compile.ptype_interp Compile.ptype_interp_cps Compile.pbase_type_interp_cps Compile.value Compile.value' Compile.app_binding_data Compile.app_ptype_interp_cps Compile.app_pbase_type_interp_cps Compile.lift_with_bindings Compile.lift_ptype_interp_cps Compile.lift_pbase_type_interp_cps cpsbind cpscall cpsreturn cps_option_bind type_base Compile.wf_binding_dataT Compile.wf_ptype_interp_id Compile.wf_ptype_interp_cps Compile.wf_pbase_type_interp_cps ident.smart_Literal rwhen AnyExpr.unwrap] in *
-              | progress destruct_head'_sig
-              | progress cbn [eq_rect option_eq projT1 projT2 fst snd base.interp In combine Option.bind Option.sequence Option.sequence_return UnderLets.splice] in *
-              | progress destruct_head'_prod
+              | progress cbn [eq_rect Compile.value' option_eq projT1 projT2 fst snd base.interp In combine Option.bind Option.sequence Option.sequence_return UnderLets.splice] in *
+              | progress destruct_head'_unit
               | progress destruct_head'_sigT
-              | progress intros
+              | progress destruct_head'_prod
               | progress eliminate_hprop_eq
+              | progress destruct_head'_and
+              | progress destruct_head'_sig
+              | progress inversion_option
+              | progress destruct_head'_ex
+              | progress cbn [Compile.binding_dataT pattern.ident.arg_types] in *
+              | progress cbn [Compile.wf_binding_dataT Compile.wf_ptype_interp_cps Compile.wf_pbase_type_interp_cps fst snd projT1 projT2] in *
+              | progress intros
+              | progress cbv [Compile.ptype_interp Compile.ptype_interp_cps Compile.pbase_type_interp_cps id] in *
+              | progress cbv [Compile.wf_ptype_interp_id] in *
+              | progress cbv [id Compile.binding_dataT pattern.ident.arg_types Compile.ptype_interp Compile.ptype_interp_cps Compile.pbase_type_interp_cps Compile.value Compile.app_binding_data Compile.app_ptype_interp_cps Compile.app_pbase_type_interp_cps Compile.lift_with_bindings Compile.lift_ptype_interp_cps Compile.lift_pbase_type_interp_cps cpsbind cpscall cpsreturn cps_option_bind type_base Compile.wf_binding_dataT Compile.wf_ptype_interp_id Compile.wf_ptype_interp_cps Compile.wf_pbase_type_interp_cps ident.smart_Literal rwhen AnyExpr.unwrap nth_default SubstVarLike.is_var_fst_snd_pair_opp] in *
               | progress cbv [Compile.option_bind' Compile.castbe Compile.castb Compile.castv] in *
               | progress type_beq_to_eq
+              | progress type.inversion_type
               | progress rewrite_type_transport_correct
+              | progress specialize_by exact eq_refl
               | break_innermost_match_step
               | wf_safe_t_step
               | rewrite !expr.reflect_list_cps_id
               | congruence
               | match goal with
+                | [ H : nth_error ?l1 ?n = Some _, H' : nth_error ?l2 ?n = None |- _ ]
+                  => let H0 := fresh in
+                    assert (H0 : length l1 = length l2) by congruence;
+                    apply nth_error_error_length in H';
+                    apply nth_error_value_length in H;
+                    exfalso; clear -H0 H H'; lia
                 | [ |- expr.wf _ (reify_list _) (reify_list _) ] => rewrite expr.wf_reify_list
                 | [ |- context[length ?ls] ] => tryif is_var ls then fail else (progress autorewrite with distr_length)
+                | [ H : context[length ?ls] |- _ ] => tryif is_var ls then fail else (progress autorewrite with distr_length in H)
+                | [ |- @ex (_ = _) _ ] => (exists eq_refl)
                 | [ |- ex _ ] => eexists
                 | [ |- UnderLets.wf _ _ _ _ ] => constructor
+                | [ |- UnderLets.wf _ _ (UnderLets.splice _ _) (UnderLets.splice _ _) ]
+                  => eapply UnderLets.wf_splice; [ eapply UnderLets.wf_Proper_list; [ | | solve [ repeat good_t_step ] ] | ]
                 | [ |- UnderLets.wf _ _ (UnderLets.splice _ _) (UnderLets.splice _ _) ] => eapply UnderLets.wf_splice
+                | [ |- UnderLets.wf _ _ (UnderLets.splice_list _ _) (UnderLets.splice_list _ _) ]
+                  => apply @UnderLets.wf_splice_list_no_order with (P:=fun G' => expr.wf G')
                 | [ |- Compile.wf_anyexpr _ _ _ _ ] => constructor
-                | [ H : Compile.wf_value ?G ?e1 ?e2 |- UnderLets.wf _ ?G (?e1 _) (?e2 _) ] => eapply (H nil)
-                | [ H : Compile.wf_value ?G ?e1 ?e2 |- UnderLets.wf _ ?G (?e1 _ _) (?e2 _ _) ]
-                  => eapply UnderLets.wf_Proper_list; [ | | eapply H; [ reflexivity | | reflexivity | ] ]; revgoals
                 | [ |- context[@rlist_rect_cast ?var ?A ?A' ?P ?ivar ?N_case ?C_case ?ls ?T ?k] ]
                   => (tryif (let __ := constr:(eq_refl : k = (fun x => x)) in idtac)
-                       then fail
-                       else rewrite (@rlist_rect_cast_cps_id var A A' P ivar N_case C_case ls T k))
+                      then fail
+                      else rewrite (@rlist_rect_cast_cps_id var A A' P ivar N_case C_case ls T k))
                 | [ |- context[@rlist_rect ?var ?A ?P ?ivar ?N_case ?C_case ?ls ?T ?k] ]
                   => (tryif (let __ := constr:(eq_refl : k = (fun x => x)) in idtac)
-                       then fail
-                       else rewrite (@rlist_rect_cps_id var A P ivar N_case C_case ls T k))
+                      then fail
+                      else rewrite (@rlist_rect_cps_id var A P ivar N_case C_case ls T k))
                 | [ |- ?x = ?x /\ _ ] => split; [ reflexivity | ]
+                | [ |- context[invert_expr.reflect_list ?v] ] => destruct (invert_expr.reflect_list v) eqn:?
+                | [ H : invert_expr.reflect_list ?v = Some _, H' : invert_expr.reflect_list ?v' = None |- _ ]
+                  => first [ erewrite <- expr.wf_reflect_list in H' by eassumption
+                          | erewrite -> expr.wf_reflect_list in H' by eassumption ];
+                    exfalso; clear -H H'; congruence
+                | [ H : Compile.wf_value _ (reify_list _) (reify_list _) |- _ ]
+                  => hnf in H; rewrite expr.wf_reify_list in H
+                | [ H : length ?l = length ?l' |- context[length ?l] ] => rewrite H
+                | [ H : context[combine (firstn ?n _) (firstn ?n _)] |- _ ] => rewrite <- firstn_combine in H
+                | [ H : context[combine (skipn ?n _) (skipn ?n _)] |- _ ] => rewrite <- skipn_combine in H
+                | [ H : context[In _ (firstn _ _)] |- _ ] => solve [ eauto using In_firstn ]
+                | [ H : context[In _ (skipn _ _)] |- _ ] => solve [ eauto using In_skipn ]
+                | [ H : context[combine (repeat _ _) (repeat _ _)] |- _ ] => rewrite combine_repeat in H
+                | [ H : context[combine (Lists.List.repeat _ _) (Lists.List.repeat _ _)] |- _ ] => rewrite combine_repeat in H
+                | [ H : In _ (repeat _ _) |- _ ] => apply repeat_spec in H
+                | [ H : In _ (Lists.List.repeat _ _) |- _ ] => apply repeat_spec in H
+                | [ H : context[combine (rev ?l1) (rev ?l2)] |- _ ] => rewrite (@combine_rev_rev_samelength _ _ l1 l2) in H by congruence
+                | [ H : In _ (rev _) |- _ ] => rewrite <- in_rev in H
+                | [ H : forall e1' e2', In (e1', e2') (combine ?l1 ?l2) -> _, H1 : nth_error ?l1 ?n = Some ?e1, H2 : nth_error ?l2 ?n = Some ?e2 |- _ ]
+                  => specialize (fun pf => H e1 e2 (@nth_error_In _ _ n _ pf))
+                | [ H : context[nth_error (combine _ _) _] |- _ ] => rewrite nth_error_combine in H
+                | [ H : ?x = Some _, H' : context[?x] |- _ ] => rewrite H in H'
+                | [ H : ?x = None, H' : context[?x] |- _ ] => rewrite H in H'
+                | [ H : context[combine (map _ _) (map _ _)] |- _ ] => rewrite combine_map_map in H
+                | [ H : context[nth_error (update_nth _ _ _) _] |- _ ] => rewrite nth_update_nth in H
+                | [ H : nth_error (map _ _) _ = Some _ |- _ ] => apply nth_error_map in H
+                | [ H : In _ (map _ _) |- _ ] => rewrite in_map_iff in H
+                | [ H : In _ (combine _ _) |- _ ] => apply In_nth_error_value in H
+                | [ |- expr.wf ?G (fold_right _ _ (map _ (seq ?a ?b))) (fold_right _ _ (map _ (seq ?a ?b))) ]
+                  => induction (seq a b); cbn [fold_right map]
+                | [ Hwf : Compile.wf_value _ ?x _, H : context[SubstVarLike.is_recursively_var_or_ident _ ?x] |- _ ] => erewrite SubstVarLike.wfT_is_recursively_var_or_ident in H by exact Hwf
+                | [ |- UnderLets.wf _ _ (nat_rect _ _ _ _) (nat_rect _ _ _ _) ] => apply wf_nat_rect
+                | [ |- UnderLets.wf _ _ (nat_rect _ _ _ _ _) (nat_rect _ _ _ _ _) ]
+                  => eapply UnderLets.wf_Proper_list; [ | | eapply wf_nat_rect_arrow; [ | | reflexivity | ]; cycle 1 ]; revgoals; hnf
+                | [ H : Compile.wf_value _ ?e1 ?e2 |- UnderLets.wf _ _ (?e1 _) (?e2 _) ]
+                  => eapply UnderLets.wf_Proper_list; [ | | eapply H; [ reflexivity | ] ]; revgoals
+                | [ H : Compile.wf_value _ ?e1 ?e2 |- UnderLets.wf _ _ (?e1 _ _) (?e2 _ _) ]
+                  => eapply UnderLets.wf_Proper_list; [ | | eapply H; [ reflexivity | | reflexivity | ] ]; revgoals
+                | [ H : Compile.wf_value _ ?e1 ?e2 |- UnderLets.wf _ _ (?e1 _ _ _) (?e2 _ _ _) ]
+                  => eapply UnderLets.wf_Proper_list; [ | | eapply H; [ reflexivity | | reflexivity | | reflexivity | ]; cycle 1 ]; revgoals
+                | [ H : Compile.wf_value _ ?e1 ?e2 |- Compile.wf_value' _ (?e1 _) (?e2 _) ]
+                  => eapply UnderLets.wf_Proper_list; [ | | eapply H; [ reflexivity | ] ]; revgoals
+                | [ H : Compile.wf_value _ ?e1 ?e2 |- Compile.wf_value' _ (?e1 _ _) (?e2 _ _) ]
+                  => eapply UnderLets.wf_Proper_list; [ | | eapply H; [ reflexivity | | reflexivity | ] ]; revgoals
+                | [ H : Compile.wf_value _ ?e1 ?e2 |- Compile.wf_value' _ (?e1 _ _ _) (?e2 _ _ _) ]
+                  => eapply UnderLets.wf_Proper_list; [ | | eapply H; [ reflexivity | | reflexivity | | reflexivity | ]; cycle 1 ]; revgoals
+                | [ |- Compile.wf_value _ (fun _ => _) (fun _ => _) ] => hnf
+                | [ H : Compile.wf_value _ ?f ?g |- UnderLets.wf _ _ (?f _) (?g _) ] => eapply UnderLets.wf_Proper_list; [ | | eapply H; solve [ eauto ] ]; solve [ repeat good_t_step ]
+                | [ H : Compile.wf_value _ ?f ?g |- UnderLets.wf _ _ (?f _ _) (?g _ _) ] => eapply UnderLets.wf_Proper_list; [ | | eapply H; solve [ eauto ] ]; solve [ repeat good_t_step ]
+                | [ H : Compile.wf_value _ ?f ?g |- UnderLets.wf _ _ (?f _ _ _) (?g _ _ _) ] => eapply UnderLets.wf_Proper_list; [ | | eapply H; solve [ eauto ] ]; solve [ repeat good_t_step ]
+                | [ H : Compile.wf_value ?G ?e1 ?e2 |- UnderLets.wf _ ?G (?e1 _) (?e2 _) ] => eapply (H nil)
+                | [ |- Compile.wf_anyexpr _ _ _ _ ] => constructor
+                | [ H : Compile.wf_value ?G ?ls1 ?ls2, H1 : rlist_rect_cast ?N1 ?C1 ?ls1 _ (fun x => x) = _, H2 : rlist_rect_cast ?N2 ?C2 ?ls2 _ (fun y => y) = _ |- _ ]
+                  => let H' := fresh in
+                    pose proof (@wf_rlist_rect_cast _ _ _ N1 N2 C1 C2 ls1 ls2 G H) as H'; cbv [id Compile.value] in H', H1, H2; rewrite H1, H2 in H';
+                    clear H1 H2;
+                    first [ apply H'
+                          | refine ((fun pf : Some _ = None => _) _); [ inversion_option | apply H' ] ]
+                | [ H : Compile.wf_value ?G ?ls1 ?ls2, H1 : rlist_rect_cast ?N1 ?C1 ?ls1 _ (fun x => x) = _, H2 : rlist_rect_cast ?N2 ?C2 ?ls2 _ (fun y => y) = _ |- _ ]
+                  => let H' := fresh in
+                    pose proof (@wf_rlist_rect_castv _ _ _ N1 N2 C1 C2 ls1 ls2 G H) as H'; cbv [id Compile.value] in H', H1, H2; rewrite H1, H2 in H';
+                    clear H1 H2;
+                    first [ apply H'
+                          | refine ((fun pf : Some _ = None => _) _); [ inversion_option | apply H' ] ]
+                | [ H : Compile.wf_value ?G ?ls1 ?ls2, H1 : rlist_rect ?N1 ?C1 ?ls1 _ (fun x => x) = _, H2 : rlist_rect ?N2 ?C2 ?ls2 _ (fun y => y) = _ |- _ ]
+                  => let H' := fresh in
+                    pose proof (@wf_rlist_rect _ _ N1 N2 C1 C2 ls1 ls2 G H) as H'; cbv [id Compile.value] in H', H1, H2; rewrite H1, H2 in H';
+                    clear H1 H2;
+                    first [ apply H'
+                          | refine ((fun pf : Some _ = None => _) _); [ inversion_option | apply H' ] ]
+                | [ H : Compile.wf_value ?G ?ls1 ?ls2, H1 : rlist_rect ?N1 ?C1 ?ls1 _ (fun x => x) = _, H2 : rlist_rect ?N2 ?C2 ?ls2 _ (fun y => y) = _ |- _ ]
+                  => let H' := fresh in
+                    pose proof (@wf_rlist_rectv _ _ N1 N2 C1 C2 ls1 ls2 G H) as H'; cbv [id Compile.value] in H', H1, H2; rewrite H1, H2 in H';
+                    clear H1 H2;
+                    first [ apply H'
+                          | refine ((fun pf : Some _ = None => _) _); [ inversion_option | apply H' ] ]
+                | [ H : ?R ?G ?a ?b |- expr.wf ?G ?a ?b ]
+                  => is_evar R; revert H; instantiate (1:=fun G' => expr.wf G'); solve [ auto ]
+                | [ H : expr.wf ?G ?a ?b |- ?R ?G ?a ?b ]
+                  => is_evar R; instantiate (1:=fun G' => expr.wf G'); solve [ auto ]
                 end
+              | progress expr.invert_subst
               | solve [ wf_t ]
-(*| progress cbv [Option.bind]
-                          | break_match_step ltac:(fun _ => idtac)*) ].
+              | break_match_hyps_step ltac:(fun v => let h := head v in constr_eq h (@nth_error))
+              | break_match_hyps_step ltac:(fun v => match v with Nat.eq_dec _ _ => idtac end)
+              | progress cbv [option_map] in * ].
 
       Lemma nbe_rewrite_rules_good
         : rewrite_rules_goodT nbe_rewrite_rules nbe_rewrite_rules.
       Proof.
-        start_good (@nbe_cps_id) (@nbe_rewrite_rules).
-        all: repeat good_t_step.
+        (*Time start_good (@nbe_cps_id) (@nbe_rewrite_rules).
+        Set Ltac Profiling.
+        Time all: try solve [ repeat repeat good_t_step ].
+        Show Ltac Profile.
+        (*start_good (@nbe_cps_id) (@nbe_rewrite_rules).
+        all: repeat good_t_step.*)
+         *)
       Admitted.
 
       Lemma arith_rewrite_rules_good max_const
         : rewrite_rules_goodT (arith_rewrite_rules max_const) (arith_rewrite_rules max_const).
       Proof.
-        start_good (@arith_cps_id) (@arith_rewrite_rules).
-        all: repeat good_t_step.
+        (*
+        Time start_good (@arith_cps_id) (@arith_rewrite_rules).
+        Time all: repeat good_t_step.
+         *)
       Admitted.
 
       Lemma fancy_rewrite_rules_good
@@ -197,11 +581,11 @@ Module Compilers.
             (Hhigh : forall s v v', invert_high s v = Some v' -> v = Z.shiftr v' (s/2))
         : rewrite_rules_goodT (fancy_rewrite_rules invert_low invert_high) (fancy_rewrite_rules invert_low invert_high).
       Proof.
-        start_good (@fancy_cps_id) (@fancy_rewrite_rules).
-        all: repeat good_t_step.
+        Time start_good (@fancy_cps_id) (@fancy_rewrite_rules).
+        Time all: repeat good_t_step.
         all: cbv [Option.bind].
-        all: repeat good_t_step.
-      Qed.
+        Time all: repeat good_t_step.
+      Time Qed.
     End good.
   End RewriteRules.
 End Compilers.
diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v
index 7046b83a2..0cbaaaacf 100644
--- a/src/Experiments/NewPipeline/RewriterWf1.v
+++ b/src/Experiments/NewPipeline/RewriterWf1.v
@@ -625,7 +625,7 @@ Module Compilers.
                                                  (fun G' v1 v2
                                                   => exists (pf1 : anyexpr_ty v1 = t) (pf2 : anyexpr_ty v2 = t),
                                                       forall G'',
-                                                        (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> wf_value G v1' v2')
+                                                        (forall t' v1' v2', List.In (existT _ t' (v1', v2')) G'' -> wf_value G' v1' v2')
                                                         -> expr.wf G''
                                                                    (rew [fun t : base.type => expr t] pf1 in unwrap v1)
                                                                    (rew [fun t : base.type => expr t] pf2 in unwrap v2))
diff --git a/src/Experiments/NewPipeline/RewriterWf2.v b/src/Experiments/NewPipeline/RewriterWf2.v
index 754360994..bdad9d840 100644
--- a/src/Experiments/NewPipeline/RewriterWf2.v
+++ b/src/Experiments/NewPipeline/RewriterWf2.v
@@ -526,6 +526,7 @@ Module Compilers.
                               | progress cbv [rewrite_ruleT id] in *
                               | progress destruct_head'_sigT
                               | rewrite Equality.transport_const
+                              | progress cbv [type.try_transport_cps type.try_make_transport_cps]
                               | progress rewrite_type_transport_correct
                               | progress type_beq_to_eq
                               | congruence