moved lemmas from ModularBaseSystemProofs to various Util files

5 files changed, 75 insertions, 48 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 0a7070922..f39f32ea5 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -268,49 +268,6 @@ Section CarryProofs.
     apply limb_widths_nonneg.
     eapply nth_error_value_In; eauto.
   Qed.
-
-  (* TODO : move to ZUtil *)
-  Lemma div_pow2succ : forall n x, (0 <= x) ->
-    n / 2 ^ Z.succ x = Z.div2 (n / 2 ^ x).
-  Proof.
-    intros.
-    rewrite Z.pow_succ_r, Z.mul_comm by auto.
-    rewrite <- Z.div_div by (try apply Z.pow_nonzero; omega).
-    rewrite Zdiv2_div.
-    reflexivity.
-  Qed.
-
-  (* TODO: move to ZUtil *)
-  Lemma shiftr_succ : forall n x,
-    Z.shiftr n (Z.succ x) = Z.shiftr (Z.shiftr n x) 1.
-  Proof.
-    intros.
-    rewrite Z.shiftr_shiftr by omega.
-    reflexivity.
-  Qed.
-
-  (* TODO : move to ZUtil *)
-  Lemma shiftr_div : forall n i, (0 <= i) -> Z.shiftr n i = n / (2 ^ i).
-  Proof.
-    intro.
-    apply natlike_ind; intros; [boring|].
-    rewrite div_pow2succ by auto.
-    rewrite shiftr_succ.
-    unfold Z.shiftr.
-    simpl; f_equal.
-    auto.
-  Qed.
-
-  (* TODO : move to ListUtil *)
-  Lemma nth_error_Some_nth_default : forall {T} i x (l : list T), (i < length l)%nat ->
-    nth_error l i = Some (nth_default x l i).
-  Proof.
-    intros ? ? ? ? i_lt_length.
-    destruct (nth_error_length_exists_value _ _ i_lt_length) as [k nth_err_k].
-    unfold nth_default.
-    rewrite nth_err_k.
-    reflexivity.
-  Qed.
     
   Lemma nth_default_base_succ : forall i, (S i < length base)%nat ->
     nth_default 0 base (S i) = 2 ^ log_cap i * nth_default 0 base i.
@@ -338,7 +295,7 @@ Section CarryProofs.
     rewrite set_nth_sum by omega.
     unfold pow2_mod.
     rewrite Z.land_ones by apply log_cap_nonneg.
-    rewrite shiftr_div by apply log_cap_nonneg.
+    rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg.
     rewrite nth_default_base_succ by omega.
     rewrite Z.mul_assoc.
     rewrite (Z.mul_comm _ (2 ^ log_cap i)).
diff --git a/src/Util/CaseUtil.v b/src/Util/CaseUtil.v
index af04a1e49..cf3ebf29c 100644
--- a/src/Util/CaseUtil.v
+++ b/src/Util/CaseUtil.v
@@ -10,3 +10,9 @@ Ltac case_max :=
           (exact (le_Sn_le _ _ (not_le _ _ H)))
       end
   end.
+
+Lemma pull_app_if_sumbool {A B X Y} (b : sumbool X Y) (f g : A -> B) (x : A)
+  : (if b then f x else g x) = (if b then f else g) x.
+Proof.
+  destruct b; reflexivity.
+Qed.
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index d65c65723..0e061d5e5 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -439,6 +439,16 @@ Proof.
   boring.
 Qed.
 
+Lemma nth_error_Some_nth_default : forall {T} i x (l : list T), (i < length l)%nat ->
+  nth_error l i = Some (nth_default x l i).
+Proof.
+  intros ? ? ? ? i_lt_length.
+  destruct (nth_error_length_exists_value _ _ i_lt_length) as [k nth_err_k].
+  unfold nth_default.
+  rewrite nth_err_k.
+  reflexivity.
+Qed.
+
 Lemma set_nth_cons : forall {T} (x u0 : T) us, set_nth 0 x (u0 :: us) = x :: us.
 Proof.
   auto.
@@ -539,3 +549,10 @@ Lemma cons_eq_tail : forall {T} (x y:T) xs ys, x::xs = y::ys -> xs=ys.
 Proof.
   intros; solve_by_inversion.
 Qed.
+
+Lemma map_nth_default_always {A B} (f : A -> B) (n : nat) (x : A) (l : list A)
+  : nth_default (f x) (map f l) n = f (nth_default x l n).
+Proof.
+  revert n; induction l; simpl; intro n; destruct n; [ try reflexivity.. ].
+  nth_tac.
+Qed.
diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index 6a62d6c22..1f69b04d2 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -56,3 +56,14 @@ Proof.
     rewrite <- nat_compare_lt; auto.
   }
 Qed.
+
+
+
+Lemma beq_nat_eq_nat_dec {R} (x y : nat) (a b : R)
+  : (if EqNat.beq_nat x y then a else b) = (if eq_nat_dec x y then a else b).
+Proof.
+  destruct (eq_nat_dec x y) as [H|H];
+    [ rewrite (proj2 (@beq_nat_true_iff _ _) H); reflexivity
+    | rewrite (proj2 (@beq_nat_false_iff _ _) H); reflexivity ].
+Qed.
+
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index d919c8c8b..9f7b1d645 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1,6 +1,7 @@
 Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv.
 Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
 Require Import Crypto.Util.NatUtil.
+Require Import Coq.Lists.List.
 Local Open Scope Z.
 
 Lemma gt_lt_symmetry: forall n m, n > m <-> m < n.
@@ -190,8 +191,6 @@ Proof.
   auto using Z.mod_pow2_bits_low.
 Qed.
 
-SearchAbout Z.testbit.
-
 Lemma Z_mod_div_eq0 : forall a b, 0 < b -> (a mod b) / b = 0.
 Proof.
   intros.
@@ -227,14 +226,12 @@ Proof.
     (rewrite (le_plus_minus m n) at 2; try assumption;
      rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg; ring).
   rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat m)); omega).
-  SearchAbout ((_ mod _) mod _).
   symmetry. apply Znumtheory.Zmod_div_mod; try (apply Z.pow_pos_nonneg; omega).
   rewrite (le_plus_minus m n) by assumption.
   rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg.
   apply Z.divide_factor_l.
 Qed.
 
-
 Lemma Z_pow_gt0 : forall a, 0 < a -> forall b, 0 <= b -> 0 < a ^ b.
 Proof.
   intros until 1.
@@ -244,6 +241,45 @@ Proof.
   apply Z.mul_pos_pos; assumption.
 Qed.
 
+Lemma div_pow2succ : forall n x, (0 <= x) ->
+  n / 2 ^ Z.succ x = Z.div2 (n / 2 ^ x).
+Proof.
+  intros.
+  rewrite Z.pow_succ_r, Z.mul_comm by auto.
+  rewrite <- Z.div_div by (try apply Z.pow_nonzero; omega).
+  rewrite Zdiv2_div.
+  reflexivity.
+Qed.
+
+Lemma shiftr_succ : forall n x,
+  Z.shiftr n (Z.succ x) = Z.shiftr (Z.shiftr n x) 1.
+Proof.
+  intros.
+  rewrite Z.shiftr_shiftr by omega.
+  reflexivity.
+Qed.
+
+
+Definition Z_shiftl_by n a := Z.shiftl a n.
+
+Lemma Z_shiftl_by_mul_pow2 : forall n a, 0 <= n -> Z.mul (2 ^ n) a = Z_shiftl_by n a.
+Proof.
+  intros.
+  unfold Z_shiftl_by.
+  rewrite Z.shiftl_mul_pow2 by assumption.
+  apply Z.mul_comm.
+Qed.
+
+Lemma map_shiftl : forall n l, 0 <= n -> map (Z.mul (2 ^ n)) l = map (Z_shiftl_by n) l.
+Proof.
+  intros; induction l; auto using Z_shiftl_by_mul_pow2.
+  simpl.
+  rewrite IHl.
+  f_equal.
+  apply Z_shiftl_by_mul_pow2.
+  assumption.
+Qed.
+
 (* prove that known nonnegative numbers are nonnegative *)
 Ltac zero_bounds' :=
   repeat match goal with