Refactor/generalize some pipeline definitions/proofs

When we do rewriting after casts, we will need to do extra passes of DCE
and subst01 to fully reduce things, so we generalize some of the interp
proofs over cast behavior.

For ease of rewriting, we make [ident.interp] an alias (notation) for
[ident.gen_interp], rather than a [Definition].

We also factor out the rewriting wrapper inside the pipeline module into
its own definition.

6 files changed, 237 insertions, 197 deletions

diff --git a/.gitignore b/.gitignore
index 51f1d10ce..a832118d6 100644
--- a/.gitignore
+++ b/.gitignore
@@ -45,6 +45,8 @@ nra.cache
 /time-of-build-pretty.log
 /time-of-build.log
 
+/*.out
+
 # compilation outputs
 /*.o
 etc/tscfreq
diff --git a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
index 2d871b103..0e7d55c7a 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
@@ -1281,8 +1281,8 @@ Module Compilers.
     assert (arg1_Proper : Proper (type.and_for_each_lhs_of_arrow (@type.related base.type base.interp (fun _ => eq))) arg1)
         by (hnf; etransitivity; [ eassumption | symmetry; eassumption ]).
     assert (arg2_Proper : Proper (type.and_for_each_lhs_of_arrow (@type.related base.type base.interp (fun _ => eq))) arg2)
-        by (hnf; etransitivity; [ symmetry; eassumption | eassumption ]).
-    rewrite <- (@GeneralizeVar.Interp_GeneralizeVar _ E) by auto.
+      by (hnf; etransitivity; [ symmetry; eassumption | eassumption ]).
+    rewrite <- (@GeneralizeVar.Interp_GeneralizeVar _ _ E) by auto.
     apply Interp_EtaExpandWithListInfoFromBound; auto with wf.
   Qed.
 
@@ -1324,7 +1324,6 @@ Module Compilers.
                         | rewrite <- Extract_FromFlat_ToFlat by auto with typeclass_instances; apply Interp_PartialEvaluateWithBounds_bounded; auto
                         | rewrite Extract_FromFlat_ToFlat by auto with wf typeclass_instances
                         | progress intros
-                        | progress cbv [ident.interp]
                         | eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; [ eassumption | ]
                         | solve [ eauto with wf typeclass_instances ]
                         | erewrite !Interp_PartialEvaluateWithBounds
diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v
index bd668c50e..07b416f54 100644
--- a/src/Experiments/NewPipeline/Language.v
+++ b/src/Experiments/NewPipeline/Language.v
@@ -1021,13 +1021,11 @@ Module Compilers.
 
       Definition cast_outside_of_range (r : zrange) (v : BinInt.Z) : BinInt.Z.
       Proof. exact v. Qed.
-
-      (** Interpret identifiers where [Z_cast] is an opaque identity
-         function when the value is not inside the range *)
-      Definition interp {t} (idc : ident t) : type.interp base.interp t
-        := @gen_interp cast_outside_of_range t idc.
-      Global Arguments interp _ !_ / .
     End with_base.
+
+    (** Interpret identifiers where [Z_cast] is an opaque identity
+        function when the value is not inside the range *)
+    Notation interp := (@gen_interp cast_outside_of_range).
     Notation LiteralUnit := (@Literal base.type.unit).
     Notation LiteralZ := (@Literal base.type.Z).
     Notation LiteralBool := (@Literal base.type.bool).
@@ -1297,14 +1295,13 @@ Module Compilers.
       Notation "x || y" := (#Z_lor @ x @ y)%expr : expr_scope.
       Notation "x 'mod' y" := (#Z_modulo @ x @ y)%expr : expr_scope.
       Notation "- x" := (#Z_opp @ x)%expr : expr_scope.
-      Global Arguments interp _ !_.
       Global Arguments gen_interp _ _ !_.
     End Notations.
   End ident.
   Export ident.Notations.
   Notation ident := ident.ident.
 
-  Global Strategy -1000 [expr.Interp expr.interp ident.interp type.interp base.interp base.base_interp ident.gen_interp].
+  Global Strategy -1000 [expr.Interp expr.interp type.interp base.interp base.base_interp ident.gen_interp].
   Ltac reify var term :=
     expr.reify base.type ident ltac:(base.reify) ident.reify var term.
   Ltac Reify term :=
diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v
index 4caa34297..1a90024e4 100644
--- a/src/Experiments/NewPipeline/LanguageWf.v
+++ b/src/Experiments/NewPipeline/LanguageWf.v
@@ -728,18 +728,21 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
       End with_1.
     End interp_gen.
 
-    Section for_interp.
+    Section with_cast.
+      Context {cast_outside_of_range : ZRange.zrange -> BinInt.Z -> BinInt.Z}.
+      Local Notation ident_interp := (@ident.gen_interp cast_outside_of_range).
+      Local Notation interp := (@expr.interp _ _ _ (@ident_interp)).
+      Local Notation Interp := (@expr.Interp _ _ _ (@ident_interp)).
       Local Open Scope etype_scope.
-      Import defaults.
       Lemma wf_interp_Proper G {t} e1 e2
             (Hwf : @wf _ _ _ _ G t e1 e2)
             (HG : forall t v1 v2, In (existT _ t (v1, v2)) G -> v1 == v2)
         : interp e1 == interp e2.
-      Proof. apply @wf_interp_Proper_gen1 with (G:=G); eauto using ident.interp_Proper. Qed.
+      Proof. apply @wf_interp_Proper_gen1 with (G:=G); eauto using ident.gen_interp_Proper. Qed.
 
-      Lemma Wf_Interp_Proper {t} (e : Expr t) : Wf e -> Proper type.eqv (Interp e).
+      Lemma Wf_Interp_Proper {t} (e : expr.Expr t) : Wf e -> Proper type.eqv (Interp e).
       Proof. repeat intro; apply wf_interp_Proper with (G:=nil); cbn [List.In]; intuition eauto. Qed.
-    End for_interp.
+    End with_cast.
 
     Section invert.
       Section with_var2.
@@ -1420,21 +1423,17 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
       Proof. apply @Interp_gen2_GeneralizeVar; eassumption. Qed.
     End gen1.
 
-    Lemma interp_from_flat_to_flat'
-          {t} (e1 : expr t) (e2 : expr t) G ctx
-          (H_ctx_G : forall t v1 v2, List.In (existT _ t (v1, v2)) G
-                                     -> (exists v2', PositiveMap.find v1 ctx = Some (existT _ t v2') /\ v2' == v2))
-          (Hwf : expr.wf G e1 e2)
-          cur_idx
-          (Hidx : forall p, PositiveMap.mem p ctx = true -> BinPos.Pos.lt p cur_idx)
-      : interp (from_flat (to_flat' e1 cur_idx) _ ctx) == interp e2.
-    Proof. apply @interp_gen1_from_flat_to_flat' with (G:=G); eauto using ident.interp_Proper. Qed.
+    Section with_cast.
+      Context {cast_outside_of_range : zrange -> Z -> Z}.
+
+      Local Notation Interp := (expr.Interp (@ident.gen_interp cast_outside_of_range)).
 
-    Lemma Interp_FromFlat_ToFlat {t} (e : Expr t) (Hwf : expr.Wf e) : Interp (FromFlat (ToFlat e)) == Interp e.
-    Proof. apply @Interp_gen1_FromFlat_ToFlat; eauto using ident.interp_Proper. Qed.
+      Lemma Interp_FromFlat_ToFlat {t} (e : Expr t) (Hwf : expr.Wf e) : Interp (FromFlat (ToFlat e)) == Interp e.
+      Proof. apply @Interp_gen1_FromFlat_ToFlat; eauto using ident.gen_interp_Proper. Qed.
 
-    Lemma Interp_GeneralizeVar {t} (e : Expr t) (Hwf : expr.Wf e) : Interp (GeneralizeVar (e _)) == Interp e.
-    Proof. apply Interp_FromFlat_ToFlat, Hwf. Qed.
+      Lemma Interp_GeneralizeVar {t} (e : Expr t) (Hwf : expr.Wf e) : Interp (GeneralizeVar (e _)) == Interp e.
+      Proof. apply Interp_FromFlat_ToFlat, Hwf. Qed.
+    End with_cast.
   End GeneralizeVar.
 
   Ltac prove_Wf _ :=
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v
index 59ce4a33e..ac6cd218d 100644
--- a/src/Experiments/NewPipeline/Toplevel1.v
+++ b/src/Experiments/NewPipeline/Toplevel1.v
@@ -675,6 +675,30 @@ Module Pipeline.
 
   Record to_fancy_args := { invert_low : Z (*log2wordmax*) -> Z -> option Z ; invert_high : Z (*log2wordmax*) -> Z -> option Z }.
 
+  Definition RewriteAndEliminateDeadAndInline {t}
+             (DoRewrite : Expr t -> Expr t)
+             (with_dead_code_elimination : bool)
+             (with_subst01 : bool)
+             (E : Expr t)
+    : Expr t
+    := let E := DoRewrite E in
+       (* Note that DCE evaluates the expr with two different [var]
+          arguments, and so results in a pipeline that is 2x slower
+          unless we pass through a uniformly concrete [var] type
+          first *)
+       dlet_nd e := ToFlat E in
+       let E := FromFlat e in
+       let E := if with_dead_code_elimination then DeadCodeElimination.EliminateDead E else E in
+       dlet_nd e := ToFlat E in
+       let E := FromFlat e in
+       let E := if with_subst01 then Subst01.Subst01 E else E in
+       let E := UnderLets.LetBindReturn E in
+       let E := DoRewrite E in (* after inlining, see if any new rewrite redexes are available *)
+       dlet_nd e := ToFlat E in
+       let E := FromFlat e in
+       let E := if with_dead_code_elimination then DeadCodeElimination.EliminateDead E else E in
+       E.
+
   Definition BoundsPipeline
              (with_dead_code_elimination : bool := true)
              (with_subst01 : bool)
@@ -688,22 +712,7 @@ Module Pipeline.
     := (*let E := expr.Uncurry E in*)
       let E := PartialEvaluateWithListInfoFromBounds E arg_bounds in
       let E := PartialEvaluate E in
-      let E := RewriteRules.RewriteArith 0 E in
-      (* Note that DCE evaluates the expr with two different [var]
-         arguments, and so results in a pipeline that is 2x slower
-         unless we pass through a uniformly concrete [var] type
-         first *)
-      dlet_nd e := ToFlat E in
-      let E := FromFlat e in
-      let E := if with_dead_code_elimination then DeadCodeElimination.EliminateDead E else E in
-      dlet_nd e := ToFlat E in
-      let E := FromFlat e in
-      let E := if with_subst01 then Subst01.Subst01 E else E in
-      let E := UnderLets.LetBindReturn E in
-      let E := RewriteRules.RewriteArith 0 E in (* after inlining, see if any new rewrite redexes are available *)
-      dlet_nd e := ToFlat E in
-      let E := FromFlat e in
-      let E := if with_dead_code_elimination then DeadCodeElimination.EliminateDead E else E in
+      let E := RewriteAndEliminateDeadAndInline (RewriteRules.RewriteArith 0) with_dead_code_elimination with_subst01 E in
       let E := RewriteRules.RewriteArith (2^8) E in (* reassociate small consts *)
       let E := match translate_to_fancy with
                | Some {| invert_low := invert_low ; invert_high := invert_high |} => RewriteRules.RewriteToFancy invert_low invert_high E
@@ -788,7 +797,8 @@ Module Pipeline.
                  | solve [ auto with interp wf ]
                  | solve [ typeclasses eauto ]
                  | break_innermost_match_step
-                 | solve [ auto 100 with wf ] ].
+                 | solve [ auto 100 with wf ]
+                 | progress intros ].
 
   Class bounds_goodT {t} bounds
     := bounds_good :
@@ -800,6 +810,30 @@ Module Pipeline.
 
   Hint Extern 1 (type_goodT _) => vm_compute; reflexivity : typeclass_instances.
 
+  Lemma Wf_RewriteAndEliminateDeadAndInline {t} DoRewrite with_dead_code_elimination with_subst01
+        (Wf_DoRewrite : forall E, Wf E -> Wf (DoRewrite E))
+        E
+        (Hwf : Wf E)
+    : Wf (@RewriteAndEliminateDeadAndInline t DoRewrite with_dead_code_elimination with_subst01 E).
+  Proof. cbv [RewriteAndEliminateDeadAndInline Let_In]; wf_interp_t. Qed.
+
+  Global Hint Resolve @Wf_RewriteAndEliminateDeadAndInline : wf.
+
+  Lemma Interp_RewriteAndEliminateDeadAndInline {cast_outside_of_range} {t} DoRewrite with_dead_code_elimination with_subst01
+        (Interp_DoRewrite : forall E, Wf E -> expr.Interp (@ident.gen_interp cast_outside_of_range) (DoRewrite E) == expr.Interp (@ident.gen_interp cast_outside_of_range) E)
+        (Wf_DoRewrite : forall E, Wf E -> Wf (DoRewrite E))
+        E
+        (Hwf : Wf E)
+    : expr.Interp (@ident.gen_interp cast_outside_of_range) (@RewriteAndEliminateDeadAndInline t DoRewrite with_dead_code_elimination with_subst01 E)
+      == expr.Interp (@ident.gen_interp cast_outside_of_range) E.
+  Proof.
+    cbv [RewriteAndEliminateDeadAndInline Let_In];
+      repeat (wf_interp_t || rewrite !Interp_DoRewrite).
+  Qed.
+
+  Global Hint Rewrite @Interp_RewriteAndEliminateDeadAndInline : interp.
+
+  Local Opaque RewriteAndEliminateDeadAndInline.
   Lemma BoundsPipeline_correct
              (with_dead_code_elimination : bool := true)
              (with_subst01 : bool)
@@ -862,6 +896,7 @@ Module Pipeline.
         all: wf_interp_t. }
       { wf_interp_t. } }
   Qed.
+  Local Transparent RewriteAndEliminateDeadAndInline.
 
   Definition BoundsPipeline_correct_transT
              {t}
diff --git a/src/Experiments/NewPipeline/UnderLetsProofs.v b/src/Experiments/NewPipeline/UnderLetsProofs.v
index 8882f7a47..dcc5cf28b 100644
--- a/src/Experiments/NewPipeline/UnderLetsProofs.v
+++ b/src/Experiments/NewPipeline/UnderLetsProofs.v
@@ -144,9 +144,16 @@ Module Compilers.
       : expr.Wf e -> expr.Wf (SubstVarLike.SubstVarFstSndPairOpp e).
     Proof. apply Wf_SubstVarOrIdent. Qed.
 
-    Lemma Interp_SubstVarFstSndPairOpp {t} (e : expr.Expr t) (Hwf : expr.Wf e)
-      : defaults.Interp (SubstVarLike.SubstVarFstSndPairOpp e) == defaults.Interp e.
-    Proof. apply Interp_SubstVarOrIdent, Hwf. Qed.
+    Section with_cast.
+      Context {cast_outside_of_range : ZRange.zrange -> BinInt.Z -> BinInt.Z}.
+      Local Notation ident_interp := (@ident.gen_interp cast_outside_of_range).
+      Local Notation interp := (@expr.interp _ _ _ (@ident_interp)).
+      Local Notation Interp := (@expr.Interp _ _ _ (@ident_interp)).
+
+      Lemma Interp_SubstVarFstSndPairOpp {t} (e : expr.Expr t) (Hwf : expr.Wf e)
+        : Interp (SubstVarLike.SubstVarFstSndPairOpp e) == Interp e.
+      Proof. apply Interp_SubstVarOrIdent, Hwf. Qed.
+    End with_cast.
   End SubstVarLike.
 
   Hint Resolve SubstVarLike.Wf_SubstVar SubstVarLike.Wf_SubstVarFstSndPairOpp SubstVarLike.Wf_SubstVarLike SubstVarLike.Wf_SubstVarOrIdent : wf.
@@ -477,6 +484,7 @@ Module Compilers.
         Context (cast_outside_of_range : ZRange.zrange -> BinInt.Z -> BinInt.Z).
         Local Notation ident_interp := (@ident.gen_interp cast_outside_of_range).
         Local Notation interp := (@expr.interp _ _ _ (@ident_interp)).
+        Local Notation Interp := (@expr.Interp _ _ _ (@ident_interp)).
 
         Lemma interp_reify_and_let_binds_base_cps
               {t e T k}
@@ -512,161 +520,161 @@ Module Compilers.
           eapply interp_reify_and_let_binds_base_cps; cbn [UnderLets.interp].
           trivial.
         Qed.
-      End with_cast.
 
-      Lemma Wf_LetBindReturn {t} (e : expr.Expr t) (Hwf : expr.Wf e) : expr.Wf (LetBindReturn e).
-      Proof. intros ??; apply wf_let_bind_return, Hwf. Qed.
+        Local Ltac interp_to_expr_reify_and_let_binds_base_cps_t Hk :=
+          repeat first [ progress subst
+                       | progress destruct_head' False
+                       | progress destruct_head'_and
+                       | progress destruct_head' iff
+                       | progress specialize_by_assumption
+                       | progress expr.inversion_wf_constr
+                       | progress expr.inversion_expr
+                       | progress expr.invert_subst
+                       | progress destruct_head'_sig
+                       | progress destruct_head'_ex
+                       | progress destruct_head'_and
+                       | progress type.inversion_type
+                       | progress base.type.inversion_type
+                       | progress cbn [invert_Var invert_Literal ident.invert_Literal eq_rect f_equal f_equal2 type.decode fst snd projT1 projT2 invert_pair Option.bind to_expr expr.interp ident.interp ident.gen_interp type.eqv length list_rect combine In] in *
+                       | progress cbv [type.try_transport type.try_transport_cps CPSNotations.cps_option_bind CPSNotations.cpsreturn CPSNotations.cpsbind CPSNotations.cpscall type.try_make_transport_cps id] in *
+                       | rewrite base.try_make_transport_cps_correct in *
+                       | progress type_beq_to_eq
+                       | discriminate
+                       | congruence
+                       | apply Hk
+                       | exists nil; reflexivity
+                       | eexists (cons _ nil); reflexivity
+                       | rewrite app_assoc; eexists; reflexivity
+                       | rewrite expr.reify_list_cons
+                       | rewrite expr.reify_list_nil
+                       | progress interp_safe_t
+                       | match goal with
+                         | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H
+                         | [ H : forall t v1 v2, In _ _ -> _ == _, H' : In _ _ |- _ ] => apply H in H'
+                         end
+                       | progress inversion_option
+                       | progress break_innermost_match_hyps
+                       | progress expr.inversion_wf_one_constr
+                       | progress expr.invert_match_step
+                       | match goal with
+                         | [ |- ?R (expr.interp _ ?e1) (expr.interp _ ?e2) ]
+                           => solve [ eapply (@expr.wf_interp_Proper _ _ _ e1 e2); eauto ]
+                         | [ H : context[reflect_list (reify_list _)] |- _ ] => rewrite expr.reflect_reify_list in H
+                         | [ H : forall x y, @?A x y \/ @?B x y -> @?C x y |- _ ]
+                           => pose proof (fun x y pf => H x y (or_introl pf));
+                              pose proof (fun x y pf => H x y (or_intror pf));
+                              clear H
+                         end
+                       | progress interp_unsafe_t_step
+                       | match goal with
+                         | [ H : expr.wf _ (reify_list _) ?e |- _ ]
+                           => is_var e; destruct (reflect_list e) eqn:?; expr.invert_subst;
+                              [ rewrite expr.wf_reify_list in H | apply expr.wf_reflect_list in H ]
+                         | [ H : SubstVarLike.is_recursively_var_or_ident _ _ = _ |- _ ] => clear H
+                         | [ H : context[expr.interp _ _ = _] |- expr.interp _ (to_expr _) = ?k2 _ ]
+                           => erewrite H; clear H;
+                              [ match goal with
+                                | [ |- ?k (expr.interp ?ii ?e) = ?k' ?v ]
+                                  => has_evar e;
+                                     let p := fresh in
+                                     set (p := expr.interp ii e);
+                                     match v with
+                                     | context G[expr.interp ii ?e']
+                                       => unify e e'; let v' := context G[p] in change (k p = k' v')
+                                     end;
+                                     clearbody p; reflexivity
+                                end
+                              | .. ]
+                         end ].
 
-      Local Ltac interp_to_expr_reify_and_let_binds_base_cps_t Hk :=
-        repeat first [ progress subst
-                     | progress destruct_head' False
-                     | progress destruct_head'_and
-                     | progress destruct_head' iff
-                     | progress specialize_by_assumption
-                     | progress expr.inversion_wf_constr
-                     | progress expr.inversion_expr
-                     | progress expr.invert_subst
-                     | progress destruct_head'_sig
-                     | progress destruct_head'_ex
-                     | progress destruct_head'_and
-                     | progress type.inversion_type
-                     | progress base.type.inversion_type
-                     | progress cbn [invert_Var invert_Literal ident.invert_Literal eq_rect f_equal f_equal2 type.decode fst snd projT1 projT2 invert_pair Option.bind to_expr expr.interp ident.interp ident.gen_interp type.eqv length list_rect combine In] in *
-                     | progress cbv [type.try_transport type.try_transport_cps CPSNotations.cps_option_bind CPSNotations.cpsreturn CPSNotations.cpsbind CPSNotations.cpscall type.try_make_transport_cps id] in *
-                     | rewrite base.try_make_transport_cps_correct in *
-                     | progress type_beq_to_eq
-                     | discriminate
-                     | congruence
-                     | apply Hk
-                     | exists nil; reflexivity
-                     | eexists (cons _ nil); reflexivity
-                     | rewrite app_assoc; eexists; reflexivity
-                     | rewrite expr.reify_list_cons
-                     | rewrite expr.reify_list_nil
-                     | progress interp_safe_t
-                     | match goal with
-                       | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H
-                       | [ H : forall t v1 v2, In _ _ -> _ == _, H' : In _ _ |- _ ] => apply H in H'
-                       end
-                     | progress inversion_option
-                     | progress break_innermost_match_hyps
-                     | progress expr.inversion_wf_one_constr
-                     | progress expr.invert_match_step
-                     | match goal with
-                       | [ |- ?R (expr.interp _ ?e1) (expr.interp _ ?e2) ]
-                         => solve [ eapply (@expr.wf_interp_Proper _ _ e1 e2); eauto ]
-                       | [ H : context[reflect_list (reify_list _)] |- _ ] => rewrite expr.reflect_reify_list in H
-                       | [ H : forall x y, @?A x y \/ @?B x y -> @?C x y |- _ ]
-                         => pose proof (fun x y pf => H x y (or_introl pf));
-                            pose proof (fun x y pf => H x y (or_intror pf));
-                            clear H
-                       end
-                     | progress interp_unsafe_t_step
-                     | match goal with
-                       | [ H : expr.wf _ (reify_list _) ?e |- _ ]
-                         => is_var e; destruct (reflect_list e) eqn:?; expr.invert_subst;
-                            [ rewrite expr.wf_reify_list in H | apply expr.wf_reflect_list in H ]
-                       | [ H : SubstVarLike.is_recursively_var_or_ident _ _ = _ |- _ ] => clear H
-                       | [ H : context[expr.interp _ _ = _] |- expr.interp _ (to_expr _) = ?k2 _ ]
-                         => erewrite H; clear H;
-                            [ match goal with
-                              | [ |- ?k (expr.interp ?ii ?e) = ?k' ?v ]
-                                => has_evar e;
-                                   let p := fresh in
-                                   set (p := expr.interp ii e);
-                                   match v with
-                                   | context G[expr.interp ii ?e']
-                                     => unify e e'; let v' := context G[p] in change (k p = k' v')
-                                   end;
-                                   clearbody p; reflexivity
-                              end
-                            | .. ]
-                       end ].
-
-      Lemma interp_to_expr_reify_and_let_binds_base_cps {t : base.type} {t' : base.type} (e1 : expr (type.base t)) (e2 : expr (type.base t))
-            G
-            (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> v1 == v2)
-            (Hwf : expr.wf G e1 e2)
-            (k1 : expr (type.base t) -> UnderLets _ (expr (type.base t')))
-            (k2 : base.interp t -> base.interp t')
-            (Hk : forall e1 v, defaults.interp e1 == v -> defaults.interp (to_expr (k1 e1)) == k2 v)
-        : defaults.interp (to_expr (reify_and_let_binds_base_cps e1 _ k1)) == k2 (defaults.interp e2).
-      Proof.
-        revert dependent G; revert dependent t'; induction t; cbn [reify_and_let_binds_base_cps]; intros;
+        Lemma interp_to_expr_reify_and_let_binds_base_cps {t : base.type} {t' : base.type} (e1 : expr (type.base t)) (e2 : expr (type.base t))
+              G
+              (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> v1 == v2)
+              (Hwf : expr.wf G e1 e2)
+              (k1 : expr (type.base t) -> UnderLets _ (expr (type.base t')))
+              (k2 : base.interp t -> base.interp t')
+              (Hk : forall e1 v, interp e1 == v -> interp (to_expr (k1 e1)) == k2 v)
+          : interp (to_expr (reify_and_let_binds_base_cps e1 _ k1)) == k2 (interp e2).
+        Proof.
+          revert dependent G; revert dependent t'; induction t; cbn [reify_and_let_binds_base_cps]; intros;
             try (cbv [SubstVarLike.is_var_fst_snd_pair_opp] in *; erewrite !SubstVarLike.wfT_is_recursively_var_or_ident by eassumption);
             break_innermost_match; interp_to_expr_reify_and_let_binds_base_cps_t Hk.
-        all: repeat match goal with H : list (sigT _) |- _ => revert dependent H end.
-        all: revert dependent k1; revert dependent k2.
-        all: lazymatch goal with
-             | [ H : length ?l1 = length ?l2 |- _ ]
-               => is_var l1; is_var l2; revert dependent l2; induction l1; intro l2; destruct l2; intros
-             end;
-          interp_to_expr_reify_and_let_binds_base_cps_t Hk.
-      Qed.
+          all: repeat match goal with H : list (sigT _) |- _ => revert dependent H end.
+          all: revert dependent k1; revert dependent k2.
+          all: lazymatch goal with
+               | [ H : length ?l1 = length ?l2 |- _ ]
+                 => is_var l1; is_var l2; revert dependent l2; induction l1; intro l2; destruct l2; intros
+               end;
+            interp_to_expr_reify_and_let_binds_base_cps_t Hk.
+        Qed.
 
-      Lemma interp_let_bind_return {t} (e1 e2 : expr t)
-            G
-            (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> v1 == v2)
-            (Hwf : expr.wf G e1 e2)
-        : defaults.interp (let_bind_return e1) == defaults.interp e2.
-      Proof.
-        revert dependent G; induction t; intros; cbn [let_bind_return type.eqv expr.interp] in *; cbv [invert_Abs respectful] in *;
-          repeat first [ progress wf_safe_t
-                       | progress expr.invert_subst
-                       | progress expr.invert_match
-                       | progress expr.inversion_wf
-                       | progress break_innermost_match_hyps
-                       | progress destruct_head' False
-                       | solve [ wf_t ]
-                       | match goal with
-                         | [ H : _ |- expr.interp _ (let_bind_return ?e0) == expr.interp _ ?e ?v ]
-                           => eapply (H e0 (e @ $v)%expr (cons _ _)); [ .. | solve [ wf_t ] ]; solve [ wf_t ]
-                         | [ H : _ |- expr.interp _ (let_bind_return ?e0) == expr.interp _ ?e ?v ]
-                           => cbn [expr.interp]; eapply H; [ | solve [ wf_t ] ]; solve [ wf_t ]
-                         end ];
-          [].
-        { pose (P := fun t => { e1e2 : expr t * expr t | expr.wf G (fst e1e2) (snd e1e2) }).
-          pose ((exist _ (e1, e2) Hwf) : P _) as pkg.
-          change e1 with (fst (proj1_sig pkg)).
-          change e2 with (snd (proj1_sig pkg)).
-          clearbody pkg; clear Hwf e1 e2.
-          type.generalize_one_eq_var pkg; subst P; destruct pkg as [ [e1 e2] Hwf ].
-          cbn [fst snd proj1_sig proj2_sig] in *.
-          repeat match goal with
-                 | [ |- context[proj1_sig (rew [fun t => @sig (@?A t) (@?P t)] ?pf in exist ?P0 ?x ?p)] ]
-                   => progress replace (proj1_sig (rew pf in exist P0 x p)) with (rew [A] pf in x) by (case pf; reflexivity)
-                 | [ |- context[fst (rew [fun t => @prod (@?A t) (@?B t)] ?pf in pair ?x ?y)] ]
-                   => progress replace (fst (rew pf in pair x y)) with (rew [A] pf in x) by (case pf; reflexivity)
-                 | [ |- context[snd (rew [fun t => @prod (@?A t) (@?B t)] ?pf in pair ?x ?y)] ]
-                   => progress replace (fst (rew pf in pair x y)) with (rew [B] pf in y) by (case pf; reflexivity)
-                 end.
-          assert (H' : t = match t' with type.base t' => t' | _ => t end) by (subst; reflexivity).
-          revert pf.
-          rewrite H'; clear H'.
-          induction Hwf; break_innermost_match; break_innermost_match_hyps;
-            repeat first [ progress intros
-                         | progress type.inversion_type
-                         | progress base.type.inversion_type
-                         | progress wf_safe_t
-                         | progress cbn [of_expr fst snd splice eq_rect type.decode f_equal to_expr] in *
+        Lemma interp_let_bind_return {t} (e1 e2 : expr t)
+              G
+              (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> v1 == v2)
+              (Hwf : expr.wf G e1 e2)
+          : interp (let_bind_return e1) == interp e2.
+        Proof.
+          revert dependent G; induction t; intros; cbn [let_bind_return type.eqv expr.interp] in *; cbv [invert_Abs respectful] in *;
+            repeat first [ progress wf_safe_t
+                         | progress expr.invert_subst
+                         | progress expr.invert_match
+                         | progress expr.inversion_wf
+                         | progress break_innermost_match_hyps
+                         | progress destruct_head' False
+                         | solve [ wf_t ]
                          | match goal with
-                           | [ H : forall pf : ?x = ?x, _ |- _ ] => specialize (H eq_refl)
-                           | [ H : forall x (pf : ?a = ?a), _ |- _ ] => specialize (fun x => H x eq_refl)
-                           | [ H : forall x y (pf : ?a = ?a), _ |- _ ] => specialize (fun x y => H x y eq_refl)
-                           | [ H : forall x y z (pf : ?a = ?a), _ |- _ ] => specialize (fun x y z => H x y z eq_refl)
-                           | [ |- context[(expr_let x := _ in _)%expr] ] => progress cbn [expr.interp]; cbv [LetIn.Let_In]
-                           | [ H : context[expr.interp _ _ = expr.interp _ _] |- expr.interp _ _ = expr.interp _ _ ]
-                             => eapply H; eauto with nocore
-                           end
-                         | solve [ eauto ]
-                         | solve [ eapply expr.wf_interp_Proper; eauto ] ].
-          all: eapply interp_to_expr_reify_and_let_binds_base_cps with (k1:=Base) (k2:=(fun x => x)); eauto; wf_safe_t. }
-      Qed.
+                           | [ H : _ |- expr.interp _ (let_bind_return ?e0) == expr.interp _ ?e ?v ]
+                             => eapply (H e0 (e @ $v)%expr (cons _ _)); [ .. | solve [ wf_t ] ]; solve [ wf_t ]
+                           | [ H : _ |- expr.interp _ (let_bind_return ?e0) == expr.interp _ ?e ?v ]
+                             => cbn [expr.interp]; eapply H; [ | solve [ wf_t ] ]; solve [ wf_t ]
+                           end ];
+            [].
+          { pose (P := fun t => { e1e2 : expr t * expr t | expr.wf G (fst e1e2) (snd e1e2) }).
+            pose ((exist _ (e1, e2) Hwf) : P _) as pkg.
+            change e1 with (fst (proj1_sig pkg)).
+            change e2 with (snd (proj1_sig pkg)).
+            clearbody pkg; clear Hwf e1 e2.
+            type.generalize_one_eq_var pkg; subst P; destruct pkg as [ [e1 e2] Hwf ].
+            cbn [fst snd proj1_sig proj2_sig] in *.
+            repeat match goal with
+                   | [ |- context[proj1_sig (rew [fun t => @sig (@?A t) (@?P t)] ?pf in exist ?P0 ?x ?p)] ]
+                     => progress replace (proj1_sig (rew pf in exist P0 x p)) with (rew [A] pf in x) by (case pf; reflexivity)
+                   | [ |- context[fst (rew [fun t => @prod (@?A t) (@?B t)] ?pf in pair ?x ?y)] ]
+                     => progress replace (fst (rew pf in pair x y)) with (rew [A] pf in x) by (case pf; reflexivity)
+                   | [ |- context[snd (rew [fun t => @prod (@?A t) (@?B t)] ?pf in pair ?x ?y)] ]
+                     => progress replace (fst (rew pf in pair x y)) with (rew [B] pf in y) by (case pf; reflexivity)
+                   end.
+            assert (H' : t = match t' with type.base t' => t' | _ => t end) by (subst; reflexivity).
+            revert pf.
+            rewrite H'; clear H'.
+            induction Hwf; break_innermost_match; break_innermost_match_hyps;
+              repeat first [ progress intros
+                           | progress type.inversion_type
+                           | progress base.type.inversion_type
+                           | progress wf_safe_t
+                           | progress cbn [of_expr fst snd splice eq_rect type.decode f_equal to_expr] in *
+                           | match goal with
+                             | [ H : forall pf : ?x = ?x, _ |- _ ] => specialize (H eq_refl)
+                             | [ H : forall x (pf : ?a = ?a), _ |- _ ] => specialize (fun x => H x eq_refl)
+                             | [ H : forall x y (pf : ?a = ?a), _ |- _ ] => specialize (fun x y => H x y eq_refl)
+                             | [ H : forall x y z (pf : ?a = ?a), _ |- _ ] => specialize (fun x y z => H x y z eq_refl)
+                             | [ |- context[(expr_let x := _ in _)%expr] ] => progress cbn [expr.interp]; cbv [LetIn.Let_In]
+                             | [ H : context[expr.interp _ _ = expr.interp _ _] |- expr.interp _ _ = expr.interp _ _ ]
+                               => eapply H; eauto with nocore
+                             end
+                           | solve [ eauto ]
+                           | solve [ eapply expr.wf_interp_Proper; eauto ] ].
+            all: eapply interp_to_expr_reify_and_let_binds_base_cps with (k1:=Base) (k2:=(fun x => x)); eauto; wf_safe_t. }
+        Qed.
 
-      Lemma Interp_LetBindReturn {t} (e : expr.Expr t) (Hwf : expr.Wf e) : defaults.Interp (LetBindReturn e) == defaults.Interp e.
-      Proof.
-        apply interp_let_bind_return with (G:=nil); cbn [List.In]; eauto; tauto.
-      Qed.
+        Lemma Interp_LetBindReturn {t} (e : expr.Expr t) (Hwf : expr.Wf e) : Interp (LetBindReturn e) == Interp e.
+        Proof.
+          apply interp_let_bind_return with (G:=nil); cbn [List.In]; eauto; tauto.
+        Qed.
+      End with_cast.
+
+      Lemma Wf_LetBindReturn {t} (e : expr.Expr t) (Hwf : expr.Wf e) : expr.Wf (LetBindReturn e).
+      Proof. intros ??; apply wf_let_bind_return, Hwf. Qed.
     End reify.
   End UnderLets.