diff options
Diffstat (limited to 'src/Arithmetic/Saturated')
| -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 |
4 files changed, 21 insertions, 6 deletions
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. |