diff options
Diffstat (limited to 'src/LegacyArithmetic/Double/Proofs')
10 files changed, 31 insertions, 13 deletions
diff --git a/src/LegacyArithmetic/Double/Proofs/BitwiseOr.v b/src/LegacyArithmetic/Double/Proofs/BitwiseOr.v index 0f07c6299..8588836ee 100644 --- a/src/LegacyArithmetic/Double/Proofs/BitwiseOr.v +++ b/src/LegacyArithmetic/Double/Proofs/BitwiseOr.v @@ -2,7 +2,8 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.LegacyArithmetic.Interface. Require Import Crypto.LegacyArithmetic.Double.Core. Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.LandLorShiftBounds. Require Import Crypto.Util.Tactics.BreakMatch. Local Open Scope Z_scope. diff --git a/src/LegacyArithmetic/Double/Proofs/Decode.v b/src/LegacyArithmetic/Double/Proofs/Decode.v index 1cd5bf06d..c0748cf8e 100644 --- a/src/LegacyArithmetic/Double/Proofs/Decode.v +++ b/src/LegacyArithmetic/Double/Proofs/Decode.v @@ -3,7 +3,7 @@ Require Import Crypto.LegacyArithmetic.Interface. Require Import Crypto.LegacyArithmetic.InterfaceProofs. Require Import Crypto.LegacyArithmetic.Double.Core. Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Notations. Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.Notations. diff --git a/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v b/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v index 2c7f87dd7..13847b50a 100644 --- a/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v +++ b/src/LegacyArithmetic/Double/Proofs/LoadImmediate.v @@ -3,7 +3,7 @@ Require Import Crypto.LegacyArithmetic.Interface. Require Import Crypto.LegacyArithmetic.InterfaceProofs. Require Import Crypto.LegacyArithmetic.Double.Core. Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. Local Open Scope Z_scope. Local Opaque tuple_decoder. diff --git a/src/LegacyArithmetic/Double/Proofs/Multiply.v b/src/LegacyArithmetic/Double/Proofs/Multiply.v index 98692ed7f..ebe19cc46 100644 --- a/src/LegacyArithmetic/Double/Proofs/Multiply.v +++ b/src/LegacyArithmetic/Double/Proofs/Multiply.v @@ -5,7 +5,10 @@ Require Import Crypto.LegacyArithmetic.Double.Core. Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. Require Import Crypto.LegacyArithmetic.Double.Proofs.SpreadLeftImmediate. Require Import Crypto.LegacyArithmetic.Double.Proofs.RippleCarryAddSub. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. +Require Import Crypto.Util.ZUtil.Modulo. Require Import Crypto.Util.Tactics.SimplifyProjections. Require Import Crypto.Util.Notations. Require Import Crypto.Util.LetIn. diff --git a/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v b/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v index 4f6a79e8d..b2d53a33a 100644 --- a/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v +++ b/src/LegacyArithmetic/Double/Proofs/RippleCarryAddSub.v @@ -4,7 +4,10 @@ Require Import Crypto.LegacyArithmetic.InterfaceProofs. Require Import Crypto.LegacyArithmetic.Double.Core. Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SimplifyProjections. Require Import Crypto.Util.Notations. diff --git a/src/LegacyArithmetic/Double/Proofs/ShiftLeft.v b/src/LegacyArithmetic/Double/Proofs/ShiftLeft.v index 2230e36b6..1944f99b2 100644 --- a/src/LegacyArithmetic/Double/Proofs/ShiftLeft.v +++ b/src/LegacyArithmetic/Double/Proofs/ShiftLeft.v @@ -3,8 +3,8 @@ Require Import Crypto.LegacyArithmetic.Interface. Require Import Crypto.LegacyArithmetic.Double.Core. Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. Require Import Crypto.LegacyArithmetic.Double.Proofs.ShiftLeftRightTactic. -Require Import Crypto.Util.ZUtil. -(*Require Import Crypto.Util.Tactics.*) +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Definitions. Local Open Scope Z_scope. diff --git a/src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v b/src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v index 41234bf6e..98cf3cf9c 100644 --- a/src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v +++ b/src/LegacyArithmetic/Double/Proofs/ShiftLeftRightTactic.v @@ -1,8 +1,17 @@ Require Import Coq.ZArith.ZArith. Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Testbit. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Tactics.Ztestbit. Require Import Crypto.Util.Tactics.UniquePose. Require Import Crypto.Util.Tactics.BreakMatch. +Require Export Crypto.Util.ZUtil.ZSimplify.Autogenerated. +Require Export Crypto.Util.ZUtil.ZSimplify.Core. +Require Export Crypto.Util.ZUtil.ZSimplify.Simple. +Require Export Crypto.Util.ZUtil.LandLorShiftBounds. Local Open Scope Z_scope. diff --git a/src/LegacyArithmetic/Double/Proofs/ShiftRight.v b/src/LegacyArithmetic/Double/Proofs/ShiftRight.v index 16e7c5d6a..245e03480 100644 --- a/src/LegacyArithmetic/Double/Proofs/ShiftRight.v +++ b/src/LegacyArithmetic/Double/Proofs/ShiftRight.v @@ -3,8 +3,6 @@ Require Import Crypto.LegacyArithmetic.Interface. Require Import Crypto.LegacyArithmetic.Double.Core. Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. Require Import Crypto.LegacyArithmetic.Double.Proofs.ShiftLeftRightTactic. -Require Import Crypto.Util.ZUtil. -(*Require Import Crypto.Util.Tactics.*) Local Open Scope Z_scope. diff --git a/src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v b/src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v index 00a6d03cd..7210d80d5 100644 --- a/src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v +++ b/src/LegacyArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate.v @@ -3,8 +3,8 @@ Require Import Crypto.LegacyArithmetic.Interface. Require Import Crypto.LegacyArithmetic.Double.Core. Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. Require Import Crypto.LegacyArithmetic.Double.Proofs.ShiftLeftRightTactic. -Require Import Crypto.Util.ZUtil. -(*Require Import Crypto.Util.Tactics.*) +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Definitions. Local Open Scope Z_scope. diff --git a/src/LegacyArithmetic/Double/Proofs/SpreadLeftImmediate.v b/src/LegacyArithmetic/Double/Proofs/SpreadLeftImmediate.v index c50d43616..0cbc237d2 100644 --- a/src/LegacyArithmetic/Double/Proofs/SpreadLeftImmediate.v +++ b/src/LegacyArithmetic/Double/Proofs/SpreadLeftImmediate.v @@ -3,7 +3,11 @@ Require Import Crypto.LegacyArithmetic.Interface. Require Import Crypto.LegacyArithmetic.InterfaceProofs. Require Import Crypto.LegacyArithmetic.Double.Core. Require Import Crypto.LegacyArithmetic.Double.Proofs.Decode. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +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. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Notations. |