1 files changed, 0 insertions, 48 deletions
diff --git a/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v b/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v
deleted file mode 100644
index 1217cd721..000000000
--- a/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v
+++ /dev/null
@@ -1,48 +0,0 @@
-Require Import Crypto.Compilers.Syntax.
-Require Import Crypto.Compilers.Wf.
-Require Import Crypto.Compilers.SmartMap.
-Require Import Crypto.Compilers.Relations.
-Require Import Crypto.Compilers.Z.MapCastByDeBruijnInterp.
-Require Import Crypto.Compilers.Z.Syntax.
-Require Import Crypto.Compilers.Z.Syntax.Util.
-Require Import Crypto.Compilers.Z.InterpSideConditions.
-Require Import Crypto.Compilers.Z.Bounds.Interpretation.
-Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.IsBoundedBy.
-Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.PullCast.
-Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn.
-Require Import Crypto.Util.PointedProp.
-
-Lemma MapCastCorrect
-      {round_up}
-      {t} (e : Expr t)
-      (Hwf : Wf e)
-      (input_bounds : interp_flat_type Bounds.interp_base_type (domain t))
-  : forall {b} e' (He':MapCast round_up e input_bounds = Some (existT _ b e'))
-           v v' (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v)
-           (Hside : to_prop (InterpSideConditions e v)),
-    Compilers.Syntax.Interp (@Bounds.interp_op) e input_bounds = b
-    /\ Bounds.is_bounded_by b (Compilers.Syntax.Interp interp_op e v)
-    /\ cast_back_flat_const (Compilers.Syntax.Interp interp_op e' v') = (Compilers.Syntax.Interp interp_op e v).
-Proof.
-  apply MapCastCorrect; auto.
-  { apply is_bounded_by_interp_op. }
-  { apply pull_cast_genericize_op, is_bounded_by_interp_op. }
-Qed.
-
-Lemma MapCastCorrect_eq
-      {round_up}
-      {t} (e : Expr t)
-      {evb ev}
-      (Hwf : Wf e)
-      (input_bounds : interp_flat_type Bounds.interp_base_type (domain t))
-  : forall {b} e' (He':MapCast round_up e input_bounds = Some (existT _ b e'))
-           v v' (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v)
-           (Hside : to_prop (InterpSideConditions e v))
-           (Hevb : evb = Compilers.Syntax.Interp (@Bounds.interp_op) e input_bounds)
-           (Hev : ev = Compilers.Syntax.Interp interp_op e v),
-    evb = b
-    /\ Bounds.is_bounded_by b ev
-    /\ cast_back_flat_const (Compilers.Syntax.Interp interp_op e' v') = ev.
-Proof.
-  intros; subst; apply MapCastCorrect; auto.
-Qed.