Split off lemmas about [InlineConst]

11 files changed, 416 insertions, 238 deletions

diff --git a/src/Reflection/Inline.v b/src/Reflection/Inline.v
new file mode 100644
index 000000000..a565835b0
--- /dev/null
+++ b/src/Reflection/Inline.v
@@ -0,0 +1,50 @@
+(** * Inline: Remove some [Let] expressions *)
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Util.Tactics.
+
+Local Open Scope ctype_scope.
+Section language.
+  Context (base_type_code : Type).
+  Context (interp_base_type : base_type_code -> Type).
+  Context (op : flat_type base_type_code -> flat_type base_type_code -> Type).
+
+  Local Notation flat_type := (flat_type base_type_code).
+  Local Notation type := (type base_type_code).
+  Let Tbase := @Tbase base_type_code.
+  Local Coercion Tbase : base_type_code >-> Syntax.flat_type.
+  Let interp_type := interp_type interp_base_type.
+  Let interp_flat_type := interp_flat_type_gen interp_base_type.
+  Local Notation Expr := (@Expr base_type_code interp_base_type op).
+
+  Section with_var.
+    Context {var : base_type_code -> Type}.
+    Local Notation exprf := (@exprf base_type_code interp_base_type op).
+    Local Notation expr := (@expr base_type_code interp_base_type op).
+
+    Fixpoint inline_constf {t} (e : @exprf (@exprf var) t) : @exprf var t
+      := match e in Syntax.exprf _ _ _ t return @exprf var t with
+         | Let _ ex tC eC
+           => match @inline_constf _ ex in Syntax.exprf _ _ _ t' return (interp_flat_type_gen _ t' -> @exprf var tC) -> @exprf var tC with
+              | Const _ x => fun eC => eC (SmartConst (op:=op) (var:=var) x)
+              | ex => fun eC => Let ex (fun x => eC (SmartVarVar x))
+              end (fun x => @inline_constf _ (eC x))
+         | Var _ x => x
+         | Const _ x => Const x
+         | Pair _ ex _ ey => Pair (@inline_constf _ ex) (@inline_constf _ ey)
+         | Op _ _ op args => Op op (@inline_constf _ args)
+         end.
+
+    Fixpoint inline_const {t} (e : @expr (@exprf var) t) : @expr var t
+      := match e in Syntax.expr _ _ _ t return @expr var t with
+         | Return _ x => Return (inline_constf x)
+         | Abs _ _ f => Abs (fun x => @inline_const _ (f (Var x)))
+         end.
+  End with_var.
+
+  Definition InlineConst {t} (e : Expr t) : Expr t
+    := fun var => inline_const (e _).
+End language.
+
+Global Arguments inline_constf {_ _ _ _ _} _.
+Global Arguments inline_const {_ _ _ _ _} _.
+Global Arguments InlineConst {_ _ _ _} _ var.
diff --git a/src/Reflection/InlineInterp.v b/src/Reflection/InlineInterp.v
new file mode 100644
index 000000000..d24cc2799
--- /dev/null
+++ b/src/Reflection/InlineInterp.v
@@ -0,0 +1,96 @@
+(** * Inline: Remove some [Let] expressions *)
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.InlineWf.
+Require Import Crypto.Reflection.InterpProofs.
+Require Import Crypto.Reflection.Inline.
+Require Import Crypto.Util.Tactics Crypto.Util.Sigma Crypto.Util.Prod.
+
+
+Local Open Scope ctype_scope.
+Section language.
+  Context (base_type_code : Type).
+  Context (interp_base_type : base_type_code -> Type).
+  Context (op : flat_type base_type_code -> flat_type base_type_code -> Type).
+  Context (interp_op : forall src dst, op src dst -> interp_flat_type_gen interp_base_type src -> interp_flat_type_gen interp_base_type dst).
+
+  Local Notation flat_type := (flat_type base_type_code).
+  Local Notation type := (type base_type_code).
+  Let Tbase := @Tbase base_type_code.
+  Local Coercion Tbase : base_type_code >-> Syntax.flat_type.
+  Let interp_type := interp_type interp_base_type.
+  Let interp_flat_type := interp_flat_type_gen interp_base_type.
+  Local Notation exprf := (@exprf base_type_code interp_base_type op).
+  Local Notation expr := (@expr base_type_code interp_base_type op).
+  Local Notation Expr := (@Expr base_type_code interp_base_type op).
+  Local Notation wff := (@wff base_type_code interp_base_type op).
+  Local Notation wf := (@wf base_type_code interp_base_type op).
+
+  Local Hint Extern 1 => eapply interpf_SmartConst.
+  Local Hint Extern 1 => eapply interpf_SmartVarVar.
+
+  Local Ltac t_fin :=
+    repeat match goal with
+           | _ => reflexivity
+           | _ => progress simpl in *
+           | _ => progress intros
+           | _ => progress inversion_sigma
+           | _ => progress inversion_prod
+           | _ => solve [ intuition eauto ]
+           | _ => apply (f_equal (interp_op _ _ _))
+           | _ => apply (f_equal2 (@pair _ _))
+           | _ => progress specialize_by assumption
+           | _ => progress subst
+           | [ H : context[List.In _ (_ ++ _)] |- _ ] => setoid_rewrite List.in_app_iff in H
+           | [ H : or _ _ |- _ ] => destruct H
+           | _ => progress break_match
+           | _ => rewrite <- !surjective_pairing
+           | [ H : ?x = _, H' : context[?x] |- _ ] => rewrite H in H'
+           | [ H : _ |- _ ] => apply H
+           | [ H : _ |- _ ] => rewrite H
+           end.
+
+  Lemma interpf_inline_constf G {t} e1 e2
+        (wf : @wff _ _ G t e1 e2)
+        (H : forall t x x',
+            List.In
+              (existT (fun t : base_type_code => (exprf (Syntax.Tbase t) * interp_base_type t)%type) t
+                      (x, x')) G
+            -> interpf interp_op x = x')
+    : interpf interp_op (inline_constf e1) = interpf interp_op e2.
+  Proof.
+    clear -wf H.
+    induction wf; t_fin.
+  Qed.
+
+  Local Hint Resolve interpf_inline_constf.
+
+  Lemma interp_inline_const G {t} e1 e2
+        (wf : @wf _ _ G t e1 e2)
+        (H : forall t x x',
+            List.In
+              (existT (fun t : base_type_code => (exprf (Syntax.Tbase t) * interp_base_type t)%type) t
+                      (x, x')) G
+            -> interpf interp_op x = x')
+    : interp_type_gen_rel_pointwise interp_flat_type (fun _ => @eq _)
+                                    (interp interp_op (inline_const e1))
+                                    (interp interp_op e2).
+  Proof.
+    induction wf.
+    { eapply interpf_inline_constf; eauto. }
+    { simpl in *; intro.
+      match goal with
+      | [ H : _ |- _ ]
+        => apply H; intuition (inversion_sigma; inversion_prod; subst; eauto)
+      end. }
+  Qed.
+
+  Lemma Interp_InlineConst {t} (e : Expr t)
+        (wf : Wf e)
+    : interp_type_gen_rel_pointwise interp_flat_type (fun _ => @eq _)
+                                    (Interp interp_op (InlineConst e))
+                                    (Interp interp_op e).
+  Proof.
+    unfold Interp, InlineConst.
+    eapply interp_inline_const with (G := nil); simpl; intuition.
+  Qed.
+End language.
diff --git a/src/Reflection/InlineWf.v b/src/Reflection/InlineWf.v
new file mode 100644
index 000000000..5822066e3
--- /dev/null
+++ b/src/Reflection/InlineWf.v
@@ -0,0 +1,166 @@
+(** * Inline: Remove some [Let] expressions *)
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.WfProofs.
+Require Import Crypto.Reflection.Inline.
+Require Import Crypto.Util.Tactics Crypto.Util.Sigma Crypto.Util.Prod.
+
+Local Open Scope ctype_scope.
+Section language.
+  Context (base_type_code : Type).
+  Context (interp_base_type : base_type_code -> Type).
+  Context (op : flat_type base_type_code -> flat_type base_type_code -> Type).
+
+  Local Notation flat_type := (flat_type base_type_code).
+  Local Notation type := (type base_type_code).
+  Let Tbase := @Tbase base_type_code.
+  Local Coercion Tbase : base_type_code >-> Syntax.flat_type.
+  Let interp_type := interp_type interp_base_type.
+  Let interp_flat_type := interp_flat_type_gen interp_base_type.
+  Local Notation exprf := (@exprf base_type_code interp_base_type op).
+  Local Notation expr := (@expr base_type_code interp_base_type op).
+  Local Notation Expr := (@Expr base_type_code interp_base_type op).
+  Local Notation wff := (@wff base_type_code interp_base_type op).
+  Local Notation wf := (@wf base_type_code interp_base_type op).
+
+  Section with_var.
+    Context {var1 var2 : base_type_code -> Type}.
+
+    Local Ltac t_fin_step tac :=
+      match goal with
+      | _ => assumption
+      | _ => progress simpl in *
+      | _ => progress subst
+      | _ => progress inversion_sigma
+      | _ => setoid_rewrite List.in_app_iff
+      | [ H : context[List.In _ (_ ++ _)] |- _ ] => setoid_rewrite List.in_app_iff in H
+      | _ => progress intros
+      | _ => solve [ eauto ]
+      | _ => solve [ intuition (subst; eauto) ]
+      | [ H : forall (x : prod _ _) (y : prod _ _), _ |- _ ] => specialize (fun x x' y y' => H (x, x') (y, y'))
+      | _ => rewrite !List.app_assoc
+      | [ H : _ \/ _ |- _ ] => destruct H
+      | [ H : _ |- _ ] => apply H
+      | _ => eapply wff_in_impl_Proper; [ solve [ eauto ] | ]
+      | _ => progress tac
+      | [ |- wff _ _ _ ] => constructor
+      | [ |- wf _ _ _ ] => constructor
+      end.
+    Local Ltac t_fin tac := repeat t_fin_step tac.
+
+    Local Hint Constructors Syntax.wff.
+    Local Hint Resolve List.in_app_or List.in_or_app.
+
+    Local Ltac small_inversion_helper wf G0 e2 :=
+      let t0 := match type of wf with wff (t:=?t0) _ _ _ => t0 end in
+      let e1 := match goal with
+                | |- context[wff _ (inline_constf ?e1) (inline_constf e2)] => e1
+                end in
+      pattern G0, t0, e1, e2;
+      lazymatch goal with
+      | [ |- ?retP _ _ _ _ ]
+        => first [ refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2
+                                return match v1 return Prop with
+                                       | Const _ _ => retP G t v1 v2
+                                       | _ => forall P : Prop, P -> P
+                                       end with
+                          | WfConst _ _ _ => _
+                          | _ => fun _ p => p
+                          end)
+                | refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2
+                                return match v1 return Prop with
+                                       | Var _ _ => retP G t v1 v2
+                                       | _ => forall P : Prop, P -> P
+                                       end with
+                          | WfVar _ _ _ _ _ => _
+                          | _ => fun _ p => p
+                          end)
+                | refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2
+                                return match v1 return Prop with
+                                       | Op _ _ _ _ => retP G t v1 v2
+                                       | _ => forall P : Prop, P -> P
+                                       end with
+                          | WfOp _ _ _ _ _ _ _ => _
+                          | _ => fun _ p => p
+                          end)
+                | refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2
+                                return match v1 return Prop with
+                                       | Let _ _ _ _ => retP G t v1 v2
+                                       | _ => forall P : Prop, P -> P
+                                       end with
+                          | WfLet _ _ _ _ _ _ _ _ _ => _
+                          | _ => fun _ p => p
+                          end)
+                | refine (match wf in @Syntax.wff _ _ _ _ _ G t v1 v2
+                                return match v1 return Prop with
+                                       | Pair _ _ _ _ => retP G t v1 v2
+                                       | _ => forall P : Prop, P -> P
+                                       end with
+                          | WfPair _ _ _ _ _ _ _ _ _ => _
+                          | _ => fun _ p => p
+                          end) ]
+      end.
+
+    Local Hint Constructors or.
+    Local Hint Extern 1 => progress unfold List.In in *.
+    Local Hint Resolve wff_in_impl_Proper.
+    Local Hint Resolve wff_SmartVar.
+    Local Hint Resolve wff_SmartConst.
+
+    Fixpoint wff_inline_constf {t} e1 e2 G G'
+             (H : forall t x x', List.In (existT (fun t : base_type_code => (exprf t * exprf t)%type) t (x, x')) G'
+                            -> wff G x x')
+             (wf : wff G' e1 e2)
+             {struct e1}
+      : @wff var1 var2 G t (inline_constf e1) (inline_constf e2).
+    Proof.
+      (*revert H.
+      set (e1v := e1) in *.
+      destruct e1 as [ | | ? ? ? args | tx ex tC0 eC0 | ? ex ? ey ];
+        [ clear wff_inline_constf
+        | clear wff_inline_constf
+        | generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with
+                      | Op _ _ _ args => wff_inline_constf _ args
+                      | _ => I
+                      end);
+          clear wff_inline_constf
+        | generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with
+                      | Let _ ex _ eC => wff_inline_constf _ ex
+                      | _ => I
+                      end);
+          generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with
+                      | Let _ ex _ eC => fun x => wff_inline_constf _ (eC x)
+                      | _ => I
+                      end);
+          clear wff_inline_constf
+        | generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with
+                      | Pair _ ex _ ey => wff_inline_constf _ ex
+                      | _ => I
+                      end);
+          generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with
+                      | Pair _ ex _ ey => wff_inline_constf _ ey
+                      | _ => I
+                      end);
+          clear wff_inline_constf ];
+        revert G;
+        (* alas, Coq's refiner isn't smart enough to figure out these small inversions for us *)
+        small_inversion_helper wf G' e2;
+        t_fin idtac;
+        repeat match goal with
+               | [ H : context[(_ -> wff _ (inline_constf ?e) (inline_constf _))%type], e2 : exprf _ |- _ ]
+                 => is_var e; not constr_eq e e2; specialize (H e2)
+               | [ H : context[wff _ (@inline_constf ?A ?B ?C ?D ?E ?e) _] |- context[match @inline_constf ?A ?B ?C ?D ?E ?e with _ => _ end] ]
+                 => destruct (@inline_constf A B C D E e)
+               | [ H : context[wff _ _ (@inline_constf ?A ?B ?C ?D ?E ?e)] |- context[match @inline_constf ?A ?B ?C ?D ?E ?e with _ => _ end] ]
+                 => destruct (@inline_constf A B C D E e)
+               | [ IHwf : forall x y : list _, _, H1 : forall z : _, _, H2 : wff _ _ _ |- _ ]
+                 => solve [ specialize (IHwf _ _ H1 H2); inversion IHwf ]
+               | [ |- wff _ _ _ ] => constructor
+               end.
+      3:t_fin idtac.
+      4:t_fin idtac.
+      { match goal with
+        | [ H : _ |- _ ] => eapply H; [ | solve [ eauto ] ]; t_fin idtac
+        end. }*)
+    Abort.
+  End with_var.
+End language.
diff --git a/src/Reflection/InterpProofs.v b/src/Reflection/InterpProofs.v
index 2d4ad5e0f..eb3e617e5 100644
--- a/src/Reflection/InterpProofs.v
+++ b/src/Reflection/InterpProofs.v
@@ -1,5 +1,6 @@
 Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Util.Tactics.
+Require Import Crypto.Reflection.WfProofs.
+Require Import Crypto.Util.Tactics Crypto.Util.Sigma Crypto.Util.Prod.
 
 Local Open Scope ctype_scope.
 Section language.
@@ -26,4 +27,43 @@ Section language.
              | _ => rewrite <- surjective_pairing
              end.
   Qed.
+
+  Lemma interpf_SmartConst {t t'} v x x'
+        (Hin : List.In
+                 (existT (fun t : base_type_code => (exprf base_type_code interp_base_type op (Syntax.Tbase t) * interp_base_type t)%type)
+                         t (x, x'))
+                 (flatten_binding_list (t := t') base_type_code (SmartConst v) v))
+    : interpf interp_op x = x'.
+  Proof.
+    clear -Hin.
+    induction t'; simpl in *.
+    { intuition (inversion_sigma; inversion_prod; subst; eauto). }
+    { apply List.in_app_iff in Hin.
+      intuition (inversion_sigma; inversion_prod; subst; eauto). }
+  Qed.
+
+  Lemma interpf_SmartVarVar {t t'} v x x'
+        (Hin : List.In
+                 (existT (fun t : base_type_code => (exprf base_type_code interp_base_type op (Syntax.Tbase t) * interp_base_type t)%type)
+                         t (x, x'))
+                 (flatten_binding_list (t := t') base_type_code (SmartVarVar v) v))
+    : interpf interp_op x = x'.
+  Proof.
+    clear -Hin.
+    induction t'; simpl in *.
+    { intuition (inversion_sigma; inversion_prod; subst; eauto). }
+    { apply List.in_app_iff in Hin.
+      intuition (inversion_sigma; inversion_prod; subst; eauto). }
+  Qed.
+
+  Lemma interpf_SmartVarVar_eq {t t'} v v' x x'
+        (Heq : v = v')
+        (Hin : List.In
+                 (existT (fun t : base_type_code => (exprf base_type_code interp_base_type op (Syntax.Tbase t) * interp_base_type t)%type)
+                         t (x, x'))
+                 (flatten_binding_list (t := t') base_type_code (SmartVarVar v') v))
+    : interpf interp_op x = x'.
+  Proof.
+    eapply interpf_SmartVarVar; subst; eassumption.
+  Qed.
 End language.
diff --git a/src/Reflection/Linearize.v b/src/Reflection/Linearize.v
index 0c5a9083d..f60352e66 100644
--- a/src/Reflection/Linearize.v
+++ b/src/Reflection/Linearize.v
@@ -66,35 +66,8 @@ Section language.
          end.
   End with_var.
 
-  Section inline.
-    Context {var : base_type_code -> Type}.
-    Local Notation exprf := (@exprf base_type_code interp_base_type op).
-    Local Notation expr := (@expr base_type_code interp_base_type op).
-
-    Fixpoint inline_constf {t} (e : @exprf (@exprf var) t) : @exprf var t
-      := match e in Syntax.exprf _ _ _ t return @exprf var t with
-         | Let _ ex tC eC
-           => match @inline_constf _ ex in Syntax.exprf _ _ _ t' return (interp_flat_type_gen _ t' -> @exprf var tC) -> @exprf var tC with
-              | Const _ x => fun eC => eC (SmartConst (op:=op) (var:=var) x)
-              | ex => fun eC => Let ex (fun x => eC (SmartVarVar x))
-              end (fun x => @inline_constf _ (eC x))
-         | Var _ x => x
-         | Const _ x => Const x
-         | Pair _ ex _ ey => Pair (@inline_constf _ ex) (@inline_constf _ ey)
-         | Op _ _ op args => Op op (@inline_constf _ args)
-         end.
-
-    Fixpoint inline_const {t} (e : @expr (@exprf var) t) : @expr var t
-      := match e in Syntax.expr _ _ _ t return @expr var t with
-         | Return _ x => Return (inline_constf x)
-         | Abs _ _ f => Abs (fun x => @inline_const _ (f (Var x)))
-         end.
-  End inline.
-
   Definition Linearize {t} (e : Expr t) : Expr t
     := fun var => linearize (e _).
-  Definition InlineConst {t} (e : Expr t) : Expr t
-    := fun var => inline_const (e _).
 End language.
 
 Global Arguments let_bind_const {_ _ _ _ t} _ {tC} _.
@@ -102,6 +75,3 @@ Global Arguments under_letsf {_ _ _ _ _} _ {tC} _.
 Global Arguments linearizef {_ _ _ _ _} _.
 Global Arguments linearize {_ _ _ _ _} _.
 Global Arguments Linearize {_ _ _ _} _ var.
-Global Arguments inline_constf {_ _ _ _ _} _.
-Global Arguments inline_const {_ _ _ _ _} _.
-Global Arguments InlineConst {_ _ _ _} _ var.
diff --git a/src/Reflection/LinearizeInterp.v b/src/Reflection/LinearizeInterp.v
index 0b477605d..e8c58a84a 100644
--- a/src/Reflection/LinearizeInterp.v
+++ b/src/Reflection/LinearizeInterp.v
@@ -25,45 +25,6 @@ Section language.
   Local Notation wff := (@wff base_type_code interp_base_type op).
   Local Notation wf := (@wf base_type_code interp_base_type op).
 
-  Lemma interpf_SmartConst {t t'} v x x'
-        (Hin : List.In
-                 (existT (fun t : base_type_code => (exprf (Syntax.Tbase t) * interp_base_type t)%type)
-                         t (x, x'))
-                 (flatten_binding_list (t := t') base_type_code (SmartConst v) v))
-    : interpf interp_op x = x'.
-  Proof.
-    clear -Hin.
-    induction t'; simpl in *.
-    { intuition (inversion_sigma; inversion_prod; subst; eauto). }
-    { apply List.in_app_iff in Hin.
-      intuition (inversion_sigma; inversion_prod; subst; eauto). }
-  Qed.
-
-  Lemma interpf_SmartVarVar {t t'} v x x'
-        (Hin : List.In
-                 (existT (fun t : base_type_code => (exprf (Syntax.Tbase t) * interp_base_type t)%type)
-                         t (x, x'))
-                 (flatten_binding_list (t := t') base_type_code (SmartVarVar v) v))
-    : interpf interp_op x = x'.
-  Proof.
-    clear -Hin.
-    induction t'; simpl in *.
-    { intuition (inversion_sigma; inversion_prod; subst; eauto). }
-    { apply List.in_app_iff in Hin.
-      intuition (inversion_sigma; inversion_prod; subst; eauto). }
-  Qed.
-
-  Lemma interpf_SmartVarVar_eq {t t'} v v' x x'
-        (Heq : v = v')
-        (Hin : List.In
-                 (existT (fun t : base_type_code => (exprf (Syntax.Tbase t) * interp_base_type t)%type)
-                         t (x, x'))
-                 (flatten_binding_list (t := t') base_type_code (SmartVarVar v') v))
-    : interpf interp_op x = x'.
-  Proof.
-    eapply interpf_SmartVarVar; subst; eassumption.
-  Qed.
-
   Local Hint Extern 1 => eapply interpf_SmartConst.
   Local Hint Extern 1 => eapply interpf_SmartVarVar.
 
@@ -88,19 +49,6 @@ Section language.
            | [ H : _ |- _ ] => rewrite H
            end.
 
-  Lemma interpf_inline_constf G {t} e1 e2
-        (wf : @wff _ _ G t e1 e2)
-        (H : forall t x x',
-            List.In
-              (existT (fun t : base_type_code => (exprf (Syntax.Tbase t) * interp_base_type t)%type) t
-                      (x, x')) G
-            -> interpf interp_op x = x')
-    : interpf interp_op (inline_constf e1) = interpf interp_op e2.
-  Proof.
-    clear -wf H.
-    induction wf; t_fin.
-  Qed.
-
   Lemma interpf_let_bind_const {t tC} ex (eC : _ -> exprf tC)
     : interpf interp_op (let_bind_const (t:=t) ex eC) = interpf interp_op (eC ex).
   Proof.
@@ -116,13 +64,6 @@ Section language.
     rewrite interpf_let_bind_const; reflexivity.
   Qed.
 
-  Lemma interpf_SmartVar {t} v
-    : interpf interp_op (SmartVar (t:=t) v) = v.
-  Proof.
-    clear.
-    unfold SmartVar; induction t; t_fin.
-  Qed.
-
   Lemma interpf_linearizef {t} e
     : interpf interp_op (linearizef (t:=t) e) = interpf interp_op e.
   Proof.
@@ -133,28 +74,6 @@ Section language.
                    | t_fin ].
   Qed.
 
-  Local Hint Resolve interpf_inline_constf.
-
-  Lemma interp_inline_const G {t} e1 e2
-        (wf : @wf _ _ G t e1 e2)
-        (H : forall t x x',
-            List.In
-              (existT (fun t : base_type_code => (exprf (Syntax.Tbase t) * interp_base_type t)%type) t
-                      (x, x')) G
-            -> interpf interp_op x = x')
-    : interp_type_gen_rel_pointwise interp_flat_type (fun _ => @eq _)
-                                    (interp interp_op (inline_const e1))
-                                    (interp interp_op e2).
-  Proof.
-    induction wf.
-    { eapply interpf_inline_constf; eauto. }
-    { simpl in *; intro.
-      match goal with
-      | [ H : _ |- _ ]
-        => apply H; intuition (inversion_sigma; inversion_prod; subst; eauto)
-      end. }
-  Qed.
-
   Local Hint Resolve interpf_linearizef.
 
   Lemma interp_linearize {t} e
@@ -166,16 +85,6 @@ Section language.
     eapply interpf_linearizef.
   Qed.
 
-  Lemma Interp_InlineConst {t} (e : Expr t)
-        (wf : Wf e)
-    : interp_type_gen_rel_pointwise interp_flat_type (fun _ => @eq _)
-                                    (Interp interp_op (InlineConst e))
-                                    (Interp interp_op e).
-  Proof.
-    unfold Interp, InlineConst.
-    eapply interp_inline_const with (G := nil); simpl; intuition.
-  Qed.
-
   Lemma Interp_Linearize {t} (e : Expr t)
     : interp_type_gen_rel_pointwise interp_flat_type (fun _ => @eq _)
                                     (Interp interp_op (Linearize e))
@@ -184,12 +93,4 @@ Section language.
     unfold Interp, Linearize.
     eapply interp_linearize.
   Qed.
-
-  Lemma Interp_InlineConst_Linearize {t} (e : Expr t) (wf : Wf e)
-    : interp_type_gen_rel_pointwise interp_flat_type (fun _ => @eq _)
-                                    (Interp interp_op (InlineConst (Linearize e)))
-                                    (Interp interp_op e).
-  Proof.
-    etransitivity; [ apply Interp_InlineConst, Wf_Linearize, wf | apply Interp_Linearize ].
-  Qed.
 End language.
diff --git a/src/Reflection/LinearizeWf.v b/src/Reflection/LinearizeWf.v
index 9cf82b3e2..f06db6594 100644
--- a/src/Reflection/LinearizeWf.v
+++ b/src/Reflection/LinearizeWf.v
@@ -2,7 +2,7 @@
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.WfProofs.
 Require Import Crypto.Reflection.Linearize.
-Require Import Crypto.Util.Tactics Crypto.Util.Sigma Crypto.Util.Prod.
+Require Import Crypto.Util.Tactics Crypto.Util.Sigma.
 
 Local Open Scope ctype_scope.
 Section language.
@@ -63,7 +63,6 @@ Section language.
       let t0 := match type of wf with wff (t:=?t0) _ _ _ => t0 end in
       let e1 := match goal with
                 | |- context[wff G0 (under_letsf ?e1 _) (under_letsf e2 _)] => e1
-                | |- context[wff _ (inline_constf ?e1) (inline_constf e2)] => e1
                 end in
       pattern G0, t0, e1, e2;
       lazymatch goal with
@@ -161,14 +160,6 @@ Section language.
     Local Hint Constructors or.
     Local Hint Extern 1 => progress unfold List.In in *.
     Local Hint Resolve wff_in_impl_Proper.
-
-    Lemma wff_SmartVar {t} x1 x2
-      : @wff var1 var2 (flatten_binding_list base_type_code x1 x2) t (SmartVar x1) (SmartVar x2).
-    Proof.
-      unfold SmartVar.
-      induction t; simpl; constructor; eauto.
-    Qed.
-
     Local Hint Resolve wff_SmartVar.
 
     Lemma wff_linearizef G {t} e1 e2
@@ -186,101 +177,6 @@ Section language.
     Proof.
       induction 1; t_fin idtac.
     Qed.
-
-    Definition invert_Const {var t} (e : @exprf var t) : option (interp_type t)
-      := match e with
-         | Const _ v => Some v
-         | _ => None
-         end.
-
-    Lemma wff_Const_eta G {A B} v1 v2
-      : @wff var1 var2 G (Prod A B) (Const v1) (Const v2)
-        -> (@wff var1 var2 G A (Const (fst v1)) (Const (fst v2))
-           /\ @wff var1 var2 G B (Const (snd v1)) (Const (snd v2))).
-    Proof.
-      intro wf.
-      assert (H : Some v1 = Some v2).
-      { refine match wf in @Syntax.wff _ _ _ _ _ G t e1 e2 return invert_Const e1 = invert_Const e2 with
-               | WfConst _ _ _ => eq_refl
-               | _ => eq_refl
-               end. }
-      inversion H; subst; repeat constructor.
-    Qed.
-
-    Local Hint Resolve (fun G A B c1 c2 wf => proj1 (@wff_Const_eta G A B c1 c2 wf))
-          (fun G A B c1 c2 wf => proj2 (@wff_Const_eta G A B c1 c2 wf)).
-
-    Lemma wff_SmartConst G {t t'} v1 v2 x1 x2
-          (Hin : List.In (existT (fun t : base_type_code => (@exprf var1 t * @exprf var2 t)%type) t (x1, x2))
-                         (flatten_binding_list base_type_code (SmartConst v1) (SmartConst v2)))
-          (Hwf : @wff var1 var2 G t' (Const v1) (Const v2))
-      : @wff var1 var2 G t x1 x2.
-    Proof.
-      induction t'. simpl in *.
-      { intuition (inversion_sigma; inversion_prod; subst; eauto). }
-      { unfold SmartConst in *; simpl in *.
-        apply List.in_app_iff in Hin.
-        intuition (inversion_sigma; inversion_prod; subst; eauto). }
-    Qed.
-
-    Local Hint Resolve wff_SmartConst.
-
-    Fixpoint wff_inline_constf {t} e1 e2 G G'
-             (H : forall t x x', List.In (existT (fun t : base_type_code => (exprf t * exprf t)%type) t (x, x')) G'
-                            -> wff G x x')
-             (wf : wff G' e1 e2)
-             {struct e1}
-      : @wff var1 var2 G t (inline_constf e1) (inline_constf e2).
-    Proof.
-      (*revert H.
-      set (e1v := e1) in *.
-      destruct e1 as [ | | ? ? ? args | tx ex tC0 eC0 | ? ex ? ey ];
-        [ clear wff_inline_constf
-        | clear wff_inline_constf
-        | generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with
-                      | Op _ _ _ args => wff_inline_constf _ args
-                      | _ => I
-                      end);
-          clear wff_inline_constf
-        | generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with
-                      | Let _ ex _ eC => wff_inline_constf _ ex
-                      | _ => I
-                      end);
-          generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with
-                      | Let _ ex _ eC => fun x => wff_inline_constf _ (eC x)
-                      | _ => I
-                      end);
-          clear wff_inline_constf
-        | generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with
-                      | Pair _ ex _ ey => wff_inline_constf _ ex
-                      | _ => I
-                      end);
-          generalize (match e1v return match e1v with Let _ _ _ _ => _ | _ => _ end with
-                      | Pair _ ex _ ey => wff_inline_constf _ ey
-                      | _ => I
-                      end);
-          clear wff_inline_constf ];
-        revert G;
-        (* alas, Coq's refiner isn't smart enough to figure out these small inversions for us *)
-        small_inversion_helper wf G' e2;
-        t_fin idtac;
-        repeat match goal with
-               | [ H : context[(_ -> wff _ (inline_constf ?e) (inline_constf _))%type], e2 : exprf _ |- _ ]
-                 => is_var e; not constr_eq e e2; specialize (H e2)
-               | [ H : context[wff _ (@inline_constf ?A ?B ?C ?D ?E ?e) _] |- context[match @inline_constf ?A ?B ?C ?D ?E ?e with _ => _ end] ]
-                 => destruct (@inline_constf A B C D E e)
-               | [ H : context[wff _ _ (@inline_constf ?A ?B ?C ?D ?E ?e)] |- context[match @inline_constf ?A ?B ?C ?D ?E ?e with _ => _ end] ]
-                 => destruct (@inline_constf A B C D E e)
-               | [ IHwf : forall x y : list _, _, H1 : forall z : _, _, H2 : wff _ _ _ |- _ ]
-                 => solve [ specialize (IHwf _ _ H1 H2); inversion IHwf ]
-               | [ |- wff _ _ _ ] => constructor
-               end.
-      3:t_fin idtac.
-      4:t_fin idtac.
-      { match goal with
-        | [ H : _ |- _ ] => eapply H; [ | solve [ eauto ] ]; t_fin idtac
-        end. }*)
-    Abort.
   End with_var.
 
   Lemma Wf_Linearize {t} (e : Expr t) : Wf e -> Wf (Linearize e).
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v
index 784beeac3..87ca9274e 100644
--- a/src/Reflection/Syntax.v
+++ b/src/Reflection/Syntax.v
@@ -178,6 +178,14 @@ Section language.
            end.
     End map.
 
+    Section misc.
+      Definition invert_Const {var t} (e : @exprf var t) : option (interp_type t)
+        := match e with
+           | Const _ v => Some v
+           | _ => None
+           end.
+    End misc.
+
     Section wf.
       Context {var1 var2 : base_type_code -> Type}.
 
@@ -246,6 +254,7 @@ Global Arguments Wf {_ _ _ t} _.
 Global Arguments Interp {_ _ _} interp_op {t} _.
 Global Arguments interp {_ _ _} interp_op {t} _.
 Global Arguments interpf {_ _ _} interp_op {t} _.
+Global Arguments invert_Const {_ _ _ _ _} _.
 
 Notation "'slet' x := A 'in' b" := (Let A (fun x => b)) : expr_scope.
 Notation "'λ'  x .. y , t" := (Abs (fun x => .. (Abs (fun y => t%expr)) ..)) : expr_scope.
diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v
index 05b3dab4b..d5b374ec4 100644
--- a/src/Reflection/TestCase.v
+++ b/src/Reflection/TestCase.v
@@ -2,7 +2,7 @@ Require Import Crypto.Reflection.Syntax.
 Require Export Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.InputSyntax.
 Require Import Crypto.Reflection.CommonSubexpressionElimination.
-Require Crypto.Reflection.Linearize.
+Require Crypto.Reflection.Linearize Crypto.Reflection.Inline.
 Require Import Crypto.Reflection.WfReflective.
 
 Import ReifyDebugNotations.
@@ -67,7 +67,7 @@ Goal (0 = let x := 1 in let y := 2 in x * y)%nat.
   Reify_rhs.
 Abort.
 
-Import Linearize.
+Import Linearize Inline.
 
 Goal True.
   let x := Reify (fun x y => (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in
diff --git a/src/Reflection/WfProofs.v b/src/Reflection/WfProofs.v
index 83c253c43..226172b5d 100644
--- a/src/Reflection/WfProofs.v
+++ b/src/Reflection/WfProofs.v
@@ -1,5 +1,5 @@
 Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Tactics Crypto.Util.Sigma Crypto.Util.Prod.
 
 Local Open Scope ctype_scope.
 Section language.
@@ -36,5 +36,54 @@ Section language.
                | _ => solve [ intuition eauto ]
                end.
     Qed.
+
+    Local Hint Resolve List.in_app_or List.in_or_app.
+    Local Hint Extern 1 => progress unfold List.In in *.
+    Local Hint Resolve wff_in_impl_Proper.
+
+    Lemma wff_SmartVar {t} x1 x2
+      : @wff var1 var2 (flatten_binding_list base_type_code x1 x2) t (SmartVar x1) (SmartVar x2).
+    Proof.
+      unfold SmartVar.
+      induction t; simpl; constructor; eauto.
+    Qed.
+
+    Local Hint Resolve wff_SmartVar.
+
+    Lemma wff_Const_eta G {A B} v1 v2
+      : @wff var1 var2 G (Prod A B) (Const v1) (Const v2)
+        -> (@wff var1 var2 G A (Const (fst v1)) (Const (fst v2))
+           /\ @wff var1 var2 G B (Const (snd v1)) (Const (snd v2))).
+    Proof.
+      intro wf.
+      assert (H : Some v1 = Some v2).
+      { refine match wf in @Syntax.wff _ _ _ _ _ G t e1 e2 return invert_Const e1 = invert_Const e2 with
+               | WfConst _ _ _ => eq_refl
+               | _ => eq_refl
+               end. }
+      inversion H; subst; repeat constructor.
+    Qed.
+
+    Definition wff_Const_eta_fst G {A B} v1 v2 H
+      := proj1 (@wff_Const_eta G A B v1 v2 H).
+    Definition wff_Const_eta_snd G {A B} v1 v2 H
+      := proj2 (@wff_Const_eta G A B v1 v2 H).
+
+    Local Hint Resolve wff_Const_eta_fst wff_Const_eta_snd.
+
+    Lemma wff_SmartConst G {t t'} v1 v2 x1 x2
+          (Hin : List.In (existT (fun t : base_type_code => (@exprf var1 t * @exprf var2 t)%type) t (x1, x2))
+                         (flatten_binding_list base_type_code (SmartConst v1) (SmartConst v2)))
+          (Hwf : @wff var1 var2 G t' (Const v1) (Const v2))
+      : @wff var1 var2 G t x1 x2.
+    Proof.
+      induction t'. simpl in *.
+      { intuition (inversion_sigma; inversion_prod; subst; eauto). }
+      { unfold SmartConst in *; simpl in *.
+        apply List.in_app_iff in Hin.
+        intuition (inversion_sigma; inversion_prod; subst; eauto). }
+    Qed.
+
+    Local Hint Resolve wff_SmartConst.
   End with_var.
 End language.
diff --git a/src/Specific/FancyMachine256/Core.v b/src/Specific/FancyMachine256/Core.v
index d11cfe6ad..19f04fd89 100644
--- a/src/Specific/FancyMachine256/Core.v
+++ b/src/Specific/FancyMachine256/Core.v
@@ -8,6 +8,7 @@ Require Export Crypto.Util.Tuple.
 Require Import Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod.
 Require Export Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Linearize.
+Require Import Crypto.Reflection.Inline.
 Require Import Crypto.Reflection.CommonSubexpressionElimination.
 Require Export Crypto.Reflection.Reify.
 Require Export Crypto.Util.ZUtil.