From 49a861f1329749f89a01c2d6a7ad90df151f7178 Mon Sep 17 00:00:00 2001 From: jadep Date: Thu, 21 Jul 2016 17:38:27 -0400 Subject: Changed name of [carry_and_reduce_single] to [carry_single], since it does not perform reduction --- src/ModularArithmetic/ModularBaseSystemOpt.v | 2 +- src/ModularArithmetic/Pow2Base.v | 4 ++-- src/ModularArithmetic/Pow2BaseProofs.v | 8 ++++---- 3 files changed, 7 insertions(+), 7 deletions(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index ed8f80659..33b2d7f2d 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -124,7 +124,7 @@ Section Carries. rewrite <-from_list_default_eq with (d := 0%Z). rewrite <-pull_app_if_sumbool. cbv beta delta - [carry carry_and_reduce Pow2Base.carry_gen Pow2Base.carry_and_reduce_single Pow2Base.carry_simple + [carry carry_and_reduce Pow2Base.carry_gen Pow2Base.carry_single Pow2Base.carry_simple Z.pow2_mod Z.ones Z.pred PseudoMersenneBaseParams.limb_widths]. rewrite !add_to_nth_set_nth. diff --git a/src/ModularArithmetic/Pow2Base.v b/src/ModularArithmetic/Pow2Base.v index c23cf8f40..a2c76016d 100644 --- a/src/ModularArithmetic/Pow2Base.v +++ b/src/ModularArithmetic/Pow2Base.v @@ -49,14 +49,14 @@ Section Pow2Base. Definition add_to_nth n (x:Z) xs := update_nth n (fun y => x + y) xs. - Definition carry_and_reduce_single i := fun di => + Definition carry_single i := fun di => (Z.pow2_mod di (log_cap i), Z.shiftr di (log_cap i)). Definition carry_gen fc fi i := fun us => let i := fi (length us) i in let di := nth_default 0 us i in - let '(di', ci) := carry_and_reduce_single i di in + let '(di', ci) := carry_single i di in let us' := set_nth i di' us in add_to_nth (fi (length us) (S i)) (fc ci) us'. diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 78c6bba0f..9255f033f 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -688,7 +688,7 @@ Section carrying. Local Hint Resolve limb_widths_nonneg sum_firstn_limb_widths_nonneg. Lemma length_carry_gen : forall fc fi i us, length (carry_gen limb_widths fc fi i us) = length us. - Proof. intros; unfold carry_gen, carry_and_reduce_single; distr_length; reflexivity. Qed. + Proof. intros; unfold carry_gen, carry_single; distr_length; reflexivity. Qed. Hint Rewrite @length_carry_gen : distr_length. @@ -722,14 +722,14 @@ Section carrying. destruct (eq_nat_dec 0 (length base)); [ destruct limb_widths, us, i; simpl in *; try congruence; break_match; - unfold carry_gen, carry_and_reduce_single, add_to_nth; + unfold carry_gen, carry_single, add_to_nth; autorewrite with zsimplify simpl_nth_default simpl_set_nth simpl_update_nth distr_length; reflexivity | ]. (*assert (0 <= i < length base)%nat by (subst i; auto with arith).*) assert (0 <= log_cap i) by auto using log_cap_nonneg. assert (2 ^ log_cap i <> 0) by (apply Z.pow_nonzero; lia). - unfold carry_gen, carry_and_reduce_single. + unfold carry_gen, carry_single. rewrite H; change (i' mod length base)%nat with i. rewrite add_to_nth_sum by (rewrite length_set_nth; omega). rewrite set_nth_sum by omega. @@ -798,7 +798,7 @@ Section carrying. else 0 else d. Proof. - unfold carry_gen, carry_and_reduce_single. + unfold carry_gen, carry_single. intros; autorewrite with push_nth_default natsimplify distr_length. edestruct (lt_dec n (length us)) as [H|H]; [ | reflexivity ]. rewrite !(@nth_default_in_bounds Z 0 d) by assumption. -- cgit v1.2.3