From 64d7f47edd9148c3d4d78489d3bfaf1dd35423dc Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 19 Jul 2016 15:55:10 -0700 Subject: Remove stuff from PseudoMersenneBaseParamProofs.v --- src/ModularArithmetic/ExtendedBaseVector.v | 10 +-- src/ModularArithmetic/ModularBaseSystemProofs.v | 19 ++++-- src/ModularArithmetic/Pow2BaseProofs.v | 79 +++++++++++++++++++--- .../PseudoMersenneBaseParamProofs.v | 68 +------------------ 4 files changed, 92 insertions(+), 84 deletions(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v index e2fcab9a0..1c9555fe6 100644 --- a/src/ModularArithmetic/ExtendedBaseVector.v +++ b/src/ModularArithmetic/ExtendedBaseVector.v @@ -63,7 +63,7 @@ Section ExtendedBaseVector. apply (Zmult_gt_compat_l b' 0 (2 ^ k)); [| apply base_pos; intuition]. rewrite Z.gt_lt_iff. apply Z.pow_pos_nonneg; intuition. - pose proof k_nonneg; omega. + apply sum_firstn_limb_widths_nonneg; auto using limb_widths_nonneg. Qed. Lemma base_length_nonzero : (0 < length base)%nat. @@ -105,10 +105,10 @@ Section ExtendedBaseVector. Proof. intros. remember (nth_default 0 base) as b. - rewrite Zdiv_mult_cancel_l by (exact two_k_nonzero). + rewrite Zdiv_mult_cancel_l by apply two_sum_firstn_limb_widths_nonzero, limb_widths_nonneg. replace (b i * b j' / b (i + j')%nat * (2 ^ k * b (i + j')%nat)) with ((2 ^ k * (b (i + j')%nat * (b i * b j' / b (i + j')%nat)))) by ring. - rewrite Z.mul_cancel_l by (exact two_k_nonzero). + rewrite Z.mul_cancel_l by apply two_sum_firstn_limb_widths_nonzero, limb_widths_nonneg. replace (b (i + j')%nat * (b i * b j' / b (i + j')%nat)) with ((b i * b j' / b (i + j')%nat) * b (i + j')%nat) by ring. subst b. @@ -131,7 +131,9 @@ Section ExtendedBaseVector. auto using BaseSystem.base_good. } { (* i < length base, j < length base, i + j >= length base *) rewrite (map_nth_default _ _ _ _ 0) by omega. - apply (base_matches_modulus i j); rewrite <-base_length by auto using limb_widths_nonneg; omega. + autorewrite with distr_length in * |- . + apply base_matches_modulus; auto using limb_widths_nonneg, limb_widths_match_modulus. + omega. } { (* i < length base, j >= length base, i + j >= length base *) do 2 rewrite map_nth_default_base_high by omega. remember (j - length base)%nat as j'. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 5d1becc00..c3b1b76b4 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -57,6 +57,15 @@ Section PseudoMersenneProofs. pose proof (NumTheoryUtil.lt_1_p _ prime_modulus); omega. Qed. Hint Resolve modulus_pos. + (** TODO(jadep, from jgross): The abstraction barrier of + [base]/[limb_widths] is repeatedly broken in the following + proofs. This lemma should almost never be needed, but removing + it breaks everything. (And using [distr_length] is too much of + a sledgehammer, and demolishes the abstraction barrier that's + currently merely in pieces.) *) + Lemma base_length : length base = length limb_widths. + Proof. distr_length. Qed. + Lemma encode'_eq : forall (x : F modulus) i, (i <= length limb_widths)%nat -> encode' limb_widths x i = BaseSystem.encode' base x (2 ^ k) i. Proof. @@ -99,7 +108,7 @@ Section PseudoMersenneProofs. match goal with H : (_ <= length base)%nat |- _ => apply le_lt_or_eq in H; destruct H end. - apply Z.mod_divide. - * apply nth_default_base_nonzero; auto using bv, two_k_nonzero. + * apply nth_default_base_nonzero, two_sum_firstn_limb_widths_nonzero; auto using bv. * rewrite !nth_default_eq. do 2 (erewrite nth_indep with (d := 2 ^ k) (d' := 0) by omega). rewrite <-!nth_default_eq. @@ -150,7 +159,7 @@ Section PseudoMersenneProofs. (BaseSystem.decode base us) * (BaseSystem.decode base vs) = BaseSystem.decode ext_base (BaseSystem.mul ext_base us vs). Proof. intros; apply mul_rep_two_base; auto; - autorewrite with distr_length; try omega. + distr_length. Qed. Lemma modulus_nonzero : modulus <> 0. @@ -396,7 +405,7 @@ Section CarryProofs. Proof. pose proof length_carry. pose proof carry_decode_eq_reduce. pose proof (@carry_simple_decode_eq limb_widths). specialize_by eauto. - intros; split; auto. + intros; split; try solve [ distr_length ]. unfold rep, decode, carry in *. intuition; break_if; subst; eauto; apply F_eq; simpl; intuition. Qed. @@ -412,7 +421,7 @@ Section CarryProofs. Lemma carry_sequence_length: forall is us, (length us = length base)%nat -> (length (carry_sequence is us) = length base)%nat. - Proof. intros; autorewrite with distr_length; congruence. Qed. + Proof. intros; distr_length. Qed. Hint Resolve carry_sequence_length. Lemma carry_sequence_rep : forall is us x, @@ -432,7 +441,7 @@ Section CarryProofs. Lemma carry_full_length : forall us, (length us = length base)%nat -> length (carry_full us) = length base. - Proof. intros; autorewrite with distr_length; congruence. Qed. + Proof. intros; distr_length. Qed. Lemma carry_full_preserves_rep : forall us x, rep us x -> rep (carry_full us) x. diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index ca28896dd..d95de5bd1 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -15,22 +15,25 @@ Section Pow2BaseProofs. Lemma base_from_limb_widths_length : length base = length limb_widths. Proof. - induction limb_widths; try reflexivity. - simpl; rewrite map_length. - simpl in limb_widths_nonneg. - rewrite IHl; auto. + clear limb_widths_nonneg. + induction limb_widths; [ reflexivity | simpl in * ]. + autorewrite with distr_length; auto. Qed. + Hint Rewrite base_from_limb_widths_length : distr_length. Lemma sum_firstn_limb_widths_nonneg : forall n, 0 <= sum_firstn limb_widths n. Proof. unfold sum_firstn; intros. apply fold_right_invariant; try omega. - intros y In_y_lw ? ?. - apply Z.add_nonneg_nonneg; try assumption. - apply limb_widths_nonneg. - eapply In_firstn; eauto. + eauto using Z.add_nonneg_nonneg, limb_widths_nonneg, In_firstn. Qed. Hint Resolve sum_firstn_limb_widths_nonneg. + Lemma two_sum_firstn_limb_widths_pos n : 0 < 2^sum_firstn limb_widths n. + Proof. auto with zarith. Qed. + + Lemma two_sum_firstn_limb_widths_nonzero n : 2^sum_firstn limb_widths n <> 0. + Proof. pose proof (two_sum_firstn_limb_widths_pos n); omega. Qed. + Lemma base_from_limb_widths_step : forall i b w, (S i < length base)%nat -> nth_error base i = Some b -> nth_error limb_widths i = Some w -> @@ -162,6 +165,63 @@ Section Pow2BaseProofs. do 2 f_equal; apply map_ext; intros; lia. } Qed. + Section make_base_vector. + Local Notation k := (sum_firstn limb_widths (length limb_widths)). + Context (limb_widths_match_modulus : forall i j, + (i < length limb_widths)%nat -> + (j < length limb_widths)%nat -> + (i + j >= length limb_widths)%nat -> + let w_sum := sum_firstn limb_widths in + k + w_sum (i + j - length limb_widths)%nat <= w_sum i + w_sum j) + (limb_widths_good : forall i j, (i + j < length limb_widths)%nat -> + sum_firstn limb_widths (i + j) <= + sum_firstn limb_widths i + sum_firstn limb_widths j). + + Lemma base_matches_modulus: forall i j, + (i < length limb_widths)%nat -> + (j < length limb_widths)%nat -> + (i+j >= length limb_widths)%nat-> + let b := nth_default 0 base in + let r := (b i * b j) / (2^k * b (i+j-length base)%nat) in + b i * b j = r * (2^k * b (i+j-length base)%nat). + Proof. + intros. + rewrite (Z.mul_comm r). + subst r. + assert (i + j - length limb_widths < length limb_widths)%nat by omega. + rewrite Z.mul_div_eq by (apply Z.gt_lt_iff; apply Z.mul_pos_pos; + subst b; rewrite ?nth_default_base; zero_bounds; rewrite ?base_from_limb_widths_length; + auto using sum_firstn_limb_widths_nonneg, limb_widths_nonneg). + rewrite (Zminus_0_l_reverse (b i * b j)) at 1. + f_equal. + subst b. + repeat rewrite nth_default_base by (rewrite ?base_from_limb_widths_length; auto). + do 2 rewrite <- Z.pow_add_r by auto using sum_firstn_limb_widths_nonneg. + symmetry. + apply Z.mod_same_pow. + split. + + apply Z.add_nonneg_nonneg; auto using sum_firstn_limb_widths_nonneg. + + rewrite base_from_limb_widths_length; auto using limb_widths_nonneg, limb_widths_match_modulus. + Qed. + + Lemma base_good : forall i j : nat, + (i + j < length base)%nat -> + let b := nth_default 0 base in + let r := b i * b j / b (i + j)%nat in + b i * b j = r * b (i + j)%nat. + Proof. + intros; subst b r. + repeat rewrite nth_default_base by (omega || auto). + rewrite (Z.mul_comm _ (2 ^ (sum_firstn limb_widths (i+j)))). + rewrite Z.mul_div_eq by (apply Z.gt_lt_iff; zero_bounds; + auto using sum_firstn_limb_widths_nonneg). + rewrite <- Z.pow_add_r by auto using sum_firstn_limb_widths_nonneg. + rewrite Z.mod_same_pow; try ring. + split; [ auto using sum_firstn_limb_widths_nonneg | ]. + apply limb_widths_good. + rewrite <-base_from_limb_widths_length; auto using limb_widths_nonneg. + Qed. + End make_base_vector. End Pow2BaseProofs. Section BitwiseDecodeEncode. @@ -788,8 +848,7 @@ Section carrying. Hint Rewrite @nth_default_carry_simple using (omega || distr_length; omega) : push_nth_default. End carrying. -Hint Rewrite @length_carry_gen : distr_length. +Hint Rewrite @length_carry_gen @base_from_limb_widths_length : distr_length. Hint Rewrite @length_carry_simple @length_carry_simple_sequence @length_make_chain @length_full_carry_chain @length_carry_simple_full : distr_length. Hint Rewrite @nth_default_carry_simple_full @nth_default_carry_gen_full : push_nth_default. Hint Rewrite @nth_default_carry_simple @nth_default_carry_gen using (omega || distr_length; omega) : push_nth_default. -Hint Rewrite @base_from_limb_widths_length using auto with nocore distr_length : distr_length. diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v index 1cb87910d..14482fe5e 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v @@ -14,77 +14,15 @@ Section PseudoMersenneBaseParamProofs. Local Notation base := (base_from_limb_widths limb_widths). Lemma limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w. - Proof. - intros. - apply Z.lt_le_incl. - auto using limb_widths_pos. - Qed. Hint Resolve limb_widths_nonneg. + Proof. auto using Z.lt_le_incl, limb_widths_pos. Qed. Lemma k_nonneg : 0 <= k. - Proof. - apply sum_firstn_limb_widths_nonneg; auto. - Qed. Hint Resolve k_nonneg. - - Lemma two_k_nonzero : 2^k <> 0. - Proof. - pose proof (Z.pow_eq_0 2 k k_nonneg). - intuition. - Qed. - - Lemma base_matches_modulus: forall i j, - (i < length limb_widths)%nat -> - (j < length limb_widths)%nat -> - (i+j >= length limb_widths)%nat-> - let b := nth_default 0 base in - let r := (b i * b j) / (2^k * b (i+j-length base)%nat) in - b i * b j = r * (2^k * b (i+j-length base)%nat). - Proof. - intros. - rewrite (Z.mul_comm r). - subst r. - assert (i + j - length limb_widths < length limb_widths)%nat by omega. - rewrite Z.mul_div_eq by (apply Z.gt_lt_iff; apply Z.mul_pos_pos; - subst b; rewrite ?nth_default_base; zero_bounds; rewrite ?base_from_limb_widths_length; - auto using sum_firstn_limb_widths_nonneg, limb_widths_nonneg). - rewrite (Zminus_0_l_reverse (b i * b j)) at 1. - f_equal. - subst b. - repeat rewrite nth_default_base by (rewrite ?base_from_limb_widths_length; auto). - do 2 rewrite <- Z.pow_add_r by auto using sum_firstn_limb_widths_nonneg. - symmetry. - apply Z.mod_same_pow. - split. - + apply Z.add_nonneg_nonneg; auto using sum_firstn_limb_widths_nonneg. - + rewrite base_from_limb_widths_length; auto using limb_widths_nonneg, limb_widths_match_modulus. - Qed. - - Lemma base_good : forall i j : nat, - (i + j < length base)%nat -> - let b := nth_default 0 base in - let r := b i * b j / b (i + j)%nat in - b i * b j = r * b (i + j)%nat. - Proof. - intros; subst b r. - repeat rewrite nth_default_base by (omega || auto). - rewrite (Z.mul_comm _ (2 ^ (sum_firstn limb_widths (i+j)))). - rewrite Z.mul_div_eq by (apply Z.gt_lt_iff; zero_bounds; - auto using sum_firstn_limb_widths_nonneg). - rewrite <- Z.pow_add_r by auto using sum_firstn_limb_widths_nonneg. - rewrite Z.mod_same_pow; try ring. - split; [ auto using sum_firstn_limb_widths_nonneg | ]. - apply limb_widths_good. - rewrite <-base_from_limb_widths_length; auto using limb_widths_nonneg. - Qed. - - Lemma base_length : length base = length limb_widths. - Proof. - auto using base_from_limb_widths_length. - Qed. + Proof. apply sum_firstn_limb_widths_nonneg, limb_widths_nonneg. Qed. Global Instance bv : BaseSystem.BaseVector base := { base_positive := base_positive limb_widths_nonneg; b0_1 := fun x => b0_1 x limb_widths_nonnil; - base_good := base_good + base_good := base_good limb_widths_nonneg limb_widths_good }. End PseudoMersenneBaseParamProofs. -- cgit v1.2.3