remove unneeded, commented-out code

1 files changed, 0 insertions, 77 deletions

diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v
index b4e59719f..9a5d12be5 100644
--- a/src/Experiments/SimplyTypedArithmetic.v
+++ b/src/Experiments/SimplyTypedArithmetic.v
@@ -902,83 +902,6 @@ Module Columns.
           cbv [mul_converted].
           rewrite <-!convert_single_correct.
           cbv [convert_single].
-
-          (*
-          (* assert some things for omega to use later *)
-          rewrite <-(w'_sq 1) in *.
-          pose proof (Z.mod_pos_bound p1 (w' 1) ltac:(auto using Z.gt_lt)).
-          pose proof (Z.mod_pos_bound p2 (w' 1) ltac:(auto using Z.gt_lt)).
-          assert (0 <= p1 / w' 1 < w' 1) by (split; [ Z.zero_bounds | apply Z.div_lt_upper_bound; omega ]).
-          assert (0 <= p2 / w' 1 < w' 1) by (split; [ Z.zero_bounds | apply Z.div_lt_upper_bound; omega ]).
-          assert (w' 1 < w' 1 * w' 1) by (apply Z.lt_mul_diag_r; omega).
-          assert (w' 1 =? 0 = false) by (apply Z.eqb_neq; omega).
-          assert (1 =? 0 = false) by reflexivity.
-          assert (0 < w' 1 * w' 1) by Z.zero_bounds.
-
-          (* simplify carry *)
-          match goal with |- context [Associational.carry ?w ?fw ?x] =>
-                          remember (Associational.carry w fw x) as X eqn:HeqX
-          end.
-          cbv - [Z.modulo Z.div Z.eqb Z.mul app] in HeqX. cbn [app] in HeqX.
-          rewrite w'_0 in HeqX; autorewrite with zsimplify_fast in HeqX.
-          rewrite Z.eqb_refl in HeqX.
-          repeat match type of HeqX with context [if ?x =? ?y then _ else _] =>
-                                  let H := fresh "H" in
-                                  case_eq (x =? y); intro H; rewrite H in HeqX;
-                                    rewrite ?Z.eqb_eq, ?Z.eqb_neq in H; try omega
-          end.
-          cbn [app] in HeqX.
-          rewrite !Z.div_small with (b:= w' 1 * w' 1) in HeqX by nia.
-          rewrite !Z.mod_small with (b:= w' 1 * w' 1) in HeqX by nia.
-          subst X.
-
-          (* simplify from_associational *)
-          match goal with |- context [from_associational ?w ?n ?x] =>
-                          remember (from_associational w n x) as X eqn:HeqX
-          end.
-          cbv - [Z.modulo Z.div Z.eqb Z.mul cons_to_nth] in HeqX. cbn [app] in HeqX.
-          rewrite <-w'_sq in HeqX.
-          autorewrite with zsimplify_fast in HeqX.
-          rewrite !Z.mod_1_l in HeqX by omega.
-          rewrite !Z.mod_mul in HeqX by omega.
-          rewrite !Z.mod_small with (b:= w' 1 * w' 1) in HeqX by nia.
-          rewrite Z.eqb_refl in HeqX.
-          repeat match goal with H : Z.eqb _ _ = _ |- _ => rewrite H in HeqX end.
-          cbv - [Z.modulo Z.div Z.mul] in HeqX.
-          autorewrite with zsimplify in HeqX.
-          subst X.
-
-          (* simplify flatten *)
-          match goal with |- context [flatten ?w ?x] =>
-                          remember (flatten w x) as X eqn:HeqX
-          end.
-          cbn in HeqX.
-          cbv [flatten_step] in HeqX. cbn in HeqX.
-          autorewrite with to_div_mod in HeqX.
-          cbn [fst snd] in HeqX.
-          rewrite w_0 in HeqX.
-          autorewrite with zsimplify in HeqX.
-          Check Z.div_small.
-          match type of HeqX with context [
-
-          cbv [Let_In] in HeqX.
-          autorewrite with to_div_mod in HeqX.
-          cbn [fst snd] in HeqX.
-          cbv - [flatten_column Z.div Z.modulo Z.mul] in HeqX.
-          cbv [flatten_step] in HeqX.
-          cbv - [Z.modulo Z.div Z.eqb Z.mul Z.add_get_carry_full Z.add fst snd] in HeqX. cbn [app] in HeqX.
-          rewrite <-w'_sq in HeqX.
-          autorewrite with zsimplify_fast in HeqX.
-          rewrite !Z.mod_1_l in HeqX by omega.
-          rewrite !Z.mod_mul in HeqX by omega.
-          rewrite !Z.mod_small with (b:= w' 1 * w' 1) in HeqX by nia.
-          rewrite Z.eqb_refl in HeqX.
-          repeat match goal with H : Z.eqb _ _ = _ |- _ => rewrite H in HeqX end.
-          cbv - [Z.modulo Z.div Z.mul] in HeqX.
-          autorewrite with zsimplify in HeqX.
-          subst X.
-          *)
-
           subst mul_converted_single.
           reflexivity.
         Qed.