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') 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