1 files changed, 0 insertions, 135 deletions
diff --git a/src/LegacyArithmetic/Double/Proofs/Multiply.v b/src/LegacyArithmetic/Double/Proofs/Multiply.v
deleted file mode 100644
index ebe19cc46..000000000
--- a/src/LegacyArithmetic/Double/Proofs/Multiply.v
+++ /dev/null
@@ -1,135 +0,0 @@
-Require Import Coq.ZArith.ZArith Coq.micromega.Psatz.
-Require Import Crypto.LegacyArithmetic.Interface.
-Require Import Crypto.LegacyArithmetic.InterfaceProofs.
-Require Import Crypto.LegacyArithmetic.Double.Core.
-Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode.
-Require Import Crypto.LegacyArithmetic.Double.Proofs.SpreadLeftImmediate.
-Require Import Crypto.LegacyArithmetic.Double.Proofs.RippleCarryAddSub.
-Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
-Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
-Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
-Require Import Crypto.Util.ZUtil.Modulo.
-Require Import Crypto.Util.Tactics.SimplifyProjections.
-Require Import Crypto.Util.Notations.
-Require Import Crypto.Util.LetIn.
-Require Import Crypto.Util.Prod.
-Import Bug5107WorkAround.
-Import BoundedRewriteNotations.
-
-Local Open Scope Z_scope.
-
-Local Opaque tuple_decoder.
-
-Lemma decode_mul_double_iff
-      {n W}
-      {decode : decoder n W}
-      {muldw : multiply_double W}
-      {isdecode : is_decode decode}
-  : is_mul_double muldw
-    <-> (forall x y, tuple_decoder (muldw x y) = (decode x * decode y)%Z).
-Proof.
-  rewrite is_mul_double_alt by assumption.
-  split; intros H x y; specialize (H x y); revert H;
-    pose proof (decode_range x); pose proof (decode_range y);
-      assert (0 <= decode x * decode y < 2^n * 2^n) by nia;
-      assert (0 <= n) by eauto using decode_exponent_nonnegative;
-      autorewrite with simpl_tuple_decoder;
-      simpl; intro H'; rewrite H';
-        Z.rewrite_mod_small; reflexivity.
-Qed.
-
-Global Instance decode_mul_double
-           {n W}
-           {decode : decoder n W}
-           {muldw : multiply_double W}
-           {isdecode : is_decode decode}
-           {ismuldw : is_mul_double muldw}
-  : forall x y, tuple_decoder (muldw x y) <~=~> (decode x * decode y)%Z
-  := proj1 decode_mul_double_iff _.
-
-Section tuple2.
-  Local Arguments Z.pow !_ !_.
-  Local Arguments Z.mul !_ !_.
-
-  Local Opaque ripple_carry_adc.
-  Section full_from_half.
-    Context {W}
-            {mulhwll : multiply_low_low W}
-            {mulhwhl : multiply_high_low W}
-            {mulhwhh : multiply_high_high W}
-            {adc : add_with_carry W}
-            {shl : shift_left_immediate W}
-            {shr : shift_right_immediate W}
-            {half_n : Z}
-            {ldi : load_immediate W}
-            {decode : decoder (2 * half_n) W}
-            {ismulhwll : is_mul_low_low half_n mulhwll}
-            {ismulhwhl : is_mul_high_low half_n mulhwhl}
-            {ismulhwhh : is_mul_high_high half_n mulhwhh}
-            {isadc : is_add_with_carry adc}
-            {isshl : is_shift_left_immediate shl}
-            {isshr : is_shift_right_immediate shr}
-            {isldi : is_load_immediate ldi}
-            {isdecode : is_decode decode}.
-
-    Local Arguments Z.mul !_ !_.
-
-    Lemma decode_mul_double_mod x y
-      : (tuple_decoder (mul_double half_n x y) = (decode x * decode y) mod (2^(2 * half_n) * 2^(2*half_n)))%Z.
-    Proof using Type*.
-      assert (0 <= 2 * half_n) by eauto using decode_exponent_nonnegative.
-      assert (0 <= half_n) by omega.
-      unfold mul_double, Let_In.
-      push_decode; autorewrite with simpl_tuple_decoder; simplify_projections.
-      autorewrite with zsimplify Zshift_to_pow push_Zpow.
-      rewrite !spread_left_from_shift_half_correct.
-      push_decode.
-      generalize_decode_var.
-      simpl in *.
-      autorewrite with push_Zpow in *.
-      repeat autorewrite with Zshift_to_pow zsimplify push_Zpow.
-      rewrite <- !(Z.mul_mod_distr_r_full _ _ (_^_ * _^_)), ?Z.mul_assoc.
-      Z.rewrite_mod_small.
-      push_Zmod; pull_Zmod.
-      apply f_equal2; [ | reflexivity ].
-      Z.div_mod_to_quot_rem_in_goal; nia.
-    Qed.
-
-    Lemma decode_mul_double_function x y
-      : tuple_decoder (mul_double half_n x y) = (decode x * decode y)%Z.
-    Proof using Type*.
-      rewrite decode_mul_double_mod; generalize_decode_var.
-      simpl in *; Z.rewrite_mod_small; reflexivity.
-    Qed.
-
-    Global Instance mul_double_is_multiply_double : is_mul_double mul_double_multiply.
-    Proof using Type*.
-      apply decode_mul_double_iff; apply decode_mul_double_function.
-    Qed.
-  End full_from_half.
-
-  Section half_from_full.
-    Context {n W}
-            {decode : decoder n W}
-            {muldw : multiply_double W}
-            {isdecode : is_decode decode}
-            {ismuldw : is_mul_double muldw}.
-
-    Local Ltac t :=
-      hnf; intros [??] [??];
-      assert (0 <= n) by eauto using decode_exponent_nonnegative;
-      assert (0 < 2^n) by auto with zarith;
-      assert (forall x y, 0 <= x < 2^n -> 0 <= y < 2^n -> 0 <= x * y < 2^n * 2^n) by auto with zarith;
-      simpl @Interface.mulhwhh; simpl @Interface.mulhwhl; simpl @Interface.mulhwll;
-      rewrite decode_mul_double; autorewrite with simpl_tuple_decoder Zshift_to_pow zsimplify push_Zpow;
-      Z.rewrite_mod_small;
-      try reflexivity.
-
-    Global Instance mul_double_is_multiply_low_low : is_mul_low_low n mul_double_multiply_low_low.
-    Proof using Type*. t. Qed.
-    Global Instance mul_double_is_multiply_high_low : is_mul_high_low n mul_double_multiply_high_low.
-    Proof using Type*. t. Qed.
-    Global Instance mul_double_is_multiply_high_high : is_mul_high_high n mul_double_multiply_high_high.
-    Proof using Type*. t. Qed.
-  End half_from_full.
-End tuple2.