diff options
Diffstat (limited to 'src/Arithmetic/UniformWeight.v')
| -rw-r--r-- | src/Arithmetic/UniformWeight.v | 71 |
1 files changed, 14 insertions, 57 deletions
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). |