From cdd44cf2718255b699ce6e77cfd4333a736ee804 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 19 Jul 2016 14:48:15 -0700 Subject: Add another lemma to distr_length --- src/ModularArithmetic/Pow2BaseProofs.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 6a8d4a8ff..45fea0356 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -788,7 +788,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. -- cgit v1.2.3 From 70f3ef2ad457248aeb361c68af25a74169e0e861 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 19 Jul 2016 14:50:50 -0700 Subject: Fix side-condition from previous commit --- src/ModularArithmetic/Pow2BaseProofs.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v index 45fea0356..ca28896dd 100644 --- a/src/ModularArithmetic/Pow2BaseProofs.v +++ b/src/ModularArithmetic/Pow2BaseProofs.v @@ -788,7 +788,8 @@ Section carrying. Hint Rewrite @nth_default_carry_simple using (omega || distr_length; omega) : push_nth_default. End carrying. -Hint Rewrite @length_carry_gen @base_from_limb_widths_length : distr_length. +Hint Rewrite @length_carry_gen : 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. -- cgit v1.2.3 From af5bff992249f84cbb0c0dc38c273b974bf07a41 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 19 Jul 2016 14:55:56 -0700 Subject: Move two_k_nonzero to PseudoMersenneBaseParamProofs.v It has nothing to do with ext_base --- src/ModularArithmetic/ExtendedBaseVector.v | 6 ------ src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | 8 +++++++- 2 files changed, 7 insertions(+), 7 deletions(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v index 0afd6b484..e2fcab9a0 100644 --- a/src/ModularArithmetic/ExtendedBaseVector.v +++ b/src/ModularArithmetic/ExtendedBaseVector.v @@ -83,12 +83,6 @@ Section ExtendedBaseVector. destruct (lt_dec 0 (length base)); try apply BaseSystem.b0_1; try omega. Qed. - Lemma two_k_nonzero : 2^k <> 0. - Proof. - pose proof (Z.pow_eq_0 2 k k_nonneg). - intuition. - Qed. - Lemma map_nth_default_base_high : forall n, (n < (length base))%nat -> nth_default 0 (map (Z.mul (2 ^ k)) base) n = (2 ^ k) * (nth_default 0 base n). diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v index e0a194c3b..07114b1e4 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v @@ -25,6 +25,12 @@ Section PseudoMersenneBaseParamProofs. 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 -> @@ -81,4 +87,4 @@ Section PseudoMersenneBaseParamProofs. base_good := base_good }. -End PseudoMersenneBaseParamProofs. \ No newline at end of file +End PseudoMersenneBaseParamProofs. -- cgit v1.2.3 From ecf3e0f6ae2cf7267956fd5c2fe52a56d043f465 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 19 Jul 2016 15:01:21 -0700 Subject: {base} -> base --- src/ModularArithmetic/PseudoMersenneBaseParamProofs.v | 16 ++++++++-------- src/Testbit.v | 8 ++++---- 2 files changed, 12 insertions(+), 12 deletions(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v index 07114b1e4..1cb87910d 100644 --- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v +++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v @@ -11,7 +11,7 @@ Local Open Scope Z_scope. Section PseudoMersenneBaseParamProofs. Context `{prm : PseudoMersenneBaseParams}. - Local Notation "{base}" := (base_from_limb_widths limb_widths). + Local Notation base := (base_from_limb_widths limb_widths). Lemma limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w. Proof. @@ -35,9 +35,9 @@ Section PseudoMersenneBaseParamProofs. (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). + 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). @@ -59,8 +59,8 @@ Section PseudoMersenneBaseParamProofs. Qed. Lemma base_good : forall i j : nat, - (i + j < length {base})%nat -> - let b := nth_default 0 {base} in + (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. @@ -76,12 +76,12 @@ Section PseudoMersenneBaseParamProofs. rewrite <-base_from_limb_widths_length; auto using limb_widths_nonneg. Qed. - Lemma base_length : length {base} = length limb_widths. + Lemma base_length : length base = length limb_widths. Proof. auto using base_from_limb_widths_length. Qed. - Global Instance bv : BaseSystem.BaseVector {base} := { + 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 diff --git a/src/Testbit.v b/src/Testbit.v index 13d56f207..8a9b12c61 100644 --- a/src/Testbit.v +++ b/src/Testbit.v @@ -13,7 +13,7 @@ Section Testbit. Context {width : Z} (limb_width_pos : 0 < width). Context (limb_widths : list Z) (limb_widths_nonnil : limb_widths <> nil) (limb_widths_uniform : forall w, In w limb_widths -> w = width). - Local Notation "{base}" := (base_from_limb_widths limb_widths). + Local Notation base := (base_from_limb_widths limb_widths). Definition testbit (us : list Z) (n : nat) := Z.testbit (nth_default 0 us (n / (Z.to_nat width))) (Z.of_nat (n mod Z.to_nat width)%nat). @@ -22,7 +22,7 @@ Section Testbit. Lemma testbit_spec' : forall a b us, (0 <= b < width) -> bounded limb_widths us -> (length us <= length limb_widths)%nat -> - Z.testbit (nth_default 0 us a) b = Z.testbit (decode {base} us) (Z.of_nat a * width + b). + Z.testbit (nth_default 0 us a) b = Z.testbit (decode base us) (Z.of_nat a * width + b). Proof. induction a; destruct us; intros; match goal with H : bounded _ _ |- _ => @@ -42,7 +42,7 @@ Section Testbit. Lemma testbit_spec : forall n us, (length us = length limb_widths)%nat -> bounded limb_widths us -> - testbit us n = Z.testbit (BaseSystem.decode {base} us) (Z.of_nat n). + testbit us n = Z.testbit (BaseSystem.decode base us) (Z.of_nat n). Proof. cbv [testbit]; intros. pose proof limb_width_pos as limb_width_pos_nat. @@ -54,4 +54,4 @@ Section Testbit. rewrite Nat2Z.inj_add, Nat2Z.inj_mul, Z2Nat.id; ring || omega. Qed. -End Testbit. \ No newline at end of file +End Testbit. -- cgit v1.2.3 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 +------------------ src/Util/ZUtil.v | 2 +- 5 files changed, 93 insertions(+), 85 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. diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index a64515427..5e917455b 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -14,7 +14,7 @@ Hint Extern 1 => lia : lia. Hint Extern 1 => lra : lra. Hint Extern 1 => nia : nia. Hint Extern 1 => omega : omega. -Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l : zarith. +Hint Resolve Z.log2_nonneg Z.div_small Z.mod_small Z.pow_neg_r Z.pow_0_l Z.pow_pos_nonneg : zarith. Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z.mod_pos_bound a b H)) : zarith. (** Only hints that are always safe to apply (i.e., reversible), and -- cgit v1.2.3 From 89b3547b231851c739c58c20e2f19073a5cb4c5b Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 19 Jul 2016 17:02:53 -0700 Subject: Work around bad design in Coq This is https://coq.inria.fr/bugs/show_bug.cgi?id=4949, [intuition] should not use [auto with *] by default --- folkwisdom.md | 2 ++ src/ModularArithmetic/ModularBaseSystemProofs.v | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) (limited to 'src/ModularArithmetic') diff --git a/folkwisdom.md b/folkwisdom.md index 3c8d92036..d6d65f12e 100644 --- a/folkwisdom.md +++ b/folkwisdom.md @@ -280,6 +280,8 @@ Considerations not (yet) covered in this document include the following: - how to write tactics that are debuggable - how to write tactics that are robust against small changes - reification: ltac, typeclasses, canonical structures (maybe reference an existing document) + - how `intuition` should never be used because it calls `auto with *`, which + leads to fragile documents, and `intuition auto` should be used instead - performance of proofs and proof checking - `simpl`, `cbn`, `cbv` - `Qed slowness, `change` vs `rewrite` diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index c3b1b76b4..c06dcdf98 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -127,7 +127,7 @@ Section PseudoMersenneProofs. Lemma add_rep : forall u v x y, u ~= x -> v ~= y -> BaseSystem.add u v ~= (x+y)%F. Proof. - autounfold; intuition. { + autounfold; intuition auto. { unfold add. auto using add_same_length. } -- cgit v1.2.3 From 0a4d512d77e34e0d0f5fe4f7711414dd5cd9939e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 20 Jul 2016 09:48:17 -0700 Subject: Use a proof that doesn't require as many assumptions in extended_base_length --- src/ModularArithmetic/ExtendedBaseVector.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v index 1c9555fe6..580156bca 100644 --- a/src/ModularArithmetic/ExtendedBaseVector.v +++ b/src/ModularArithmetic/ExtendedBaseVector.v @@ -162,7 +162,7 @@ Section ExtendedBaseVector. Lemma extended_base_length: length ext_base = (length base + length base)%nat. Proof. - rewrite ext_base_alt, app_length, map_length; auto. + unfold ext_base, ext_limb_widths; autorewrite with distr_length; reflexivity. Qed. Lemma firstn_us_base_ext_base : forall (us : BaseSystem.digits), -- cgit v1.2.3 From 79e6c4ea6cd0ed52fda2168cda78c52e4bc4896a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 20 Jul 2016 10:13:48 -0700 Subject: Remove dependency of ext_base on pseudomersenne --- src/ModularArithmetic/ExtendedBaseVector.v | 193 ++++++++++++------------ src/ModularArithmetic/ModularBaseSystem.v | 2 +- src/ModularArithmetic/ModularBaseSystemOpt.v | 4 +- src/ModularArithmetic/ModularBaseSystemProofs.v | 47 +++--- 4 files changed, 120 insertions(+), 126 deletions(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v index 580156bca..ed21d10f9 100644 --- a/src/ModularArithmetic/ExtendedBaseVector.v +++ b/src/ModularArithmetic/ExtendedBaseVector.v @@ -5,14 +5,14 @@ Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import VerdiTactics. Require Import Crypto.ModularArithmetic.Pow2Base. Require Import Crypto.ModularArithmetic.Pow2BaseProofs. -Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. -Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. Require Import Crypto.BaseSystemProofs. Require Crypto.BaseSystem. Local Open Scope Z_scope. Section ExtendedBaseVector. - Context `{prm : PseudoMersenneBaseParams}. + Context (limb_widths : list Z) + (limb_widths_nonnegative : forall x, In x limb_widths -> 0 <= x). + Local Notation k := (sum_firstn limb_widths (length limb_widths)). Local Notation base := (base_from_limb_widths limb_widths). (* This section defines a new BaseVector that has double the length of the BaseVector @@ -43,44 +43,21 @@ Section ExtendedBaseVector. Lemma ext_base_alt : ext_base = base ++ (map (Z.mul (2^k)) base). Proof. unfold ext_base, ext_limb_widths. - rewrite base_from_limb_widths_app by auto using limb_widths_pos, Z.lt_le_incl. + rewrite base_from_limb_widths_app by auto. rewrite two_p_equiv. reflexivity. Qed. Lemma ext_base_positive : forall b, In b ext_base -> b > 0. Proof. - rewrite ext_base_alt. intros b In_b_base. - rewrite in_app_iff in In_b_base. - destruct In_b_base as [In_b_base | In_b_extbase]. - + eapply BaseSystem.base_positive. - eapply In_b_base. - + eapply in_map_iff in In_b_extbase. - destruct In_b_extbase as [b' [b'_2k_b In_b'_base]]. - subst. - specialize (BaseSystem.base_positive b' In_b'_base); intro base_pos. - replace 0 with (2 ^ k * 0) by ring. - apply (Zmult_gt_compat_l b' 0 (2 ^ k)); [| apply base_pos; intuition]. - rewrite Z.gt_lt_iff. - apply Z.pow_pos_nonneg; intuition. - apply sum_firstn_limb_widths_nonneg; auto using limb_widths_nonneg. + apply base_positive; unfold ext_limb_widths. + intros ? H. apply in_app_or in H; destruct H; auto. Qed. - Lemma base_length_nonzero : (0 < length base)%nat. + Lemma b0_1 : forall x, nth_default x base 0 = 1 -> nth_default x ext_base 0 = 1. Proof. - assert (nth_default 0 base 0 = 1) by (apply BaseSystem.b0_1). - unfold nth_default in H. - case_eq (nth_error base 0); intros; - try (rewrite H0 in H; omega). - apply (nth_error_value_length _ 0 base z); auto. - Qed. - - Lemma b0_1 : forall x, nth_default x ext_base 0 = 1. - Proof. - intros. rewrite ext_base_alt. - rewrite nth_default_app. - assert (0 < length base)%nat by (apply base_length_nonzero). - destruct (lt_dec 0 (length base)); try apply BaseSystem.b0_1; try omega. + intros. rewrite ext_base_alt, nth_default_app. + destruct base; assumption. Qed. Lemma map_nth_default_base_high : forall n, (n < (length base))%nat -> @@ -91,77 +68,84 @@ Section ExtendedBaseVector. erewrite map_nth_default; auto. Qed. - Lemma base_good_over_boundary : forall - (i : nat) - (l : (i < length base)%nat) - (j' : nat) - (Hj': (i + j' < length base)%nat) - , - 2 ^ k * (nth_default 0 base i * nth_default 0 base j') = - 2 ^ k * (nth_default 0 base i * nth_default 0 base j') / - (2 ^ k * nth_default 0 base (i + j')) * - (2 ^ k * nth_default 0 base (i + j')) - . - Proof. - intros. - remember (nth_default 0 base) as b. - 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 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. - apply (BaseSystem.base_good i j'); omega. - Qed. + Section base_good. + Context (two_k_nonzero : 2^k <> 0) + (base_good : forall i j, (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) + (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). - Lemma ext_base_good : - forall i j, (i+j < length ext_base)%nat -> - let b := nth_default 0 ext_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. subst r. - rewrite ext_base_alt in *. - rewrite app_length in H; rewrite map_length in H. - repeat rewrite nth_default_app. - repeat break_if; try omega. - { (* i < length base, j < length base, i + j < length base *) - auto using BaseSystem.base_good. - } { (* i < length base, j < length base, i + j >= length base *) - rewrite (map_nth_default _ _ _ _ 0) by 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'. - replace (i + j - length base)%nat with (i + j')%nat by omega. - replace (nth_default 0 base i * (2 ^ k * nth_default 0 base j')) - with (2 ^ k * (nth_default 0 base i * nth_default 0 base j')) - by ring. - eapply base_good_over_boundary; eauto; omega. - } { (* i >= length base, j < length base, i + j >= length base *) - do 2 rewrite map_nth_default_base_high by omega. - remember (i - length base)%nat as i'. - replace (i + j - length base)%nat with (j + i')%nat by omega. - replace (2 ^ k * nth_default 0 base i' * nth_default 0 base j) - with (2 ^ k * (nth_default 0 base j * nth_default 0 base i')) - by ring. - eapply base_good_over_boundary; eauto; omega. - } - Qed. + Lemma base_good_over_boundary + : forall (i : nat) + (l : (i < length base)%nat) + (j' : nat) + (Hj': (i + j' < length base)%nat), + 2 ^ k * (nth_default 0 base i * nth_default 0 base j') = + (2 ^ k * (nth_default 0 base i * nth_default 0 base j')) + / (2 ^ k * nth_default 0 base (i + j')) * + (2 ^ k * nth_default 0 base (i + j')). + Proof. + clear limb_widths_match_modulus. + intros. + remember (nth_default 0 base) as b. + rewrite Zdiv_mult_cancel_l by (exact two_k_nonzero). + 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). + 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. + apply (base_good i j'); omega. + Qed. - Instance ExtBaseVector : BaseSystem.BaseVector ext_base := { - base_positive := ext_base_positive; - b0_1 := b0_1; - base_good := ext_base_good - }. + Lemma ext_base_good : + forall i j, (i+j < length ext_base)%nat -> + let b := nth_default 0 ext_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. subst r. + rewrite ext_base_alt in *. + rewrite app_length in H; rewrite map_length in H. + repeat rewrite nth_default_app. + repeat break_if; try omega. + { (* i < length base, j < length base, i + j < length base *) + 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; auto using limb_widths_nonnegative, limb_widths_match_modulus; + distr_length. + } { (* 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'. + replace (i + j - length base)%nat with (i + j')%nat by omega. + replace (nth_default 0 base i * (2 ^ k * nth_default 0 base j')) + with (2 ^ k * (nth_default 0 base i * nth_default 0 base j')) + by ring. + eapply base_good_over_boundary; eauto; omega. + } { (* i >= length base, j < length base, i + j >= length base *) + do 2 rewrite map_nth_default_base_high by omega. + remember (i - length base)%nat as i'. + replace (i + j - length base)%nat with (j + i')%nat by omega. + replace (2 ^ k * nth_default 0 base i' * nth_default 0 base j) + with (2 ^ k * (nth_default 0 base j * nth_default 0 base i')) + by ring. + eapply base_good_over_boundary; eauto; omega. + } + Qed. + End base_good. Lemma extended_base_length: length ext_base = (length base + length base)%nat. Proof. + clear limb_widths_nonnegative. unfold ext_base, ext_limb_widths; autorewrite with distr_length; reflexivity. Qed. @@ -177,6 +161,21 @@ Section ExtendedBaseVector. (length us <= length base)%nat -> BaseSystem.decode base us = BaseSystem.decode ext_base us. Proof. auto using decode_short_initial, firstn_us_base_ext_base. Qed. + + Section BaseVector. + Context {bv : BaseSystem.BaseVector base} + (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). + + Instance ExtBaseVector : BaseSystem.BaseVector ext_base := + { base_positive := ext_base_positive; + b0_1 x := b0_1 x (BaseSystem.b0_1 _); + base_good := ext_base_good (two_sum_firstn_limb_widths_nonzero limb_widths_nonnegative _) BaseSystem.base_good limb_widths_match_modulus }. + End BaseVector. End ExtendedBaseVector. Hint Rewrite @extended_base_length : distr_length. diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index 23b0c2ef6..8c850c941 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -30,7 +30,7 @@ Section PseudoMersenneBase. let wrap := map (Z.mul c) high in BaseSystem.add low wrap. - Definition mul (us vs : digits) := reduce (BaseSystem.mul ext_base us vs). + Definition mul (us vs : digits) := reduce (BaseSystem.mul (ext_base limb_widths) us vs). (* In order to subtract without underflowing, we add a multiple of the modulus first. *) Definition sub (us vs : digits) := BaseSystem.sub (add modulus_multiple us) vs. diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 696f10438..1e748892d 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -478,12 +478,12 @@ Section Multiplication. Proof. eexists. cbv [BaseSystem.mul mul mul_each mul_bi mul_bi' zeros reduce]. - rewrite ext_base_alt. + rewrite ext_base_alt by auto using limb_widths_pos with zarith. rewrite <- mul'_opt_correct. change @Pow2Base.base_from_limb_widths with base_from_limb_widths_opt. rewrite Z.map_shiftl by apply k_nonneg. rewrite c_subst. - rewrite k_subst. + fold k; rewrite k_subst. change @map with @map_opt. change @Z.shiftl_by with @Z_shiftl_by_opt. reflexivity. diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index c06dcdf98..73146fe75 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -66,6 +66,13 @@ Section PseudoMersenneProofs. Lemma base_length : length base = length limb_widths. Proof. distr_length. Qed. + Lemma base_length_nonzero : length base <> 0%nat. + Proof. + distr_length. + pose proof limb_widths_nonnil. + destruct limb_widths; simpl in *; congruence. + 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. @@ -137,29 +144,15 @@ Section PseudoMersenneProofs. subst; auto. Qed. - Lemma firstn_us_base_ext_base : forall (us : BaseSystem.digits), - (length us <= length base)%nat - -> firstn (length us) base = firstn (length us) ext_base. - Proof. - rewrite ext_base_alt; intros. - rewrite firstn_app_inleft; auto; omega. - Qed. - Local Hint Immediate firstn_us_base_ext_base. - - Lemma decode_short : forall (us : BaseSystem.digits), - (length us <= length base)%nat -> - BaseSystem.decode base us = BaseSystem.decode ext_base us. - Proof. auto using decode_short_initial. Qed. - - Local Hint Immediate ExtBaseVector. + Local Hint Resolve firstn_us_base_ext_base bv ExtBaseVector limb_widths_match_modulus. + Local Hint Extern 1 => apply limb_widths_match_modulus. Lemma mul_rep_extended : forall (us vs : BaseSystem.digits), (length us <= length base)%nat -> (length vs <= length base)%nat -> - (BaseSystem.decode base us) * (BaseSystem.decode base vs) = BaseSystem.decode ext_base (BaseSystem.mul ext_base us vs). + (BaseSystem.decode base us) * (BaseSystem.decode base vs) = BaseSystem.decode (ext_base limb_widths) (BaseSystem.mul (ext_base limb_widths) us vs). Proof. - intros; apply mul_rep_two_base; auto; - distr_length. + intros; apply mul_rep_two_base; auto with arith distr_length. Qed. Lemma modulus_nonzero : modulus <> 0. @@ -187,13 +180,14 @@ Section PseudoMersenneProofs. Qed. Lemma extended_shiftadd: forall (us : BaseSystem.digits), - BaseSystem.decode ext_base us = + BaseSystem.decode (ext_base limb_widths) us = BaseSystem.decode base (firstn (length base) us) + (2^k * BaseSystem.decode base (skipn (length base) us)). Proof. intros. unfold BaseSystem.decode; rewrite <- mul_each_rep. - rewrite ext_base_alt. + rewrite ext_base_alt by auto. + fold k. replace (map (Z.mul (2 ^ k)) base) with (BaseSystem.mul_each (2 ^ k) base) by auto. rewrite base_mul_app. rewrite <- mul_each_rep; auto. @@ -201,7 +195,7 @@ Section PseudoMersenneProofs. Lemma reduce_rep : forall us, BaseSystem.decode base (reduce us) mod modulus = - BaseSystem.decode ext_base us mod modulus. + BaseSystem.decode (ext_base limb_widths) us mod modulus. Proof. intros. rewrite extended_shiftadd. @@ -216,7 +210,7 @@ Section PseudoMersenneProofs. Qed. Lemma reduce_length : forall us, - (length base <= length us <= length ext_base)%nat -> + (length base <= length us <= length (ext_base limb_widths))%nat -> (length (reduce us) = length base)%nat. Proof. rewrite extended_base_length. @@ -236,8 +230,9 @@ Section PseudoMersenneProofs. apply reduce_length. rewrite mul_length_exact, extended_base_length; try omega. destruct u; try congruence. - rewrite @nil_length0 in *. - pose proof base_length_nonzero; omega. + pose proof limb_widths_nonnil. + autorewrite with distr_length in *. + destruct limb_widths; simpl in *; congruence. Qed. Lemma mul_rep : forall u v x y, u ~= x -> v ~= y -> u .* v ~= (x*y)%F. @@ -246,8 +241,8 @@ Section PseudoMersenneProofs. { apply length_mul; intuition auto. } { intuition idtac; subst. rewrite ZToField_mod, reduce_rep, <-ZToField_mod. - rewrite mul_rep by (apply ExtBaseVector || rewrite extended_base_length; omega). - rewrite 2decode_short by omega. + rewrite mul_rep by (auto using ExtBaseVector || rewrite extended_base_length; omega). + rewrite 2decode_short by auto with omega. apply ZToField_mul. } Qed. -- cgit v1.2.3 From 4c13852425991ad28dd9aeaa5f6a1d1b65b4db45 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 20 Jul 2016 12:14:23 -0700 Subject: Absolutize some imports --- src/ModularArithmetic/ExtendedBaseVector.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v index ed21d10f9..fcd871aae 100644 --- a/src/ModularArithmetic/ExtendedBaseVector.v +++ b/src/ModularArithmetic/ExtendedBaseVector.v @@ -1,8 +1,8 @@ -Require Import Zpower ZArith. -Require Import List. +Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith. +Require Import Coq.Lists.List. Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import VerdiTactics. +Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.ModularArithmetic.Pow2Base. Require Import Crypto.ModularArithmetic.Pow2BaseProofs. Require Import Crypto.BaseSystemProofs. -- cgit v1.2.3 From 4fbf246cb392496e676e314c11bc2962d37caad7 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 20 Jul 2016 13:04:31 -0700 Subject: Don't use auto with * It's fragile and slow. Now we're 45 seconds faster. After | File Name | Before || Change ------------------------------------------------------------------------------- 1m03.42s | Total | 1m49.00s || -0m45.57s ------------------------------------------------------------------------------- 0m20.01s | ModularArithmetic/ModularBaseSystemProofs | 1m05.69s || -0m45.67s 0m32.14s | Specific/GF25519 | 0m31.92s || +0m00.21s 0m07.05s | Specific/GF1305 | 0m07.07s || -0m00.02s 0m02.84s | ModularArithmetic/ModularBaseSystemOpt | 0m02.90s || -0m00.06s 0m00.69s | Experiments/SpecificCurve25519 | 0m00.69s || +0m00.00s 0m00.69s | ModularArithmetic/ModularBaseSystemInterface | 0m00.73s || -0m00.04s --- src/ModularArithmetic/ModularBaseSystemProofs.v | 48 ++++++++++++------------- 1 file changed, 24 insertions(+), 24 deletions(-) (limited to 'src/ModularArithmetic') diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 73146fe75..e74051319 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -32,12 +32,12 @@ Section PseudoMersenneProofs. Lemma rep_decode : forall us x, us ~= x -> decode us = x. Proof. - autounfold; intuition. + autounfold; intuition auto. Qed. Lemma rep_length : forall us x, us ~= x -> length us = length base. Proof. - autounfold; intuition. + autounfold; intuition auto. Qed. Lemma decode_rep : forall us, length us = length base -> @@ -284,7 +284,7 @@ Section PseudoMersenneProofs. intros ? ?; unfold carry_done; split; [ intros Hcarry_done i | intros Hbounds i i_lt ]. + destruct (lt_dec i (length base)) as [i_lt | i_nlt]. - specialize (Hcarry_done i i_lt). - split; [ intuition | ]. + split; [ intuition auto | ]. destruct Hcarry_done as [Hnth_nonneg Hshiftr_0]. apply Z.shiftr_eq_0_iff in Hshiftr_0. destruct Hshiftr_0 as [nth_0 | []]; [ rewrite nth_0; zero_bounds | ]. @@ -292,7 +292,7 @@ Section PseudoMersenneProofs. - rewrite nth_default_out_of_bounds by omega. split; zero_bounds. + specialize (Hbounds i). - split; [ intuition | ]. + split; [ intuition auto | ]. destruct Hbounds as [nth_nonneg nth_lt_pow2]. apply Z.shiftr_eq_0_iff. apply Z.le_lteq in nth_nonneg; destruct nth_nonneg; try solve [left; auto]. @@ -402,7 +402,7 @@ Section CarryProofs. specialize_by eauto. intros; split; try solve [ distr_length ]. unfold rep, decode, carry in *. - intuition; break_if; subst; eauto; apply F_eq; simpl; intuition. + intuition auto; break_if; subst; eauto; apply F_eq; simpl; intuition auto with zarith. Qed. Hint Resolve carry_rep. @@ -575,7 +575,7 @@ Section CanonicalizationProofs. Proof. intros ? ? shiftr_0. apply Z.shiftr_eq_0_iff in shiftr_0. - intuition; subst; try apply max_bound_nonneg. + intuition auto; subst; try apply max_bound_nonneg. match goal with H : Z.log2 _ < log_cap _ |- _ => apply Z.log2_lt_pow2 in H; replace (2 ^ log_cap i) with (Z.succ (max_bound i)) in H by (unfold max_bound, Z.ones; rewrite Z.shiftl_1_l; omega) @@ -725,7 +725,7 @@ Section CanonicalizationProofs. || omega). Qed. - Hint Rewrite pow2_mod_log_cap_small using (intuition; auto using shiftr_eq_0_max_bound) : core. + Hint Rewrite pow2_mod_log_cap_small using (intuition auto; auto using shiftr_eq_0_max_bound) : core. Lemma carry_carry_done_done : forall i us, (length us = length base)%nat -> @@ -744,7 +744,7 @@ Section CanonicalizationProofs. - add_set_nth; subst. * rewrite shiftr_0_i, Z.mul_0_r, Z.add_0_l. assumption. - * rewrite pow2_mod_log_cap_small by (intuition; auto using shiftr_eq_0_max_bound). + * rewrite pow2_mod_log_cap_small by (intuition auto; auto using shiftr_eq_0_max_bound). assumption. - repeat (carry_length_conditions || (autorewrite with push_nth_default natsimplify core zsimplify) @@ -886,13 +886,13 @@ Section CanonicalizationProofs. intros ? ? PCB ?. induction i. + simpl. specialize (PCB 0%nat). - intuition. + intuition auto. + simpl. destruct (lt_eq_lt_dec i (pred (length base))) as [[? | ? ] | ? ]. - apply carry_simple_no_overflow; carry_length_conditions; carry_seq_lower_bound. rewrite carry_sequence_unaffected; try omega. specialize (PCB (S i)); rewrite Nat.pred_succ in PCB. - break_if; intuition. + break_if; intuition auto with zarith. - unfold carry; break_if; try omega. rewrite nth_default_out_of_bounds; [ apply Z.pow_pos_nonneg; omega | ]. subst; unfold carry_and_reduce. @@ -1085,7 +1085,7 @@ Section CanonicalizationProofs. apply pow2_mod_log_cap_bounds_lower. + rewrite carry_unaffected_low by carry_length_conditions. assert (0 < S i < length base)%nat by omega. - intuition. + intuition auto. Qed. Lemma carry_full_2_bounds_lower :forall us i, pre_carry_bounds us -> @@ -1139,7 +1139,7 @@ Section CanonicalizationProofs. ring_simplify | ]; pose proof c_pos; omega. + rewrite carry_unaffected_low by carry_length_conditions. assert (0 < S i < length base)%nat by omega. - intuition; right. + intuition auto; right. apply carry_carry_done_done; try solve [carry_length_conditions]. assumption. Qed. @@ -1170,7 +1170,7 @@ Section CanonicalizationProofs. - eapply carry_carry_full_2_bounds_0_lower; eauto; omega. + pose proof (carry_carry_full_2_bounds_0_upper us (pred (length base))). assert (0 < pred (length base) < length base)%nat by omega. - intuition. + intuition auto. - replace (max_bound 0) with (c + (max_bound 0 - c)) by ring. apply Z.add_le_mono; try assumption. etransitivity; [ | replace c with (c * 1) by ring; reflexivity ]. @@ -1280,12 +1280,12 @@ Section CanonicalizationProofs. Proof. induction j; intros. + cbv [isFull']; apply Bool.andb_true_iff. - rewrite Z.ltb_lt; intuition. - + intuition. + rewrite Z.ltb_lt; intuition auto. + + intuition auto. simpl. match goal with H : forall j, _ -> ?b j = ?a j |- appcontext[?a ?i =? ?b ?i] => replace (a i =? b i) with true by (symmetry; apply Z.eqb_eq; symmetry; apply H; omega) end. - apply IHj; auto; intuition. + apply IHj; auto; intuition auto. Qed. Lemma isFull'_true_iff : forall j us, (length us = length base) -> (isFull' us true j = true <-> @@ -1390,7 +1390,7 @@ Section CanonicalizationProofs. replace 1 with (Z.succ 0) by reflexivity. rewrite Z.le_succ_l, Z.lt_0_sub. match goal with H : carry_done us |- _ => rewrite carry_done_bounds in H by auto; specialize (H n) end. - replace x with (log_cap n); try intuition. + replace x with (log_cap n); try intuition auto. apply nth_error_value_eq_nth_default; auto. + repeat erewrite firstn_all_strong by omega. rewrite sum_firstn_all_succ by (rewrite <-base_length; omega). @@ -1419,7 +1419,7 @@ Section CanonicalizationProofs. - rewrite nth_default_base by (omega || eauto). apply Z.pow_nonneg; omega. - match goal with H : carry_done us |- _ => rewrite carry_done_bounds in H by auto; specialize (H n) end. - intuition. + intuition auto. + eapply Z.le_trans; [ apply IHn; eauto | ]. repeat rewrite firstn_all_strong by omega. omega. @@ -1588,7 +1588,7 @@ Section CanonicalizationProofs. Lemma freeze_preserves_rep : forall us x, rep us x -> rep (freeze us) x. Proof. unfold rep; intros. - intuition; rewrite ?freeze_length; auto. + intuition auto; rewrite ?freeze_length; auto. unfold freeze, and_term. break_if. + apply decode_mod with (us := carry_full (carry_full (carry_full us))). @@ -1597,7 +1597,7 @@ Section CanonicalizationProofs. apply Min.min_r. simpl_lengths; omega. - repeat apply carry_full_preserves_rep; repeat rewrite carry_full_length; auto. - unfold rep; intuition. + unfold rep; intuition auto. - rewrite decode_map2_sub by (simpl_lengths; omega). rewrite map_land_max_ones_modulus_digits. rewrite decode_modulus_digits. @@ -2016,7 +2016,7 @@ Section CanonicalizationProofs. (BaseSystem.decode base us) mod modulus = (BaseSystem.decode base vs) mod modulus. Proof. unfold rep, decode; intros. - intuition. + intuition auto. repeat rewrite <-FieldToZ_ZToField. congruence. Qed. @@ -2032,7 +2032,7 @@ Section CanonicalizationProofs. repeat match goal with Hmin : minimal_rep ?us |- _ => unfold minimal_rep in Hmin; rewrite <- Hmin in eqmod; clear Hmin end. apply Z.compare_eq_iff in eqmod. - rewrite decode_compare in eqmod; unfold rep in *; auto; intuition; try congruence. + rewrite decode_compare in eqmod; unfold rep in *; auto; intuition auto; try congruence. apply compare_Eq; auto. congruence. Qed. @@ -2043,8 +2043,8 @@ Section CanonicalizationProofs. freeze us = freeze vs. Proof. intros. - assert (length us = length base) by (unfold rep in *; intuition). - assert (length vs = length base) by (unfold rep in *; intuition). + assert (length us = length base) by (unfold rep in *; intuition auto). + assert (length vs = length base) by (unfold rep in *; intuition auto). eapply minimal_rep_unique; eauto; rewrite freeze_length; assumption. Qed. -- cgit v1.2.3