remove old loops code

4 files changed, 0 insertions, 805 deletions

diff --git a/src/Util/ForLoop/Instances.v b/src/Util/ForLoop/Instances.v
deleted file mode 100644
index 0a1f65e29..000000000
--- a/src/Util/ForLoop/Instances.v
+++ /dev/null
@@ -1,67 +0,0 @@
-Require Import Coq.omega.Omega.
-Require Import Coq.Classes.Morphisms.
-Require Import Crypto.Util.ForLoop.
-Require Import Crypto.Util.Notations.
-
-Lemma repeat_function_Proper_rel_le {stateT} R f g n
-      (Hfg : forall c, 0 < c <= n -> forall s1 s2, R s1 s2 -> R (f c s1) (g c s2))
-      s1 s2 (Hs : R s1 s2)
-  : R (@repeat_function stateT f n s1) (@repeat_function stateT g n s2).
-Proof.
-  revert s1 s2 Hs.
-  induction n; simpl; auto.
-  intros; apply IHn; auto;
-    intros; apply Hfg; auto;
-      omega.
-Qed.
-
-Global Instance repeat_function_Proper_rel {stateT} R
-  : Proper (pointwise_relation _ (R ==> R) ==> eq ==> R ==> R) (@repeat_function stateT) | 10.
-Proof.
-  unfold pointwise_relation, respectful.
-  intros body1 body2 Hbody c y ?; subst y.
-  induction c; simpl; auto.
-Qed.
-
-Lemma repeat_function_Proper_le {stateT} f g n
-      (Hfg : forall c, 0 < c <= n -> forall st, f c st = g c st)
-      st
-  : @repeat_function stateT f n st = @repeat_function stateT g n st.
-Proof.
-  apply repeat_function_Proper_rel_le; try reflexivity; intros; subst; auto.
-Qed.
-
-Global Instance repeat_function_Proper {stateT}
-  : Proper (pointwise_relation _ (pointwise_relation _ eq) ==> eq ==> eq ==> eq) (@repeat_function stateT).
-Proof.
-  intros ???; eapply repeat_function_Proper_rel; repeat intro; subst.
-  unfold pointwise_relation, respectful in *; auto.
-Qed.
-About for_loop.
-
-Global Instance for_loop_Proper_rel {stateT} R i0 final step
-  : Proper (R ==> pointwise_relation _ (R ==> R) ==> R) (@for_loop stateT i0 final step) | 10.
-Proof.
-  intros ?? Hinitial ?? Hbody; revert Hinitial.
-  unfold for_loop; eapply repeat_function_Proper_rel;
-    unfold pointwise_relation, respectful in *; auto.
-Qed.
-
-Global Instance for_loop_Proper_rel_full {stateT} R
-  : Proper (eq ==> eq ==> eq ==> R ==> pointwise_relation _ (R ==> R) ==> R) (@for_loop stateT) | 20.
-Proof.
-  intros ?????????; subst; apply for_loop_Proper_rel.
-Qed.
-
-Global Instance for_loop_Proper {stateT} i0 final step initial
-  : Proper (pointwise_relation _ (pointwise_relation _ eq) ==> eq) (@for_loop stateT i0 final step initial).
-Proof.
-  unfold pointwise_relation.
-  intros ???; eapply for_loop_Proper_rel; try reflexivity; repeat intro; subst; auto.
-Qed.
-
-Global Instance for_loop_Proper_full {stateT}
-  : Proper (eq ==> eq ==> eq ==> eq ==> pointwise_relation _ (pointwise_relation _ eq) ==> eq) (@for_loop stateT) | 5.
-Proof.
-  intros ????????????; subst; apply for_loop_Proper.
-Qed.
diff --git a/src/Util/ForLoop/InvariantFramework.v b/src/Util/ForLoop/InvariantFramework.v
deleted file mode 100644
index 2bff6bef9..000000000
--- a/src/Util/ForLoop/InvariantFramework.v
+++ /dev/null
@@ -1,369 +0,0 @@
-(** * Proving properties of for-loops via loop-invariants *)
-Require Import Coq.micromega.Psatz.
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Util.ForLoop.
-Require Import Crypto.Util.ForLoop.Unrolling.
-Require Import Crypto.Util.ZUtil.
-Require Import Crypto.Util.Bool.
-Require Import Crypto.Util.Tactics.UniquePose.
-Require Import Crypto.Util.Notations.
-
-Lemma repeat_function_ind {stateT} (P : nat -> stateT -> Prop)
-      (body : nat -> stateT -> stateT)
-      (count : nat) (st : stateT)
-      (Pbefore : P count st)
-      (Pbody : forall c st, c < count -> P (S c) st -> P c (body (S c) st))
-  : P 0 (repeat_function body count st).
-Proof.
-  revert dependent st; revert dependent body; revert dependent P.
-  induction count as [|? IHcount]; intros P body Pbody st Pbefore; [ exact Pbefore | ].
-  { rewrite repeat_function_unroll1_end; apply Pbody; [ omega | ].
-    apply (IHcount (fun c => P (S c))); auto with omega. }
-Qed.
-
-Local Open Scope bool_scope.
-Local Open Scope Z_scope.
-
-Section for_loop.
-  Context (i0 finish : Z) (step : Z) {stateT} (initial : stateT) (body : Z -> stateT -> stateT)
-          (P : Z -> stateT -> Prop)
-          (Pbefore : P i0 initial)
-          (Pbody : forall c st n, c = i0 + n * step -> i0 <= c < finish \/ finish < c <= i0 -> P c st -> P (c + step) (body c st))
-          (Hgood : Z.sgn step = Z.sgn (finish - i0)).
-
-  Let countZ := (Z.quot (finish - i0 + step - Z.sgn step) step).
-  Let count := Z.to_nat countZ.
-  Let of_nat_count c := (i0 + step * Z.of_nat (count - c)).
-  Let nat_body := (fun c => body (of_nat_count c)).
-
-  Local Arguments Z.mul !_ !_.
-  Local Arguments Z.add !_ !_.
-  Local Arguments Z.sub !_ !_.
-
-  Local Lemma Hgood_complex : Z.sgn step = Z.sgn (finish - i0 + step - Z.sgn step).
-  Proof using Hgood.
-    clear -Hgood.
-    revert Hgood.
-    generalize dependent (finish - i0); intro z; intros.
-    destruct step, z; simpl in * |- ; try (simpl; omega);
-      repeat change (Z.sgn (Z.pos _)) with 1;
-      repeat change (Z.sgn (Z.neg _)) with (-1);
-      symmetry;
-      [ apply Z.sgn_pos_iff | apply Z.sgn_neg_iff ];
-      lia.
-  Qed.
-
-  Local Lemma Hcount_nonneg : 0 <= countZ.
-  Proof using Hgood.
-    apply Z.quot_nonneg_same_sgn.
-    symmetry; apply Hgood_complex.
-  Qed.
-
-  Lemma for_loop_ind
-    : P (finish - Z.sgn (finish - i0 + step - Z.sgn step) * (Z.abs (finish - i0 + step - Z.sgn step) mod Z.abs step) + step - Z.sgn step)
-        (for_loop i0 finish step initial body).
-  Proof using Pbody Pbefore Hgood.
-    destruct (Z_zerop step).
-    { subst; unfold for_loop; simpl in *.
-      rewrite Z.quot_div_full; simpl.
-      symmetry in Hgood; rewrite Z.sgn_null_iff in Hgood.
-      assert (finish = i0) by omega; subst.
-      simpl; autorewrite with zsimplify_const; simpl; auto. }
-    assert (Hsgn_step : Z.sgn step <> 0) by (rewrite Z.sgn_null_iff; auto).
-    assert (Hsgn : Z.sgn ((finish - i0 + step - Z.sgn step) / step) = Z.sgn ((finish - i0 + step - Z.sgn step) / step) * Z.sgn (finish - i0 + step - Z.sgn step) * Z.sgn step)
-           by (rewrite <- Hgood_complex, <- Z.mul_assoc, <- Z.sgn_mul, (Z.sgn_pos (_ * _)) by nia; omega).
-    assert (Hfis_div : 0 <= (finish - i0 + step - Z.sgn step) / step)
-      by (apply Z.sgn_nonneg; rewrite Hsgn; apply Zdiv_sgn).
-    clear Hsgn.
-    let rhs := match goal with |- ?P ?rhs _ => rhs end in
-    assert (Heq : i0 + step * Z.of_nat count = rhs).
-    { unfold count, countZ.
-      rewrite Z.mod_eq by (rewrite Z.abs_0_iff; assumption).
-      rewrite Z.quot_div_full, <- !Z.sgn_abs, <- !Hgood_complex, !Zdiv_mult_cancel_r, !Z.mul_sub_distr_l by auto.
-      rewrite <- !Z.sgn_mul, !(Z.mul_comm _ (Z.sgn _)), !(Z.mul_assoc (Z.sgn _) _), <- Z.sgn_mul, Z.sgn_pos, !Z.mul_1_l by nia.
-      repeat rewrite ?Z.sub_add_distr, ?Z.sub_sub_distr; rewrite Z.sub_diag.
-      autorewrite with zsimplify_const.
-      rewrite Z2Nat.id by omega.
-      omega. }
-    rewrite <- Heq; clear Heq.
-    unfold for_loop.
-    generalize (@repeat_function_ind stateT (fun c => P (of_nat_count c)) nat_body count initial);
-      cbv beta in *.
-    unfold of_nat_count in *; cbv beta in *.
-    rewrite Nat.sub_diag, !Nat.sub_0_r.
-    autorewrite with zsimplify_const.
-    intro H; specialize (H Pbefore).
-    destruct (Z_dec' i0 finish) as [ Hs | Hs].
-    { apply H; clear H Pbefore.
-      { intros c st Hc.
-        assert (Hclt : 0 < Z.of_nat (count - c)) by (apply (inj_lt 0); omega).
-        intro H'; specialize (fun pf' n pf => Pbody _ _ n pf pf' H').
-        move Pbody at bottom.
-        { let T := match type of Pbody with ?T -> _ => T end in
-          let H := fresh in
-          cut T; [ intro H; specialize (Pbody H) | ].
-          { revert Pbody.
-            subst nat_body; cbv beta.
-            rewrite Nat.sub_succ_r, Nat2Z.inj_pred by omega.
-            rewrite <- Z.sub_1_r, Z.mul_sub_distr_l, Z.mul_1_r.
-            rewrite <- !Z.add_assoc, !Z.sub_add in *.
-            refine (fun p => p (Z.of_nat (count - c) - 1) _).
-            lia. }
-          { destruct Hs; [ left | right ].
-            { assert (Hstep : 0 < step)
-                by (rewrite <- Z.sgn_pos_iff, Hgood, Z.sgn_pos_iff; omega).
-              assert (0 < Z.of_nat (S c)) by (apply (inj_lt 0); omega).
-              assert (0 <= (finish - i0 + step - Z.sgn step) mod step) by auto with zarith.
-              assert (0 < step <= step * Z.of_nat (S c)) by nia.
-              split; [ nia | ].
-              rewrite Nat2Z.inj_sub, Z.mul_sub_distr_l by omega.
-              unfold count.
-              rewrite Z2Nat.id by auto using Hcount_nonneg.
-              unfold countZ.
-              rewrite Z.mul_quot_eq_full by auto.
-              rewrite <- !Hgood_complex, Z.abs_sgn.
-              rewrite !Z.add_sub_assoc, !Z.add_assoc, Zplus_minus.
-              rewrite Z.sgn_pos in * by omega.
-              omega. }
-            { assert (Hstep : step < 0)
-                by (rewrite <- Z.sgn_neg_iff, Hgood, Z.sgn_neg_iff; omega).
-              assert (Hcsc0 : 0 <= Z.of_nat (count - S c)) by auto with zarith.
-              assert (Hsc0 : 0 < Z.of_nat (S c)) by lia.
-              assert (step * Z.of_nat (count - S c) <= 0) by (clear -Hcsc0 Hstep; nia).
-              assert (step * Z.of_nat (S c) <= step < 0) by (clear -Hsc0 Hstep; nia).
-              assert (finish - i0 < 0)
-                by (rewrite <- Z.sgn_neg_iff, <- Hgood, Z.sgn_neg_iff; omega).
-              assert (finish - i0 + step - Z.sgn step < 0)
-                by (rewrite <- Z.sgn_neg_iff, <- Hgood_complex, Z.sgn_neg_iff; omega).
-              assert ((finish - i0 + step - Z.sgn step) mod step <= 0) by (apply Z_mod_neg; auto with zarith).
-              split; [ | nia ].
-              rewrite Nat2Z.inj_sub, Z.mul_sub_distr_l by omega.
-              unfold count.
-              rewrite Z2Nat.id by auto using Hcount_nonneg.
-              unfold countZ.
-              rewrite Z.mul_quot_eq_full by auto.
-              rewrite <- !Hgood_complex, Z.abs_sgn.
-              rewrite Z.sgn_neg in * by omega.
-              omega. } } } } }
-    { subst.
-      subst count nat_body countZ.
-      repeat first [ assumption
-                   | rewrite Z.sub_diag
-                   | progress autorewrite with zsimplify_const in *
-                   | rewrite Z.quot_sub_sgn ]. }
-  Qed.
-End for_loop.
-
-Lemma for_loop_notation_ind {stateT} (P : Z -> stateT -> Prop)
-      {i0 : Z} {step : Z} {finish : Z} {initial : stateT}
-      {cmp : Z -> Z -> bool}
-      {step_expr finish_expr} (body : Z -> stateT -> stateT)
-      {Hstep : class_eq (fun i => i = step) step_expr}
-      {Hfinish : class_eq (fun i => cmp i finish) finish_expr}
-      {Hgood : for_loop_is_good i0 step finish cmp}
-      (Pbefore : P i0 initial)
-      (Pbody : forall c st n, c = i0 + n * step -> i0 <= c < finish \/ finish < c <= i0 -> P c st -> P (c + step) (body c st))
-  : P (finish - Z.sgn (finish - i0 + step - Z.sgn step) * (Z.abs (finish - i0 + step - Z.sgn step) mod Z.abs step) + step - Z.sgn step)
-      (@for_loop_notation i0 step finish _ initial cmp step_expr finish_expr body Hstep Hfinish Hgood).
-Proof.
-  unfold for_loop_notation, for_loop_is_good in *; split_andb; Z.ltb_to_lt.
-  apply for_loop_ind; auto.
-Qed.
-
-Local Ltac pre_t :=
-  lazymatch goal with
-  | [ Pbefore : ?P ?i0 ?initial
-      |- ?P _ (@for_loop_notation ?i0 ?step ?finish _ ?initial _ ?step_expr ?finish_expr ?body ?Hstep ?Hfinish ?Hgood) ]
-    => generalize (@for_loop_notation_ind
-                     _ P i0 step finish initial _ step_expr finish_expr body Hstep Hfinish Hgood Pbefore)
-  end.
-Local Ltac t_step :=
-  first [ progress unfold for_loop_is_good, for_loop_notation in *
-        | progress split_andb
-        | progress Z.ltb_to_lt
-        | rewrite Z.sgn_pos by lia
-        | rewrite Z.abs_eq by lia
-        | rewrite Z.sgn_neg by lia
-        | rewrite Z.abs_neq by lia
-        | progress autorewrite with zsimplify_const
-        | match goal with
-          | [ Hsgn : Z.sgn ?step = Z.sgn _ |- _ ]
-            => unique assert (0 < step) by (rewrite <- Z.sgn_pos_iff, Hsgn, Z.sgn_pos_iff; omega); clear Hsgn
-          | [ Hsgn : Z.sgn ?step = Z.sgn _ |- _ ]
-            => unique assert (step < 0) by (rewrite <- Z.sgn_neg_iff, Hsgn, Z.sgn_neg_iff; omega); clear Hsgn
-          | [ |- (_ -> ?P ?x ?y) -> ?P ?x' ?y' ]
-            => replace x with x' by lia; let H' := fresh in intro H'; apply H'; clear H'
-          | [ |- (_ -> _) -> _ ]
-            => let H := fresh "Hbody" in intro H; progress Z.replace_all_neg_with_pos; revert H
-          end
-        | rewrite !Z.opp_sub_distr
-        | rewrite !Z.opp_add_distr
-        | rewrite !Z.opp_involutive
-        | rewrite !Z.sub_opp_r
-        | rewrite (Z.add_opp_r _ 1)
-        | progress (push_Zmod; pull_Zmod)
-        | progress Z.replace_all_neg_with_pos
-        | solve [ eauto with omega ] ].
-Local Ltac t := pre_t; repeat t_step.
-
-Lemma for_loop_ind_lt {stateT} (P : Z -> stateT -> Prop)
-      {i0 : Z} {step : Z} {finish : Z} {initial : stateT}
-      {step_expr finish_expr} (body : Z -> stateT -> stateT)
-      {Hstep : class_eq (fun i => i = step) step_expr}
-      {Hfinish : class_eq (fun i => Z.ltb i finish) finish_expr}
-      {Hgood : for_loop_is_good i0 step finish Z.ltb}
-      (Pbefore : P i0 initial)
-      (Pbody : forall c st n, c = i0 + n * step -> i0 <= c < finish -> P c st -> P (c + step) (body c st))
-  : P (finish + step - 1 - ((finish - i0 - 1) mod step))
-      (@for_loop_notation i0 step finish _ initial Z.ltb (fun i => step_expr i) (fun i => finish_expr i) (fun i st => body i st) Hstep Hfinish Hgood).
-Proof. t. Qed.
-
-Lemma for_loop_ind_gt {stateT} (P : Z -> stateT -> Prop)
-      {i0 : Z} {step : Z} {finish : Z} {initial : stateT}
-      {step_expr finish_expr} (body : Z -> stateT -> stateT)
-      {Hstep : class_eq (fun i => i = step) step_expr}
-      {Hfinish : class_eq (fun i => Z.gtb i finish) finish_expr}
-      {Hgood : for_loop_is_good i0 step finish Z.gtb}
-      (Pbefore : P i0 initial)
-      (Pbody : forall c st n, c = i0 + n * step -> finish < c <= i0 -> P c st -> P (c + step) (body c st))
-  : P (finish + step + 1 + (i0 - finish - step - 1) mod (-step))
-      (@for_loop_notation i0 step finish _ initial Z.gtb (fun i => step_expr i) (fun i => finish_expr i) (fun i st => body i st) Hstep Hfinish Hgood).
-Proof.
-  replace (i0 - finish) with (-(finish - i0)) by omega.
-  t.
-Qed.
-
-Lemma for_loop_ind_lt1 {stateT} (P : Z -> stateT -> Prop)
-      {i0 : Z} {finish : Z} {initial : stateT}
-      (body : Z -> stateT -> stateT)
-      {Hgood : for_loop_is_good i0 1 finish _}
-      (Pbefore : P i0 initial)
-      (Pbody : forall c st, i0 <= c < finish -> P c st -> P (c + 1) (body c st))
-  : P finish
-      (for (int i = i0; i < finish; i++) updating (st = initial) {{
-         body i st
-      }}).
-Proof.
-  generalize (@for_loop_ind_lt
-                stateT P i0 1 finish initial _ _ body eq_refl eq_refl Hgood Pbefore).
-  rewrite Z.mod_1_r, Z.sub_0_r, Z.add_simpl_r.
-  auto.
-Qed.
-
-Lemma for_loop_ind_gt1 {stateT} (P : Z -> stateT -> Prop)
-      {i0 : Z} {finish : Z} {initial : stateT}
-      (body : Z -> stateT -> stateT)
-      {Hgood : for_loop_is_good i0 (-1) finish _}
-      (Pbefore : P i0 initial)
-      (Pbody : forall c st, finish < c <= i0 -> P c st -> P (c - 1) (body c st))
-  : P finish
-      (for (int i = i0; i > finish; i--) updating (st = initial) {{
-         body i st
-      }}).
-Proof.
-  generalize (@for_loop_ind_gt
-                stateT P i0 (-1) finish initial _ _ body eq_refl eq_refl Hgood Pbefore).
-  simpl; rewrite Z.mod_1_r, Z.add_0_r, (Z.add_opp_r _ 1), Z.sub_simpl_r.
-  intro H; apply H; intros *.
-  rewrite (Z.add_opp_r _ 1); auto.
-Qed.
-
-Local Hint Extern 1 (for_loop_is_good (?i0 + ?step) ?step ?finish _)
-=> refine (for_loop_is_good_step_lt _); try assumption : typeclass_instances.
-Local Hint Extern 1 (for_loop_is_good (?i0 + ?step) ?step ?finish _)
-=> refine (for_loop_is_good_step_gt _); try assumption : typeclass_instances.
-Local Hint Extern 1 (for_loop_is_good (?i0 - ?step') _ ?finish _)
-=> refine (for_loop_is_good_step_gt (step:=-step') _); try assumption : typeclass_instances.
-Local Hint Extern 1 (for_loop_is_good (?i0 + 1) 1 ?finish _)
-=> refine (for_loop_is_good_step_lt' _); try assumption : typeclass_instances.
-Local Hint Extern 1 (for_loop_is_good (?i0 - 1) (-1) ?finish _)
-=> refine (for_loop_is_good_step_gt' _); try assumption : typeclass_instances.
-
-(** The Hoare-logic-like conditions for ≤ and ≥ loops seem slightly
-    unnatural; you have to choose either to state your correctness
-    property in terms of [i + 1], or talk about the correctness
-    condition when the loop counter is [i₀ - 1] (which is strange;
-    it's like saying the loop has run -1 times), or give the
-    correctness condition after the first run of the loop body, rather
-    than before it.  We give lemmas for the second two options; if
-    you're using the first one, Coq probably won't be able to infer
-    the motive ([P], below) automatically, and you might as well use
-    the vastly more general version [for_loop_ind_lt] /
-    [for_loop_ind_gt]. *)
-Lemma for_loop_ind_le1 {stateT} (P : Z -> stateT -> Prop)
-      {i0 : Z} {finish : Z} {initial : stateT}
-      (body : Z -> stateT -> stateT)
-      {Hgood : for_loop_is_good i0 1 (finish+1) _}
-      (Pbefore : P i0 (body i0 initial))
-      (Pbody : forall c st, i0 <= c <= finish -> P (c-1) st -> P c (body c st))
-  : P finish
-      (for (int i = i0; i <= finish; i++) updating (st = initial) {{
-         body i st
-      }}).
-Proof.
-  rewrite for_loop_le1_unroll1.
-  edestruct Sumbool.sumbool_of_bool; Z.ltb_to_lt; cbv zeta.
-  { generalize (@for_loop_ind_lt
-                  stateT (fun n => P (n - 1)) (i0+1) 1 (finish+1) (body i0 initial) _ _ body eq_refl eq_refl _).
-    rewrite Z.mod_1_r, Z.sub_0_r, !Z.add_simpl_r.
-    intro H; apply H; auto with omega; intros *.
-    rewrite !Z.add_simpl_r; auto with omega. }
-  { unfold for_loop_is_good, ForNotationConstants.Z.ltb', ForNotationConstants.Z.ltb in *; split_andb; Z.ltb_to_lt.
-    assert (i0 = finish) by omega; subst.
-    assumption. }
-Qed.
-
-Lemma for_loop_ind_le1_offset {stateT} (P : Z -> stateT -> Prop)
-      {i0 : Z} {finish : Z} {initial : stateT}
-      (body : Z -> stateT -> stateT)
-      {Hgood : for_loop_is_good i0 1 (finish+1) _}
-      (Pbefore : P (i0-1) initial)
-      (Pbody : forall c st, i0 <= c <= finish -> P (c-1) st -> P c (body c st))
-  : P finish
-      (for (int i = i0; i <= finish; i++) updating (st = initial) {{
-         body i st
-      }}).
-Proof.
-  apply for_loop_ind_le1; auto with omega.
-  unfold for_loop_is_good, ForNotationConstants.Z.ltb', ForNotationConstants.Z.ltb in *; split_andb; Z.ltb_to_lt.
-  auto with omega.
-Qed.
-
-Lemma for_loop_ind_ge1 {stateT} (P : Z -> stateT -> Prop)
-      {i0 : Z} {finish : Z} {initial : stateT}
-      (body : Z -> stateT -> stateT)
-      {Hgood : for_loop_is_good i0 (-1) (finish-1) _}
-      (Pbefore : P i0 (body i0 initial))
-      (Pbody : forall c st, finish <= c <= i0 -> P (c+1) st -> P c (body c st))
-  : P finish
-      (for (int i = i0; i >= finish; i--) updating (st = initial) {{
-         body i st
-      }}).
-Proof.
-  rewrite for_loop_ge1_unroll1.
-  edestruct Sumbool.sumbool_of_bool; Z.ltb_to_lt; cbv zeta.
-  { generalize (@for_loop_ind_gt
-                  stateT (fun n => P (n + 1)) (i0-1) (-1) (finish-1) (body i0 initial) _ _ body eq_refl eq_refl _).
-    simpl; rewrite Z.mod_1_r, Z.add_0_r, (Z.add_opp_r _ 1), !Z.sub_simpl_r.
-    intro H; apply H; intros *; auto with omega.
-    rewrite (Z.add_opp_r _ 1), !Z.sub_simpl_r; auto with omega. }
-  { unfold for_loop_is_good, ForNotationConstants.Z.gtb', ForNotationConstants.Z.gtb in *; split_andb; Z.ltb_to_lt.
-    assert (i0 = finish) by omega; subst.
-    assumption. }
-Qed.
-
-Lemma for_loop_ind_ge1_offset {stateT} (P : Z -> stateT -> Prop)
-      {i0 : Z} {finish : Z} {initial : stateT}
-      (body : Z -> stateT -> stateT)
-      {Hgood : for_loop_is_good i0 (-1) (finish-1) _}
-      (Pbefore : P (i0+1) initial)
-      (Pbody : forall c st, finish <= c <= i0 -> P (c+1) st -> P c (body c st))
-  : P finish
-      (for (int i = i0; i >= finish; i--) updating (st = initial) {{
-         body i st
-      }}).
-Proof.
-  apply for_loop_ind_ge1; auto with omega.
-  unfold for_loop_is_good, ForNotationConstants.Z.gtb', ForNotationConstants.Z.gtb in *; split_andb; Z.ltb_to_lt.
-  auto with omega.
-Qed.
diff --git a/src/Util/ForLoop/Tests.v b/src/Util/ForLoop/Tests.v
deleted file mode 100644
index 1061f1958..000000000
--- a/src/Util/ForLoop/Tests.v
+++ /dev/null
@@ -1,55 +0,0 @@
-Require Import Coq.ZArith.BinInt.
-Require Import Coq.micromega.Psatz.
-Require Import Crypto.Util.ForLoop.
-Require Import Crypto.Util.ForLoop.InvariantFramework.
-Require Import Crypto.Util.ZUtil.
-
-Local Open Scope Z_scope.
-
-Check (for i (:= 0; += 1; < 10) updating (v := 5) {{ v + i }}).
-Check (for (int i = 0; i < 5; i++) updating ( '(v1, v2) = (0, 0) ) {{ (v1 + i, v2 + i) }}).
-
-Compute for (int i = 0; i < 5; i++) updating (v = 0) {{ v + i }}.
-Compute for (int i = 0; i <= 5; i++) updating (v = 0) {{ v + i }}.
-Compute for (int i = 5; i > -1; i--) updating (v = 0) {{ v + i }}.
-Compute for (int i = 5; i >= 0; i--) updating (v = 0) {{ v + i }}.
-Compute for (int i = 0; i < 5; i += 2) updating (v = 0) {{ v + i }}.
-Compute for (int i = 0; i <= 5; i += 2) updating (v = 0) {{ v + i }}.
-Compute for (int i = 5; i > -1; i -= 2) updating (v = 0) {{ v + i }}.
-Compute for (int i = 5; i >= 0; i -= 2) updating (v = 0) {{ v + i }}.
-Compute for (int i = 0; i < 6; i += 2) updating (v = 0) {{ v + i }}.
-Compute for (int i = 0; i <= 6; i += 2) updating (v = 0) {{ v + i }}.
-Compute for (int i = 6; i > -1; i -= 2) updating (v = 0) {{ v + i }}.
-Compute for (int i = 6; i >= 0; i -= 2) updating (v = 0) {{ v + i }}.
-Check eq_refl : for (int i = 0; i <= 5; i++) updating (v = 0) {{ v + i }} = 15.
-Check eq_refl : for (int i = 0; i < 5; i++) updating (v = 0) {{ v + i }} = 10.
-Check eq_refl : for (int i = 5; i >= 0; i--) updating (v = 0) {{ v + i }} = 15.
-Check eq_refl : for (int i = 5; i > -1; i--) updating (v = 0) {{ v + i }} = 15.
-Check eq_refl : for (int i = 0; i <= 5; i += 2) updating (v = 0) {{ v + i }} = 6.
-Check eq_refl : for (int i = 0; i < 5; i += 2) updating (v = 0) {{ v + i }} = 6.
-Check eq_refl : for (int i = 5; i > -1; i -= 2) updating (v = 0) {{ v + i }} = 9.
-Check eq_refl : for (int i = 5; i >= 0; i -= 2) updating (v = 0) {{ v + i }} = 9.
-Check eq_refl : for (int i = 0; i <= 6; i += 2) updating (v = 0) {{ v + i }} = 12.
-Check eq_refl : for (int i = 0; i < 6; i += 2) updating (v = 0) {{ v + i }} = 6.
-Check eq_refl : for (int i = 6; i > -1; i -= 2) updating (v = 0) {{ v + i }} = 12.
-Check eq_refl : for (int i = 6; i >= 0; i -= 2) updating (v = 0) {{ v + i }} = 12.
-
-Local Notation for_sumT n'
-  := (let n := Z.pos n' in
-      (2 *
-       for (int i = 0; i <= n; i++) updating (v = 0) {{
-         v + i
-       }})%Z
-      = n * (n + 1))
-       (only parsing).
-
-Check eq_refl : for_sumT 5.
-
-(** Here we show that if we add the numbers from 0 to n, we get [n * (n + 1) / 2] *)
-Example for_sum n' : for_sumT n'.
-Proof.
-  intro n.
-  apply for_loop_ind_le1.
-  { compute; reflexivity. }
-  { intros; nia. }
-Qed.
diff --git a/src/Util/ForLoop/Unrolling.v b/src/Util/ForLoop/Unrolling.v
deleted file mode 100644
index 95b46e711..000000000
--- a/src/Util/ForLoop/Unrolling.v
+++ /dev/null
@@ -1,314 +0,0 @@
-(** * Proving properties of for-loops via loop-unrolling *)
-Require Import Coq.micromega.Psatz.
-Require Import Coq.ZArith.ZArith.
-Require Import Crypto.Util.ForLoop.
-Require Import Crypto.Util.ForLoop.Instances.
-Require Import Crypto.Util.ZUtil.
-Require Import Crypto.Util.Bool.
-Require Import Crypto.Util.Tactics.RewriteHyp.
-Require Import Crypto.Util.Tactics.BreakMatch.
-Require Import Crypto.Util.Tactics.DestructHead.
-Require Import Crypto.Util.Notations.
-
-Section with_body.
-  Context {stateT : Type}
-          (body : nat -> stateT -> stateT).
-
-  Lemma unfold_repeat_function (count : nat) (st : stateT)
-    : repeat_function body count st
-      = match count with
-        | O => st
-        | S count' => repeat_function body count' (body count st)
-        end.
-  Proof using Type. destruct count; reflexivity. Qed.
-
-  Lemma repeat_function_unroll1_start (count : nat) (st : stateT)
-    : repeat_function body (S count) st
-      = repeat_function body count (body (S count) st).
-  Proof using Type. rewrite unfold_repeat_function; reflexivity. Qed.
-
-  Lemma repeat_function_unroll1_end (count : nat) (st : stateT)
-    : repeat_function body (S count) st
-      = body 1 (repeat_function (fun count => body (S count)) count st).
-  Proof using Type.
-    revert st; induction count as [|? IHcount]; [ reflexivity | ].
-    intros; simpl in *; rewrite <- IHcount; reflexivity.
-  Qed.
-
-  Lemma repeat_function_unroll1_start_match (count : nat) (st : stateT)
-    : repeat_function body count st
-      = match count with
-        | 0 => st
-        | S count' => repeat_function body count' (body count st)
-        end.
-  Proof using Type. destruct count; [ reflexivity | apply repeat_function_unroll1_start ]. Qed.
-
-  Lemma repeat_function_unroll1_end_match (count : nat) (st : stateT)
-    : repeat_function body count st
-      = match count with
-        | 0 => st
-        | S count' => body 1 (repeat_function (fun count => body (S count)) count' st)
-        end.
-  Proof using Type. destruct count; [ reflexivity | apply repeat_function_unroll1_end ]. Qed.
-End with_body.
-
-Local Open Scope bool_scope.
-Local Open Scope Z_scope.
-
-Section for_loop.
-  Context (i0 finish : Z) (step : Z) {stateT} (initial : stateT) (body : Z -> stateT -> stateT)
-          (Hgood : Z.sgn step = Z.sgn (finish - i0)).
-
-  Let countZ := (Z.quot (finish - i0 + step - Z.sgn step) step).
-  Let count := Z.to_nat countZ.
-  Let of_nat_count c := (i0 + step * Z.of_nat (count - c)).
-  Let nat_body := (fun c => body (of_nat_count c)).
-
-  Lemma for_loop_empty
-        (Heq : finish = i0)
-    : for_loop i0 finish step initial body = initial.
-  Proof.
-    subst; unfold for_loop.
-    rewrite Z.sub_diag, Z.quot_sub_sgn; autorewrite with zsimplify_const.
-    reflexivity.
-  Qed.
-
-  Lemma for_loop_unroll1
-    : for_loop i0 finish step initial body
-      = if finish =? i0
-        then initial
-        else let initial' := body i0 initial in
-             if Z.abs (finish - i0) <=? Z.abs step
-             then initial'
-             else for_loop (i0 + step) finish step initial' body.
-  Proof.
-    break_innermost_match_step; Z.ltb_to_lt.
-    { apply for_loop_empty; assumption. }
-    { unfold for_loop.
-      rewrite repeat_function_unroll1_start_match.
-      destruct (Z_zerop step);
-        repeat first [ progress break_innermost_match
-                     | congruence
-                     | lia
-                     | progress Z.ltb_to_lt
-                     | progress subst
-                     | progress rewrite Nat.sub_diag
-                     | progress autorewrite with zsimplify_const in *
-                     | progress rewrite Z.quot_small_iff in * by omega
-                     | progress rewrite Z.quot_small_abs in * by lia
-                     | rewrite Nat.sub_succ_l by omega
-                     | progress destruct_head' and
-                     | rewrite !Z.sub_add_distr
-                     | match goal with
-                       | [ H : ?x = Z.of_nat _ |- context[?x] ] => rewrite H
-                       | [ H : Z.abs ?x <= 0 |- _ ] => assert (x = 0) by lia; clear H
-                       | [ H : 0 = Z.sgn ?x |- _ ] => assert (x = 0) by lia; clear H
-                       | [ H : ?x - ?y = 0 |- _ ] => is_var x; assert (x = y) by omega; subst x
-                       | [ H : Z.to_nat _ = _ |- _ ] => apply Nat2Z.inj_iff in H
-                       | [ H : context[Z.abs ?x] |- _ ] => rewrite (Z.abs_eq x) in H by omega
-                       | [ H : context[Z.abs ?x] |- _ ] => rewrite (Z.abs_neq x) in H by omega
-                       | [ H : Z.of_nat (Z.to_nat _) = _ |- _ ]
-                         => rewrite Z2Nat.id in H by (apply Z.quot_nonneg_same_sgn; lia)
-                       | [ H : _ = Z.of_nat (S ?x) |- _ ]
-                         => is_var x; destruct x; [ reflexivity | ]
-                       | [ H : ?x + 1 = Z.of_nat (S ?y) |- _ ]
-                         => assert (x = Z.of_nat y) by lia; clear H
-                       | [ |- repeat_function _ ?x ?y = repeat_function _ ?x ?y ]
-                         => apply repeat_function_Proper_le; intros
-                       | [ |- ?f _ ?x = ?f _ ?x ]
-                         => is_var f; apply f_equal2; [ | reflexivity ]
-                       end
-                     | progress rewrite Z.quot_add_sub_sgn_small in * |- by lia
-                     | progress autorewrite with zsimplify ]. }
-  Qed.
-End for_loop.
-
-Lemma for_loop_notation_empty {stateT}
-      {i0 : Z} {step : Z} {finish : Z} {initial : stateT}
-      {cmp : Z -> Z -> bool}
-      {step_expr finish_expr} (body : Z -> stateT -> stateT)
-      {Hstep : class_eq (fun i => i = step) step_expr}
-      {Hfinish : class_eq (fun i => cmp i finish) finish_expr}
-      {Hgood : for_loop_is_good i0 step finish cmp}
-      (Heq : i0 = finish)
-  : @for_loop_notation i0 step finish _ initial cmp step_expr finish_expr body Hstep Hfinish Hgood = initial.
-Proof.
-  unfold for_loop_notation, for_loop_is_good in *; split_andb; Z.ltb_to_lt.
-  apply for_loop_empty; auto.
-Qed.
-
-Local Notation adjust_bool b p
-  := (match b as b' return b' = true -> b' = true with
-      | true => fun _ => eq_refl
-      | false => fun x => x
-      end p).
-
-Lemma for_loop_is_good_step_gen
-      cmp
-      (Hcmp : cmp = Z.ltb \/ cmp = Z.gtb)
-      {i0 step finish}
-      {H : for_loop_is_good i0 step finish cmp}
-      (H' : cmp (i0 + step) finish = true)
-  : for_loop_is_good (i0 + step) step finish cmp.
-Proof.
-  unfold for_loop_is_good in *.
-  rewrite H', Bool.andb_true_r.
-  destruct Hcmp; subst;
-    split_andb; Z.ltb_to_lt;
-      [ rewrite (Z.sgn_pos (finish - i0)) in * by omega
-      | rewrite (Z.sgn_neg (finish - i0)) in * by omega ];
-      destruct step; simpl in *; try congruence;
-        symmetry;
-        [ apply Z.sgn_pos_iff | apply Z.sgn_neg_iff ]
-        ; omega.
-Qed.
-
-Definition for_loop_is_good_step_lt
-           {i0 step finish}
-           {H : for_loop_is_good i0 step finish Z.ltb}
-           (H' : Z.ltb (i0 + step) finish = true)
-  : for_loop_is_good (i0 + step) step finish Z.ltb
-  := for_loop_is_good_step_gen Z.ltb (or_introl eq_refl) (H:=H) H'.
-Definition for_loop_is_good_step_gt
-           {i0 step finish}
-           {H : for_loop_is_good i0 step finish Z.gtb}
-           (H' : Z.gtb (i0 + step) finish = true)
-  : for_loop_is_good (i0 + step) step finish Z.gtb
-  := for_loop_is_good_step_gen Z.gtb (or_intror eq_refl) (H:=H) H'.
-Definition for_loop_is_good_step_lt'
-           {i0 finish}
-           {H : for_loop_is_good i0 1 (finish + 1) Z.ltb}
-           (H' : Z.ltb i0 finish = true)
-  : for_loop_is_good (i0 + 1) 1 (finish + 1) Z.ltb.
-Proof.
-  apply for_loop_is_good_step_lt; Z.ltb_to_lt; omega.
-Qed.
-Definition for_loop_is_good_step_gt'
-           {i0 finish}
-           {H : for_loop_is_good i0 (-1) (finish - 1) Z.gtb}
-           (H' : Z.gtb i0 finish = true)
-  : for_loop_is_good (i0 - 1) (-1) (finish - 1) Z.gtb.
-Proof.
-  apply for_loop_is_good_step_gt; Z.ltb_to_lt; omega.
-Qed.
-
-Local Hint Extern 1 (for_loop_is_good (?i0 + ?step) ?step ?finish _)
-=> refine (adjust_bool _ (for_loop_is_good_step_lt _)); try assumption : typeclass_instances.
-Local Hint Extern 1 (for_loop_is_good (?i0 + ?step) ?step ?finish _)
-=> refine (adjust_bool _ (for_loop_is_good_step_gt _)); try assumption : typeclass_instances.
-Local Hint Extern 1 (for_loop_is_good (?i0 - ?step') _ ?finish _)
-=> refine (adjust_bool _ (for_loop_is_good_step_gt (step:=-step') _)); try assumption : typeclass_instances.
-Local Hint Extern 1 (for_loop_is_good (?i0 + 1) 1 ?finish _)
-=> refine (adjust_bool _ (for_loop_is_good_step_lt' _)); try assumption : typeclass_instances.
-Local Hint Extern 1 (for_loop_is_good (?i0 - 1) (-1) ?finish _)
-=> refine (adjust_bool _ (for_loop_is_good_step_gt' _)); try assumption : typeclass_instances.
-
-Local Ltac t :=
-  repeat match goal with
-         | _ => progress unfold for_loop_is_good, for_loop_notation in *
-         | _ => progress rewrite for_loop_unroll1 by auto
-         | _ => omega
-         | _ => progress subst
-         | _ => reflexivity
-         | _ => progress split_andb
-         | _ => progress Z.ltb_to_lt
-         | _ => progress break_innermost_match_step
-         | [ H : context[Z.abs ?x] |- _ ] => rewrite (Z.abs_eq x) in H by omega
-         | [ H : context[Z.abs ?x] |- _ ] => rewrite (Z.abs_neq x) in H by omega
-         | [ H : context[Z.sgn ?x] |- _ ] => rewrite (Z.sgn_pos x) in H by omega
-         | [ H : context[Z.sgn ?x] |- _ ] => rewrite (Z.sgn_neg x) in H by omega
-         | [ H : Z.sgn _ = 1 |- _ ] => apply Z.sgn_pos_iff in H
-         | [ H : Z.sgn _ = -1 |- _ ] => apply Z.sgn_neg_iff in H
-         end.
-
-Lemma for_loop_lt_unroll1 {stateT}
-      {i0 : Z} {step : Z} {finish : Z} {initial : stateT}
-      {step_expr finish_expr} (body : Z -> stateT -> stateT)
-      {Hstep : class_eq (fun i => i = step) step_expr}
-      {Hfinish : class_eq (fun i => Z.ltb i finish) finish_expr}
-      {Hgood : for_loop_is_good i0 step finish Z.ltb}
-  : (@for_loop_notation i0 step finish _ initial Z.ltb (fun i => step_expr i) (fun i => finish_expr i) (fun i st => body i st) Hstep Hfinish Hgood)
-    = let initial' := body i0 initial in
-      if Sumbool.sumbool_of_bool (Z.ltb (i0 + step) finish)
-      then @for_loop_notation (i0 + step) step finish _ initial' Z.ltb (fun i => step_expr i) (fun i => finish_expr i) (fun i st => body i st) Hstep Hfinish _
-      else initial'.
-Proof. t. Qed.
-
-Lemma for_loop_gt_unroll1 {stateT}
-      {i0 : Z} {step : Z} {finish : Z} {initial : stateT}
-      {step_expr finish_expr} (body : Z -> stateT -> stateT)
-      {Hstep : class_eq (fun i => i = step) step_expr}
-      {Hfinish : class_eq (fun i => Z.gtb i finish) finish_expr}
-      {Hgood : for_loop_is_good i0 step finish Z.gtb}
-  : (@for_loop_notation i0 step finish _ initial Z.gtb (fun i => step_expr i) (fun i => finish_expr i) (fun i st => body i st) Hstep Hfinish Hgood)
-    = let initial' := body i0 initial in
-      if Sumbool.sumbool_of_bool (Z.gtb (i0 + step) finish)
-      then @for_loop_notation (i0 + step) step finish _ initial' Z.gtb (fun i => step_expr i) (fun i => finish_expr i) (fun i st => body i st) Hstep Hfinish _
-      else initial'.
-Proof. t. Qed.
-
-Lemma for_loop_lt1_unroll1 {stateT}
-      {i0 : Z} {finish : Z} {initial : stateT}
-      {body : Z -> stateT -> stateT}
-      {Hgood : for_loop_is_good i0 1 finish _}
-  : for (int i = i0; i < finish; i++) updating (st = initial) {{
-      body i st
-    }}
-    = let initial' := body i0 initial in
-      if Sumbool.sumbool_of_bool (Z.ltb (i0 + 1) finish)
-      then for (int i = i0+1; i < finish; i++) updating (st = initial') {{
-             body i st
-           }}
-      else initial'.
-Proof. apply for_loop_lt_unroll1. Qed.
-
-Lemma for_loop_gt1_unroll1 {stateT}
-      {i0 : Z} {finish : Z} {initial : stateT}
-      {body : Z -> stateT -> stateT}
-      {Hgood : for_loop_is_good i0 (-1) finish _}
-  : for (int i = i0; i > finish; i--) updating (st = initial) {{
-      body i st
-    }}
-    = let initial' := body i0 initial in
-      if Sumbool.sumbool_of_bool (Z.gtb (i0 - 1) finish)
-      then for (int i = i0-1; i > finish; i--) updating (st = initial') {{
-             body i st
-           }}
-      else initial'.
-Proof. apply for_loop_gt_unroll1. Qed.
-
-Lemma for_loop_le1_unroll1 {stateT}
-      {i0 : Z} {finish : Z} {initial : stateT}
-      {body : Z -> stateT -> stateT}
-      {Hgood : for_loop_is_good i0 1 (finish+1) _}
-  : for (int i = i0; i <= finish; i++) updating (st = initial) {{
-      body i st
-    }}
-    = let initial' := body i0 initial in
-      if Sumbool.sumbool_of_bool (Z.ltb i0 finish)
-      then for (int i = i0+1; i <= finish; i++) updating (st = initial') {{
-             body i st
-           }}
-      else initial'.
-Proof.
-  rewrite for_loop_lt_unroll1; unfold for_loop_notation.
-  break_innermost_match; Z.ltb_to_lt; try omega; try reflexivity.
-Qed.
-
-Lemma for_loop_ge1_unroll1 {stateT}
-      {i0 : Z} {finish : Z} {initial : stateT}
-      {body : Z -> stateT -> stateT}
-      {Hgood : for_loop_is_good i0 (-1) (finish-1) _}
-  : for (int i = i0; i >= finish; i--) updating (st = initial) {{
-      body i st
-    }}
-    = let initial' := body i0 initial in
-      if Sumbool.sumbool_of_bool (Z.gtb i0 finish)
-      then for (int i = i0-1; i >= finish; i--) updating (st = initial') {{
-             body i st
-           }}
-      else initial'.
-Proof.
-  rewrite for_loop_gt_unroll1; unfold for_loop_notation.
-  break_innermost_match; Z.ltb_to_lt; try omega; try reflexivity.
-Qed.