diff options
Diffstat (limited to 'src/Arithmetic')
| -rw-r--r-- | src/Arithmetic/BarrettReduction/Generalized.v | 20 | ||||
| -rw-r--r-- | src/Arithmetic/BarrettReduction/HAC.v | 12 | ||||
| -rw-r--r-- | src/Arithmetic/BarrettReduction/RidiculousFish.v | 2 | ||||
| -rw-r--r-- | src/Arithmetic/BarrettReduction/Wikipedia.v | 8 | ||||
| -rw-r--r-- | src/Arithmetic/Core.v | 4 | ||||
| -rw-r--r-- | src/Arithmetic/Karatsuba.v | 3 | ||||
| -rw-r--r-- | src/Arithmetic/ModularArithmeticTheorems.v | 4 | ||||
| -rw-r--r-- | src/Arithmetic/MontgomeryReduction/Definition.v | 2 | ||||
| -rw-r--r-- | src/Arithmetic/MontgomeryReduction/Proofs.v | 4 | ||||
| -rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v | 10 | ||||
| -rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v | 10 | ||||
| -rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v | 1 | ||||
| -rw-r--r-- | src/Arithmetic/PrimeFieldTheorems.v | 23 | ||||
| -rw-r--r-- | src/Arithmetic/Saturated/Core.v | 9 | ||||
| -rw-r--r-- | src/Arithmetic/Saturated/Freeze.v | 4 | ||||
| -rw-r--r-- | src/Arithmetic/Saturated/MontgomeryAPI.v | 8 | ||||
| -rw-r--r-- | src/Arithmetic/Saturated/UniformWeight.v | 6 |
17 files changed, 94 insertions, 36 deletions
diff --git a/src/Arithmetic/BarrettReduction/Generalized.v b/src/Arithmetic/BarrettReduction/Generalized.v index 9fa37721a..c2885bc77 100644 --- a/src/Arithmetic/BarrettReduction/Generalized.v +++ b/src/Arithmetic/BarrettReduction/Generalized.v @@ -9,7 +9,15 @@ base ([b]), exponent ([k]), and the [offset] than those given in the HAC. *) Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. -Require Import Crypto.Util.ZUtil Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Modulo. +Require Import Crypto.Util.ZUtil.Pow. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.ZUtil.Tactics.SimplifyFractionsLe. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.ZSimplify. +Require Import Crypto.Util.Tactics.BreakMatch. Local Open Scope Z_scope. @@ -94,17 +102,17 @@ Section barrett. : q * n <= a. Proof using a_nonneg a_small base_good k_big_enough m_good n_pos n_reasonable offset_nonneg. subst q r m. - assert (0 < b^(k-offset)). zero_bounds. - assert (0 < b^(k+offset)) by zero_bounds. - assert (0 < b^(2 * k)) by zero_bounds. + assert (0 < b^(k-offset)). Z.zero_bounds. + assert (0 < b^(k+offset)) by Z.zero_bounds. + assert (0 < b^(2 * k)) by Z.zero_bounds. Z.simplify_fractions_le. autorewrite with pull_Zpow pull_Zdiv zsimplify; reflexivity. Qed. Lemma q_nice : { b : bool * bool | q = a / n + (if fst b then -1 else 0) + (if snd b then -1 else 0) }. Proof using a_nonneg a_small base_good k_big_enough m_good n_large n_pos n_reasonable offset_nonneg. - assert (0 < b^(k+offset)) by zero_bounds. - assert (0 < b^(k-offset)) by zero_bounds. + assert (0 < b^(k+offset)) by Z.zero_bounds. + assert (0 < b^(k-offset)) by Z.zero_bounds. assert (a / b^(k-offset) <= b^(2*k) / b^(k-offset)) by auto with zarith lia. assert (a / b^(k-offset) <= b^(k+offset)) by (autorewrite with pull_Zpow zsimplify in *; assumption). subst q r m. diff --git a/src/Arithmetic/BarrettReduction/HAC.v b/src/Arithmetic/BarrettReduction/HAC.v index 70661ee96..c9fb2f16f 100644 --- a/src/Arithmetic/BarrettReduction/HAC.v +++ b/src/Arithmetic/BarrettReduction/HAC.v @@ -9,7 +9,13 @@ have to carry around extra precision), but requires more stringint conditions on the base ([b]), exponent ([k]), and the [offset]. *) Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. -Require Import Crypto.Util.ZUtil Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Modulo. +Require Import Crypto.Util.ZUtil.Hints. +Require Import Crypto.Util.ZUtil.ZSimplify. Local Open Scope Z_scope. @@ -72,8 +78,8 @@ Section barrett. Let R := x mod m. Lemma q3_nice : { b : bool * bool | q3 = Q + (if fst b then -1 else 0) + (if snd b then -1 else 0) }. Proof using base_pos k_big_enough m_large m_pos m_small offset_nonneg x_nonneg x_small μ_good. - assert (0 < b^(k+offset)) by zero_bounds. - assert (0 < b^(k-offset)) by zero_bounds. + assert (0 < b^(k+offset)) by Z.zero_bounds. + assert (0 < b^(k-offset)) by Z.zero_bounds. assert (x / b^(k-offset) <= b^(2*k) / b^(k-offset)) by auto with zarith lia. assert (x / b^(k-offset) <= b^(k+offset)) by (autorewrite with pull_Zpow zsimplify in *; assumption). subst q1 q2 q3 Q r_mod_3m r_mod_3m_orig r1 r2 R μ. diff --git a/src/Arithmetic/BarrettReduction/RidiculousFish.v b/src/Arithmetic/BarrettReduction/RidiculousFish.v index b9697839d..af030dcfe 100644 --- a/src/Arithmetic/BarrettReduction/RidiculousFish.v +++ b/src/Arithmetic/BarrettReduction/RidiculousFish.v @@ -1,5 +1,5 @@ Require Import Crypto.Util.Notations. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Hints.ZArith. Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. Require Import Coq.ZArith.ZArith. Require Import Coq.micromega.Lia. diff --git a/src/Arithmetic/BarrettReduction/Wikipedia.v b/src/Arithmetic/BarrettReduction/Wikipedia.v index 69ce10c4b..46f831281 100644 --- a/src/Arithmetic/BarrettReduction/Wikipedia.v +++ b/src/Arithmetic/BarrettReduction/Wikipedia.v @@ -1,7 +1,11 @@ (*** Barrett Reduction *) (** This file implements Barrett Reduction on [Z]. We follow Wikipedia. *) Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.ZUtil.Tactics.SimplifyFractionsLe. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Modulo. Require Import Crypto.Util.Tactics.BreakMatch. Local Open Scope Z_scope. @@ -80,7 +84,7 @@ Section barrett. : q * n <= a. Proof using a_nonneg k_good m_good n_pos n_reasonable. pose proof k_nonnegative; subst q r m. - assert (0 <= 2^(k-1)) by zero_bounds. + assert (0 <= 2^(k-1)) by Z.zero_bounds. Z.simplify_fractions_le. Qed. diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v index 98600d9a3..48046d7e3 100644 --- a/src/Arithmetic/Core.v +++ b/src/Arithmetic/Core.v @@ -246,8 +246,9 @@ Local Open Scope Z_scope. Require Import Crypto.Algebra.Nsatz. Require Import Crypto.Util.Decidable Crypto.Util.LetIn. -Require Import Crypto.Util.ZUtil Crypto.Util.ListUtil Crypto.Util.Sigma. +Require Import Crypto.Util.ListUtil Crypto.Util.Sigma. Require Import Crypto.Util.CPSUtil Crypto.Util.Prod. +Require Import Crypto.Util.ZUtil.Modulo.PullPush. Require Import Crypto.Util.ZUtil.Zselect. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.ZUtil.Definitions. @@ -257,6 +258,7 @@ Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.UniquePose. Require Import Crypto.Util.Tactics.VM. Require Import Crypto.Util.IdfunWithAlt. +Require Import Crypto.Util.Notations. Require Import Coq.Lists.List. Import ListNotations. Require Crypto.Util.Tuple. Local Notation tuple := Tuple.tuple. diff --git a/src/Arithmetic/Karatsuba.v b/src/Arithmetic/Karatsuba.v index ad5e25be8..1873e5ef1 100644 --- a/src/Arithmetic/Karatsuba.v +++ b/src/Arithmetic/Karatsuba.v @@ -1,10 +1,11 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.micromega.Lia. Require Import Crypto.Algebra.Nsatz. -Require Import Crypto.Util.ZUtil Crypto.Util.LetIn Crypto.Util.CPSUtil. +Require Import Crypto.Util.LetIn Crypto.Util.CPSUtil. Require Import Crypto.Arithmetic.Core. Import B. Import Positional. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.IdfunWithAlt. +Require Import Crypto.Util.ZUtil.EquivModulo. Local Open Scope Z_scope. Section Karatsuba. diff --git a/src/Arithmetic/ModularArithmeticTheorems.v b/src/Arithmetic/ModularArithmeticTheorems.v index 666dd54eb..d1fcd80b9 100644 --- a/src/Arithmetic/ModularArithmeticTheorems.v +++ b/src/Arithmetic/ModularArithmeticTheorems.v @@ -8,7 +8,9 @@ Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Ring_tac. Require Import Crypto.Algebra.Hierarchy Crypto.Algebra.ScalarMult. Require Crypto.Algebra.Ring Crypto.Algebra.Field. -Require Import Crypto.Util.Decidable Crypto.Util.ZUtil. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.ZUtil.Modulo. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. Require Export Crypto.Util.FixCoqMistakes. Module F. diff --git a/src/Arithmetic/MontgomeryReduction/Definition.v b/src/Arithmetic/MontgomeryReduction/Definition.v index 04c097460..e5cdcc603 100644 --- a/src/Arithmetic/MontgomeryReduction/Definition.v +++ b/src/Arithmetic/MontgomeryReduction/Definition.v @@ -2,7 +2,7 @@ (** This file implements Montgomery Form, Montgomery Reduction, and Montgomery Multiplication on [Z]. We follow Wikipedia. *) Require Import Coq.ZArith.ZArith. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.EquivModulo. Require Import Crypto.Util.Notations. Local Open Scope Z_scope. diff --git a/src/Arithmetic/MontgomeryReduction/Proofs.v b/src/Arithmetic/MontgomeryReduction/Proofs.v index 5f459e52d..e6be440fb 100644 --- a/src/Arithmetic/MontgomeryReduction/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/Proofs.v @@ -4,7 +4,9 @@ Wikipedia. *) Require Import Coq.ZArith.ZArith Coq.micromega.Psatz Coq.Structures.Equalities. Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.EquivModulo. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SimplifyRepeatedIfs. Require Import Crypto.Util.Notations. diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v index 266fc1f6f..3dd7fc0b3 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Dependent/Proofs.v @@ -4,11 +4,19 @@ Require Import Coq.ZArith.BinInt Coq.ZArith.ZArith Coq.ZArith.Zdiv Coq.micromega Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Prod. Require Import Crypto.Util.NatUtil. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Arithmetic.ModularArithmeticTheorems Crypto.Spec.ModularArithmetic. Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Dependent.Definition. Require Import Crypto.Algebra.Ring. Require Import Crypto.Util.ZUtil.MulSplit. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.EquivModulo. +Require Import Crypto.Util.ZUtil.Modulo. +Require Import Crypto.Util.ZUtil.Modulo.PullPush. +Require Import Crypto.Util.ZUtil.Tactics.PeelLe. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.Sigma. Require Import Crypto.Util.Tactics.SetEvars. Require Import Crypto.Util.Tactics.SubstEvars. diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v index 9ca2cf4e9..9eabc5ce4 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Proofs.v @@ -4,11 +4,19 @@ Require Import Coq.ZArith.BinInt Coq.ZArith.ZArith Coq.ZArith.Zdiv Coq.micromega Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Prod. Require Import Crypto.Util.NatUtil. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Arithmetic.ModularArithmeticTheorems Crypto.Spec.ModularArithmetic. Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Definition. Require Import Crypto.Algebra.Ring. Require Import Crypto.Util.ZUtil.MulSplit. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.EquivModulo. +Require Import Crypto.Util.ZUtil.Modulo. +Require Import Crypto.Util.ZUtil.Modulo.PullPush. +Require Import Crypto.Util.ZUtil.Tactics.PeelLe. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.Sigma. Require Import Crypto.Util.Tactics.SetEvars. Require Import Crypto.Util.Tactics.SubstEvars. diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v index 6d2925d6b..35c9e377b 100644 --- a/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v +++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v @@ -6,7 +6,6 @@ Require Import Crypto.Arithmetic.Saturated.MontgomeryAPI. Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Dependent.Definition. Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Dependent.Proofs. Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Definition. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics.BreakMatch. Local Open Scope Z_scope. diff --git a/src/Arithmetic/PrimeFieldTheorems.v b/src/Arithmetic/PrimeFieldTheorems.v index a4305a849..47ea89e31 100644 --- a/src/Arithmetic/PrimeFieldTheorems.v +++ b/src/Arithmetic/PrimeFieldTheorems.v @@ -8,7 +8,10 @@ Require Import Crypto.Util.NumTheoryUtil. Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid. Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.ZArith.ZArith Coq.ZArith.Znumtheory Coq.NArith.NArith. (* import Zdiv before Znumtheory *) Require Import Coq.Logic.Eqdep_dec. -Require Import Crypto.Util.NumTheoryUtil Crypto.Util.ZUtil. +Require Import Crypto.Util.NumTheoryUtil. +Require Import Crypto.Util.ZUtil.Odd. +Require Import Crypto.Util.ZUtil.Modulo. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Decidable. Require Export Crypto.Util.FixCoqMistakes. @@ -105,7 +108,7 @@ Module F. repeat match goal with | |- _ => progress subst | |- _ => progress rewrite ?F.pow_0_l, <-?F.pow_add_r - | |- _ => progress rewrite <-?Z2N.inj_0, <-?Z2N.inj_add by zero_bounds + | |- _ => progress rewrite <-?Z2N.inj_0, <-?Z2N.inj_add by Z.zero_bounds | |- _ => rewrite <-@euler_criterion by auto | |- ?x ^ (?f _) = ?a <-> ?x ^ (?f _) = ?a => do 3 f_equiv; [ ] | |- _ => rewrite !Zmod_odd in *; repeat (break_match; break_match_hyps); omega @@ -114,10 +117,10 @@ Module F. | |- (?x ^ Z.to_N ?a = 1) <-> _ => transitivity (x ^ Z.to_N a * x ^ Z.to_N 1 = x); [ rewrite F.pow_1_r, Algebra.Field.mul_cancel_l_iff by auto; reflexivity | ] - | |- (_ <> _)%N => rewrite Z2N.inj_iff by zero_bounds - | |- (?a <> 0)%Z => assert (0 < a) by zero_bounds; omega + | |- (_ <> _)%N => rewrite Z2N.inj_iff by Z.zero_bounds + | |- (?a <> 0)%Z => assert (0 < a) by Z.zero_bounds; omega | |- (_ = _)%Z => replace 4 with (2 * 2)%Z in * by ring; - rewrite <-Z.div_div by zero_bounds; + rewrite <-Z.div_div by Z.zero_bounds; rewrite Z.add_diag, Z.mul_add_distr_l, Z.mul_div_eq by omega end. Qed. @@ -166,8 +169,8 @@ Module F. replace (Z.to_N (q / 8 + 1) * (2*2))%N with (Z.to_N (q / 2 + 2))%N. Focus 2. { (* this is a boring but gnarly proof :/ *) change (2*2)%N with (Z.to_N 4). - rewrite <- Z2N.inj_mul by zero_bounds. - apply Z2N.inj_iff; try zero_bounds. + rewrite <- Z2N.inj_mul by Z.zero_bounds. + apply Z2N.inj_iff; try Z.zero_bounds. rewrite <- Z.mul_cancel_l with (p := 2) by omega. ring_simplify. rewrite Z.mul_div_eq by omega. @@ -179,7 +182,7 @@ Module F. ring. } Unfocus. - rewrite Z2N.inj_add, F.pow_add_r by zero_bounds. + rewrite Z2N.inj_add, F.pow_add_r by Z.zero_bounds. replace (x ^ Z.to_N (q / 2)) with (F.of_Z q 1) by (symmetry; apply @euler_criterion; eauto). change (Z.to_N 2) with 2%N; ring. @@ -215,8 +218,8 @@ Module F. repeat match goal with | |- _ => progress subst | |- _ => progress rewrite ?F.pow_0_l - | |- (_ <> _)%N => rewrite <-Z2N.inj_0, Z2N.inj_iff by zero_bounds - | |- (?a <> 0)%Z => assert (0 < a) by zero_bounds; omega + | |- (_ <> _)%N => rewrite <-Z2N.inj_0, Z2N.inj_iff by Z.zero_bounds + | |- (?a <> 0)%Z => assert (0 < a) by Z.zero_bounds; omega | |- _ => congruence end. break_match; diff --git a/src/Arithmetic/Saturated/Core.v b/src/Arithmetic/Saturated/Core.v index 189e76113..9c796ad57 100644 --- a/src/Arithmetic/Saturated/Core.v +++ b/src/Arithmetic/Saturated/Core.v @@ -9,7 +9,12 @@ Require Import Crypto.Arithmetic.Core. Require Import Crypto.Util.LetIn Crypto.Util.CPSUtil. Require Import Crypto.Util.Tuple Crypto.Util.ListUtil. Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Decidable Crypto.Util.ZUtil. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.ZUtil.Modulo.PullPush. +Require Import Crypto.Util.ZUtil.Le. +Require Import Crypto.Util.ZUtil.Modulo. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. Require Import Crypto.Util.NatUtil. Require Import Crypto.Util.Tactics.SpecializeBy. Local Notation "A ^ n" := (tuple A n) : type_scope. @@ -273,7 +278,7 @@ Module Columns. rewrite <-Z.mul_mod_distr_l with (c:=a) by omega. rewrite Z.mul_add_distr_l, Z.mul_div_eq, <-Z.add_mod_full by omega. f_equal; ring. } - { split; [zero_bounds|]. + { split; [Z.zero_bounds|]. apply Z.lt_le_trans with (m:=a*(b-1)+a); [|ring_simplify; omega]. apply Z.add_le_lt_mono; try apply Z.mul_le_mono_nonneg_l; omega. } Qed. diff --git a/src/Arithmetic/Saturated/Freeze.v b/src/Arithmetic/Saturated/Freeze.v index 78a86bc73..d8e7f4b5e 100644 --- a/src/Arithmetic/Saturated/Freeze.v +++ b/src/Arithmetic/Saturated/Freeze.v @@ -7,9 +7,11 @@ Require Import Crypto.Arithmetic.Saturated.Core. Require Import Crypto.Arithmetic.Saturated.Wrappers. Require Import Crypto.Util.ZUtil.AddGetCarry. Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Modulo.PullPush. +Require Import Crypto.Util.ZUtil.Le. Require Import Crypto.Util.ZUtil.CPS. Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Decidable Crypto.Util.ZUtil. +Require Import Crypto.Util.Decidable. Require Import Crypto.Util.Tuple Crypto.Util.LetIn. Local Notation "A ^ n" := (tuple A n) : type_scope. diff --git a/src/Arithmetic/Saturated/MontgomeryAPI.v b/src/Arithmetic/Saturated/MontgomeryAPI.v index 6dee1d22b..d08fe7a8b 100644 --- a/src/Arithmetic/Saturated/MontgomeryAPI.v +++ b/src/Arithmetic/Saturated/MontgomeryAPI.v @@ -11,12 +11,18 @@ Require Import Crypto.Arithmetic.Saturated.AddSub. Require Import Crypto.Util.LetIn Crypto.Util.CPSUtil. Require Import Crypto.Util.Tuple Crypto.Util.LetIn. Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.ZUtil Crypto.Util.ListUtil. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Modulo. Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.CPS. Require Import Crypto.Util.ZUtil.Zselect. Require Import Crypto.Util.ZUtil.AddGetCarry. Require Import Crypto.Util.ZUtil.MulSplit. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Opp. Require Import Crypto.Util.Tactics.UniquePose. Local Notation "A ^ n" := (tuple A n) : type_scope. diff --git a/src/Arithmetic/Saturated/UniformWeight.v b/src/Arithmetic/Saturated/UniformWeight.v index bd351b6cd..bf069f2d6 100644 --- a/src/Arithmetic/Saturated/UniformWeight.v +++ b/src/Arithmetic/Saturated/UniformWeight.v @@ -4,7 +4,9 @@ Local Open Scope Z_scope. Require Import Crypto.Arithmetic.Core. Require Import Crypto.Arithmetic.Saturated.Core. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Le. +Require Import Crypto.Util.ZUtil.Modulo. +Require Import Crypto.Util.ZUtil.Tactics.PeelLe. Require Import Crypto.Util.LetIn Crypto.Util.Tuple. Local Notation "A ^ n" := (tuple A n) : type_scope. @@ -88,4 +90,4 @@ Section UniformWeight. Definition small {n} (p : Z^n) : Prop := forall x, In x (to_list _ p) -> 0 <= x < bound. -End UniformWeight.
\ No newline at end of file +End UniformWeight. |