1 files changed, 41 insertions, 0 deletions
diff --git a/src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v b/src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v
new file mode 100644
index 000000000..41234bf6e
--- /dev/null
+++ b/src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v
@@ -0,0 +1,41 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.LegacyArithmetic.Interface.
+Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.Tactics.UniquePose.
+Require Import Crypto.Util.Tactics.BreakMatch.
+
+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.