Support type variables in patterns in the rewriter

This paves the way for writing down interpretation proofs for the
rewriter by writing down "default interpretations".  Otherwise, e.g.,
there was not enough type information to write down any good
interpretation for [map fst nil] (which would bind no type variables in
the previous veresion).

Unfortunately the rewriter itself got a bit slower (though the proof of
rewrite-rule-correctness got a bit faster).

After     | File Name                                                            | Before    || Change    | % Change
--------------------------------------------------------------------------------------------------------------------
24m05.07s | Total                                                                | 24m08.92s || -0m03.85s | -0.26%
--------------------------------------------------------------------------------------------------------------------
1m13.28s  | Experiments/NewPipeline/RewriterRulesGood.vo                         | 3m58.20s  || -2m44.91s | -69.23%
2m50.62s  | Experiments/NewPipeline/Rewriter.vo                                  | 1m12.64s  || +1m37.98s | +134.88%
1m45.22s  | Experiments/NewPipeline/RewriterWf2.vo                               | 1m13.64s  || +0m31.57s | +42.88%
0m16.82s  | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.vo    | 0m11.46s  || +0m05.35s | +46.77%
0m08.04s  | Experiments/NewPipeline/RewriterWf1.vo                               | 0m04.52s  || +0m03.51s | +77.87%
6m07.90s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo                | 6m05.01s  || +0m02.88s | +0.79%
0m39.74s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 0m37.09s  || +0m02.64s | +7.14%
0m37.83s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 0m34.94s  || +0m02.89s | +8.27%
0m26.05s  | p384_32.c                                                            | 0m23.72s  || +0m02.33s | +9.82%
0m23.37s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 0m21.01s  || +0m02.35s | +11.23%
0m21.30s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 0m19.02s  || +0m02.28s | +11.98%
0m16.22s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 0m14.01s  || +0m02.20s | +15.77%
4m34.84s  | Experiments/NewPipeline/Toplevel1.vo                                 | 4m36.15s  || -0m01.30s | -0.47%
1m42.79s  | Experiments/NewPipeline/Toplevel2.vo                                 | 1m44.07s  || -0m01.28s | -1.22%
0m40.07s  | p521_32.c                                                            | 0m38.58s  || +0m01.49s | +3.86%
0m33.52s  | p521_64.c                                                            | 0m32.04s  || +0m01.48s | +4.61%
0m12.80s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m11.12s  || +0m01.68s | +15.10%
0m09.01s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m08.76s  || +0m00.25s | +2.85%
0m08.80s  | p384_64.c                                                            | 0m08.49s  || +0m00.31s | +3.65%
0m07.65s  | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.vo          | 0m07.83s  || -0m00.17s | -2.29%
0m05.92s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m05.40s  || +0m00.51s | +9.62%
0m05.59s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.61s  || -0m00.02s | -0.35%
0m04.40s  | secp256k1_32.c                                                       | 0m03.95s  || +0m00.45s | +11.39%
0m04.27s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m03.98s  || +0m00.28s | +7.28%
0m04.27s  | p256_32.c                                                            | 0m03.76s  || +0m00.50s | +13.56%
0m04.23s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m04.14s  || +0m00.09s | +2.17%
0m03.39s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m03.35s  || +0m00.04s | +1.19%
0m02.56s  | p224_32.c                                                            | 0m02.24s  || +0m00.31s | +14.28%
0m02.37s  | curve25519_32.c                                                      | 0m02.18s  || +0m00.18s | +8.71%
0m01.66s  | p224_64.c                                                            | 0m01.66s  || +0m00.00s | +0.00%
0m01.64s  | p256_64.c                                                            | 0m01.53s  || +0m00.10s | +7.18%
0m01.60s  | secp256k1_64.c                                                       | 0m01.50s  || +0m00.10s | +6.66%
0m01.52s  | curve25519_64.c                                                      | 0m01.51s  || +0m00.01s | +0.66%
0m01.38s  | Experiments/NewPipeline/CLI.vo                                       | 0m01.37s  || +0m00.00s | +0.72%
0m01.27s  | Experiments/NewPipeline/StandaloneHaskellMain.vo                     | 0m01.16s  || +0m00.11s | +9.48%
0m01.19s  | Experiments/NewPipeline/StandaloneOCamlMain.vo                       | 0m01.29s  || -0m00.10s | -7.75%
0m01.05s  | Experiments/NewPipeline/CompilersTestCases.vo                        | 0m01.06s  || -0m00.01s | -0.94%
0m00.90s  | Experiments/NewPipeline/RewriterProofs.vo                            | 0m00.94s  || -0m00.03s | -4.25%

1 files changed, 49 insertions, 246 deletions

diff --git a/src/Experiments/NewPipeline/RewriterRulesGood.v b/src/Experiments/NewPipeline/RewriterRulesGood.v
index ef087686a..4e5c79cae 100644
--- a/src/Experiments/NewPipeline/RewriterRulesGood.v
+++ b/src/Experiments/NewPipeline/RewriterRulesGood.v
@@ -65,38 +65,25 @@ Module Compilers.
     Section good.
       Context {var1 var2 : type -> Type}.
 
-      Local Notation rewrite_rules_goodT := (@Compile.rewrite_rules_goodT ident pattern.ident pattern.ident.arg_types var1 var2).
+      Local Notation rewrite_rules_goodT := (@Compile.rewrite_rules_goodT ident pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars) var1 var2).
 
-      Lemma rlist_rect_cps_id {var} A P {ivar} N_case C_case ls T k
-        : @rlist_rect var A P ivar N_case C_case ls T k = k (@rlist_rect var A P ivar N_case C_case ls _ id).
-      Proof.
-        cbv [rlist_rect id Compile.option_bind']; rewrite !expr.reflect_list_cps_id.
-        destruct (invert_expr.reflect_list ls) eqn:?; cbn [Option.bind Option.sequence_return]; reflexivity.
-      Qed.
-      Lemma rlist_rect_cast_cps_id {var} A A' P {ivar} N_case C_case ls T k
-        : @rlist_rect_cast var A A' P ivar N_case C_case ls T k = k (@rlist_rect_cast var A A' P ivar N_case C_case ls _ id).
-      Proof.
-        cbv [rlist_rect_cast Compile.castbe Compile.castb id Compile.option_bind']; rewrite_type_transport_correct;
-          break_innermost_match; type_beq_to_eq; subst; cbn [eq_rect Option.bind Option.sequence_return]; [ | reflexivity ].
-        apply rlist_rect_cps_id.
-      Qed.
-
-      Lemma wf_rlist_rect {A P}
+      Lemma wf_rlist_rect_gen
+            {ivar1 ivar2 A P}
+            Q
             N1 N2 C1 C2 ls1 ls2 G
             (Hwf : expr.wf G ls1 ls2)
-            (HN : UnderLets.wf (fun G' => expr.wf G') G N1 N2)
+            (HN : UnderLets.wf Q 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.
+                -> Q G' rec1 rec2
+                -> UnderLets.wf Q G' (C1 x xs rec1) (C2 y ys rec2))
+        : option_eq (UnderLets.wf Q G)
+                    (@rlist_rect var1 A P ivar1 N1 C1 ls1)
+                    (@rlist_rect var2 A P ivar2 N2 C2 ls2).
+      Proof using Type.
         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
@@ -105,7 +92,6 @@ Module Compilers.
                                       | 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]
@@ -133,35 +119,26 @@ Module Compilers.
                           | reflexivity
                           | solve [ auto ]
                           | progress subst
-                          | apply @UnderLets.wf_splice with (P:=fun G' => expr.wf G')
+                          | apply @UnderLets.wf_splice with (P:=Q)
                           | progress intros
                           | wf_safe_t_step
                           | progress type.inversion_type
                           | progress expr.inversion_wf_constr ].
       Qed.
-
-      Lemma wf_rlist_rect_cast {A A' P}
+      Lemma wf_rlist_rect {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)
+            (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_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.
-
+        : option_eq (UnderLets.wf (fun G' => expr.wf G') G)
+                    (@rlist_rect var1 A P var1 N1 C1 ls1)
+                    (@rlist_rect var2 A P var2 N2 C2 ls2).
+      Proof using Type. apply wf_rlist_rect_gen; assumption. Qed.
       Lemma wf_rlist_rectv {A P}
             N1 N2 C1 C2 ls1 ls2 G
             (Hwf : expr.wf G ls1 ls2)
@@ -182,107 +159,13 @@ Module Compilers.
                                 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) G'',
+                        => exists 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))
+                            /\ expr.wf G'' v1 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
-                          | (exists eq_refl)
-                          | apply @UnderLets.wf_splice with (P:=fun G' v1 v2
-                                                                => exists 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
-                                                                => exists 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
-                                => exists 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)
-                -> (exists 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
-                                => exists 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) 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).
-        destruct H as [? [H0 H1] ].
-        inversion H1; inversion_sigma; type.inversion_type; subst; eauto.
-      Qed.
-
+                    (@rlist_rect var1 A P (@Compile.value _ ident var1) N1 C1 ls1)
+                    (@rlist_rect var2 A P (@Compile.value _ ident var2) N2 C2 ls2).
+      Proof using Type. apply wf_rlist_rect_gen; assumption. Qed.
 
       Lemma wf_nat_rect {A}
             G O1 O2 S1 S2 n
@@ -327,60 +210,6 @@ Module Compilers.
         eapply fold_right_impl_Proper; [ | | refine IHxs ]; intuition (subst; eauto).
       Qed.
 
-      Local Ltac start_cps_id :=
-        lazymatch goal with
-        | [ |- 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;
-        try reflexivity.
-
-      Local Ltac cps_id_step :=
-        first [ reflexivity
-              | progress intros
-              | progress destruct_head' False
-              | progress subst
-              | progress inversion_option
-              | 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
-              | 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] ]
-                  => (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))
-                | [ |- 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))
-                end
-              | progress cbv [Option.bind] in *
-              | break_match_step ltac:(fun _ => idtac) ].
-
-      Local Ltac cps_id_t := start_cps_id; repeat cps_id_step.
-
-      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}
-        : 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}
-        : 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
@@ -394,14 +223,21 @@ Module Compilers.
         eapply fold_right_impl_Proper; [ | | refine IHxs ]; intuition (inversion_prod; subst; eauto).
       Qed.
 
-      Local Ltac start_good cps_id rewrite_rules :=
+      Local Ltac start_good :=
         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 | ]).
+        (exists eq_refl);
+        cbn [eq_rect];
+        cbv [Compile.wf_deep_rewrite_ruleTP_gen Compile.wf_rewrite_rule_data Compile.rew_replacement Compile.rew_is_cps Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unif_rewrite_ruleTP_gen Compile.wf_with_unification_resultT pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.wf_maybe_under_lets_expr Compile.wf_maybe_do_again_expr Compile.wf_with_unification_resultT' pattern.type.under_forall_vars_relation Compile.with_unification_resultT' pattern.collect_vars Compile.ident_collect_vars pattern.ident.type_vars pattern.type.collect_vars pattern.base.collect_vars PositiveSet.empty PositiveSet.elements Compile.forall2_type_of_list_cps pattern.ident.arg_types pattern.type.subst_default pattern.base.subst_default PositiveSet.rev PositiveMap.empty];
+        cbn [List.map List.fold_right PositiveSet.union PositiveSet.xelements List.rev List.app projT1 projT2 list_rect PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add PositiveMap.find orb];
+        repeat first [ progress intros
+                     | match goal with
+                       | [ |- { pf : ?x = ?x | _ } ] => (exists eq_refl)
+                       end
+                     | progress cbn [eq_rect] in * ].
 
       Local Ltac good_t_step :=
         first [ progress subst
@@ -414,17 +250,18 @@ Module Compilers.
               | 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 cbn [pattern.ident.arg_types] in *
+              | progress cbn [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 [id pattern.ident.arg_types Compile.value cpsbind cpscall cpsreturn cps_option_bind type_base ident.smart_Literal rwhen rwhenl 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
+              | match goal with
+                | [ |- context[invert_expr.reflect_list ?v] ] => destruct (invert_expr.reflect_list v) eqn:?
+                end
               | break_innermost_match_step
               | wf_safe_t_step
               | rewrite !expr.reflect_list_cps_id
@@ -437,6 +274,8 @@ Module Compilers.
                     apply nth_error_value_length in H;
                     exfalso; clear -H0 H H'; lia
                 | [ |- expr.wf _ (reify_list _) (reify_list _) ] => rewrite expr.wf_reify_list
+                | [ |- option_eq _ (rlist_rect _ _ _) (rlist_rect _ _ _) ]
+                  => first [ apply wf_rlist_rect | apply wf_rlist_rectv ]
                 | [ |- 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)
@@ -447,20 +286,10 @@ Module Compilers.
                 | [ |- 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
-                | [ |- 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))
-                | [ |- 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))
                 | [ |- ?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 ];
+                           | 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
@@ -508,37 +337,11 @@ Module Compilers.
                 | [ 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 ]
                 | [ |- (forall t v1 v2, In _ _ -> _) /\ expr.wf _ _ _ ] => apply conj; revgoals
-                | [ |- (forall t v1 v2, In _ _ -> _) /\ Compile.wf_anyexpr _ _ _ _ ] => apply conj; revgoals
                 | [ H : expr.wf _ ?x ?y |- Compile.wf_value _ ?x ?y ] => hnf
                 | [ |- Compile.wf_value _ ?x ?y ] => eapply Compile.wf_value'_Proper_list; [ | solve [ cbv [Compile.wf_value] in *; eauto ] ]; solve [ wf_t ]
                 | [ |- In ?x ?ls ] => is_evar ls; refine (or_introl eq_refl : In x (x :: _)); shelve
@@ -553,15 +356,15 @@ Module Compilers.
 
       Lemma nbe_rewrite_rules_good
         : rewrite_rules_goodT nbe_rewrite_rules nbe_rewrite_rules.
-      Proof.
-        Time start_good (@nbe_cps_id) (@nbe_rewrite_rules).
+      Proof using Type.
+        Time start_good.
         Time all: repeat repeat good_t_step.
       Qed.
 
       Lemma arith_rewrite_rules_good max_const
         : rewrite_rules_goodT (arith_rewrite_rules max_const) (arith_rewrite_rules max_const).
-      Proof.
-        Time start_good (@arith_cps_id) (@arith_rewrite_rules).
+      Proof using Type.
+        Time start_good.
         Time all: repeat good_t_step.
       Qed.
 
@@ -570,12 +373,12 @@ Module Compilers.
             (Hlow : forall s v v', invert_low s v = Some v' -> v = Z.land v' (2^(s/2)-1))
             (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.
-        Time start_good (@fancy_cps_id) (@fancy_rewrite_rules).
+      Proof using Type.
+        Time start_good.
         Time all: repeat good_t_step.
         all: cbv [Option.bind].
         Time all: repeat good_t_step.
-      Time Qed.
+      Qed.
     End good.
   End RewriteRules.
 End Compilers.