Cleanup: mostly moving lemmas to Util files, some moving lemmas to more general contexts.

3 files changed, 61 insertions, 1 deletions

diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index b640fb8e8..36d8a3ad3 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -563,4 +563,22 @@ Proof.
   induction l; intros; simpl; try tauto.
   rewrite <- IHl.
   intuition (subst; auto).
-Qed. 
\ No newline at end of file
+Qed.
+
+Lemma fold_right_invariant : forall {A} P (f: A -> A -> A) l x,
+  P x -> (forall y, In y l -> forall z, P z -> P (f y z)) ->
+  P (fold_right f x l).
+Proof.
+  induction l; intros ? ? step; auto.
+  simpl.
+  apply step; try apply in_eq.
+  apply IHl; auto.
+  intros y in_y_l.
+  apply (in_cons a) in in_y_l.
+  auto.
+Qed.
+
+Lemma In_firstn : forall {T} n l (x : T), In x (firstn n l) -> In x l.
+Proof.
+  induction n; destruct l; boring.
+Qed.
diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 17d04c60a..d655d046d 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -1,5 +1,6 @@
 Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.NatUtil.
 Require Import Bedrock.Word.
 
 Local Open Scope nat_scope.
@@ -21,6 +22,30 @@ Proof.
   auto.
 Qed.
 
+Lemma wordToN_NToWord_idempotent : forall sz n, (n < Npow2 sz)%N ->
+  wordToN (NToWord sz n) = n.
+Proof.
+  intros.
+  rewrite wordToN_nat, NToWord_nat.
+  rewrite wordToNat_natToWord_idempotent; rewrite Nnat.N2Nat.id; auto.
+Qed.
+
+Lemma NToWord_wordToN : forall sz w, NToWord sz (wordToN w) = w.
+Proof.
+  intros.
+  rewrite wordToN_nat, NToWord_nat, Nnat.Nat2N.id.
+  apply natToWord_wordToNat.
+Qed.
+
+Lemma bound_check_nat_N : forall x n, (Z.to_nat x < 2 ^ n)%nat -> (Z.to_N x < Npow2 n)%N.
+Proof.
+  intros x n bound_nat.
+  rewrite <- Nnat.N2Nat.id, Npow2_nat.
+  replace (Z.to_N x) with (N.of_nat (Z.to_nat x)) by apply Z_nat_N.
+  apply (Nat2N_inj_lt _ (pow2 n)).
+  rewrite pow2_id; assumption.
+Qed.
+
 Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n.
   refine (Word.split1 n (m - n) (match _ in _ = N return Word.word N with
                             | eq_refl => w
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 9f7b1d645..bc7e9d740 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -280,6 +280,23 @@ Proof.
   assumption.
 Qed.
 
+Lemma Z_odd_mod : forall a b, (b <> 0)%Z ->
+  Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a.
+Proof.
+  intros.
+  rewrite Zmod_eq_full by assumption.
+  rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul.
+  case_eq (Z.odd b); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r.
+Qed.
+
+Lemma mod_same_pow : forall a b c, 0 <= c <= b -> a ^ b mod a ^ c = 0.
+Proof.
+  intros.
+  replace b with (b - c + c) by ring.
+  rewrite Z.pow_add_r by omega.
+  apply Z_mod_mult.
+Qed.
+
 (* prove that known nonnegative numbers are nonnegative *)
 Ltac zero_bounds' :=
   repeat match goal with