From 9c5a967ababd80425fe3b09f17f502ed5f0d6a11 Mon Sep 17 00:00:00 2001 From: jadep Date: Thu, 14 Mar 2019 14:53:38 -0400 Subject: update _CoqProject, fix indentations, and prune dependencies of new Arithmetic files --- src/Arithmetic/BarrettReduction.v | 81 ++----- src/Arithmetic/BaseConversion.v | 79 ++----- src/Arithmetic/Core.v | 71 ++---- src/Arithmetic/FancyMontgomeryReduction.v | 82 +++---- src/Arithmetic/Freeze.v | 352 ++++++++++++++++++++++++++++++ src/Arithmetic/ModOps.v | 58 +---- src/Arithmetic/Partition.v | 79 ++----- src/Arithmetic/Saturated.v | 227 ++++++++----------- src/Arithmetic/UniformWeight.v | 71 ++---- src/Arithmetic/WordByWordMontgomery.v | 81 +++---- 10 files changed, 583 insertions(+), 598 deletions(-) create mode 100644 src/Arithmetic/Freeze.v (limited to 'src') diff --git a/src/Arithmetic/BarrettReduction.v b/src/Arithmetic/BarrettReduction.v index c5cc1ecde..b679a168c 100644 --- a/src/Arithmetic/BarrettReduction.v +++ b/src/Arithmetic/BarrettReduction.v @@ -1,61 +1,29 @@ -(* TODO: prune these *) -Require Import Crypto.Algebra.Nsatz. Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz. -Require Import Coq.Sorting.Mergesort Coq.Structures.Orders. -Require Import Coq.Sorting.Permutation. Require Import Coq.derive.Derive. -Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *) -Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *) -Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable. -Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn. -Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil. -Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil. -Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop. -Require Import Crypto.Arithmetic.BarrettReduction.Generalized. +Require Import Coq.Lists.List. +Require Import Crypto.Algebra.Ring. +Require Import Crypto.Arithmetic.BaseConversion. +Require Import Crypto.Arithmetic.Core. Require Import Crypto.Arithmetic.Partition. -Require Import Crypto.Arithmetic.ModularArithmeticTheorems. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.Tactics.RunTacticAsConstr. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.OptionList. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Sum. -Require Import Crypto.Util.Bool. -Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. -Require Import Crypto.Util.ZUtil.Tactics.PeelLe. -Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute. -Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Arithmetic.Saturated. +Require Import Crypto.Arithmetic.UniformWeight. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Arithmetic.BarrettReduction.Generalized. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.AddModulo. +Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi. +Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Hints.Core. Require Import Crypto.Util.ZUtil.Modulo.PullPush. -Require Import Crypto.Util.ZUtil.Opp. -Require Import Crypto.Util.ZUtil.Log2. -Require Import Crypto.Util.ZUtil.Le. -Require Import Crypto.Util.ZUtil.Hints.PullPush. -Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.SubstEvars. + Require Import Crypto.Util.Notations. -Require Import Crypto.Util.ZUtil.Definitions. -Require Import Crypto.Util.ZUtil.Sorting. -Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi. -Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo. -Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div. -Require Import Crypto.Util.ZUtil.Hints.PullPush. -Require Import Crypto.Util.ZUtil.EquivModulo. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.CPSNotations. -Require Import Crypto.Util.Equality. -Require Import Crypto.Util.Tactics.SetEvars. -Import Coq.Lists.List ListNotations. Local Open Scope Z_scope. +Import ListNotations. Local Open Scope Z_scope. Section Generic. Context (b k M mu width : Z) (n : nat) @@ -66,8 +34,8 @@ Section Generic. (mu_eq : mu = b ^ (2 * k) / M) (width_pos : 0 < width) (strong_bound : b ^ 1 * (b ^ (2 * k) mod M) <= b ^ (k + 1) - mu). - Local Notation weight := (UniformWeight.uweight width). - Local Notation partition := (Partition.partition weight). + Local Notation weight := (uweight width). + Local Notation partition := (partition weight). Context (q1 : list Z -> list Z) (q1_correct : forall x, @@ -389,9 +357,6 @@ Module Fancy. apply Z.pow_le_mono_r; lia. Qed. - (* use zero_bounds in zutil_arith *) - Local Ltac zutil_arith ::= solve [ omega | Psatz.lia | auto with nocore | solve [Z.zero_bounds] ]. - Lemma muSelect_correct x : 0 <= x < w (sz * 2) -> muSelect (partition w (sz*2) x) = partition w sz (mu mod (w sz) * (x / 2 ^ (k - 1) / (w sz))). @@ -406,7 +371,8 @@ Module Fancy. | H : 0 <= ?x < ?m |- context [?x mod ?m] => rewrite (Z.mod_small x m) by auto with zarith end. replace (x / (w (sz * 2 - 1)) / (2 ^ width / 2)) with (x / (2 ^ (k - 1)) / w sz) by - (autorewrite with weight_to_pow pull_Zpow pull_Zdiv; do 2 f_equal; nia). + (autorewrite with weight_to_pow pull_Zpow; + rewrite !Z.div_div, <-!Z.pow_add_r by (Core.zutil_arith || Z.zero_bounds); do 2 f_equal; nia). rewrite Z.div_between_0_if with (a:=x / 2^(k-1)) by (Z.zero_bounds; auto using q1_range). break_innermost_match; try lia; autorewrite with zsimplify_fast; [ | ]. { apply partition_eq_mod; auto with zarith. } @@ -437,6 +403,7 @@ Module Fancy. break_innermost_match; autorewrite with zsimplify; reflexivity). rewrite shiftr_correct by (rewrite ?Z.div_small, ?Z2Nat.inj_0 by lia; auto with zarith lia). autorewrite with weight_to_pow pull_Zpow pull_Zdiv. + rewrite !Z.div_div, <-!Z.pow_add_r by (Core.zutil_arith || Z.zero_bounds). congruence. Qed. diff --git a/src/Arithmetic/BaseConversion.v b/src/Arithmetic/BaseConversion.v index a22aa0c0b..c06dd3d71 100644 --- a/src/Arithmetic/BaseConversion.v +++ b/src/Arithmetic/BaseConversion.v @@ -1,66 +1,19 @@ - -(* TODO: prune these *) -Require Import Crypto.Algebra.Nsatz. -Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz. -Require Import Coq.Sorting.Mergesort Coq.Structures.Orders. -Require Import Coq.Sorting.Permutation. +Require Import Coq.ZArith.ZArith. Require Import Coq.derive.Derive. -Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *) -Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *) -Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable. -Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn. -Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil. -Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil. -Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop. -Require Import Crypto.Arithmetic.BarrettReduction.Generalized. -Require Import Crypto.Arithmetic.ModularArithmeticTheorems. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.Tactics.RunTacticAsConstr. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.OptionList. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Sum. -Require Import Crypto.Util.Bool. -Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. -Require Import Crypto.Util.ZUtil.Tactics.PeelLe. -Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute. -Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. -Require Import Crypto.Util.ZUtil.Modulo.PullPush. -Require Import Crypto.Util.ZUtil.Opp. -Require Import Crypto.Util.ZUtil.Log2. -Require Import Crypto.Util.ZUtil.Le. -Require Import Crypto.Util.ZUtil.Hints.PullPush. -Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.SubstEvars. +Require Import Coq.Lists.List. +Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.ModOps. +Require Import Crypto.Arithmetic.Partition. +Require Import Crypto.Arithmetic.Saturated. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.ListUtil. + Require Import Crypto.Util.Notations. -Require Import Crypto.Util.ZUtil.Definitions. -Require Import Crypto.Util.ZUtil.Sorting. -Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi. -Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo. -Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div. -Require Import Crypto.Util.ZUtil.Hints.PullPush. -Require Import Crypto.Util.ZUtil.EquivModulo. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.CPSNotations. -Require Import Crypto.Util.Equality. -Require Import Crypto.Util.Tactics.SetEvars. -Import Coq.Lists.List ListNotations. Local Open Scope Z_scope. +Local Open Scope Z_scope. Module BaseConversion. - Import Positional. Import Partition. + Import Positional. Section BaseConversion. - Hint Resolve Z.positive_is_nonzero Z.lt_gt Z.gt_lt. Context (sw dw : nat -> Z) (* source/destination weight functions *) {swprops : @weight_properties sw} {dwprops : @weight_properties dw}. @@ -74,8 +27,8 @@ Module BaseConversion. eval dw dn (convert_bases sn dn p) = eval sw sn p. Proof using dwprops. cbv [convert_bases]; intros. - rewrite eval_chained_carries_no_reduce by auto. - rewrite eval_from_associational; auto. + rewrite eval_chained_carries_no_reduce by auto with zarith. + rewrite eval_from_associational; auto with zarith. Qed. Lemma length_convert_bases sn dn p @@ -109,7 +62,7 @@ Module BaseConversion. @Associational.eval_mul @Positional.eval_to_associational Associational.eval_carryterm - @eval_convert_bases using solve [auto using Z.positive_is_nonzero] : push_eval. + @eval_convert_bases using solve [auto with zarith] : push_eval. Ltac push_eval := intros; autorewrite with push_eval; auto with zarith. @@ -132,7 +85,7 @@ Module BaseConversion. autorewrite with push_fold_right. break_match; push_eval. Qed. End reorder. - Hint Rewrite eval_reordering_carry using solve [auto using Z.positive_is_nonzero] : push_eval. + Hint Rewrite eval_reordering_carry using solve [auto with zarith] : push_eval. (* carry at specified indices in dw, then use Rows.flatten to convert to Positional with sw *) Definition from_associational idxs n (p : list (Z * Z)) : list Z := @@ -257,8 +210,6 @@ Module BaseConversion. Local Notation deval := (Positional.eval dw). Local Notation seval := (Positional.eval sw). - Hint Resolve Z.gt_lt Z.positive_is_nonzero Nat2Z.is_nonneg. - Definition widemul a b := mul_converted sw dw m m mn mn nout (aligned_carries n nout) a b. Lemma widemul_correct a b : diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index 23b796d8a..91e63af9f 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -1,73 +1,28 @@ (* Following http://adam.chlipala.net/theses/andreser.pdf chapter 3 *) Require Import Coq.ZArith.ZArith Coq.micromega.Lia. +Require Import Coq.Structures.Orders. Require Import Coq.Lists.List. Require Import Crypto.Algebra.Nsatz. +Require Import Crypto.Arithmetic.ModularArithmeticTheorems. +Require Import Crypto.Util.Decidable. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.NatUtil. Require Import Crypto.Util.Prod. -Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.Decidable.Bool2Prop. +Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.UniquePose. - -Require Import Crypto.Util.Notations. - -(* -Require Import Crypto.Algebra.Nsatz. -Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz. -Require Import Coq.Sorting.Mergesort Coq.Structures.Orders. -Require Import Coq.Sorting.Permutation. -Require Import Coq.derive.Derive. -Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *) -Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *) -Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable. -Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn. -Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil. -Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil. -Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop. -Require Import Crypto.Arithmetic.BarrettReduction.Generalized. -Require Import Crypto.Arithmetic.ModularArithmeticTheorems. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.Tactics.RunTacticAsConstr. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.OptionList. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Sum. -Require Import Crypto.Util.Bool. -Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. -Require Import Crypto.Util.ZUtil.Tactics.PeelLe. -Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute. -Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.EquivModulo. +Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Zselect. +Require Import Crypto.Util.ZUtil.Hints.Core. Require Import Crypto.Util.ZUtil.Modulo.PullPush. -Require Import Crypto.Util.ZUtil.Opp. -Require Import Crypto.Util.ZUtil.Log2. -Require Import Crypto.Util.ZUtil.Le. -Require Import Crypto.Util.ZUtil.Hints.PullPush. -Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.SubstEvars. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. Require Import Crypto.Util.Notations. -Require Import Crypto.Util.ZUtil.Definitions. -Require Import Crypto.Util.ZUtil.Sorting. -Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi. -Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo. -Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div. -Require Import Crypto.Util.ZUtil.Hints.PullPush. -Require Import Crypto.Util.ZUtil.EquivModulo. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.CPSNotations. -Require Import Crypto.Util.Equality. -Require Import Crypto.Util.Tactics.SetEvars. -Import Coq.Lists.List ListNotations. Local Open Scope Z_scope. -*) Import ListNotations. Local Open Scope Z_scope. Module Associational. diff --git a/src/Arithmetic/FancyMontgomeryReduction.v b/src/Arithmetic/FancyMontgomeryReduction.v index 54b6ddd5f..258b2327e 100644 --- a/src/Arithmetic/FancyMontgomeryReduction.v +++ b/src/Arithmetic/FancyMontgomeryReduction.v @@ -1,61 +1,31 @@ - -(* TODO: prune these *) -Require Import Crypto.Algebra.Nsatz. Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz. -Require Import Coq.Sorting.Mergesort Coq.Structures.Orders. -Require Import Coq.Sorting.Permutation. Require Import Coq.derive.Derive. -Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *) -Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *) -Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable. -Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn. -Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil. -Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil. -Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop. -Require Import Crypto.Arithmetic.BarrettReduction.Generalized. -Require Import Crypto.Arithmetic.ModularArithmeticTheorems. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.Tactics.RunTacticAsConstr. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.OptionList. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Sum. -Require Import Crypto.Util.Bool. -Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. -Require Import Crypto.Util.ZUtil.Tactics.PeelLe. -Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute. -Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. -Require Import Crypto.Util.ZUtil.Modulo.PullPush. -Require Import Crypto.Util.ZUtil.Opp. -Require Import Crypto.Util.ZUtil.Log2. -Require Import Crypto.Util.ZUtil.Le. -Require Import Crypto.Util.ZUtil.Hints.PullPush. -Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.SubstEvars. -Require Import Crypto.Util.Notations. +Require Import Coq.Lists.List. +Require Import Crypto.Arithmetic.BaseConversion. +Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.ModOps. +Require Import Crypto.Arithmetic.Partition. +Require Import Crypto.Arithmetic.Saturated. +Require Import Crypto.Arithmetic.UniformWeight. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. +Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. +Require Import Crypto.Util.Tactics.UniquePose. Require Import Crypto.Util.ZUtil.Definitions. -Require Import Crypto.Util.ZUtil.Sorting. -Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi. Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo. -Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil.Hints.Core. Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div. -Require Import Crypto.Util.ZUtil.Hints.PullPush. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Modulo.PullPush. Require Import Crypto.Util.ZUtil.EquivModulo. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.CPSNotations. -Require Import Crypto.Util.Equality. -Require Import Crypto.Util.Tactics.SetEvars. -Import Coq.Lists.List ListNotations. Local Open Scope Z_scope. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. + +Require Import Crypto.Util.Notations. +Import ListNotations. Local Open Scope Z_scope. Module MontgomeryReduction. Local Coercion Z.of_nat : nat >-> Z. @@ -65,23 +35,23 @@ Module MontgomeryReduction. (N'_good : Z.equiv_modulo R (N*N') (-1)) (R'_good: Z.equiv_modulo N (R*R') 1). Context (Zlog2R : Z) . - Let w : nat -> Z := weight Zlog2R 1. + Let w : nat -> Z := uweight Zlog2R. Context (n:nat) (Hn_nz: n <> 0%nat) (n_good : Zlog2R mod Z.of_nat n = 0). Context (R_big_enough : 2 <= Zlog2R) (R_two_pow : 2^Zlog2R = R). - Let w_mul : nat -> Z := weight (Zlog2R / n) 1. + Let w_mul : nat -> Z := uweight (Zlog2R / n). Definition montred' (lo hi : Z) := dlet_nd y := nth_default 0 (BaseConversion.widemul_inlined Zlog2R 1 2 [lo] [N']) 0 in dlet_nd t1_t2 := (BaseConversion.widemul_inlined_reverse Zlog2R 1 2 [N] [y]) in - dlet_nd sum_carry := Rows.add (weight Zlog2R 1) 2 [lo;hi] t1_t2 in + dlet_nd sum_carry := Rows.add w 2 [lo;hi] t1_t2 in dlet_nd y' := Z.zselect (snd sum_carry) 0 N in dlet_nd lo''_carry := Z.sub_get_borrow_full R (nth_default 0 (fst sum_carry) 1) y' in Z.add_modulo (fst lo''_carry) 0 N. Local Lemma Hw : forall i, w i = R ^ Z.of_nat i. Proof. - clear -R_big_enough R_two_pow; cbv [w weight]; intro. + clear -R_big_enough R_two_pow; cbv [w uweight weight]; intro. autorewrite with zsimplify. rewrite Z.pow_mul_r, R_two_pow by omega; reflexivity. Qed. diff --git a/src/Arithmetic/Freeze.v b/src/Arithmetic/Freeze.v new file mode 100644 index 000000000..d59812dea --- /dev/null +++ b/src/Arithmetic/Freeze.v @@ -0,0 +1,352 @@ +Require Import Coq.ZArith.ZArith Coq.micromega.Lia. +Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil. +Require Import Crypto.Arithmetic.BaseConversion. +Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.ModOps. +Require Import Crypto.Arithmetic.Saturated. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.Prod. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.ZUtil.EquivModulo. +Require Import Crypto.Util.ZUtil.Opp. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Tactics.PeelLe. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. + +Require Import Crypto.Util.Notations. +Local Open Scope Z_scope. + +(* TODO: rename this module? (Should it be, e.g., [Rows.freeze]?) *) +Module Freeze. + Section Freeze. + Context weight {wprops : @weight_properties weight}. + + Definition freeze n mask (m p:list Z) : list Z := + let '(p, carry) := Rows.sub weight n p m in + let '(r, carry) := Rows.conditional_add weight n mask (-carry) p m in + r. + + Lemma freezeZ m s c y : + m = s - c -> + 0 < c < s -> + s <> 0 -> + 0 <= y < 2*m -> + ((y - m) + (if (dec (-((y - m) / s) = 0)) then 0 else m)) mod s + = y mod m. + Proof using Type. + clear; intros. + transitivity ((y - m) mod m); + repeat first [ progress intros + | progress subst + | rewrite Z.opp_eq_0_iff in * + | break_innermost_match_step + | progress autorewrite with zsimplify_fast + | rewrite Z.div_small_iff in * by auto + | progress (Z.rewrite_mod_small; push_Zmod; Z.rewrite_mod_small) + | progress destruct_head'_or + | omega ]. + Qed. + + Lemma length_freeze n mask m p : + length m = n -> length p = n -> length (freeze n mask m p) = n. + Proof using wprops. + cbv [freeze Rows.conditional_add Rows.add]; eta_expand; intros. + distr_length; try assumption; cbn; intros; destruct_head'_or; destruct_head' False; subst; + distr_length. + erewrite Rows.length_sum_rows by (reflexivity || eassumption || distr_length); distr_length. + Qed. + Lemma eval_freeze_eq n mask m p + (n_nonzero:n<>0%nat) + (Hmask : List.map (Z.land mask) m = m) + (Hplen : length p = n) + (Hmlen : length m = n) + : Positional.eval weight n (@freeze n mask m p) + = (Positional.eval weight n p - Positional.eval weight n m + + (if dec (-((Positional.eval weight n p - Positional.eval weight n m) / weight n) = 0) then 0 else Positional.eval weight n m)) + mod weight n. + (*if dec ((Positional.eval weight n p - Positional.eval weight n m) / weight n = 0) + then Positional.eval weight n p - Positional.eval weight n m + else Positional.eval weight n p mod weight n.*) + Proof using wprops. + pose proof (@weight_positive weight wprops n). + cbv [freeze Z.equiv_modulo]; eta_expand. + repeat first [ solve [auto] + | rewrite Rows.conditional_add_partitions + | rewrite Rows.sub_partitions + | rewrite Rows.sub_div + | rewrite Partition.eval_partition + | progress distr_length + | progress pull_Zmod (* + | progress break_innermost_match_step + | progress destruct_head'_or + | omega + | f_equal; omega + | rewrite Z.div_small_iff in * by (auto using (@weight_positive weight ltac:(assumption))) + | progress Z.rewrite_mod_small *) ]. + Qed. + + Lemma eval_freeze n c mask m p + (n_nonzero:n<>0%nat) + (Hc : 0 < Associational.eval c < weight n) + (Hmask : List.map (Z.land mask) m = m) + (modulus:=weight n - Associational.eval c) + (Hm : Positional.eval weight n m = modulus) + (Hp : 0 <= Positional.eval weight n p < 2*modulus) + (Hplen : length p = n) + (Hmlen : length m = n) + : Positional.eval weight n (@freeze n mask m p) + = Positional.eval weight n p mod modulus. + Proof using wprops. + pose proof (@weight_positive weight wprops n). + rewrite eval_freeze_eq by assumption. + erewrite freezeZ; try eassumption; try omega. + f_equal; omega. + Qed. + + Lemma freeze_partitions n c mask m p + (n_nonzero:n<>0%nat) + (Hc : 0 < Associational.eval c < weight n) + (Hmask : List.map (Z.land mask) m = m) + (modulus:=weight n - Associational.eval c) + (Hm : Positional.eval weight n m = modulus) + (Hp : 0 <= Positional.eval weight n p < 2*modulus) + (Hplen : length p = n) + (Hmlen : length m = n) + : @freeze n mask m p = Partition.partition weight n (Positional.eval weight n p mod modulus). + Proof using wprops. + pose proof (@weight_positive weight wprops n). + pose proof (fun v => Z.mod_pos_bound v (weight n) ltac:(lia)). + pose proof (Z.mod_pos_bound (Positional.eval weight n p) modulus ltac:(lia)). + subst modulus. + erewrite <- eval_freeze by eassumption. + cbv [freeze]; eta_expand. + rewrite Rows.conditional_add_partitions by (auto; rewrite Rows.sub_partitions; auto; distr_length). + rewrite !Partition.eval_partition by assumption. + apply Partition.partition_Proper; [ assumption .. | ]. + cbv [Z.equiv_modulo]. + pull_Zmod; reflexivity. + Qed. + End Freeze. +End Freeze. +Hint Rewrite Freeze.length_freeze : distr_length. + +Section freeze_mod_ops. + Import Positional. + Import Freeze. + Local Coercion Z.of_nat : nat >-> Z. + Local Coercion QArith_base.inject_Z : Z >-> Q. + (* Design constraints: + - inputs must be [Z] (b/c reification does not support Q) + - internal structure must not match on the arguments (b/c reification does not support [positive]) *) + Context (limbwidth_num limbwidth_den : Z) + (limbwidth_good : 0 < limbwidth_den <= limbwidth_num) + (s : Z) + (c : list (Z*Z)) + (n : nat) + (bitwidth : Z) + (m_enc : list Z) + (m_nz:s - Associational.eval c <> 0) (s_nz:s <> 0) + (Hn_nz : n <> 0%nat). + Local Notation bytes_weight := (@weight 8 1). + Local Notation weight := (@weight limbwidth_num limbwidth_den). + Let m := (s - Associational.eval c). + + Context (Hs : s = weight n). + Context (c_small : 0 < Associational.eval c < weight n) + (m_enc_bounded : List.map (BinInt.Z.land (Z.ones bitwidth)) m_enc = m_enc) + (m_enc_correct : Positional.eval weight n m_enc = m) + (Hm_enc_len : length m_enc = n). + + Definition wprops_bytes := (@wprops 8 1 ltac:(clear; lia)). + Local Notation wprops := (@wprops limbwidth_num limbwidth_den limbwidth_good). + + Local Notation wunique := (@weight_unique limbwidth_num limbwidth_den limbwidth_good). + Local Notation wunique_bytes := (@weight_unique 8 1 ltac:(clear; lia)). + + Local Hint Immediate (wprops). + Local Hint Immediate (wprops_bytes). + Local Hint Immediate (weight_0 wprops). + Local Hint Immediate (weight_positive wprops). + Local Hint Immediate (weight_multiples wprops). + Local Hint Immediate (weight_divides wprops). + Local Hint Immediate (weight_0 wprops_bytes). + Local Hint Immediate (weight_positive wprops_bytes). + Local Hint Immediate (weight_multiples wprops_bytes). + Local Hint Immediate (weight_divides wprops_bytes). + Local Hint Immediate (wunique) (wunique_bytes). + Local Hint Resolve (wunique) (wunique_bytes). + + Definition bytes_n + := Eval cbv [Qceiling Qdiv inject_Z Qfloor Qmult Qopp Qnum Qden Qinv Pos.mul] + in Z.to_nat (Qceiling (Z.log2_up (weight n) / 8)). + + Lemma weight_bytes_weight_matches + : weight n <= bytes_weight bytes_n. + Proof using limbwidth_good. + clear -limbwidth_good. + cbv [weight bytes_n]. + autorewrite with zsimplify_const. + rewrite Z.log2_up_pow2, !Z2Nat.id, !Z.opp_involutive by (Z.div_mod_to_quot_rem; nia). + Z.peel_le. + Z.div_mod_to_quot_rem; nia. + Qed. + + Definition to_bytes (v : list Z) + := BaseConversion.convert_bases weight bytes_weight n bytes_n v. + + Definition from_bytes (v : list Z) + := BaseConversion.convert_bases bytes_weight weight bytes_n n v. + + Definition freeze_to_bytesmod (f : list Z) : list Z + := to_bytes (freeze weight n (Z.ones bitwidth) m_enc f). + + Definition to_bytesmod (f : list Z) : list Z + := to_bytes f. + + Definition from_bytesmod (f : list Z) : list Z + := from_bytes f. + + Lemma bytes_nz : bytes_n <> 0%nat. + Proof using limbwidth_good Hn_nz. + clear -limbwidth_good Hn_nz. + cbv [bytes_n]. + cbv [Qceiling Qdiv inject_Z Qfloor Qmult Qopp Qnum Qden Qinv]. + autorewrite with zsimplify_const. + change (Z.pos (1*8)) with 8. + cbv [weight]. + rewrite Z.log2_up_pow2 by (Z.div_mod_to_quot_rem; nia). + autorewrite with zsimplify_fast. + rewrite <- Z2Nat.inj_0, Z2Nat.inj_iff by (Z.div_mod_to_quot_rem; nia). + Z.div_mod_to_quot_rem; nia. + Qed. + + Lemma bytes_n_big : weight n <= bytes_weight bytes_n. + Proof using limbwidth_good Hn_nz. + clear -limbwidth_good Hn_nz. + cbv [bytes_n bytes_weight]. + Z.peel_le. + rewrite Z.log2_up_pow2 by (Z.div_mod_to_quot_rem; nia). + autorewrite with zsimplify_fast. + rewrite Z2Nat.id by (Z.div_mod_to_quot_rem; nia). + Z.div_mod_to_quot_rem; nia. + Qed. + + Lemma eval_to_bytes + : forall (f : list Z) + (Hf : length f = n), + eval bytes_weight bytes_n (to_bytes f) = eval weight n f. + Proof using limbwidth_good Hn_nz. + generalize wprops wprops_bytes; clear -Hn_nz limbwidth_good. + intros. + cbv [to_bytes]. + rewrite BaseConversion.eval_convert_bases + by (auto using bytes_nz; distr_length; auto using wprops). + reflexivity. + Qed. + + Lemma to_bytes_partitions + : forall (f : list Z) + (Hf : length f = n) + (Hf_small : 0 <= eval weight n f < weight n), + to_bytes f = Partition.partition bytes_weight bytes_n (Positional.eval weight n f). + Proof using Hn_nz limbwidth_good. + clear -Hn_nz limbwidth_good. + intros; cbv [to_bytes]. + pose proof weight_bytes_weight_matches. + apply BaseConversion.convert_bases_partitions; eauto; lia. + Qed. + + Lemma eval_to_bytesmod + : forall (f : list Z) + (Hf : length f = n) + (Hf_small : 0 <= eval weight n f < weight n), + eval bytes_weight bytes_n (to_bytesmod f) = eval weight n f + /\ to_bytesmod f = Partition.partition bytes_weight bytes_n (Positional.eval weight n f). + Proof using Hn_nz limbwidth_good. + split; apply eval_to_bytes || apply to_bytes_partitions; assumption. + Qed. + + Lemma eval_freeze_to_bytesmod_and_partitions + : forall (f : list Z) + (Hf : length f = n) + (Hf_bounded : 0 <= eval weight n f < 2 * m), + (eval bytes_weight bytes_n (freeze_to_bytesmod f)) = (eval weight n f) mod m + /\ freeze_to_bytesmod f = Partition.partition bytes_weight bytes_n (Positional.eval weight n f mod m). + Proof using m_enc_correct Hs limbwidth_good Hn_nz c_small Hm_enc_len m_enc_bounded. + clear -m_enc_correct Hs limbwidth_good Hn_nz c_small Hm_enc_len m_enc_bounded. + intros; subst m s. + cbv [freeze_to_bytesmod]. + rewrite eval_to_bytes, to_bytes_partitions; + erewrite ?eval_freeze by eauto using wprops; + autorewrite with distr_length; eauto. + Z.div_mod_to_quot_rem; nia. + Qed. + + Lemma eval_freeze_to_bytesmod + : forall (f : list Z) + (Hf : length f = n) + (Hf_bounded : 0 <= eval weight n f < 2 * m), + (eval bytes_weight bytes_n (freeze_to_bytesmod f)) = (eval weight n f) mod m. + Proof using m_enc_correct Hs limbwidth_good Hn_nz c_small Hm_enc_len m_enc_bounded. + intros; now apply eval_freeze_to_bytesmod_and_partitions. + Qed. + + Lemma freeze_to_bytesmod_partitions + : forall (f : list Z) + (Hf : length f = n) + (Hf_bounded : 0 <= eval weight n f < 2 * m), + freeze_to_bytesmod f = Partition.partition bytes_weight bytes_n (Positional.eval weight n f mod m). + Proof using m_enc_correct Hs limbwidth_good Hn_nz c_small Hm_enc_len m_enc_bounded. + intros; now apply eval_freeze_to_bytesmod_and_partitions. + Qed. + + Lemma eval_from_bytes + : forall (f : list Z) + (Hf : length f = bytes_n), + eval weight n (from_bytes f) = eval bytes_weight bytes_n f. + Proof using limbwidth_good Hn_nz. + generalize wprops wprops_bytes; clear -Hn_nz limbwidth_good. + intros. + cbv [from_bytes]. + rewrite BaseConversion.eval_convert_bases + by (auto using bytes_nz; distr_length; auto using wprops). + reflexivity. + Qed. + + Lemma from_bytes_partitions + : forall (f : list Z) + (Hf_small : 0 <= eval bytes_weight bytes_n f < weight n), + from_bytes f = Partition.partition weight n (Positional.eval bytes_weight bytes_n f). + Proof using limbwidth_good. + clear -limbwidth_good. + intros; cbv [from_bytes]. + pose proof weight_bytes_weight_matches. + apply BaseConversion.convert_bases_partitions; eauto; lia. + Qed. + + Lemma eval_from_bytesmod + : forall (f : list Z) + (Hf : length f = bytes_n), + eval weight n (from_bytesmod f) = eval bytes_weight bytes_n f. + Proof using Hn_nz limbwidth_good. apply eval_from_bytes. Qed. + + Lemma from_bytesmod_partitions + : forall (f : list Z) + (Hf_small : 0 <= eval bytes_weight bytes_n f < weight n), + from_bytesmod f = Partition.partition weight n (Positional.eval bytes_weight bytes_n f). + Proof using limbwidth_good. apply from_bytes_partitions. Qed. + + Lemma eval_from_bytesmod_and_partitions + : forall (f : list Z) + (Hf : length f = bytes_n) + (Hf_small : 0 <= eval bytes_weight bytes_n f < weight n), + eval weight n (from_bytesmod f) = eval bytes_weight bytes_n f + /\ from_bytesmod f = Partition.partition weight n (Positional.eval bytes_weight bytes_n f). + Proof using limbwidth_good Hn_nz. + now (split; [ apply eval_from_bytesmod | apply from_bytes_partitions ]). + Qed. +End freeze_mod_ops. +Hint Rewrite eval_freeze_to_bytesmod eval_to_bytes eval_to_bytesmod eval_from_bytes eval_from_bytesmod : push_eval. \ No newline at end of file diff --git a/src/Arithmetic/ModOps.v b/src/Arithmetic/ModOps.v index 414c490aa..49f99f4fe 100644 --- a/src/Arithmetic/ModOps.v +++ b/src/Arithmetic/ModOps.v @@ -1,61 +1,13 @@ -(* TODO: prune these *) -Require Import Crypto.Algebra.Nsatz. -Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz. -Require Import Coq.Sorting.Mergesort Coq.Structures.Orders. -Require Import Coq.Sorting.Permutation. +Require Import Coq.ZArith.ZArith Coq.micromega.Lia. Require Import Coq.derive.Derive. -Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *) -Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *) -Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable. -Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn. -Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil. Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil. -Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop. -Require Import Crypto.Arithmetic.BarrettReduction.Generalized. Require Import Crypto.Arithmetic.Core. -Require Import Crypto.Arithmetic.ModularArithmeticTheorems. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.Tactics.RunTacticAsConstr. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.OptionList. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Sum. -Require Import Crypto.Util.Bool. -Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. -Require Import Crypto.Util.ZUtil.Tactics.PeelLe. -Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute. -Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. -Require Import Crypto.Util.ZUtil.Modulo.PullPush. -Require Import Crypto.Util.ZUtil.Opp. -Require Import Crypto.Util.ZUtil.Log2. -Require Import Crypto.Util.ZUtil.Le. -Require Import Crypto.Util.ZUtil.Hints.PullPush. -Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. +Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.SubstEvars. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. + Require Import Crypto.Util.Notations. -Require Import Crypto.Util.ZUtil.Definitions. -Require Import Crypto.Util.ZUtil.Sorting. -Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi. -Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo. -Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div. -Require Import Crypto.Util.ZUtil.Hints.PullPush. -Require Import Crypto.Util.ZUtil.EquivModulo. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.CPSNotations. -Require Import Crypto.Util.Equality. -Require Import Crypto.Util.Tactics.SetEvars. -Import Coq.Lists.List ListNotations. Local Open Scope Z_scope. +Local Open Scope Z_scope. Section mod_ops. Import Positional. diff --git a/src/Arithmetic/Partition.v b/src/Arithmetic/Partition.v index 4c62124bf..2d2fb87fa 100644 --- a/src/Arithmetic/Partition.v +++ b/src/Arithmetic/Partition.v @@ -1,64 +1,13 @@ - -(* TODO: prune these *) -Require Import Crypto.Algebra.Nsatz. -Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz. -Require Import Coq.Sorting.Mergesort Coq.Structures.Orders. -Require Import Coq.Sorting.Permutation. -Require Import Coq.derive.Derive. -Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *) -Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *) -Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable. -Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn. -Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil. -Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil. -Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop. +Require Import Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Require Import Coq.Structures.Orders. Require Import Crypto.Arithmetic.Core. -Require Import Crypto.Arithmetic.BarrettReduction.Generalized. -Require Import Crypto.Arithmetic.ModularArithmeticTheorems. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.Tactics.RunTacticAsConstr. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.OptionList. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Sum. -Require Import Crypto.Util.Bool. -Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. -Require Import Crypto.Util.ZUtil.Tactics.PeelLe. -Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute. -Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. -Require Import Crypto.Util.ZUtil.Modulo.PullPush. -Require Import Crypto.Util.ZUtil.Opp. -Require Import Crypto.Util.ZUtil.Log2. -Require Import Crypto.Util.ZUtil.Le. -Require Import Crypto.Util.ZUtil.Hints.PullPush. -Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.SubstEvars. -Require Import Crypto.Util.Notations. -Require Import Crypto.Util.ZUtil.Definitions. -Require Import Crypto.Util.ZUtil.Sorting. -Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi. -Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo. -Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div. -Require Import Crypto.Util.ZUtil.Hints.PullPush. +Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.ZUtil.EquivModulo. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.CPSNotations. -Require Import Crypto.Util.Equality. -Require Import Crypto.Util.Tactics.SetEvars. -Import Coq.Lists.List ListNotations. Local Open Scope Z_scope. +Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div. -Import Weight. +Require Import Crypto.Util.Notations. +Import ListNotations Weight. Local Open Scope Z_scope. Section Partition. Context weight {wprops : @weight_properties weight}. @@ -82,8 +31,8 @@ Section Partition. Proof using wprops. induction n; intros. { cbn. rewrite (weight_0); auto with zarith. } - { rewrite (Z.div_mod (x mod weight (S n)) (weight n)) by auto. - rewrite <-Znumtheory.Zmod_div_mod by (try apply Z.mod_divide; auto). + { rewrite (Z.div_mod (x mod weight (S n)) (weight n)) by auto with zarith. + rewrite <-Znumtheory.Zmod_div_mod by (try apply Z.mod_divide; auto with zarith). rewrite partition_step, Positional.eval_snoc with (n:=n) by distr_length. omega. } Qed. @@ -96,11 +45,11 @@ Section Partition. { reflexivity. } { assert (Hxyn : x mod weight n = y mod weight n). { erewrite (Znumtheory.Zmod_div_mod _ (weight (S n)) x), (Znumtheory.Zmod_div_mod _ (weight (S n)) y), Hxy - by (try apply Z.mod_divide; auto); + by (try apply Z.mod_divide; auto with zarith); reflexivity. } rewrite !partition_step, IHn by eauto. - rewrite (Z.div_mod (x mod weight (S n)) (weight n)), (Z.div_mod (y mod weight (S n)) (weight n)) by auto. - rewrite <-!Znumtheory.Zmod_div_mod by (try apply Z.mod_divide; auto). + rewrite (Z.div_mod (x mod weight (S n)) (weight n)), (Z.div_mod (y mod weight (S n)) (weight n)) by auto with zarith. + rewrite <-!Znumtheory.Zmod_div_mod by (try apply Z.mod_divide; auto with zarith). rewrite Hxy, Hxyn; reflexivity. } Qed. @@ -135,8 +84,8 @@ Section Partition. pose proof (@weight_divides _ wprops j). f_equal; repeat match goal with - | _ => rewrite Z.mod_pull_div by auto using Z.lt_le_incl - | _ => rewrite weight_multiples by auto + | _ => rewrite Z.mod_pull_div by auto with zarith + | _ => rewrite weight_multiples by auto with zarith | _ => progress autorewrite with zsimplify_fast zdiv_to_mod pull_Zdiv | _ => reflexivity end. diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v index c0fe26a43..c82f6afa9 100644 --- a/src/Arithmetic/Saturated.v +++ b/src/Arithmetic/Saturated.v @@ -1,147 +1,109 @@ - -(* TODO: prune these *) -Require Import Crypto.Algebra.Nsatz. -Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz. -Require Import Coq.Sorting.Mergesort Coq.Structures.Orders. -Require Import Coq.Sorting.Permutation. -Require Import Coq.derive.Derive. -Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *) -Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *) -Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable. -Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn. -Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil. -Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil. -Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop. -Require Import Crypto.Arithmetic.BarrettReduction.Generalized. -Require Import Crypto.Arithmetic.ModularArithmeticTheorems. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.Tactics.RunTacticAsConstr. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.OptionList. +Require Import Coq.ZArith.ZArith Coq.micromega.Lia. +Require Import Coq.Lists.List. +Require Import Crypto.Algebra.Ring. +Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.Partition. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.NatUtil. Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Sum. -Require Import Crypto.Util.Bool. -Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. -Require Import Crypto.Util.ZUtil.Tactics.PeelLe. -Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute. -Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. -Require Import Crypto.Util.ZUtil.Modulo.PullPush. -Require Import Crypto.Util.ZUtil.Opp. -Require Import Crypto.Util.ZUtil.Log2. -Require Import Crypto.Util.ZUtil.Le. -Require Import Crypto.Util.ZUtil.Hints.PullPush. -Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.SubstEvars. -Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.UniquePose. Require Import Crypto.Util.ZUtil.Definitions. -Require Import Crypto.Util.ZUtil.Sorting. -Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi. -Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo. Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil.Hints.Core. Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div. -Require Import Crypto.Util.ZUtil.Hints.PullPush. -Require Import Crypto.Util.ZUtil.EquivModulo. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.CPSNotations. -Require Import Crypto.Util.Equality. -Require Import Crypto.Util.Tactics.SetEvars. -Import Coq.Lists.List ListNotations. Local Open Scope Z_scope. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Module Saturated. - Module Associational. - Section Associational. +Require Import Crypto.Util.Notations. +Import ListNotations. Local Open Scope Z_scope. - Definition sat_multerm s (t t' : (Z * Z)) : list (Z * Z) := - dlet_nd xy := Z.mul_split s (snd t) (snd t') in - [(fst t * fst t', fst xy); (fst t * fst t' * s, snd xy)]. +Module Associational. + Section Associational. - Definition sat_mul s (p q : list (Z * Z)) : list (Z * Z) := - flat_map (fun t => flat_map (fun t' => sat_multerm s t t') q) p. + Definition sat_multerm s (t t' : (Z * Z)) : list (Z * Z) := + dlet_nd xy := Z.mul_split s (snd t) (snd t') in + [(fst t * fst t', fst xy); (fst t * fst t' * s, snd xy)]. - Lemma eval_map_sat_multerm s a q (s_nonzero:s<>0): - Associational.eval (flat_map (sat_multerm s a) q) = fst a * snd a * Associational.eval q. - Proof using Type. - cbv [sat_multerm Let_In]; induction q; - repeat match goal with - | _ => progress autorewrite with cancel_pair push_eval to_div_mod in * - | _ => progress simpl flat_map - | _ => rewrite IHq - | _ => rewrite Z.mod_eq by assumption - | _ => ring_simplify; omega - end. - Qed. - Hint Rewrite eval_map_sat_multerm using (omega || assumption) : push_eval. + Definition sat_mul s (p q : list (Z * Z)) : list (Z * Z) := + flat_map (fun t => flat_map (fun t' => sat_multerm s t t') q) p. - Lemma eval_sat_mul s p q (s_nonzero:s<>0): - Associational.eval (sat_mul s p q) = Associational.eval p * Associational.eval q. - Proof using Type. - cbv [sat_mul]; induction p; [reflexivity|]. + Lemma eval_map_sat_multerm s a q (s_nonzero:s<>0): + Associational.eval (flat_map (sat_multerm s a) q) = fst a * snd a * Associational.eval q. + Proof using Type. + cbv [sat_multerm Let_In]; induction q; repeat match goal with - | _ => progress (autorewrite with push_flat_map push_eval in * ) - | _ => rewrite IHp + | _ => progress autorewrite with cancel_pair push_eval to_div_mod in * + | _ => progress simpl flat_map + | _ => rewrite IHq + | _ => rewrite Z.mod_eq by assumption | _ => ring_simplify; omega end. - Qed. - Hint Rewrite eval_sat_mul : push_eval. - - Definition sat_multerm_const s (t t' : (Z * Z)) : list (Z * Z) := - if snd t =? 1 - then [(fst t * fst t', snd t')] - else if snd t =? -1 - then [(fst t * fst t', - snd t')] - else if snd t =? 0 - then nil - else dlet_nd xy := Z.mul_split s (snd t) (snd t') in - [(fst t * fst t', fst xy); (fst t * fst t' * s, snd xy)]. - - Definition sat_mul_const s (p q : list (Z * Z)) : list (Z * Z) := - flat_map (fun t => flat_map (fun t' => sat_multerm_const s t t') q) p. - - Lemma eval_map_sat_multerm_const s a q (s_nonzero:s<>0): - Associational.eval (flat_map (sat_multerm_const s a) q) = fst a * snd a * Associational.eval q. - Proof using Type. - cbv [sat_multerm_const Let_In]; induction q; - repeat match goal with - | _ => progress autorewrite with cancel_pair push_eval to_div_mod in * - | _ => progress simpl flat_map - | H : _ = 1 |- _ => rewrite H - | H : _ = -1 |- _ => rewrite H - | H : _ = 0 |- _ => rewrite H - | _ => progress break_match; Z.ltb_to_lt - | _ => rewrite IHq - | _ => rewrite Z.mod_eq by assumption - | _ => ring_simplify; omega - end. - Qed. - Hint Rewrite eval_map_sat_multerm_const using (omega || assumption) : push_eval. + Qed. + Hint Rewrite eval_map_sat_multerm using (omega || assumption) : push_eval. - Lemma eval_sat_mul_const s p q (s_nonzero:s<>0): - Associational.eval (sat_mul_const s p q) = Associational.eval p * Associational.eval q. - Proof using Type. - cbv [sat_mul_const]; induction p; [reflexivity|]. + Lemma eval_sat_mul s p q (s_nonzero:s<>0): + Associational.eval (sat_mul s p q) = Associational.eval p * Associational.eval q. + Proof using Type. + cbv [sat_mul]; induction p; [reflexivity|]. + repeat match goal with + | _ => progress (autorewrite with push_flat_map push_eval in * ) + | _ => rewrite IHp + | _ => ring_simplify; omega + end. + Qed. + Hint Rewrite eval_sat_mul : push_eval. + + Definition sat_multerm_const s (t t' : (Z * Z)) : list (Z * Z) := + if snd t =? 1 + then [(fst t * fst t', snd t')] + else if snd t =? -1 + then [(fst t * fst t', - snd t')] + else if snd t =? 0 + then nil + else dlet_nd xy := Z.mul_split s (snd t) (snd t') in + [(fst t * fst t', fst xy); (fst t * fst t' * s, snd xy)]. + + Definition sat_mul_const s (p q : list (Z * Z)) : list (Z * Z) := + flat_map (fun t => flat_map (fun t' => sat_multerm_const s t t') q) p. + + Lemma eval_map_sat_multerm_const s a q (s_nonzero:s<>0): + Associational.eval (flat_map (sat_multerm_const s a) q) = fst a * snd a * Associational.eval q. + Proof using Type. + cbv [sat_multerm_const Let_In]; induction q; repeat match goal with - | _ => progress (autorewrite with push_flat_map push_eval in * ) - | _ => rewrite IHp + | _ => progress autorewrite with cancel_pair push_eval to_div_mod in * + | _ => progress simpl flat_map + | H : _ = 1 |- _ => rewrite H + | H : _ = -1 |- _ => rewrite H + | H : _ = 0 |- _ => rewrite H + | _ => progress break_match; Z.ltb_to_lt + | _ => rewrite IHq + | _ => rewrite Z.mod_eq by assumption | _ => ring_simplify; omega end. - Qed. - Hint Rewrite eval_sat_mul_const : push_eval. - End Associational. + Qed. + Hint Rewrite eval_map_sat_multerm_const using (omega || assumption) : push_eval. + + Lemma eval_sat_mul_const s p q (s_nonzero:s<>0): + Associational.eval (sat_mul_const s p q) = Associational.eval p * Associational.eval q. + Proof using Type. + cbv [sat_mul_const]; induction p; [reflexivity|]. + repeat match goal with + | _ => progress (autorewrite with push_flat_map push_eval in * ) + | _ => rewrite IHp + | _ => ring_simplify; omega + end. + Qed. + Hint Rewrite eval_sat_mul_const : push_eval. End Associational. -End Saturated. +End Associational. Module Columns. - Import Saturated. Import Partition. Import Weight. + Import Weight. Section Columns. Context weight {wprops : @weight_properties weight}. @@ -375,10 +337,9 @@ Module Columns. End Columns. Module Rows. - Import Saturated. Import Partition. Import Weight. + Import Weight. Section Rows. Context weight {wprops : @weight_properties weight}. - Hint Resolve Z.positive_is_nonzero Z.lt_gt. Local Notation rows := (list (list Z)) (only parsing). Local Notation cols := (list (list Z)) (only parsing). @@ -714,7 +675,7 @@ Module Rows. | _ => rewrite partition_step by auto | _ => rewrite weight_div_pull_div by auto | _ => rewrite weight_mod_pull_div by auto - | _ => rewrite <-Z.div_add' by auto + | _ => rewrite <-Z.div_add' by auto with zarith | _ => progress push end. f_equal; push; [ ]. @@ -802,9 +763,9 @@ Module Rows. | _ => rewrite IHinp by push; clear IHinp | |- pair _ _ = pair _ _ => f_equal | _ => apply (@partition_eq_mod _ wprops) - | _ => rewrite <-Z.div_add_l' by auto + | _ => rewrite <-Z.div_add_l' by auto with zarith | _ => rewrite Z.mod_add'_full by omega - | _ => rewrite Z.mul_div_eq_full by auto + | _ => rewrite Z.mul_div_eq_full by auto with zarith | _ => progress (push_Zmod; pull_Zmod) | _ => progress push end. @@ -980,7 +941,7 @@ Module Rows. rewrite Z.div_sub_small, Z.ltb_antisym by omega. destruct (Positional.eval weight n q <=? Positional.eval weight n p); cbn [negb]; autorewrite with zsimplify_fast; - break_match; congruence. + break_match; try lia; congruence. Qed. Let sub_then_maybe_add_Z a b c := @@ -1028,7 +989,7 @@ Module Rows. cbv [adjust_s]; rewrite fold_right_map; generalize (List.rev (seq 0 fuel)); intro ls; induction ls as [|l ls IHls]; cbn. { rewrite Z.mod_same by assumption; auto. } - { break_match; cbn in *; auto. } + { break_match; cbn in *; auto with zarith. } Qed. Lemma eval_sat_reduce base s c n p : @@ -1064,7 +1025,7 @@ Module Rows. Proof using wprops. solver. cbn [fst snd]. rewrite eval_partition by auto. - rewrite <-Z.div_mod'' by auto. + rewrite <-Z.div_mod'' by auto with zarith. autorewrite with push_eval; reflexivity. Qed. diff --git a/src/Arithmetic/UniformWeight.v b/src/Arithmetic/UniformWeight.v index b880f384e..9af083994 100644 --- a/src/Arithmetic/UniformWeight.v +++ b/src/Arithmetic/UniformWeight.v @@ -1,61 +1,18 @@ - -(* TODO: prune these *) -Require Import Crypto.Algebra.Nsatz. -Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz. -Require Import Coq.Sorting.Mergesort Coq.Structures.Orders. -Require Import Coq.Sorting.Permutation. -Require Import Coq.derive.Derive. -Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *) -Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *) -Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable. -Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn. -Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil. -Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil. -Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop. -Require Import Crypto.Arithmetic.BarrettReduction.Generalized. -Require Import Crypto.Arithmetic.ModularArithmeticTheorems. -Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.Tactics.RunTacticAsConstr. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.OptionList. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Sum. -Require Import Crypto.Util.Bool. -Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. -Require Import Crypto.Util.ZUtil.Tactics.PeelLe. -Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute. -Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. -Require Import Crypto.Util.ZUtil.Modulo.PullPush. -Require Import Crypto.Util.ZUtil.Opp. -Require Import Crypto.Util.ZUtil.Log2. -Require Import Crypto.Util.ZUtil.Le. -Require Import Crypto.Util.ZUtil.Hints.PullPush. -Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Coq.ZArith.ZArith Coq.micromega.Lia. +Require Import Coq.Lists.List. +Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.ModOps. +Require Import Crypto.Arithmetic.Partition. +Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.SubstEvars. -Require Import Crypto.Util.Notations. -Require Import Crypto.Util.ZUtil.Definitions. -Require Import Crypto.Util.ZUtil.Sorting. -Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi. -Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo. -Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil.Hints.Core. Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div. -Require Import Crypto.Util.ZUtil.Hints.PullPush. -Require Import Crypto.Util.ZUtil.EquivModulo. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.CPSNotations. -Require Import Crypto.Util.Equality. -Require Import Crypto.Util.Tactics.SetEvars. -Import Coq.Lists.List ListNotations. Local Open Scope Z_scope. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. + +Require Import Crypto.Util.Notations. +Local Open Scope Z_scope. +Import Weight. Definition uweight (lgr : Z) : nat -> Z := weight lgr 1. @@ -76,14 +33,14 @@ Proof using Type. rewrite !Positional.eval_snoc with (n:=n) by distr_length. rewrite IHxs, !uweight_eq_alt by omega. autorewrite with push_Zof_nat push_Zpow. - rewrite !Z.pow_succ_r by auto using Nat2Z.is_nonneg. + rewrite !Z.pow_succ_r by auto with zarith. ring. Qed. Lemma uweight_S lgr (Hr : 0 <= lgr) n : uweight lgr (S n) = 2 ^ lgr * uweight lgr n. Proof using Type. rewrite !uweight_eq_alt by auto. autorewrite with push_Zof_nat. - rewrite Z.pow_succ_r by auto using Nat2Z.is_nonneg. + rewrite Z.pow_succ_r by auto with zarith. reflexivity. Qed. Lemma uweight_double_le lgr (Hr : 0 < lgr) n : uweight lgr n + uweight lgr n <= uweight lgr (S n). diff --git a/src/Arithmetic/WordByWordMontgomery.v b/src/Arithmetic/WordByWordMontgomery.v index f52dbdeb1..2477d212e 100644 --- a/src/Arithmetic/WordByWordMontgomery.v +++ b/src/Arithmetic/WordByWordMontgomery.v @@ -1,65 +1,36 @@ - -(* TODO: prune these *) -Require Import Crypto.Algebra.Nsatz. -Require Import Coq.ZArith.ZArith Coq.micromega.Lia Crypto.Algebra.Nsatz. -Require Import Coq.Sorting.Mergesort Coq.Structures.Orders. -Require Import Coq.Sorting.Permutation. -Require Import Coq.derive.Derive. -Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. (* For MontgomeryReduction *) -Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. (* For MontgomeryReduction *) -Require Import Crypto.Util.Tactics.UniquePose Crypto.Util.Decidable. -Require Import Crypto.Util.Tuple Crypto.Util.Prod Crypto.Util.LetIn. -Require Import Crypto.Util.ListUtil Coq.Lists.List Crypto.Util.NatUtil. -Require Import QArith.QArith_base QArith.Qround Crypto.Util.QUtil. -Require Import Crypto.Algebra.Ring Crypto.Util.Decidable.Bool2Prop. -Require Import Crypto.Arithmetic.BarrettReduction.Generalized. +Require Import Coq.ZArith.ZArith Coq.micromega.Lia. +Require Import Coq.Lists.List. +Require Import Crypto.Algebra.Ring. +Require Import Crypto.Arithmetic.Core. +Require Import Crypto.Arithmetic.Freeze. Require Import Crypto.Arithmetic.ModularArithmeticTheorems. +Require Import Crypto.Arithmetic.Partition. Require Import Crypto.Arithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.Tactics.RunTacticAsConstr. -Require Import Crypto.Util.Tactics.Head. -Require Import Crypto.Util.Option. -Require Import Crypto.Util.OptionList. +Require Import Crypto.Arithmetic.Saturated. +Require Import Crypto.Arithmetic.UniformWeight. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.Prod. -Require Import Crypto.Util.Sum. -Require Import Crypto.Util.Bool. Require Import Crypto.Util.Sigma. -Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. -Require Import Crypto.Util.ZUtil.Tactics.PeelLe. -Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute. -Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. -Require Import Crypto.Util.ZUtil.Modulo.PullPush. -Require Import Crypto.Util.ZUtil.Opp. -Require Import Crypto.Util.ZUtil.Log2. -Require Import Crypto.Util.ZUtil.Le. -Require Import Crypto.Util.ZUtil.Hints.PullPush. +Require Import Crypto.Util.Tactics.SetEvars. +Require Import Crypto.Util.Tactics.SubstEvars. +Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.EquivModulo. Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. +Require Import Crypto.Util.ZUtil.Modulo.PullPush. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Tactics.LinearSubstitute. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Tactics.PeelLe. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. -Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.SplitInContext. -Require Import Crypto.Util.Tactics.SubstEvars. + Require Import Crypto.Util.Notations. -Require Import Crypto.Util.ZUtil.Definitions. -Require Import Crypto.Util.ZUtil.Sorting. -Require Import Crypto.Util.ZUtil.CC Crypto.Util.ZUtil.Rshi. -Require Import Crypto.Util.ZUtil.Zselect Crypto.Util.ZUtil.AddModulo. -Require Import Crypto.Util.ZUtil.AddGetCarry Crypto.Util.ZUtil.MulSplit. -Require Import Crypto.Util.ZUtil.Hints.Core. -Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div. -Require Import Crypto.Util.ZUtil.Hints.PullPush. -Require Import Crypto.Util.ZUtil.EquivModulo. -Require Import Crypto.Util.Prod. -Require Import Crypto.Util.CPSNotations. -Require Import Crypto.Util.Equality. -Require Import Crypto.Util.Tactics.SetEvars. -Import Coq.Lists.List ListNotations. Local Open Scope Z_scope. +Import ListNotations. Local Open Scope Z_scope. Module WordByWordMontgomery. - Import Partition. - Local Hint Resolve Z.positive_is_nonzero Z.lt_gt Nat2Z.is_nonneg. Section with_args. Context (lgr : Z) (m : Z). @@ -201,14 +172,14 @@ Module WordByWordMontgomery. auto with zarith. Qed. - Let partition_Proper := (@partition_Proper _ wprops). + Let partition_Proper := (@Partition.partition_Proper _ wprops). Local Existing Instance partition_Proper. Lemma eval_nonzero n A : @small n A -> nonzero A = 0 <-> @eval n A = 0. Proof using lgr_big. clear -lgr_big partition_Proper. cbv [nonzero eval small]; intro Heq. do 2 rewrite Heq. - rewrite !eval_partition, Z.mod_mod by auto. + rewrite !eval_partition, Z.mod_mod by auto with zarith. generalize (Positional.eval weight n A); clear Heq A. induction n as [|n IHn]. { cbn; rewrite weight_0 by auto; intros; autorewrite with zsimplify_const; omega. } @@ -229,7 +200,7 @@ Module WordByWordMontgomery. rewrite <- !Z.mul_add_distr_l, Z.mul_eq_0. nia. } rewrite Heq at 1; rewrite IHn. - rewrite Z.mod_mod by auto. + rewrite Z.mod_mod by auto with zarith. generalize (weight_multiples ltac:(auto) n). generalize (weight_positive ltac:(auto) n). generalize (weight_positive ltac:(auto) (S n)). -- cgit v1.2.3