1 files changed, 0 insertions, 50 deletions
diff --git a/src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v b/src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v
deleted file mode 100644
index 98cf3cf9c..000000000
--- a/src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v
+++ /dev/null
@@ -1,50 +0,0 @@
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.LegacyArithmetic.Interface.
-Require Import Crypto.Util.ZUtil.Notations.
-Require Import Crypto.Util.ZUtil.Definitions.
-Require Import Crypto.Util.ZUtil.Testbit.
-Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
-Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
-Require Import Crypto.Util.ZUtil.Tactics.Ztestbit.
-Require Import Crypto.Util.Tactics.UniquePose.
-Require Import Crypto.Util.Tactics.BreakMatch.
-Require Export Crypto.Util.ZUtil.ZSimplify.Autogenerated.
-Require Export Crypto.Util.ZUtil.ZSimplify.Core.
-Require Export Crypto.Util.ZUtil.ZSimplify.Simple.
-Require Export Crypto.Util.ZUtil.LandLorShiftBounds.
-
-Local Open Scope Z_scope.
-
-Local Arguments Z.pow !_ !_.
-Local Arguments Z.mul !_ !_.
-
-Ltac shift_left_right_t :=
-  repeat match goal with
-         | [ |- ?x = ?x ] => reflexivity
-         | [ |- Z.testbit ?x ?n = Z.testbit ?x ?n' ] => apply f_equal; try omega
-         | [ |- orb (Z.testbit ?x _) (Z.testbit ?y _) = orb (Z.testbit ?x _) (Z.testbit ?y _) ]
-           => apply f_equal2
-         | _ => progress Z.ltb_to_lt
-         | _ => progress subst
-         | _ => progress unfold AutoRewrite.rewrite_eq
-         | _ => progress intros
-         | _ => omega
-         | _ => solve [ trivial ]
-         | _ => progress break_match_step ltac:(fun _ => idtac)
-         | [ |- context[Z.lor (?x >> ?count) (Z.pow2_mod (?y << (?n - ?count)) ?n)] ]
-           => unique assert (0 <= Z.lor (x >> count) (Z.pow2_mod (y << (n - count)) n) < 2 ^ n) by (autorewrite with Zshift_to_pow; auto with zarith nia)
-         | _ => progress push_decode
-         | [ |- context[Interface.decode (fst ?x)] ] => is_var x; destruct x; simpl in *
-         | [ |- context[@Interface.decode ?n ?W ?d ?x] ] => is_var x; generalize dependent (@Interface.decode n W d x); intros
-         | _ => progress Z.rewrite_mod_small
-         | _ => progress autorewrite with convert_to_Ztestbit
-         | _ => progress autorewrite with zsimplify_fast
-         | [ |- _ = _ :> Z ] => apply Z.bits_inj'; intros
-         | _ => progress autorewrite with Ztestbit_full
-         | _ => progress autorewrite with bool_congr
-         | [ |- Z.testbit _ (?x - ?y + (?y - ?z)) = false ]
-           => autorewrite with zsimplify
-         | [ H : 0 <= ?x < 2^?n |- Z.testbit ?x ?n' = false ]
-           => assert (n <= n') by auto with zarith; progress Ztestbit
-         | _ => progress Ztestbit_full
-         end.