From a201b0a8e525cab5c3cb019ccd707b7367aa3ecc Mon Sep 17 00:00:00 2001 From: jadep Date: Tue, 12 Mar 2019 15:30:56 -0400 Subject: add some hints to the global databases --- src/Arithmetic.v | 69 +++++++++++++++++------------------------ src/Util/ZUtil/Div.v | 4 +-- src/Util/ZUtil/Hints/PullPush.v | 3 ++ src/Util/ZUtil/Hints/ZArith.v | 2 ++ src/Util/ZUtil/Le.v | 2 +- 5 files changed, 36 insertions(+), 44 deletions(-) (limited to 'src') diff --git a/src/Arithmetic.v b/src/Arithmetic.v index b0d3a0c24..5cd751551 100644 --- a/src/Arithmetic.v +++ b/src/Arithmetic.v @@ -533,8 +533,6 @@ Module Weight. (weight_multiples : forall i, weight (S i) mod weight i = 0) (weight_divides : forall i : nat, 0 < weight (S i) / weight i). - Local Hint Resolve Z.positive_is_nonzero Z.lt_gt Nat2Z.is_nonneg. - Lemma weight_multiples_full' j : forall i, weight (i+j) mod weight i = 0. Proof using weight_positive weight_multiples. induction j; intros; @@ -542,7 +540,7 @@ Module Weight. | _ => rewrite Nat.add_succ_r | _ => rewrite IHj | |- context [weight (S ?x) mod weight _] => - rewrite (Z.div_mod (weight (S x)) (weight x)), weight_multiples by auto + rewrite (Z.div_mod (weight (S x)) (weight x)), weight_multiples by auto with zarith | _ => progress autorewrite with push_Zmod natsimplify zsimplify_fast | _ => reflexivity end. @@ -555,10 +553,10 @@ Module Weight. Qed. Lemma weight_divides_full j i : (i <= j)%nat -> 0 < weight j / weight i. - Proof using weight_positive weight_multiples. auto using Z.gt_lt, Z.div_positive_gt_0, weight_multiples_full. Qed. + Proof using weight_positive weight_multiples. auto using Z.gt_lt, Z.div_positive_gt_0, weight_multiples_full with zarith. Qed. Lemma weight_div_mod j i : (i <= j)%nat -> weight j = weight i * (weight j / weight i). - Proof using weight_positive weight_multiples. intros. apply Z.div_exact; auto using weight_multiples_full. Qed. + Proof using weight_positive weight_multiples. intros. apply Z.div_exact; auto using weight_multiples_full with zarith. Qed. Lemma weight_mod_pull_div n x : x mod weight (S n) / weight n = @@ -567,11 +565,11 @@ Module Weight. replace (weight (S n)) with (weight n * (weight (S n) / weight n)); repeat match goal with | _ => progress autorewrite with zsimplify_fast - | _ => rewrite Z.mul_div_eq_full by auto - | _ => rewrite Z.mul_div_eq' by auto + | _ => rewrite Z.mul_div_eq_full by auto with zarith + | _ => rewrite Z.mul_div_eq' by auto with zarith | _ => rewrite Z.mod_pull_div - | _ => rewrite weight_multiples by auto - | _ => solve [auto using Z.lt_le_incl] + | _ => rewrite weight_multiples by auto with zarith + | _ => solve [auto with zarith] end. Qed. @@ -582,11 +580,11 @@ Module Weight. replace (weight (S n)) with (weight n * (weight (S n) / weight n)); repeat match goal with | _ => progress autorewrite with zdiv_to_mod zsimplify_fast - | _ => rewrite Z.mul_div_eq_full by auto - | _ => rewrite Z.mul_div_eq' by auto - | _ => rewrite Z.div_div by auto + | _ => rewrite Z.mul_div_eq_full by auto with zarith + | _ => rewrite Z.mul_div_eq' by auto with zarith + | _ => rewrite Z.div_div by auto with zarith | _ => rewrite weight_multiples by assumption - | _ => solve [auto using Z.lt_le_incl] + | _ => solve [auto with zarith] end. Qed. End Weight. @@ -1547,7 +1545,6 @@ Section mod_ops. Local Hint Immediate (weight_positive wprops). Local Hint Immediate (weight_multiples wprops). Local Hint Immediate (weight_divides wprops). - Local Hint Resolve Z.positive_is_nonzero Z.lt_gt. Local Lemma weight_1_gt_1 : weight 1 > 1. Proof using limbwidth_good. @@ -1580,10 +1577,10 @@ Section mod_ops. As eval_carry_mulmod. Proof. intros. - rewrite <-eval_mulmod with (s:=s) (c:=c) by auto. + rewrite <-eval_mulmod with (s:=s) (c:=c) by auto with zarith. etransitivity; [ | rewrite <- @eval_chained_carries with (s:=s) (c:=c) (idxs:=idxs) - by auto; reflexivity ]. + by auto with zarith; reflexivity ]. eapply f_equal2; [|trivial]. eapply f_equal. subst carry_mulmod; reflexivity. Qed. @@ -1596,10 +1593,10 @@ Section mod_ops. As eval_carry_squaremod. Proof. intros. - rewrite <-eval_squaremod with (s:=s) (c:=c) by auto. + rewrite <-eval_squaremod with (s:=s) (c:=c) by auto with zarith. etransitivity; [ | rewrite <- @eval_chained_carries with (s:=s) (c:=c) (idxs:=idxs) - by auto; reflexivity ]. + by auto with zarith; reflexivity ]. eapply f_equal2; [|trivial]. eapply f_equal. subst carry_squaremod; reflexivity. Qed. @@ -1613,12 +1610,12 @@ Section mod_ops. Proof. intros. push_Zmod. - rewrite <-eval_encode with (s:=s) (c:=c) (x:=x) (weight:=weight) (n:=n) by auto. + rewrite <-eval_encode with (s:=s) (c:=c) (x:=x) (weight:=weight) (n:=n) by auto with zarith. pull_Zmod. - rewrite<-eval_mulmod with (s:=s) (c:=c) by (auto; distr_length). + rewrite<-eval_mulmod with (s:=s) (c:=c) by (auto with zarith; distr_length). etransitivity; [ | rewrite <- @eval_chained_carries with (s:=s) (c:=c) (idxs:=idxs) - by auto; reflexivity ]. + by auto with zarith; reflexivity ]. eapply f_equal2; [|trivial]. eapply f_equal. subst carry_scmulmod; reflexivity. Qed. @@ -1633,7 +1630,7 @@ Section mod_ops. intros. etransitivity; [ | rewrite <- @eval_chained_carries with (s:=s) (c:=c) (idxs:=idxs) - by auto; reflexivity ]. + by auto with zarith; reflexivity ]. eapply f_equal2; [|trivial]. eapply f_equal. subst carrymod; reflexivity. Qed. @@ -1647,7 +1644,7 @@ Section mod_ops. As eval_addmod. Proof. intros. - rewrite <-eval_add by auto. + rewrite <-eval_add by auto with zarith. eapply f_equal2; [|trivial]. eapply f_equal. subst addmod; reflexivity. Qed. @@ -1662,7 +1659,7 @@ Section mod_ops. As eval_submod. Proof. intros. - rewrite <-eval_sub with (coef:=coef) by auto. + rewrite <-eval_sub with (coef:=coef) by auto with zarith. eapply f_equal2; [|trivial]. eapply f_equal. subst submod; reflexivity. Qed. @@ -1676,7 +1673,7 @@ Section mod_ops. As eval_oppmod. Proof. intros. - rewrite <-eval_opp with (coef:=coef) by auto. + rewrite <-eval_opp with (coef:=coef) by auto with zarith. eapply f_equal2; [|trivial]. eapply f_equal. subst oppmod; reflexivity. Qed. @@ -1689,7 +1686,7 @@ Section mod_ops. Proof. intros. etransitivity. - 2:rewrite <-@eval_encode with (weight:=weight) (n:=n) by auto; reflexivity. + 2:rewrite <-@eval_encode with (weight:=weight) (n:=n) by auto with zarith; reflexivity. eapply f_equal2; [|trivial]. eapply f_equal. subst encodemod; reflexivity. Qed. @@ -1906,7 +1903,6 @@ Module Columns. Import Saturated. Import Partition. Import Weight. Section Columns. Context weight {wprops : @weight_properties weight}. - Hint Resolve Z.positive_is_nonzero Z.lt_gt. Definition eval n (x : list (list Z)) : Z := Positional.eval weight n (map sum x). @@ -1919,8 +1915,6 @@ Module Columns. apply Positional.eval_snoc; distr_length. Qed. Hint Rewrite eval_snoc using (solve [distr_length]) : push_eval. - Hint Rewrite <- Z.div_add' using omega : pull_Zdiv. - Ltac cases := match goal with | |- _ /\ _ => split @@ -1966,7 +1960,7 @@ Module Columns. | |- context [list_rect _ _ _ ?ls] => rewrite single_list_rect_to_match; destruct ls | _ => progress (unfold flatten_step in *; fold flatten_step in * ) | _ => rewrite Nat.add_1_r - | _ => rewrite Z.mul_div_eq_full by (auto; omega) + | _ => rewrite Z.mul_div_eq_full by (auto with zarith; omega) | _ => rewrite weight_multiples | _ => reflexivity | _ => solve [repeat (f_equal; try ring)] @@ -1995,16 +1989,18 @@ Module Columns. Lemma flatten_column_div fw (xs : list Z) (fw_nz : fw <> 0) : snd (flatten_column fw xs) = sum xs / fw. Proof using Type. + (* this hint is already in the database but Z.div_add_l' is triggered first and that screws things up *) + Hint Rewrite <- Z.div_add' using zutil_arith : pull_Zdiv. induction xs; simpl flatten_column; cbv [Let_In]; repeat match goal with | _ => rewrite IHxs + | _ => rewrite <-Z.div_add' by zutil_arith | _ => rewrite Z.mul_div_eq_full by omega | _ => progress push end. Qed. Hint Rewrite flatten_column_div using auto with zarith : to_div_mod. Hint Rewrite Positional.eval_nil : push_eval. - Hint Resolve Z.gt_lt. Lemma length_flatten_step digit state : length (fst (flatten_step digit state)) = S (length (fst state)). @@ -2111,7 +2107,7 @@ Module Columns. Lemma eval_from_associational n p (n_nonzero:n<>0%nat\/p=nil) : eval n (from_associational n p) = Associational.eval p. Proof using wprops. - erewrite <-Positional.eval_from_associational by eauto. + erewrite <-Positional.eval_from_associational by eauto with zarith. induction p; [ autorewrite with push_eval; solve [auto] |]. cbv [from_associational Positional.from_associational]; autorewrite with push_fold_right. fold (from_associational n p); fold (Positional.from_associational weight n p). @@ -4927,7 +4923,6 @@ Module WordByWordMontgomery. End modops. End WordByWordMontgomery. -Hint Rewrite Z2Nat.inj_succ using omega : push_Zto_nat. (* TODO: put in PullPush *) Module BarrettReduction. Import Partition. Section Generic. @@ -5103,11 +5098,6 @@ Module BarrettReduction. cond_subM rt. Section Proofs. - - (* TODO: move these? *) - Local Hint Resolve Z.lt_gt : zarith. - Hint Rewrite Z.div_add' using solve [auto with zarith] : zsimplify. - Lemma shiftr'_correct m n : forall t tn, (m <= tn)%nat -> 0 <= t < w tn -> 0 <= n < width -> @@ -5379,9 +5369,6 @@ Module BarrettReduction. f_equal; lia. Qed. - (* TODO: move *) - Hint Resolve Z.positive_is_nonzero Z.lt_gt : zarith. - Lemma r_idea x q3 (b:bool) : 0 <= x < M * 2 ^ k -> 0 <= q3 -> diff --git a/src/Util/ZUtil/Div.v b/src/Util/ZUtil/Div.v index 7012f83c0..4995ba76b 100644 --- a/src/Util/ZUtil/Div.v +++ b/src/Util/ZUtil/Div.v @@ -45,10 +45,10 @@ Module Z. Lemma div_add' a b c : c <> 0 -> (a + c * b) / c = a / c + b. Proof. intro; rewrite <- Z.div_add, (Z.mul_comm c); try lia. Qed. - Lemma div_add_l' a b c : b <> 0 -> (b * a + c) / b = a + c / b. Proof. intro; rewrite <- Z.div_add_l, (Z.mul_comm b); lia. Qed. - + Hint Rewrite Z.div_add' Z.div_add_l' using zutil_arith : push_Zdiv. + Hint Rewrite <- Z.div_add' Z.div_add_l' using zutil_arith : pull_Zdiv. Hint Rewrite div_add_l' div_add' using zutil_arith : zsimplify. Lemma div_sub a b c : c <> 0 -> (a - b * c) / c = a / c - b. diff --git a/src/Util/ZUtil/Hints/PullPush.v b/src/Util/ZUtil/Hints/PullPush.v index a6d4e94b4..a56357c1a 100644 --- a/src/Util/ZUtil/Hints/PullPush.v +++ b/src/Util/ZUtil/Hints/PullPush.v @@ -14,6 +14,8 @@ Hint Rewrite Z.mul_add_distr_l Z.mul_add_distr_r Z.mul_sub_distr_l Z.mul_sub_dis Hint Rewrite <- Z.mul_add_distr_l Z.mul_add_distr_r Z.mul_sub_distr_l Z.mul_sub_distr_r : pull_Zmul. Hint Rewrite Z.div_div using zutil_arith : pull_Zdiv. Hint Rewrite <- Z.div_div using zutil_arith : push_Zdiv. +Hint Rewrite Z.div_add Z.div_add_l using zutil_arith : push_Zdiv. +Hint Rewrite <- Z.div_add Z.div_add_l using zutil_arith : pull_Zdiv. Hint Rewrite <- Z.mul_mod Z.add_mod Zminus_mod using zutil_arith : pull_Zmod. Hint Rewrite Zminus_mod_idemp_l Zminus_mod_idemp_r : pull_Zmod. Hint Rewrite Z_mod_nz_opp_full using zutil_arith : push_Zmod. @@ -21,6 +23,7 @@ Hint Rewrite Z_mod_same_full : push_Zmod. Hint Rewrite Nat2Z.id : push_Zof_nat. Hint Rewrite N2Z.id : push_Zto_N. Hint Rewrite N2Z.id : pull_Zof_N. +Hint Rewrite Z2Nat.id Z2Nat.inj_succ using zutil_arith : push_Zto_nat. Hint Rewrite N2Z.inj_pos N2Z.inj_abs_N N2Z.inj_add N2Z.inj_mul N2Z.inj_sub_max N2Z.inj_succ N2Z.inj_pred_max N2Z.inj_min N2Z.inj_max N2Z.inj_div N2Z.inj_quot N2Z.inj_rem N2Z.inj_div2 N2Z.inj_pow N2Z.inj_0 nat_N_Z : push_Zof_N. Hint Rewrite N2Z.inj_compare N2Z.inj_testbit : pull_Zof_N. Hint Rewrite <- N2Z.inj_abs_N N2Z.inj_add N2Z.inj_mul N2Z.inj_sub_max N2Z.inj_succ N2Z.inj_pred_max N2Z.inj_min N2Z.inj_max N2Z.inj_div N2Z.inj_quot N2Z.inj_rem N2Z.inj_div2 N2Z.inj_pow : pull_Zof_N. diff --git a/src/Util/ZUtil/Hints/ZArith.v b/src/Util/ZUtil/Hints/ZArith.v index 2aa70dc97..97b7f261f 100644 --- a/src/Util/ZUtil/Hints/ZArith.v +++ b/src/Util/ZUtil/Hints/ZArith.v @@ -8,3 +8,5 @@ Hint Resolve (fun n m => proj1 (Z.pred_le_mono n m)) : zarith. Hint Resolve (fun a b => proj2 (Z.lor_nonneg a b)) : zarith. Hint Resolve Zmult_le_compat_r Zmult_le_compat_l Z_div_le Z.add_le_mono Z.sub_le_mono : zarith. +Hint Resolve Z.lt_gt Z.lt_le_incl : zarith. +Hint Resolve Nat2Z.is_nonneg : zarith. diff --git a/src/Util/ZUtil/Le.v b/src/Util/ZUtil/Le.v index a32d0fdd0..d49931818 100644 --- a/src/Util/ZUtil/Le.v +++ b/src/Util/ZUtil/Le.v @@ -61,4 +61,4 @@ Module Z. Lemma le_add_1_iff x y : x + 1 <= y <-> x < y. Proof. lia. Qed. -End Z. +End Z. \ No newline at end of file -- cgit v1.2.3