1 files changed, 0 insertions, 43 deletions
diff --git a/src/LegacyArithmetic/Double/Proofs/ShiftLeft.v b/src/LegacyArithmetic/Double/Proofs/ShiftLeft.v
deleted file mode 100644
index 1944f99b2..000000000
--- a/src/LegacyArithmetic/Double/Proofs/ShiftLeft.v
+++ /dev/null
@@ -1,43 +0,0 @@
-Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
-Require Import Crypto.LegacyArithmetic.Interface.
-Require Import Crypto.LegacyArithmetic.Double.Core.
-Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode.
-Require Import Crypto.LegacyArithmetic.Double.Proofs.ShiftLeftRightTactic.
-Require Import Crypto.Util.ZUtil.Notations.
-Require Import Crypto.Util.ZUtil.Definitions.
-
-Local Open Scope Z_scope.
-
-Local Opaque tuple_decoder.
-Local Arguments Z.pow !_ !_.
-Local Arguments Z.mul !_ !_.
-
-Section shl.
-  Context (n : Z) {W}
-          {ldi : load_immediate W}
-          {shl : shift_left_immediate W}
-          {shr : shift_right_immediate W}
-          {or : bitwise_or W}
-          {decode : decoder n W}
-          {isdecode : is_decode decode}
-          {isldi : is_load_immediate ldi}
-          {isshl : is_shift_left_immediate shl}
-          {isshr : is_shift_right_immediate shr}
-          {isor : is_bitwise_or or}.
-
-  Global Instance is_shift_left_immediate_double : is_shift_left_immediate (shl_double n).
-  Proof using Type*.
-    intros r count H; hnf in H.
-    assert (0 < 2^count) by auto with zarith.
-    assert (0 < 2^(n+count)) by auto with zarith.
-    assert (forall x, 0 <= Z.pow2_mod x n < 2^n) by auto with zarith.
-    unfold shl_double; simpl.
-    generalize (decode_range r).
-    pose proof (decode_range (fst r)).
-    pose proof (decode_range (snd r)).
-    assert (forall n', 2^n <= 2^n' -> 0 <= decode (fst r) < 2^n') by (simpl in *; auto with zarith).
-    assert (forall n', n <= n' -> 0 <= decode (fst r) < 2^n') by auto with zarith omega.
-    autorewrite with simpl_tuple_decoder; push_decode.
-    shift_left_right_t.
-  Qed.
-End shl.