1 files changed, 1 insertions, 105 deletions

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).