reorganized lemmas; moved several to ListUtil and ZUtil.

5 files changed, 126 insertions, 128 deletions

diff --git a/_CoqProject b/_CoqProject
index d92e7e640..8ab455d7b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,6 +4,7 @@
 src/Tactics/VerdiTactics.v
 src/Util/CaseUtil.v
 src/Util/ListUtil.v
+src/Util/ZUtil.v
 src/Galois/Galois.v
 src/Galois/GaloisTheory.v
 src/Galois/ZGaloisField.v
diff --git a/src/Galois/BaseSystem.v b/src/Galois/BaseSystem.v
index ead4f9d78..8197bed8d 100644
--- a/src/Galois/BaseSystem.v
+++ b/src/Galois/BaseSystem.v
@@ -1,17 +1,10 @@
 Require Import List.
-Require Import Util.ListUtil Util.CaseUtil.
+Require Import Util.ListUtil Util.CaseUtil Util.ZUtil.
 Require Import ZArith.ZArith ZArith.Zdiv.
 Require Import Omega NPeano Arith.
 
 Local Open Scope Z.
 
-Lemma pos_pow_nat_pos : forall x n, 
-  Z.pos x ^ Z.of_nat n > 0.
-  do 2 (intros; induction n; subst; simpl in *; auto with zarith).
-  rewrite <- Pos.add_1_r, Zpower_pos_is_exp.
-  apply Zmult_gt_0_compat; auto; reflexivity.
-Qed.
-
 Module Type BaseCoefs.
   (** [BaseCoefs] represent the weights of each digit in a positional number system, with the weight of least significant digit presented first. The following requirements on the base are preconditions for using it with BaseSystem. *)
   Parameter base : list Z.
@@ -82,6 +75,12 @@ Module BaseSystem (Import B:BaseCoefs).
     unfold decode'; induction bs; destruct vs; boring.
   Qed.
 
+  Lemma base_eq_1cons: base = 1 :: skipn 1 base.
+  Proof.
+    pose proof (b0_1 0) as H.
+    destruct base; compute in H; try discriminate; boring.
+  Qed.
+
   Lemma decode'_cons : forall x1 x2 xs1 xs2,
     decode' (x1 :: xs1) (x2 :: xs2) = x1 * x2 + decode' xs1 xs2.
   Proof.
@@ -89,6 +88,14 @@ Module BaseSystem (Import B:BaseCoefs).
   Qed.
   Hint Rewrite decode'_cons.
 
+  Lemma decode_cons : forall x us,
+    decode (x :: us) = x + decode (0 :: us).
+  Proof.
+    unfold decode; intros.
+    rewrite base_eq_1cons.
+    autorewrite with core; ring_simplify; auto.
+  Qed.
+
   Fixpoint sub (us vs:digits) : digits :=
     match us,vs with
       | u::us', v::vs' => u-v :: sub us' vs'
@@ -101,12 +108,6 @@ Module BaseSystem (Import B:BaseCoefs).
     induction bs; destruct us; destruct vs; boring.
   Qed.
 
-  Lemma base_eq_1cons: base = 1 :: skipn 1 base.
-  Proof.
-    pose proof (b0_1 0) as H.
-    destruct base; compute in H; try discriminate; boring.
-  Qed.
-
   Lemma encode_rep : forall z, decode (encode z) = z.
   Proof.
     pose proof base_eq_1cons.
@@ -119,6 +120,7 @@ Module BaseSystem (Import B:BaseCoefs).
     induction us; destruct bs; boring.
   Qed.
 
+  Hint Rewrite (@nth_default_nil Z).
   Hint Rewrite (@firstn_nil Z).
   Hint Rewrite (@skipn_nil Z).
 
@@ -205,14 +207,6 @@ Module BaseSystem (Import B:BaseCoefs).
   Qed.
   Hint Rewrite mul_bi'_zeros.
 
-  Lemma Z_div_mul' : forall a b : Z, b <> 0 -> (b * a) / b = a.
-    intros. rewrite Z.mul_comm. apply Z.div_mul; auto.
-  Qed.
-
-  Lemma Zgt0_neq0 : forall x, x > 0 -> x <> 0.
-    boring.
-  Qed.
-
   Lemma nth_error_base_nonzero : forall n x,
     nth_error base n = Some x -> x <> 0.
   Proof.
@@ -297,11 +291,6 @@ Module BaseSystem (Import B:BaseCoefs).
     unfold mul_bi'; auto.
   Qed.
 
-  Lemma cons_length : forall A (xs : list A) a, length (a :: xs) = S (length xs).
-  Proof.
-    auto.
-  Qed.
-
   Lemma add_same_length : forall us vs l, (length us = l) -> (length vs = l) ->
     length (us .+ vs) = l.
   Proof.
@@ -309,11 +298,6 @@ Module BaseSystem (Import B:BaseCoefs).
     erewrite (IHus vs (pred l)); boring.
   Qed.
 
-  Lemma length0_nil : forall {A} (xs : list A), length xs = 0%nat -> xs = nil.
-  Proof.
-    induction xs; boring; discriminate.
-  Qed.
-
   Hint Rewrite app_nil_l.
   Hint Rewrite app_nil_r.
 
@@ -324,12 +308,6 @@ Module BaseSystem (Import B:BaseCoefs).
     induction l, us, vs; boring; discriminate.
   Qed.
 
-  Lemma length_snoc : forall {T} xs (x:T),
-    length xs = pred (length (xs++x::nil)).
-  Proof.
-    boring; simpl_list; boring.
-  Qed.
-
   Lemma mul_bi'_add : forall us n vs l
     (Hlus: length us = l)
     (Hlvs: length vs = l),
@@ -422,17 +400,6 @@ Module BaseSystem (Import B:BaseCoefs).
     erewrite add_same_length by (pose proof app_length; boring); omega.
   Qed.
 
-  Ltac case_max :=
-    match goal with [ |- context[max ?x ?y] ] =>
-        destruct (le_dec x y);
-        match goal with
-          | [ H : (?x <= ?y)%nat |- context[max ?x ?y] ] => rewrite Max.max_r by
-            (exact H)
-          | [ H : ~ (?x <= ?y)%nat   |- context[max ?x ?y] ] => rewrite Max.max_l by
-            (exact (le_Sn_le _ _ (not_le _ _ H)))
-        end
-    end.
-
   Lemma add_length_le_max : forall us vs,
       (length (us .+ vs) <= max (length us) (length vs))%nat.
   Proof.
diff --git a/src/Galois/ModularBaseSystem.v b/src/Galois/ModularBaseSystem.v
index 0f6fdefba..c5eaffd94 100644
--- a/src/Galois/ModularBaseSystem.v
+++ b/src/Galois/ModularBaseSystem.v
@@ -1,9 +1,9 @@
 Require Import Zpower ZArith.
 Require Import List.
 Require Import Crypto.Galois.BaseSystem Crypto.Galois.GaloisTheory.
-Require Import Util.ListUtil.
+Require Import Util.ListUtil Util.CaseUtil Util.ZUtil.
 Require Import VerdiTactics.
-Open Scope Z_scope.
+Local Open Scope Z_scope.
 
 Module Type PseudoMersenneBaseParams (Import B:BaseCoefs) (Import M:Modulus).
   (* TODO: do we actually want B and M "up there" in the type parameters? I was
@@ -243,7 +243,7 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara
     autounfold; intuition. {
       unfold add.
       rewrite B.add_length_le_max.
-      B.case_max; try rewrite Max.max_r; omega.
+      case_max; try rewrite Max.max_r; omega.
     }
     unfold toGF in *; unfold B.decode in *.
     rewrite B.add_rep.
@@ -310,12 +310,9 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara
     apply Znumtheory.not_prime_0; auto.
   Qed.
 
-  Lemma mod_mult_plus: forall a b c, (b <> 0) -> (a * b + c) mod b = c mod b.
-  Proof.
-    intros.
-    rewrite Zplus_mod.
-    rewrite Z.mod_mul; auto; simpl.
-    rewrite Zmod_mod; auto.
+  Lemma two_k_nonzero : 2^P.k <> 0.
+    pose proof (Z.pow_eq_0 2 P.k P.k_nonneg).
+    intuition.
   Qed.
 
   (* a = r + s(2^k) = r + s(2^k - c + c) = r + s(2^k - c) + cs = r + cs *) 
@@ -427,30 +424,6 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara
     then add_to_nth   0   (P.c * (di / cap i)) us'
     else add_to_nth (S i) (      (di / cap i)) us'.
 
-  Lemma set_nth_nil : forall {T} n (x : T), set_nth n x nil = nil.
-  Proof.
-    induction n; boring.
-  Qed.
-
-  Lemma nth_default_nil : forall {T} n (d : T), nth_default d nil n = d.
-  Proof.
-    induction n; boring.
-  Qed.
-
-  Lemma B_decode_cons : forall x us,
-    B.decode (x :: us) = x + B.decode (0 :: us).
-  Proof.
-    unfold B.decode; intros.
-    rewrite B.base_eq_1cons.
-    do 2 rewrite B.decode'_cons; ring_simplify; auto.
-  Qed.
-
-  Lemma cons_set_nth : forall {T} n (x y : T) us,
-    y :: set_nth n x us = set_nth (S n) x (y :: us).
-  Proof.
-    induction n; boring.
-  Qed.
-
   Lemma decode'_splice : forall xs ys bs,
     B.decode' bs (xs ++ ys) = 
     B.decode' (firstn (length xs) bs) xs + 
@@ -462,24 +435,6 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara
     ring.
   Qed.
 
- Lemma skipn_nth_default : forall {T} n us (d : T), (n < length us)%nat ->
-   skipn n us = nth_default d us n :: skipn (S n) us.
- Proof.
-    induction n; destruct us; intros; nth_tac.
-    rewrite (IHn us d) at 1 by omega.
-    nth_tac.
-  Qed.
-
-  Lemma nth_default_out_of_bounds : forall {T} n us (d : T), (n >= length us)%nat ->
-    nth_default d us n = d.
-  Proof.
-    induction n; unfold nth_default; nth_tac; destruct us; nth_tac.
-    assert (n >= length us)%nat by omega.
-    pose proof (nth_error_length_error _ n us H1).
-    rewrite H0 in H2.
-    congruence.
-  Qed.
-
   Lemma set_nth_sum : forall n x us, (n < length us)%nat ->
     B.decode (set_nth n x us) = 
     (x - nth_default 0 us n) * nth_default 0 BC.base n + B.decode us.
@@ -527,11 +482,6 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara
     rewrite H0; auto.
   Qed.
 
-  Lemma gt_lt_symmetry: forall n m, n > m <-> m < n.
-  Proof.
-    intros; split; omega.
-  Qed.
-
   Lemma base_succ_div_mult : forall i, ((S i) < length BC.base)%nat ->
     nth_default 0 BC.base (S i) = nth_default 0 BC.base i *
     (nth_default 0 BC.base (S i) / nth_default 0 BC.base i).
@@ -541,22 +491,6 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara
     apply P.base_succ; auto.
   Qed.
 
-  Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0.
-  Proof.
-    intros; omega.
-  Qed.
-  Hint Resolve positive_is_nonzero.
-
-  Lemma div_positive_gt_0 : forall a b, a > 0 -> b > 0 -> a mod b = 0 ->
-    a / b > 0.
-  Proof.
-    intros.
-    rewrite gt_lt_symmetry.
-    apply Z.div_str_pos.
-    split; intuition.
-    apply Z.divide_pos_le; try (apply Znumtheory.Zmod_divide); omega.
-  Qed.
-
   Lemma base_length_lt_pred : (pred (length BC.base) < length BC.base)%nat.
   Proof.
     pose proof EC.base_length_nonzero; omega.
@@ -626,11 +560,6 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara
     subst i; rewrite <- two_k_div_mul_last; auto.
   Qed.
 
-  Lemma elim_mod : forall a b, a = b -> a mod modulus = b mod modulus.
-  Proof.
-    intros; subst; auto.
-  Qed.
-
   Lemma carry_decode_eq_reduce : forall us,
     (length us = length BC.base) ->
     B.decode (carry (pred (length BC.base)) us) mod modulus
@@ -645,8 +574,7 @@ Module GFPseudoMersenneBase (BC:BaseCoefs) (M:Modulus) (P:PseudoMersenneBasePara
     rewrite BC.b0_1.
     rewrite (Z.mul_comm (2 ^ P.k)).
     rewrite <- Zred_factor0.
-    rewrite <- cap_div_mod_reduce by auto.
-    apply elim_mod; ring_simplify; auto.
+    rewrite <- cap_div_mod_reduce by auto; auto.
   Qed.
 
   Lemma carry_length : forall i us,
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index ba1d8326a..350f55dd8 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -360,6 +360,22 @@ Proof.
   destruct a; omega.
 Qed.
 
+Lemma cons_length : forall A (xs : list A) a, length (a :: xs) = S (length xs).
+Proof.
+  auto.
+Qed.
+
+Lemma length0_nil : forall {A} (xs : list A), length xs = 0%nat -> xs = nil.
+Proof.
+  induction xs; boring; discriminate.
+Qed.
+
+Lemma length_snoc : forall {T} xs (x:T),
+  length xs = pred (length (xs++x::nil)).
+Proof.
+  boring; simpl_list; boring.
+Qed.
+
 Lemma firstn_combine : forall {A B} n (xs:list A) (ys:list B),
   firstn n (combine xs ys) = combine (firstn n xs) (firstn n ys).
 Proof.
@@ -442,6 +458,40 @@ Hint Rewrite
 Ltac distr_length := autorewrite with distr_length in *;
   try solve [simpl in *; omega].
 
+Lemma cons_set_nth : forall {T} n (x y : T) us,
+  y :: set_nth n x us = set_nth (S n) x (y :: us).
+Proof.
+  induction n; boring.
+Qed.
+
+Lemma set_nth_nil : forall {T} n (x : T), set_nth n x nil = nil.
+Proof.
+  induction n; boring.
+Qed.
+
+Lemma nth_default_nil : forall {T} n (d : T), nth_default d nil n = d.
+Proof.
+  induction n; boring.
+Qed.
+
+Lemma skipn_nth_default : forall {T} n us (d : T), (n < length us)%nat ->
+ skipn n us = nth_default d us n :: skipn (S n) us.
+Proof.
+  induction n; destruct us; intros; nth_tac.
+  rewrite (IHn us d) at 1 by omega.
+  nth_tac.
+Qed.
+
+Lemma nth_default_out_of_bounds : forall {T} n us (d : T), (n >= length us)%nat ->
+  nth_default d us n = d.
+Proof.
+  induction n; unfold nth_default; nth_tac; destruct us; nth_tac.
+  assert (n >= length us)%nat by omega.
+  pose proof (nth_error_length_error _ n us H1).
+  rewrite H0 in H2.
+  congruence.
+Qed.
+
 Ltac nth_error_inbounds :=
   match goal with
   | [ |- context[match nth_error ?xs ?i with Some _ => _ | None => _ end ] ] =>
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
new file mode 100644
index 000000000..5950f57ad
--- /dev/null
+++ b/src/Util/ZUtil.v
@@ -0,0 +1,52 @@
+Require Import Zpower Znumtheory ZArith.ZArith ZArith.Zdiv.
+Require Import Omega NPeano Arith.
+Local Open Scope Z.
+
+Lemma gt_lt_symmetry: forall n m, n > m <-> m < n.
+Proof.
+  intros; split; omega.
+Qed.
+
+Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0.
+Proof.
+  intros; omega.
+Qed.
+Hint Resolve positive_is_nonzero.
+
+Lemma div_positive_gt_0 : forall a b, a > 0 -> b > 0 -> a mod b = 0 ->
+  a / b > 0.
+Proof.
+  intros; rewrite gt_lt_symmetry.
+  apply Z.div_str_pos.
+  split; intuition.
+  apply Z.divide_pos_le; try (apply Zmod_divide); omega.
+Qed.
+
+Lemma elim_mod : forall a b m, a = b -> a mod m = b mod m.
+Proof.
+  intros; subst; auto.
+Qed.
+Hint Resolve elim_mod.
+
+Lemma mod_mult_plus: forall a b c, (b <> 0) -> (a * b + c) mod b = c mod b.
+Proof.
+  intros.
+  rewrite Zplus_mod.
+  rewrite Z.mod_mul; auto; simpl.
+  rewrite Zmod_mod; auto.
+Qed.
+
+Lemma pos_pow_nat_pos : forall x n, 
+  Z.pos x ^ Z.of_nat n > 0.
+  do 2 (intros; induction n; subst; simpl in *; auto with zarith).
+  rewrite <- Pos.add_1_r, Zpower_pos_is_exp.
+  apply Zmult_gt_0_compat; auto; reflexivity.
+Qed.
+
+Lemma Z_div_mul' : forall a b : Z, b <> 0 -> (b * a) / b = a.
+  intros. rewrite Z.mul_comm. apply Z.div_mul; auto.
+Qed.
+
+Lemma Zgt0_neq0 : forall x, x > 0 -> x <> 0.
+  intuition.
+Qed.