diff options
author | Jade Philipoom <jadep@mit.edu> | 2015-11-24 21:55:03 -0500 |
---|---|---|
committer | Jade Philipoom <jadep@mit.edu> | 2015-11-24 21:55:03 -0500 |
commit | d3b5a7218726aa5d21b634aabac0e915bdfe1624 (patch) | |
tree | 6cc66856ad2382e9148f3f5ae2404729adf7b49e /src/Galois | |
parent | e400e146f02bb65f198bc606fe4c3fa24e6804d5 (diff) |
reorganized lemmas; moved several to ListUtil and ZUtil.
Diffstat (limited to 'src/Galois')
-rw-r--r-- | src/Galois/BaseSystem.v | 65 | ||||
-rw-r--r-- | src/Galois/ModularBaseSystem.v | 86 |
2 files changed, 23 insertions, 128 deletions
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, |