diff options
90 files changed, 2349 insertions, 1858 deletions
diff --git a/_CoqProject b/_CoqProject index b5fb302ce..b3edfac03 100644 --- a/_CoqProject +++ b/_CoqProject @@ -6536,6 +6536,7 @@ src/Util/ListUtil/FoldBool.v src/Util/ListUtil/Forall.v src/Util/Logic/ImplAnd.v src/Util/Logic/ProdForall.v +src/Util/NUtil/WithoutReferenceToZ.v src/Util/SideConditions/AdmitPackage.v src/Util/SideConditions/Autosolve.v src/Util/SideConditions/CorePackages.v @@ -6607,22 +6608,36 @@ src/Util/ZUtil/AddModulo.v src/Util/ZUtil/CC.v src/Util/ZUtil/CPS.v src/Util/ZUtil/Definitions.v +src/Util/ZUtil/DistrIf.v src/Util/ZUtil/Div.v +src/Util/ZUtil/Divide.v src/Util/ZUtil/EquivModulo.v src/Util/ZUtil/Ge.v src/Util/ZUtil/Hints.v src/Util/ZUtil/Land.v +src/Util/ZUtil/LandLorBounds.v +src/Util/ZUtil/LandLorShiftBounds.v src/Util/ZUtil/Le.v +src/Util/ZUtil/Lnot.v +src/Util/ZUtil/Log2.v src/Util/ZUtil/ModInv.v src/Util/ZUtil/Modulo.v src/Util/ZUtil/Morphisms.v +src/Util/ZUtil/Mul.v src/Util/ZUtil/MulSplit.v +src/Util/ZUtil/N2Z.v src/Util/ZUtil/Notations.v +src/Util/ZUtil/Odd.v +src/Util/ZUtil/Ones.v +src/Util/ZUtil/Opp.v src/Util/ZUtil/Peano.v +src/Util/ZUtil/Pow.v +src/Util/ZUtil/Pow2.v src/Util/ZUtil/Pow2Mod.v src/Util/ZUtil/Quot.v src/Util/ZUtil/Rshi.v src/Util/ZUtil/Sgn.v +src/Util/ZUtil/Shift.v src/Util/ZUtil/Sorting.v src/Util/ZUtil/Stabilization.v src/Util/ZUtil/Tactics.v 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. diff --git a/src/Compilers/Named/MapCastInterp.v b/src/Compilers/Named/MapCastInterp.v index e6dbb01ed..c38eadd9c 100644 --- a/src/Compilers/Named/MapCastInterp.v +++ b/src/Compilers/Named/MapCastInterp.v @@ -11,7 +11,6 @@ Require Import Crypto.Compilers.Named.ContextProperties.SmartMap. Require Import Crypto.Compilers.Named.InterpSideConditions. Require Import Crypto.Compilers.Named.InterpSideConditionsInterp. Require Import Crypto.Compilers.Named.MapCast. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Bool. Require Import Crypto.Util.Option. Require Import Crypto.Util.Sigma. diff --git a/src/Compilers/Named/MapCastWf.v b/src/Compilers/Named/MapCastWf.v index b04613fa7..eb141cad1 100644 --- a/src/Compilers/Named/MapCastWf.v +++ b/src/Compilers/Named/MapCastWf.v @@ -11,7 +11,6 @@ Require Import Crypto.Compilers.Named.ContextProperties.SmartMap. Require Import Crypto.Compilers.Named.Wf. Require Import Crypto.Compilers.Named.MapCast. Require Import Crypto.Util.PointedProp. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Bool. Require Import Crypto.Util.Option. Require Import Crypto.Util.Prod. diff --git a/src/Compilers/Z/ArithmeticSimplifierInterp.v b/src/Compilers/Z/ArithmeticSimplifierInterp.v index c34089a60..c1c841c9f 100644 --- a/src/Compilers/Z/ArithmeticSimplifierInterp.v +++ b/src/Compilers/Z/ArithmeticSimplifierInterp.v @@ -10,8 +10,17 @@ Require Import Crypto.Compilers.Z.OpInversion. Require Import Crypto.Compilers.Z.ArithmeticSimplifier. Require Import Crypto.Compilers.Z.ArithmeticSimplifierUtil. Require Import Crypto.Compilers.Z.Syntax.Equality. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Hints. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.ZSimplify.Core. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Z2Nat. Require Import Crypto.Util.ZUtil.AddGetCarry. +Require Import Crypto.Util.ZUtil.Modulo.PullPush. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +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.Option. Require Import Crypto.Util.Prod. Require Import Crypto.Util.Sum. diff --git a/src/Compilers/Z/ArithmeticSimplifierWf.v b/src/Compilers/Z/ArithmeticSimplifierWf.v index ff690688a..4efa7445a 100644 --- a/src/Compilers/Z/ArithmeticSimplifierWf.v +++ b/src/Compilers/Z/ArithmeticSimplifierWf.v @@ -10,7 +10,6 @@ Require Import Crypto.Compilers.Z.OpInversion. Require Import Crypto.Compilers.Z.ArithmeticSimplifier. Require Import Crypto.Compilers.Z.Syntax.Equality. Require Import Crypto.Compilers.Z.Syntax.Util. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Option. Require Import Crypto.Util.Sum. Require Import Crypto.Util.Prod. diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v index 45566839a..b23e0ff1b 100644 --- a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v +++ b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v @@ -8,9 +8,13 @@ Require Import Crypto.Compilers.Z.Bounds.Interpretation. Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.Tactics. Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Util.ZRange.CornersMonotoneBounds. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.ZUtil.Stabilization. Require Import Crypto.Util.ZUtil.MulSplit. +Require Import Crypto.Util.ZUtil.Modulo. +Require Import Crypto.Util.ZUtil.LandLorShiftBounds. +Require Import Crypto.Util.ZUtil.Morphisms. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.PointedProp. Require Import Crypto.Util.Bool. Require Import Crypto.Util.FixedWordSizesEquality. diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v b/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v index 1701b4688..7ffe0beb1 100644 --- a/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v +++ b/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v @@ -7,7 +7,12 @@ Require Import Crypto.Compilers.Syntax. Require Import Crypto.Compilers.Z.Bounds.Interpretation. Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.Tactics. Require Import Crypto.Compilers.SmartMap. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Morphisms. +Require Import Crypto.Util.ZUtil.Log2. +Require Import Crypto.Util.ZUtil.Pow2. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.PeelLe. Require Import Crypto.Util.Bool. Require Import Crypto.Util.FixedWordSizesEquality. Require Import Crypto.Util.Option. diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v b/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v index 71f4b758b..6486b2e00 100644 --- a/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v +++ b/src/Compilers/Z/Bounds/InterpretationLemmas/Tactics.v @@ -1,7 +1,14 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.micromega.Psatz. Require Import Crypto.Compilers.Z.Bounds.Interpretation. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Hints. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.ZSimplify.Core. +Require Import Crypto.Util.ZUtil.Log2. +Require Import Crypto.Util.ZUtil.Shift. +Require Import Crypto.Util.ZUtil.LandLorShiftBounds. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Notations. Require Import Crypto.Util.ZRange.Operations. Require Import Crypto.Util.Bool. Require Import Crypto.Util.FixedWordSizesEquality. diff --git a/src/Compilers/Z/Bounds/Relax.v b/src/Compilers/Z/Bounds/Relax.v index 328ea5f48..8178592ed 100644 --- a/src/Compilers/Z/Bounds/Relax.v +++ b/src/Compilers/Z/Bounds/Relax.v @@ -15,7 +15,8 @@ Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Option. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Log2. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.Bool. Local Lemma helper logsz v diff --git a/src/Compilers/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v index a4f5506fe..110e6b816 100644 --- a/src/Compilers/Z/Syntax/Util.v +++ b/src/Compilers/Z/Syntax/Util.v @@ -1,4 +1,5 @@ Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. Require Import Crypto.Compilers.Syntax. Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Compilers.Wf. @@ -6,9 +7,7 @@ Require Import Crypto.Compilers.TypeUtil. Require Import Crypto.Compilers.TypeInversion. Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Util.FixedWordSizesEquality. -Require Import Crypto.Util.NatUtil. Require Import Crypto.Util.HProp. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.Notations. @@ -113,8 +112,8 @@ Proof. | [ H : ?leb _ _ = false |- _ ] => apply Compare_dec.leb_iff_conv in H | [ H : TWord _ = TWord _ |- _ ] => inversion H; clear H end - | rewrite ZToWord_wordToZ_ZToWord by omega * - | rewrite wordToZ_ZToWord_wordToZ by omega * + | rewrite ZToWord_wordToZ_ZToWord by lia + | rewrite wordToZ_ZToWord_wordToZ by lia | rewrite wordToZ_ZToWord by assumption | rewrite ZToWord_wordToZ_ZToWord_small by omega ]. Qed. @@ -182,8 +181,8 @@ Proof. | [ H : ?leb _ _ = false |- _ ] => apply Compare_dec.leb_iff_conv in H | [ H : TWord _ = TWord _ |- _ ] => inversion H; clear H end - | rewrite ZToWord_wordToZ_ZToWord by omega * - | rewrite wordToZ_ZToWord_wordToZ by omega * ]. + | rewrite ZToWord_wordToZ_ZToWord by lia + | rewrite wordToZ_ZToWord_wordToZ by lia ]. Qed. Lemma ZToInterp_eq_inj {a} x y diff --git a/src/Curves/Montgomery/XZProofs.v b/src/Curves/Montgomery/XZProofs.v index 650ed6920..632ec7bd9 100644 --- a/src/Curves/Montgomery/XZProofs.v +++ b/src/Curves/Montgomery/XZProofs.v @@ -3,7 +3,9 @@ Require Import Crypto.Algebra.ScalarMult. Require Import Crypto.Util.Sum Crypto.Util.Prod Crypto.Util.LetIn. Require Import Crypto.Util.Decidable. Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Shift. Require Import Crypto.Util.ZUtil.Peano. Require Import Crypto.Util.Tactics.SetoidSubst. Require Import Crypto.Util.Tactics.SpecializeBy. @@ -248,7 +250,7 @@ Module M. Proof. t. Qed. Lemma transitive_eq {p} q {r} : projective q -> eq p q -> eq q r -> eq p r. Proof. t. Qed. - + Lemma projective_to_xz Q : projective (to_xz Q). Proof. t. Qed. diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v index 410cb8dfe..56a7051af 100644 --- a/src/Experiments/NewPipeline/Arithmetic.v +++ b/src/Experiments/NewPipeline/Arithmetic.v @@ -21,8 +21,15 @@ 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. 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. @@ -37,7 +44,7 @@ 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 Crypto.Util.ZUtil.Hints.Core. +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. diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v index 869abea8e..01018c3e2 100644 --- a/src/Experiments/NewPipeline/Toplevel1.v +++ b/src/Experiments/NewPipeline/Toplevel1.v @@ -30,10 +30,17 @@ Require Import Crypto.Util.ZUtil.Rshi. Require Import Crypto.Util.Option. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Log2. Require Import Crypto.Util.ZUtil.Zselect. Require Import Crypto.Util.ZUtil.AddModulo. Require Import Crypto.Util.ZUtil.CC. +Require Import Crypto.Util.ZUtil.EquivModulo. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Modulo. Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. Require Import Crypto.Util.ZUtil.ModInv. diff --git a/src/Experiments/NewPipeline/Toplevel2.v b/src/Experiments/NewPipeline/Toplevel2.v index e35e14616..ffb6b0215 100644 --- a/src/Experiments/NewPipeline/Toplevel2.v +++ b/src/Experiments/NewPipeline/Toplevel2.v @@ -16,6 +16,7 @@ Require Import Crypto.Util.LetIn. Require Import Crypto.Arithmetic.PrimeFieldTheorems. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Tactics.SubstEvars. Require Import Crypto.Util.Tactics.DestructHead. @@ -29,10 +30,14 @@ Require Import Crypto.Util.ZUtil.Rshi. Require Import Crypto.Util.Option. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.ZUtil.Zselect. Require Import Crypto.Util.ZUtil.AddModulo. Require Import Crypto.Util.ZUtil.CC. +Require Import Crypto.Util.ZUtil.Modulo. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.EquivModulo. Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. Require Import Crypto.Util.ErrorT. @@ -2087,24 +2092,13 @@ Module ProdEquiv. let new_ctx := fun n => if reg_eqb n rd then result mod wordmax else ctx n in interp256 cont new_cc new_ctx. Proof. reflexivity. Qed. - (* TODO : move *) - Lemma tuple_map_ext {A B} (f g : A -> B) n (t : tuple A n) : - (forall x : A, f x = g x) -> - Tuple.map f t = Tuple.map g t. - Proof. - destruct n; [reflexivity|]; cbn in *. - induction n; cbn in *; intro H; auto; [ ]. - rewrite IHn by assumption. - rewrite H; reflexivity. - Qed. - Lemma interp_state_equiv e : forall cc ctx cc' ctx', cc = cc' -> (forall r, ctx r = ctx' r) -> interp256 e cc ctx = interp256 e cc' ctx'. Proof. induction e; intros; subst; cbn; [solve[auto]|]. - apply IHe; rewrite tuple_map_ext with (g:=ctx') by auto; + apply IHe; rewrite Tuple.map_ext with (g:=ctx') by auto; [reflexivity|]. intros; break_match; auto. Qed. @@ -2116,17 +2110,6 @@ Module ProdEquiv. reflexivity. Qed. - Lemma tuple_map_ext_In {A B} (f g : A -> B) n (t : tuple A n) : - (forall x, In x (to_list n t) -> f x = g x) -> - Tuple.map f t = Tuple.map g t. - Proof. - destruct n; [reflexivity|]; cbn in *. - induction n; cbn in *; intro H; auto; [ ]. - destruct t. - rewrite IHn by auto using in_cons. - rewrite H; auto using in_eq. - Qed. - Definition value_unused r e : Prop := forall x cc ctx, interp256 e cc ctx = interp256 e cc (fun r' => if reg_eqb r' r then x else ctx r'). @@ -2141,7 +2124,7 @@ Module ProdEquiv. match goal with |- ?lhs = ?rhs => match lhs with context [Tuple.map ?f ?t] => match rhs with context [Tuple.map ?g ?t] => - rewrite (tuple_map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence) + rewrite (Tuple.map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence) end end end. apply interp_state_equiv; [ congruence | ]. { intros; cbv [reg_eqb] in *; break_match; congruence. } @@ -2155,7 +2138,7 @@ Module ProdEquiv. match goal with |- ?lhs = ?rhs => match lhs with context [Tuple.map ?f ?t] => match rhs with context [Tuple.map ?g ?t] => - rewrite (tuple_map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence) + rewrite (Tuple.map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence) end end end. apply interp_state_equiv; [ congruence | ]. { intros; cbv [reg_eqb] in *; break_match; congruence. } @@ -2649,19 +2632,6 @@ Module Barrett256. => apply interp_equivZZ_256; [ simplify_op_equiv ctx | simplify_op_equiv ctx | generalize_result] end. - (* TODO: move this lemma to ZUtil *) - Lemma testbit_neg_eq_if x n : - 0 <= n -> - - (2 ^ n) <= x < 2 ^ n -> - Z.b2z (if x <? 0 then true else Z.testbit x n) = - (x / 2 ^ n) mod 2. - Proof. - intros. break_match; Z.ltb_to_lt. - { autorewrite with zsimplify. reflexivity. } - { autorewrite with zsimplify. - rewrite Z.bits_above_pow2 by omega. - reflexivity. } - Qed. - Lemma prod_barrett_red256_correct : forall (cc_start_state : Fancy.CC.state) (* starting carry flags *) (start_context : register -> Z) (* starting register values *) @@ -2755,7 +2725,7 @@ Module Barrett256. { reflexivity. } { autorewrite with zsimplify_fast. match goal with |- context [?x mod ?m] => pose proof (Z.mod_pos_bound x m ltac:(omega)) end. - rewrite <-testbit_neg_eq_if with (n:=256) by (cbn; omega). + rewrite <-Z.testbit_neg_eq_if with (n:=256) by (cbn; omega). reflexivity. } step start_context. { reflexivity. } @@ -2763,7 +2733,7 @@ Module Barrett256. rewrite Z.mod_small with (a:=(if (if _ <? 0 then true else _) then _ else _)) (b:=2) by (break_innermost_match; omega). match goal with |- context [?a - ?b - ?c] => replace (a - b - c) with (a - (b + c)) by ring end. match goal with |- context [?x mod ?m] => pose proof (Z.mod_pos_bound x m ltac:(omega)) end. - rewrite <-testbit_neg_eq_if with (n:=256) by (break_innermost_match; cbn; omega). + rewrite <-Z.testbit_neg_eq_if with (n:=256) by (break_innermost_match; cbn; omega). reflexivity. } step start_context. { rewrite Z.bit0_eqb. @@ -2782,7 +2752,7 @@ Module Barrett256. { reflexivity. } { autorewrite with zsimplify_fast. repeat match goal with |- context [?x mod ?m] => unique pose proof (Z.mod_pos_bound x m ltac:(omega)) end. - rewrite <-testbit_neg_eq_if with (n:=256) by (cbn; omega). + rewrite <-Z.testbit_neg_eq_if with (n:=256) by (cbn; omega). reflexivity. } step start_context; [ break_innermost_match; Z.ltb_to_lt; omega | ]. reflexivity. @@ -3169,19 +3139,6 @@ Module Montgomery256. => apply interp_equivZZ_256; [ simplify_op_equiv ctx | simplify_op_equiv ctx | generalize_result] end. - (* TODO: move this lemma to ZUtil *) - Lemma testbit_neg_eq_if x y n : - 0 <= n -> - 0 <= x < 2 ^ n -> - 0 <= y < 2 ^ n -> - Z.b2z (if (x - y) <? 0 then true else Z.testbit (x - y) n) = - ((x - y) / 2 ^ n) mod 2. - Proof. - intros. rewrite Z.sub_pos_bound_div_eq by omega. - break_innermost_match; Z.ltb_to_lt; try lia; try reflexivity; [ ]. - rewrite Z.testbit_eqb, Z.div_between_0_if by omega. - break_innermost_match; Z.ltb_to_lt; try lia; reflexivity. - Qed. - Local Ltac break_ifs := repeat (break_innermost_match_step; Z.ltb_to_lt; try (exfalso; omega); []). @@ -3228,7 +3185,7 @@ Module Montgomery256. { let r := eval cbv in (2^256) in replace (2^256) with r by reflexivity. rewrite !Z.shiftl_0_r, !Z.mod_mod by omega. - apply testbit_neg_eq_if; + apply Z.testbit_neg_eq_if; let r := eval cbv in (2^256) in replace (2^256) with r by reflexivity; auto using Z.mod_pos_bound with omega. } step start_context; [ break_innermost_match; Z.ltb_to_lt; omega | ]. diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v index 3745e59ff..c0c8dbdeb 100644 --- a/src/Experiments/SimplyTypedArithmetic.v +++ b/src/Experiments/SimplyTypedArithmetic.v @@ -23,13 +23,21 @@ Require Import Crypto.Util.Tactics.Head. Require Import Crypto.Util.Option. Require Import Crypto.Util.OptionList. Require Import Crypto.Util.Sum. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.ZUtil.Modulo Crypto.Util.ZUtil.Div Crypto.Util.ZUtil.Hints.Core. 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.ZUtil.Le. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Log2. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Shift. +Require Import Crypto.Util.ZUtil.LandLorShiftBounds. +Require Import Crypto.Util.ZUtil.Testbit. +Require Import Crypto.Util.ZUtil.Notations. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.SplitInContext. Require Import Crypto.Util.Tactics.SubstEvars. @@ -41,7 +49,7 @@ Require Import Crypto.Util.ZUtil.Definitions. 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 Crypto.Util.ZUtil.Hints.Core. +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. @@ -1245,13 +1253,6 @@ Module Rows. rewrite Columns.length_from_associational in *; auto. Qed. - (* TODO : move *) - Lemma max_0_iff a b : Nat.max a b = 0%nat <-> (a = 0%nat /\ b = 0%nat). - Proof. - destruct a, b; try tauto. - rewrite <-Nat.succ_max_distr. - split; [ | destruct 1]; congruence. - Qed. Lemma max_column_size_zero_iff x : max_column_size x = 0%nat <-> (forall c, In c x -> c = nil). Proof. @@ -10402,24 +10403,13 @@ Module ProdEquiv. let new_ctx := fun n => if reg_eqb n rd then result mod wordmax else ctx n in interp256 cont new_cc new_ctx. Proof. reflexivity. Qed. - (* TODO : move *) - Lemma tuple_map_ext {A B} (f g : A -> B) n (t : tuple A n) : - (forall x : A, f x = g x) -> - Tuple.map f t = Tuple.map g t. - Proof. - destruct n; [reflexivity|]; cbn in *. - induction n; cbn in *; intro H; auto; [ ]. - rewrite IHn by assumption. - rewrite H; reflexivity. - Qed. - Lemma interp_state_equiv e : forall cc ctx cc' ctx', cc = cc' -> (forall r, ctx r = ctx' r) -> interp256 e cc ctx = interp256 e cc' ctx'. Proof. induction e; intros; subst; cbn; [solve[auto]|]. - apply IHe; rewrite tuple_map_ext with (g:=ctx') by auto; + apply IHe; rewrite Tuple.map_ext with (g:=ctx') by auto; [reflexivity|]. intros; break_match; auto. Qed. @@ -10431,17 +10421,6 @@ Module ProdEquiv. reflexivity. Qed. - Lemma tuple_map_ext_In {A B} (f g : A -> B) n (t : tuple A n) : - (forall x, In x (to_list n t) -> f x = g x) -> - Tuple.map f t = Tuple.map g t. - Proof. - destruct n; [reflexivity|]; cbn in *. - induction n; cbn in *; intro H; auto; [ ]. - destruct t. - rewrite IHn by auto using in_cons. - rewrite H; auto using in_eq. - Qed. - Definition value_unused r e : Prop := forall x cc ctx, interp256 e cc ctx = interp256 e cc (fun r' => if reg_eqb r' r then x else ctx r'). @@ -10456,7 +10435,7 @@ Module ProdEquiv. match goal with |- ?lhs = ?rhs => match lhs with context [Tuple.map ?f ?t] => match rhs with context [Tuple.map ?g ?t] => - rewrite (tuple_map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence) + rewrite (Tuple.map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence) end end end. apply interp_state_equiv; [ congruence | ]. { intros; cbv [reg_eqb] in *; break_match; congruence. } @@ -10470,7 +10449,7 @@ Module ProdEquiv. match goal with |- ?lhs = ?rhs => match lhs with context [Tuple.map ?f ?t] => match rhs with context [Tuple.map ?g ?t] => - rewrite (tuple_map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence) + rewrite (Tuple.map_ext_In f g) by (intros; cbv [reg_eqb]; break_match; congruence) end end end. apply interp_state_equiv; [ congruence | ]. { intros; cbv [reg_eqb] in *; break_match; congruence. } @@ -11525,19 +11504,6 @@ Module Barrett256. | _ => apply interp_equivZZ_256; [ simplify_op_equiv ctx | simplify_op_equiv ctx | generalize_result] end. - (* TODO: move this lemma to ZUtil *) - Lemma testbit_neg_eq_if x n : - 0 <= n -> - - (2 ^ n) <= x < 2 ^ n -> - Z.b2z (if x <? 0 then true else Z.testbit x n) = - (x / 2 ^ n) mod 2. - Proof. - intros. break_match; Z.ltb_to_lt. - { autorewrite with zsimplify. reflexivity. } - { autorewrite with zsimplify. - rewrite Z.bits_above_pow2 by omega. - reflexivity. } - Qed. - Lemma prod_barrett_red256_correct : forall (cc_start_state : Fancy.CC.state) (* starting carry flags *) (start_context : register -> Z) (* starting register values *) @@ -11631,7 +11597,7 @@ Module Barrett256. { reflexivity. } { autorewrite with zsimplify_fast. match goal with |- context [?x mod ?m] => pose proof (Z.mod_pos_bound x m ltac:(omega)) end. - rewrite <-testbit_neg_eq_if with (n:=256) by (cbn; omega). + rewrite <-Z.testbit_neg_eq_if with (n:=256) by (cbn; omega). reflexivity. } step start_context. { reflexivity. } @@ -11639,7 +11605,7 @@ Module Barrett256. rewrite Z.mod_small with (a:=(if (if _ <? 0 then true else _) then _ else _)) (b:=2) by (break_innermost_match; omega). match goal with |- context [?a - ?b - ?c] => replace (a - b - c) with (a - (b + c)) by ring end. match goal with |- context [?x mod ?m] => pose proof (Z.mod_pos_bound x m ltac:(omega)) end. - rewrite <-testbit_neg_eq_if with (n:=256) by (break_innermost_match; cbn; omega). + rewrite <-Z.testbit_neg_eq_if with (n:=256) by (break_innermost_match; cbn; omega). reflexivity. } step start_context. { rewrite Z.bit0_eqb. @@ -11658,7 +11624,7 @@ Module Barrett256. { reflexivity. } { autorewrite with zsimplify_fast. repeat match goal with |- context [?x mod ?m] => unique pose proof (Z.mod_pos_bound x m ltac:(omega)) end. - rewrite <-testbit_neg_eq_if with (n:=256) by (cbn; omega). + rewrite <-Z.testbit_neg_eq_if with (n:=256) by (cbn; omega). reflexivity. } step start_context; [ break_innermost_match; Z.ltb_to_lt; omega | ]. reflexivity. @@ -12567,19 +12533,6 @@ Module Montgomery256. | _ => apply interp_equivZZ_256; [ simplify_op_equiv ctx | simplify_op_equiv ctx | generalize_result] end. - (* TODO: move this lemma to ZUtil *) - Lemma testbit_neg_eq_if x y n : - 0 <= n -> - 0 <= x < 2 ^ n -> - 0 <= y < 2 ^ n -> - Z.b2z (if (x - y) <? 0 then true else Z.testbit (x - y) n) = - ((x - y) / 2 ^ n) mod 2. - Proof. - intros. rewrite Z.sub_pos_bound_div_eq by omega. - break_innermost_match; Z.ltb_to_lt; try lia; try reflexivity; [ ]. - rewrite Z.testbit_eqb, Z.div_between_0_if by omega. - break_innermost_match; Z.ltb_to_lt; try lia; reflexivity. - Qed. - Lemma prod_montred256_correct : forall (cc_start_state : Fancy.CC.state) (* starting carry flags can be anything *) (start_context : register -> Z) (* starting register values *) @@ -12622,9 +12575,12 @@ Module Montgomery256. { let r := eval cbv in (2^256) in replace (2^256) with r by reflexivity. rewrite !Z.shiftl_0_r, !Z.mod_mod by omega. - apply testbit_neg_eq_if; + repeat match goal with + | |- context [?a mod ?b] => unique pose proof (Z.mod_pos_bound a b ltac:(omega)) + end. + apply Z.testbit_neg_eq_if; let r := eval cbv in (2^256) in replace (2^256) with r by reflexivity; - auto using Z.mod_pos_bound with omega. } + omega. } step start_context; [ break_innermost_match; Z.ltb_to_lt; omega | ]. reflexivity. Qed. diff --git a/src/LegacyArithmetic/ArchitectureToZLikeProofs.v b/src/LegacyArithmetic/ArchitectureToZLikeProofs.v index 8d4b59ceb..5ff67d7ec 100644 --- a/src/LegacyArithmetic/ArchitectureToZLikeProofs.v +++ b/src/LegacyArithmetic/ArchitectureToZLikeProofs.v @@ -8,7 +8,8 @@ Require Import Crypto.LegacyArithmetic.Double.Proofs.Multiply. Require Import Crypto.LegacyArithmetic.ArchitectureToZLike. Require Import Crypto.LegacyArithmetic.ZBounded. Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. Require Import Crypto.Util.Tactics.UniquePose. Require Import Crypto.Util.LetIn. diff --git a/src/LegacyArithmetic/BarretReduction.v b/src/LegacyArithmetic/BarretReduction.v index e278dc082..37c4d4915 100644 --- a/src/LegacyArithmetic/BarretReduction.v +++ b/src/LegacyArithmetic/BarretReduction.v @@ -4,7 +4,6 @@ Require Import Coq.ZArith.ZArith Coq.Lists.List Coq.Classes.Morphisms Coq.micromega.Psatz. Require Import Crypto.Arithmetic.BarrettReduction.HAC. Require Import Crypto.LegacyArithmetic.ZBounded. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Notations. Local Open Scope small_zlike_scope. diff --git a/src/LegacyArithmetic/BaseSystem.v b/src/LegacyArithmetic/BaseSystem.v index 3f426e98b..359b4313b 100644 --- a/src/LegacyArithmetic/BaseSystem.v +++ b/src/LegacyArithmetic/BaseSystem.v @@ -1,7 +1,7 @@ Require Import Coq.Lists.List. Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv. Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. -Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil. +Require Import Crypto.Util.ListUtil. Require Import Crypto.Util.Notations. Require Export Crypto.Util.FixCoqMistakes. Import Nat. diff --git a/src/LegacyArithmetic/BaseSystemProofs.v b/src/LegacyArithmetic/BaseSystemProofs.v index f0f0a80d2..042fdb270 100644 --- a/src/LegacyArithmetic/BaseSystemProofs.v +++ b/src/LegacyArithmetic/BaseSystemProofs.v @@ -1,5 +1,5 @@ Require Import Coq.Lists.List Coq.micromega.Psatz. -Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil. +Require Import Crypto.Util.ListUtil. Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv. Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. Require Import Crypto.LegacyArithmetic.BaseSystem. 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. diff --git a/src/LegacyArithmetic/Interface.v b/src/LegacyArithmetic/Interface.v index 4a671eb4c..9a652bbd4 100644 --- a/src/LegacyArithmetic/Interface.v +++ b/src/LegacyArithmetic/Interface.v @@ -1,6 +1,7 @@ (*** Interface for bounded arithmetic *) Require Import Coq.ZArith.ZArith. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Notations. + Require Import Crypto.Util.Tuple. Require Import Crypto.Util.AutoRewrite. Require Import Crypto.Util.Notations. diff --git a/src/LegacyArithmetic/InterfaceProofs.v b/src/LegacyArithmetic/InterfaceProofs.v index 33917e00d..a2c8d9de5 100644 --- a/src/LegacyArithmetic/InterfaceProofs.v +++ b/src/LegacyArithmetic/InterfaceProofs.v @@ -1,7 +1,13 @@ (** * Alternate forms for Interface for bounded arithmetic *) Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. Require Import Crypto.LegacyArithmetic.Interface. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Hints. +Require Import Crypto.Util.ZUtil.Hints.ZArith. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.EquivModulo. Require Import Crypto.Util.Tuple. Require Import Crypto.Util.AutoRewrite. Require Import Crypto.Util.Notations. diff --git a/src/LegacyArithmetic/MontgomeryReduction.v b/src/LegacyArithmetic/MontgomeryReduction.v index c3538dd01..786e08d28 100644 --- a/src/LegacyArithmetic/MontgomeryReduction.v +++ b/src/LegacyArithmetic/MontgomeryReduction.v @@ -5,7 +5,7 @@ Require Import Coq.ZArith.ZArith Coq.Lists.List Coq.Classes.Morphisms Coq.microm Require Import Crypto.Arithmetic.MontgomeryReduction.Definition. Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. Require Import Crypto.LegacyArithmetic.ZBounded. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.EquivModulo. Require Import Crypto.Util.Tactics.Test. Require Import Crypto.Util.Tactics.Not. Require Import Crypto.Util.LetIn. diff --git a/src/LegacyArithmetic/Pow2Base.v b/src/LegacyArithmetic/Pow2Base.v index 62f1f742d..c5c69e684 100644 --- a/src/LegacyArithmetic/Pow2Base.v +++ b/src/LegacyArithmetic/Pow2Base.v @@ -1,6 +1,5 @@ Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith. Require Import Crypto.Util.ListUtil. -Require Import Crypto.Util.ZUtil. Require Import Coq.Lists.List. Local Open Scope Z_scope. diff --git a/src/LegacyArithmetic/Pow2BaseProofs.v b/src/LegacyArithmetic/Pow2BaseProofs.v index b6df85f5c..495636be7 100644 --- a/src/LegacyArithmetic/Pow2BaseProofs.v +++ b/src/LegacyArithmetic/Pow2BaseProofs.v @@ -2,7 +2,13 @@ Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.micromega.Psatz. Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Coq.Lists.List. Require Import Coq.funind.Recdef. -Require Import Crypto.Util.ListUtil Crypto.Util.ZUtil Crypto.Util.NatUtil. +Require Import Crypto.Util.ListUtil Crypto.Util.NatUtil. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Testbit. +Require Import Crypto.Util.ZUtil.Pow2Mod. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Shift. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. Require Import Crypto.LegacyArithmetic.VerdiTactics. Require Import Crypto.Util.Tactics.SpecializeBy. Require Import Crypto.Util.Tactics.BreakMatch. @@ -282,7 +288,7 @@ Section Pow2BaseProofs. | |- _ => rewrite BaseSystemProofs.set_higher | |- _ => rewrite nth_default_base | |- _ => rewrite IHi - | |- _ => rewrite <-Z.lor_shiftl by (rewrite ?Z.pow2_mod_spec; try apply Z.mod_pos_bound; zero_bounds) + | |- _ => rewrite <-Z.lor_shiftl by (rewrite ?Z.pow2_mod_spec; try apply Z.mod_pos_bound; Z.zero_bounds) | |- context[min ?x ?y] => (rewrite Nat.min_l by omega || rewrite Nat.min_r by omega) | |- context[2 ^ ?a * _] => rewrite (Z.mul_comm (2 ^ a)); rewrite <-Z.shiftl_mul_pow2 | |- _ => solve [auto] @@ -452,7 +458,7 @@ Section UniformBase. intros; apply Z.eq_le_incl. f_equal; auto. + apply nth_default_preserves_properties_length_dep; - try solve [apply nth_default_preserves_properties; split; zero_bounds; rewrite limb_widths_uniform; auto || omega]. + try solve [apply nth_default_preserves_properties; split; Z.zero_bounds; rewrite limb_widths_uniform; auto || omega]. intros; apply nth_default_preserves_properties_length_dep; try solve [intros; omega]. let x := fresh "x" in intro x; intros; replace x with width; try symmetry; auto. diff --git a/src/LegacyArithmetic/ZBounded.v b/src/LegacyArithmetic/ZBounded.v index bccbf7428..2eec4122b 100644 --- a/src/LegacyArithmetic/ZBounded.v +++ b/src/LegacyArithmetic/ZBounded.v @@ -2,7 +2,7 @@ (** This file specifies a ℤ-like type of bounded integers, with operations for Montgomery Reduction and Barrett Reduction. *) Require Import Coq.ZArith.ZArith. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Notations. diff --git a/src/LegacyArithmetic/ZBoundedZ.v b/src/LegacyArithmetic/ZBoundedZ.v index fef654f47..2943598c1 100644 --- a/src/LegacyArithmetic/ZBoundedZ.v +++ b/src/LegacyArithmetic/ZBoundedZ.v @@ -1,7 +1,9 @@ (*** ℤ can be a bounded ℤ-Like type *) Require Import Coq.ZArith.ZArith Coq.micromega.Psatz. Require Import Crypto.LegacyArithmetic.ZBounded. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Pow2Mod. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.LetIn. Require Import Crypto.Util.Notations. diff --git a/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v b/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v index 7274d2c35..58f5279ab 100644 --- a/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v +++ b/src/Specific/Framework/ArithmeticSynthesis/Karatsuba.v @@ -6,7 +6,7 @@ Require Import Crypto.Arithmetic.Core. Import B. Require Import Crypto.Arithmetic.PrimeFieldTheorems. Require Crypto.Specific.Framework.CurveParameters. Require Import Crypto.Util.Decidable. -Require Import Crypto.Util.LetIn Crypto.Util.ZUtil. +Require Import Crypto.Util.LetIn. Require Import Crypto.Arithmetic.Karatsuba. Require Import Crypto.Util.Tactics.BreakMatch. Require Crypto.Util.Tuple. diff --git a/src/Specific/NISTP256/FancyMachine256/Core.v b/src/Specific/NISTP256/FancyMachine256/Core.v index fec353c6f..881fa2e1e 100644 --- a/src/Specific/NISTP256/FancyMachine256/Core.v +++ b/src/Specific/NISTP256/FancyMachine256/Core.v @@ -20,7 +20,6 @@ Require Import Crypto.Compilers.Linearize. Require Import Crypto.Compilers.Inline. Require Import Crypto.Compilers.CommonSubexpressionElimination. Require Export Crypto.Compilers.Reify. -Require Export Crypto.Util.ZUtil. Require Export Crypto.Util.Option. Require Export Crypto.Util.Notations. Require Import Crypto.Util.ListUtil. diff --git a/src/Specific/NISTP256/FancyMachine256/Montgomery.v b/src/Specific/NISTP256/FancyMachine256/Montgomery.v index b8510614e..4caecca6b 100644 --- a/src/Specific/NISTP256/FancyMachine256/Montgomery.v +++ b/src/Specific/NISTP256/FancyMachine256/Montgomery.v @@ -1,6 +1,7 @@ Require Import Crypto.Specific.NISTP256.FancyMachine256.Core. Require Import Crypto.LegacyArithmetic.MontgomeryReduction. Require Import Crypto.Arithmetic.MontgomeryReduction.Proofs. +Require Import Crypto.Util.ZUtil.EquivModulo. Section expression. Context (ops : fancy_machine.instructions (2 * 128)) (props : fancy_machine.arithmetic ops) (modulus : Z) (m' : Z) (Hm : modulus <> 0) (H : 0 <= modulus < 2^256) (Hm' : 0 <= m' < 2^256). diff --git a/src/Util/FixedWordSizesEquality.v b/src/Util/FixedWordSizesEquality.v index bd71f5b80..797c7ee3b 100644 --- a/src/Util/FixedWordSizesEquality.v +++ b/src/Util/FixedWordSizesEquality.v @@ -4,7 +4,8 @@ Require Import Coq.Arith.Arith. Require Import bbv.WordScope. Require Import Crypto.Util.FixedWordSizes. Require Import Crypto.Util.WordUtil. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Log2. +Require Import Crypto.Util.ZUtil.Z2Nat. Require Import Crypto.Util.Tactics.BreakMatch. Definition wordT_beq_hetero {logsz1 logsz2} : wordT logsz1 -> wordT logsz2 -> bool diff --git a/src/Util/NUtil.v b/src/Util/NUtil.v index 8c354690b..1d78e3276 100644 --- a/src/Util/NUtil.v +++ b/src/Util/NUtil.v @@ -1,42 +1,14 @@ Require Import Coq.NArith.NArith. Require Import Coq.Numbers.Natural.Peano.NPeano. Require Import Crypto.Util.NatUtil Crypto.Util.Decidable. +Require Export Crypto.Util.NUtil.WithoutReferenceToZ. Require bbv.WordScope. Require Import bbv.NatLib. Require Crypto.Util.WordUtil. +Require Import Crypto.Util.ZUtil.Z2Nat. +Require Import Crypto.Util.ZUtil.Shift. Module N. - Lemma size_le a b : (a <= b -> N.size a <= N.size b)%N. - Proof. - destruct (dec (a=0)%N), (dec (b=0)%N); subst; auto using N.le_0_l. - { destruct a; auto. } - { rewrite !N.size_log2 by assumption. - rewrite <-N.succ_le_mono. - apply N.log2_le_mono. } - Qed. - - Lemma le_to_nat a b : (a <= b)%N <-> (N.to_nat a <= N.to_nat b)%nat. - Proof. - rewrite <-N.lt_succ_r. - rewrite <-Nat.lt_succ_r. - rewrite <-Nnat.N2Nat.inj_succ. - rewrite <-NatUtil.Nat2N_inj_lt. - rewrite !Nnat.N2Nat.id. - reflexivity. - Qed. - - Lemma size_nat_equiv : forall n, N.size_nat n = N.to_nat (N.size n). - Proof. - destruct n as [|p]; auto; simpl; induction p as [p IHp|p IHp|]; simpl; auto; rewrite IHp, Pnat.Pos2Nat.inj_succ; reflexivity. - Qed. - - Lemma size_nat_le a b : (a <= b)%N -> (N.size_nat a <= N.size_nat b)%nat. - Proof. - rewrite !size_nat_equiv. - rewrite <-le_to_nat. - apply size_le. - Qed. - Lemma shiftr_size : forall n bound, N.size_nat n <= bound -> N.shiftr_nat n bound = 0%N. Proof. @@ -45,7 +17,7 @@ Module N. rewrite Nshiftr_nat_equiv. destruct (N.eq_dec n 0); subst; [apply N.shiftr_0_l|]. apply N.shiftr_eq_0. - rewrite size_nat_equiv in *. + rewrite N.size_nat_equiv in *. rewrite N.size_log2 in * by auto. apply N.le_succ_l. rewrite <- N.compare_le_iff. @@ -114,7 +86,7 @@ Module N. apply WordUtil.bound_check_nat_N. apply Znat.Nat2Z.inj_lt. rewrite Znat.Z2Nat.id by omega. - rewrite ZUtil.Z.pow_Zpow. + rewrite Z.pow_Zpow. replace (Z.of_nat 2) with 2%Z by reflexivity. omega. Qed. @@ -134,13 +106,13 @@ Module N. rewrite WordUtil.wordToNat_combine. rewrite !Word.wordToNat_natToWord_idempotent by (rewrite Nnat.N2Nat.id; auto using ZToN_NPow2_lt). f_equal. - rewrite ZUtil.Z.lor_shiftl by auto. + rewrite Z.lor_shiftl by auto. rewrite !Z_N_nat. rewrite Znat.Z2Nat.inj_add by (try apply Z.shiftl_nonneg; omega). f_equal. rewrite Z.shiftl_mul_pow2 by auto. rewrite Znat.Z2Nat.inj_mul by omega. - rewrite <-ZUtil.Z.pow_Z2N_Zpow by omega. + rewrite <-Z.pow_Z2N_Zpow by omega. rewrite Nat.mul_comm. f_equal. Qed. diff --git a/src/Util/NUtil/WithoutReferenceToZ.v b/src/Util/NUtil/WithoutReferenceToZ.v new file mode 100644 index 000000000..1955b53d2 --- /dev/null +++ b/src/Util/NUtil/WithoutReferenceToZ.v @@ -0,0 +1,54 @@ +(** NUtil that doesn't depend on ZUtil stuff *) +(** Should probably come up with a better organization of this stuff *) +Require Import Coq.NArith.NArith. +Require Import Coq.Numbers.Natural.Peano.NPeano. +Require Import Crypto.Util.NatUtil Crypto.Util.Decidable. + +Module N. + Lemma size_le a b : (a <= b -> N.size a <= N.size b)%N. + Proof. + destruct (dec (a=0)%N), (dec (b=0)%N); subst; auto using N.le_0_l. + { destruct a; auto. } + { rewrite !N.size_log2 by assumption. + rewrite <-N.succ_le_mono. + apply N.log2_le_mono. } + Qed. + + Lemma N_le_1_l : forall p, (1 <= N.pos p)%N. + Proof. + destruct p; cbv; congruence. + Qed. + + Lemma Pos_land_upper_bound_l : forall a b, (Pos.land a b <= N.pos a)%N. + Proof. + induction a as [a IHa|a IHa|]; destruct b as [b|b|]; try solve [cbv; congruence]; + simpl; specialize (IHa b); case_eq (Pos.land a b); intro p; simpl; + try (apply N_le_1_l || apply N.le_0_l); intro land_eq; + rewrite land_eq in *; unfold N.le, N.compare in *; + rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI, ?Pos.compare_xO_xO; + try assumption. + destruct (p ?=a)%positive; cbv; congruence. + Qed. + + Lemma le_to_nat a b : (a <= b)%N <-> (N.to_nat a <= N.to_nat b)%nat. + Proof. + rewrite <-N.lt_succ_r. + rewrite <-Nat.lt_succ_r. + rewrite <-Nnat.N2Nat.inj_succ. + rewrite <-NatUtil.Nat2N_inj_lt. + rewrite !Nnat.N2Nat.id. + reflexivity. + Qed. + + Lemma size_nat_equiv : forall n, N.size_nat n = N.to_nat (N.size n). + Proof. + destruct n as [|p]; auto; simpl; induction p as [p IHp|p IHp|]; simpl; auto; rewrite IHp, Pnat.Pos2Nat.inj_succ; reflexivity. + Qed. + + Lemma size_nat_le a b : (a <= b)%N -> (N.size_nat a <= N.size_nat b)%nat. + Proof. + rewrite !size_nat_equiv. + rewrite <-le_to_nat. + apply size_le. + Qed. +End N. diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v index a59a6bbaa..3db3e3dca 100644 --- a/src/Util/NumTheoryUtil.v +++ b/src/Util/NumTheoryUtil.v @@ -1,6 +1,10 @@ Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv. Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. -Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Divide. +Require Import Crypto.Util.ZUtil.Modulo. +Require Import Crypto.Util.ZUtil.Odd. +Require Import Crypto.Util.NatUtil. +Require Import Crypto.Util.ZUtil.Tactics.PrimeBound. Require Export Crypto.Util.FixCoqMistakes. Require Import Crypto.Util.Tactics.BreakMatch. Local Open Scope Z. @@ -48,9 +52,9 @@ Hypothesis prime_p : prime p. Hypothesis neq_p_2 : p <> 2. (* Euler's Criterion is also provable with p = 2, but we do not need it and are lazy.*) Hypothesis x_id : x * 2 + 1 = p. -Lemma lt_1_p : 1 < p. Proof using prime_p. prime_bound. Qed. -Lemma x_pos: 0 < x. Proof using prime_p x_id. prime_bound. Qed. -Lemma x_nonneg: 0 <= x. Proof using prime_p x_id. prime_bound. Qed. +Lemma lt_1_p : 1 < p. Proof using prime_p. Z.prime_bound. Qed. +Lemma x_pos: 0 < x. Proof using prime_p x_id. Z.prime_bound. Qed. +Lemma x_nonneg: 0 <= x. Proof using prime_p x_id. Z.prime_bound. Qed. Lemma x_id_inv : x = (p - 1) / 2. Proof using x_id. @@ -85,12 +89,12 @@ Lemma fermat_little: forall a (a_nonzero : a mod p <> 0), Proof using prime_p. intros a a_nonzero. assert (rel_prime a p). { - apply rel_prime_mod_rev; try prime_bound. - assert (0 < p) as p_pos by prime_bound. + apply rel_prime_mod_rev; try Z.prime_bound. + assert (0 < p) as p_pos by Z.prime_bound. apply rel_prime_le_prime; auto; pose proof (Z.mod_pos_bound a p p_pos). omega. } - rewrite (Coqprime.PrimalityTest.Zp.Zpower_mod_is_gpow _ _ _ lt_1_p) by (auto || prime_bound). + rewrite (Coqprime.PrimalityTest.Zp.Zpower_mod_is_gpow _ _ _ lt_1_p) by (auto || Z.prime_bound). rewrite <- mod_p_order. apply Coqprime.PrimalityTest.EGroup.fermat_gen; try apply Z.eq_dec. apply Coqprime.PrimalityTest.Zp.in_mod_ZPGroup; auto. @@ -126,14 +130,14 @@ Proof using Type*. assert (b mod p <> 0) as b_nonzero. { intuition. rewrite <- Z.pow_2_r in a_square. - rewrite Z.mod_exp_0 in a_square by prime_bound. + rewrite Z.mod_exp_0 in a_square by Z.prime_bound. rewrite <- a_square in a_nonzero. auto. } pose proof (squared_fermat_little b b_nonzero). - rewrite Z.mod_pow in * by prime_bound. + rewrite Z.mod_pow in * by Z.prime_bound. rewrite <- a_square. - rewrite Z.mod_mod; prime_bound. + rewrite Z.mod_mod; Z.prime_bound. Qed. Lemma exists_primitive_root_power : @@ -174,10 +178,10 @@ Proof using Type*. intros a a_range pow_a_x. destruct (exists_primitive_root_power) as [y [in_ZPGroup_y [y_order gpow_y]]]; auto. destruct (gpow_y a a_range) as [j [j_range pow_y_j]]; clear gpow_y. - rewrite Z.mod_pow in pow_a_x by prime_bound. + rewrite Z.mod_pow in pow_a_x by Z.prime_bound. replace a with (a mod p) in pow_y_j by (apply Z.mod_small; omega). rewrite <- pow_y_j in pow_a_x. - rewrite <- Z.mod_pow in pow_a_x by prime_bound. + rewrite <- Z.mod_pow in pow_a_x by Z.prime_bound. rewrite <- Z.pow_mul_r in pow_a_x by omega. assert (p - 1 | j * x) as divide_mul_j_x. { rewrite <- Coqprime.PrimalityTest.Zp.phi_is_order in y_order. @@ -196,7 +200,7 @@ Proof using Type*. rewrite Z.mul_comm. rewrite x_id_inv in divide_mul_j_x; auto. apply (Z.divide_mul_div _ j 2) in divide_mul_j_x; - try (apply prime_pred_divide2 || prime_bound); auto. + try (apply prime_pred_divide2 || Z.prime_bound); auto. rewrite <- Zdivide_Zdiv_eq by (auto || omega). rewrite Zplus_diag_eq_mult_2. replace (a mod p) with a in pow_y_j by (symmetry; apply Z.mod_small; omega). @@ -296,8 +300,8 @@ Proof. apply (euler_criterion (p / 2) p prime_p). + auto. + apply div2_p_1mod4; auto. - + prime_bound. - + apply minus1_even_pow; [apply divide2_1mod4 | | apply Z_div_pos]; prime_bound. + + Z.prime_bound. + + apply minus1_even_pow; [apply divide2_1mod4 | | apply Z_div_pos]; Z.prime_bound. Qed. diff --git a/src/Util/QUtil.v b/src/Util/QUtil.v index dbdf4fba0..2c2dfd8c8 100644 --- a/src/Util/QUtil.v +++ b/src/Util/QUtil.v @@ -1,6 +1,8 @@ Require Import Coq.ZArith.ZArith Coq.QArith.QArith QArith.Qround. +Require Import Coq.micromega.Lia. Require Import Crypto.Util.Decidable. -Require Import ZUtil Lia. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Morphisms. Local Open Scope Z_scope. diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index cf7732a4c..eda97f556 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -618,6 +618,27 @@ Proof. auto using fieldwiseb'_fieldwise'. Qed. +Lemma map_ext {A B} (f g : A -> B) n (t : tuple A n) : + (forall x : A, f x = g x) -> + map f t = map g t. +Proof. + destruct n; [reflexivity|]; cbn in *. + induction n; cbn in *; intro H; auto; [ ]. + rewrite IHn by assumption. + rewrite H; reflexivity. +Qed. + +Lemma map_ext_In {A B} (f g : A -> B) n (t : tuple A n) : + (forall x, In x (to_list n t) -> f x = g x) -> + map f t = map g t. +Proof. + destruct n; [reflexivity|]; cbn in *. + induction n; cbn in *; intro H; auto; [ ]. + destruct t. + rewrite IHn by auto using in_cons. + rewrite H; auto using in_eq. +Qed. + Fixpoint from_list_default' {T} (d y:T) (n:nat) (xs:list T) : tuple' T n := match n return tuple' T n with diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index 2faafe6c6..932f48fee 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -9,12 +9,15 @@ Require Import Coq.Bool.Bool. Require Import Crypto.Util.Bool. Require Import Crypto.Util.NatUtil. -Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.Tactics.RewriteHyp. Require Import Crypto.Util.Sigma. +Require Import Crypto.Util.ZUtil.LandLorShiftBounds. +Require Import Crypto.Util.ZUtil.N2Z. +Require Import Crypto.Util.ZUtil.Definitions. + Require Import bbv.WordScope. Require Import bbv.Nomega. diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 270bd0c90..765142c39 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1,1520 +1,69 @@ -Require Import Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv. -Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms. -Require Import Coq.Structures.Equalities. -Require Import Coq.omega.Omega Coq.micromega.Psatz Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. -Require Import Crypto.Util.NatUtil. -Require Import Crypto.Util.Tactics.SpecializeBy. -Require Import Crypto.Util.Tactics.BreakMatch. -Require Import Crypto.Util.Tactics.Contains. -Require Import Crypto.Util.Tactics.Not. -Require Import Crypto.Util.Bool. -Require Import Crypto.Util.Notations. -Require Import Coq.Lists.List. -Require Export Crypto.Util.FixCoqMistakes. -Require Export Crypto.Util.ZUtil.Definitions. -Require Export Crypto.Util.ZUtil.Div. -Require Export Crypto.Util.ZUtil.Le. -Require Export Crypto.Util.ZUtil.EquivModulo. -Require Export Crypto.Util.ZUtil.Hints. -Require Export Crypto.Util.ZUtil.Land. -Require Export Crypto.Util.ZUtil.Modulo. -Require Export Crypto.Util.ZUtil.Modulo.PullPush. -Require Export Crypto.Util.ZUtil.Morphisms. -Require Export Crypto.Util.ZUtil.Notations. -Require Export Crypto.Util.ZUtil.Pow2Mod. -Require Export Crypto.Util.ZUtil.Quot. -Require Export Crypto.Util.ZUtil.Sgn. -Require Export Crypto.Util.ZUtil.Tactics. -Require Export Crypto.Util.ZUtil.Testbit. -Require Export Crypto.Util.ZUtil.ZSimplify. -Import Nat. -Local Open Scope Z. - -Module Z. - Lemma mul_comm3 x y z : x * (y * z) = y * (x * z). - Proof. lia. Qed. - - Lemma pos_pow_nat_pos : forall x n, - Z.pos x ^ Z.of_nat n > 0. - Proof. - do 2 (try intros x n; induction n as [|n]; subst; simpl in *; auto with zarith). - rewrite <- Pos.add_1_r, Zpower_pos_is_exp. - apply Zmult_gt_0_compat; auto; reflexivity. - Qed. - - (** TODO: Should we get rid of this duplicate? *) - Notation gt0_neq0 := Z.positive_is_nonzero (only parsing). - - Lemma pow_Z2N_Zpow : forall a n, 0 <= a -> - ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat. - Proof. - intros a n H; induction n as [|n IHn]; try reflexivity. - rewrite Nat2Z.inj_succ. - rewrite pow_succ_r by apply le_0_n. - rewrite Z.pow_succ_r by apply Zle_0_nat. - rewrite IHn. - rewrite Z2Nat.inj_mul; auto using Z.pow_nonneg. - Qed. - - Lemma pow_Zpow : forall a n : nat, Z.of_nat (a ^ n) = Z.of_nat a ^ Z.of_nat n. - Proof with auto using Zle_0_nat, Z.pow_nonneg. - intros; apply Z2Nat.inj... - rewrite <- pow_Z2N_Zpow, !Nat2Z.id... - Qed. - Hint Rewrite pow_Zpow : push_Zof_nat. - Hint Rewrite <- pow_Zpow : pull_Zof_nat. - - Lemma Zpow_sub_1_nat_pow a v - : (Z.pos a^Z.of_nat v - 1 = Z.of_nat (Z.to_nat (Z.pos a)^v - 1))%Z. - Proof. - rewrite <- (Z2Nat.id (Z.pos a)) at 1 by lia. - change 2%Z with (Z.of_nat 2); change 1%Z with (Z.of_nat 1); - autorewrite with pull_Zof_nat. - rewrite Nat2Z.inj_sub - by (change 1%nat with (Z.to_nat (Z.pos a)^0)%nat; apply Nat.pow_le_mono_r; simpl; lia). - reflexivity. - Qed. - Hint Rewrite Zpow_sub_1_nat_pow : pull_Zof_nat. - Hint Rewrite <- Zpow_sub_1_nat_pow : push_Zof_nat. - - Lemma divide_mul_div: forall a b c (a_nonzero : a <> 0) (c_nonzero : c <> 0), - (a | b * (a / c)) -> (c | a) -> (c | b). - Proof. - intros ? ? ? ? ? divide_a divide_c_a; do 2 Z.divide_exists_mul. - rewrite divide_c_a in divide_a. - rewrite Z.div_mul' in divide_a by auto. - replace (b * k) with (k * b) in divide_a by ring. - replace (c * k * k0) with (k * (k0 * c)) in divide_a by ring. - rewrite Z.mul_cancel_l in divide_a by (intuition auto with nia; rewrite H in divide_c_a; ring_simplify in divide_a; intuition). - eapply Zdivide_intro; eauto. - Qed. - - Lemma divide2_even_iff : forall n, (2 | n) <-> Z.even n = true. - Proof. - intros n; split. { - intro divide2_n. - Z.divide_exists_mul; [ | pose proof (Z.mod_pos_bound n 2); omega]. - rewrite divide2_n. - apply Z.even_mul. - } { - intro n_even. - pose proof (Zmod_even n) as H. - rewrite n_even in H. - apply Zmod_divide; omega || auto. - } - Qed. - - Lemma prime_odd_or_2 : forall p (prime_p : prime p), p = 2 \/ Z.odd p = true. - Proof. - intros p prime_p. - apply Decidable.imp_not_l; try apply Z.eq_decidable. - intros p_neq2. - pose proof (Zmod_odd p) as mod_odd. - destruct (Sumbool.sumbool_of_bool (Z.odd p)) as [? | p_not_odd]; auto. - rewrite p_not_odd in mod_odd. - apply Zmod_divides in mod_odd; try omega. - destruct mod_odd as [c c_id]. - rewrite Z.mul_comm in c_id. - apply Zdivide_intro in c_id. - apply prime_divisors in c_id; auto. - destruct c_id; [omega | destruct H; [omega | destruct H; auto] ]. - pose proof (prime_ge_2 p prime_p); omega. - Qed. - - Lemma shiftr_add_shiftl_high : forall n m a b, 0 <= n <= m -> 0 <= a < 2 ^ n -> - Z.shiftr (a + (Z.shiftl b n)) m = Z.shiftr b (m - n). - Proof. - intros n m a b H H0. - rewrite !Z.shiftr_div_pow2, Z.shiftl_mul_pow2 by omega. - replace (2 ^ m) with (2 ^ n * 2 ^ (m - n)) by - (rewrite <-Z.pow_add_r by omega; f_equal; ring). - rewrite <-Z.div_div, Z.div_add, (Z.div_small a) ; try solve - [assumption || apply Z.pow_nonzero || apply Z.pow_pos_nonneg; omega]. - f_equal; ring. - Qed. - Hint Rewrite Z.shiftr_add_shiftl_high using zutil_arith : pull_Zshift. - Hint Rewrite <- Z.shiftr_add_shiftl_high using zutil_arith : push_Zshift. - - Lemma shiftr_add_shiftl_low : forall n m a b, 0 <= m <= n -> 0 <= a < 2 ^ n -> - Z.shiftr (a + (Z.shiftl b n)) m = Z.shiftr a m + Z.shiftr b (m - n). - Proof. - intros n m a b H H0. - rewrite !Z.shiftr_div_pow2, Z.shiftl_mul_pow2, Z.shiftr_mul_pow2 by omega. - replace (2 ^ n) with (2 ^ (n - m) * 2 ^ m) by - (rewrite <-Z.pow_add_r by omega; f_equal; ring). - rewrite Z.mul_assoc, Z.div_add by (apply Z.pow_nonzero; omega). - repeat f_equal; ring. - Qed. - Hint Rewrite Z.shiftr_add_shiftl_low using zutil_arith : pull_Zshift. - Hint Rewrite <- Z.shiftr_add_shiftl_low using zutil_arith : push_Zshift. - - Lemma testbit_add_shiftl_high : forall i, (0 <= i) -> forall a b n, (0 <= n <= i) -> - 0 <= a < 2 ^ n -> - Z.testbit (a + Z.shiftl b n) i = Z.testbit b (i - n). - Proof. - intros i ?. - apply natlike_ind with (x := i); [ intros a b n | intros x H0 H1 a b n | ]; intros; try assumption; - (destruct (Z.eq_dec 0 n); [ subst; rewrite Z.pow_0_r in *; - replace a with 0 by omega; f_equal; ring | ]); try omega. - rewrite <-Z.add_1_r at 1. rewrite <-Z.shiftr_spec by assumption. - replace (Z.succ x - n) with (x - (n - 1)) by ring. - rewrite shiftr_add_shiftl_low, <-Z.shiftl_opp_r with (a := b) by omega. - rewrite <-H1 with (a := Z.shiftr a 1); try omega; [ repeat f_equal; ring | ]. - rewrite Z.shiftr_div_pow2 by omega. - split; apply Z.div_pos || apply Z.div_lt_upper_bound; - try solve [rewrite ?Z.pow_1_r; omega]. - rewrite <-Z.pow_add_r by omega. - replace (1 + (n - 1)) with n by ring; omega. - Qed. - Hint Rewrite testbit_add_shiftl_high using zutil_arith : Ztestbit. - - Lemma nonneg_pow_pos a b : 0 < a -> 0 < a^b -> 0 <= b. - Proof. - destruct (Z_lt_le_dec b 0); intros; auto. - erewrite Z.pow_neg_r in * by eassumption. - omega. - Qed. - Hint Resolve nonneg_pow_pos (fun n => nonneg_pow_pos 2 n Z.lt_0_2) : zarith. - Lemma nonneg_pow_pos_helper a b dummy : 0 < a -> 0 <= dummy < a^b -> 0 <= b. - Proof. eauto with zarith omega. Qed. - Hint Resolve nonneg_pow_pos_helper (fun n dummy => nonneg_pow_pos_helper 2 n dummy Z.lt_0_2) : zarith. - - Lemma testbit_add_shiftl_full i (Hi : 0 <= i) a b n (Ha : 0 <= a < 2^n) - : Z.testbit (a + b << n) i - = if (i <? n) then Z.testbit a i else Z.testbit b (i - n). - Proof. - assert (0 < 2^n) by omega. - assert (0 <= n) by eauto 2 with zarith. - pose proof (Zlt_cases i n); break_match; autorewrite with Ztestbit; reflexivity. - Qed. - Hint Rewrite testbit_add_shiftl_full using zutil_arith : Ztestbit. - - Lemma land_add_land : forall n m a b, (m <= n)%nat -> - Z.land ((Z.land a (Z.ones (Z.of_nat n))) + (Z.shiftl b (Z.of_nat n))) (Z.ones (Z.of_nat m)) = Z.land a (Z.ones (Z.of_nat m)). - Proof. - intros n m a b H. - rewrite !Z.land_ones by apply Nat2Z.is_nonneg. - rewrite Z.shiftl_mul_pow2 by apply Nat2Z.is_nonneg. - replace (b * 2 ^ Z.of_nat n) with - ((b * 2 ^ Z.of_nat (n - m)) * 2 ^ Z.of_nat m) by - (rewrite (le_plus_minus m n) at 2; try assumption; - rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg; ring). - rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat m)); omega). - symmetry. apply Znumtheory.Zmod_div_mod; try (apply Z.pow_pos_nonneg; omega). - rewrite (le_plus_minus m n) by assumption. - rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg. - apply Z.divide_factor_l. - Qed. - - Lemma div_pow2succ : forall n x, (0 <= x) -> - n / 2 ^ Z.succ x = Z.div2 (n / 2 ^ x). - Proof. - intros. - rewrite Z.pow_succ_r, Z.mul_comm by auto. - rewrite <- Z.div_div by (try apply Z.pow_nonzero; omega). - rewrite Zdiv2_div. - reflexivity. - Qed. - - Lemma shiftr_succ : forall n x, - Z.shiftr n (Z.succ x) = Z.shiftr (Z.shiftr n x) 1. - Proof. - intros. - rewrite Z.shiftr_shiftr by omega. - reflexivity. - Qed. - Hint Rewrite Z.shiftr_succ using zutil_arith : push_Zshift. - Hint Rewrite <- Z.shiftr_succ using zutil_arith : pull_Zshift. - - Lemma pow2_lt_or_divides : forall a b, 0 <= b -> - 2 ^ a < 2 ^ b \/ (2 ^ a) mod 2 ^ b = 0. - Proof. - intros a b H. - destruct (Z_lt_dec a b); [left|right]. - { apply Z.pow_lt_mono_r; auto; omega. } - { replace a with (a - b + b) by ring. - rewrite Z.pow_add_r by omega. - apply Z.mod_mul, Z.pow_nonzero; omega. } - Qed. - - Lemma odd_mod : forall a b, (b <> 0)%Z -> - Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a. - Proof. - intros a b H. - rewrite Zmod_eq_full by assumption. - rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul. - case_eq (Z.odd b); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r. - Qed. - - Lemma mod_same_pow : forall a b c, 0 <= c <= b -> a ^ b mod a ^ c = 0. - Proof. - intros a b c H. - replace b with (b - c + c) by ring. - rewrite Z.pow_add_r by omega. - apply Z_mod_mult. - Qed. - Hint Rewrite mod_same_pow using zutil_arith : zsimplify. - - Lemma ones_succ : forall x, (0 <= x) -> - Z.ones (Z.succ x) = 2 ^ x + Z.ones x. - Proof. - unfold Z.ones; intros. - rewrite !Z.shiftl_1_l. - rewrite Z.add_pred_r. - apply Z.succ_inj. - rewrite !Z.succ_pred. - rewrite Z.pow_succ_r; omega. - Qed. - - Lemma div_floor : forall a b c, 0 < b -> a < b * (Z.succ c) -> a / b <= c. - Proof. - intros. - apply Z.lt_succ_r. - apply Z.div_lt_upper_bound; try omega. - Qed. - - Lemma shiftr_1_r_le : forall a b, a <= b -> - Z.shiftr a 1 <= Z.shiftr b 1. - Proof. - intros. - rewrite !Z.shiftr_div_pow2, Z.pow_1_r by omega. - apply Z.div_le_mono; omega. - Qed. - Hint Resolve shiftr_1_r_le : zarith. - - Lemma shiftr_le : forall a b i : Z, 0 <= i -> a <= b -> a >> i <= b >> i. - Proof. - intros a b i ?; revert a b. apply natlike_ind with (x := i); intros; auto. - rewrite !shiftr_succ, shiftr_1_r_le; eauto. reflexivity. - Qed. - Hint Resolve shiftr_le : zarith. - - Lemma ones_pred : forall i, 0 < i -> Z.ones (Z.pred i) = Z.shiftr (Z.ones i) 1. - Proof. - induction i as [|p|p]; [ | | pose proof (Pos2Z.neg_is_neg p) ]; try omega. - intros. - unfold Z.ones. - rewrite !Z.shiftl_1_l, Z.shiftr_div_pow2, <-!Z.sub_1_r, Z.pow_1_r, <-!Z.add_opp_r by omega. - replace (2 ^ (Z.pos p)) with (2 ^ (Z.pos p - 1)* 2). - rewrite Z.div_add_l by omega. - reflexivity. - change 2 with (2 ^ 1) at 2. - rewrite <-Z.pow_add_r by (pose proof (Pos2Z.is_pos p); omega). - f_equal. omega. - Qed. - Hint Rewrite <- ones_pred using zutil_arith : push_Zshift. - - Lemma shiftr_ones' : forall a n, 0 <= a < 2 ^ n -> forall i, (0 <= i) -> - Z.shiftr a i <= Z.ones (n - i) \/ n <= i. - Proof. - intros a n H. - apply natlike_ind. - + unfold Z.ones. - rewrite Z.shiftr_0_r, Z.shiftl_1_l, Z.sub_0_r. - omega. - + intros x H0 H1. - destruct (Z_lt_le_dec x n); try omega. - intuition auto with zarith lia. - left. - rewrite shiftr_succ. - replace (n - Z.succ x) with (Z.pred (n - x)) by omega. - rewrite Z.ones_pred by omega. - apply Z.shiftr_1_r_le. - assumption. - Qed. - - Lemma shiftr_ones : forall a n i, 0 <= a < 2 ^ n -> (0 <= i) -> (i <= n) -> - Z.shiftr a i <= Z.ones (n - i) . - Proof. - intros a n i G G0 G1. - destruct (Z_le_lt_eq_dec i n G1). - + destruct (Z.shiftr_ones' a n G i G0); omega. - + subst; rewrite Z.sub_diag. - destruct (Z.eq_dec a 0). - - subst; rewrite Z.shiftr_0_l; reflexivity. - - rewrite Z.shiftr_eq_0; try omega; try reflexivity. - apply Z.log2_lt_pow2; omega. - Qed. - Hint Resolve shiftr_ones : zarith. - - Lemma shiftr_upper_bound : forall a n, 0 <= n -> 0 <= a <= 2 ^ n -> Z.shiftr a n <= 1. - Proof. - intros a ? ? [a_nonneg a_upper_bound]. - apply Z_le_lt_eq_dec in a_upper_bound. - destruct a_upper_bound. - + destruct (Z.eq_dec 0 a). - - subst; rewrite Z.shiftr_0_l; omega. - - rewrite Z.shiftr_eq_0; auto; try omega. - apply Z.log2_lt_pow2; auto; omega. - + subst. - rewrite Z.shiftr_div_pow2 by assumption. - rewrite Z.div_same; try omega. - assert (0 < 2 ^ n) by (apply Z.pow_pos_nonneg; omega). - omega. - Qed. - Hint Resolve shiftr_upper_bound : zarith. - - Lemma lor_shiftl : forall a b n, 0 <= n -> 0 <= a < 2 ^ n -> - Z.lor a (Z.shiftl b n) = a + (Z.shiftl b n). - Proof. - intros a b n H H0. - apply Z.bits_inj'; intros t ?. - rewrite Z.lor_spec, Z.shiftl_spec by assumption. - destruct (Z_lt_dec t n). - + rewrite Z.testbit_add_shiftl_low by omega. - rewrite Z.testbit_neg_r with (n := t - n) by omega. - apply Bool.orb_false_r. - + rewrite testbit_add_shiftl_high by omega. - replace (Z.testbit a t) with false; [ apply Bool.orb_false_l | ]. - symmetry. - apply Z.testbit_false; try omega. - rewrite Z.div_small; try reflexivity. - split; try eapply Z.lt_le_trans with (m := 2 ^ n); try omega. - apply Z.pow_le_mono_r; omega. - Qed. - Hint Rewrite <- Z.lor_shiftl using zutil_arith : convert_to_Ztestbit. - - Lemma lor_shiftl' : forall a b n, 0 <= n -> 0 <= a < 2 ^ n -> - Z.lor (Z.shiftl b n) a = (Z.shiftl b n) + a. - Proof. - intros; rewrite Z.lor_comm, Z.add_comm; apply lor_shiftl; assumption. - Qed. - Hint Rewrite <- Z.lor_shiftl' using zutil_arith : convert_to_Ztestbit. - - Lemma shiftl_spec_full a n m - : Z.testbit (a << n) m = if Z_lt_dec m n - then false - else if Z_le_dec 0 m - then Z.testbit a (m - n) - else false. - Proof. - repeat break_match; auto using Z.shiftl_spec_low, Z.shiftl_spec, Z.testbit_neg_r with omega. - Qed. - Hint Rewrite shiftl_spec_full : Ztestbit_full. - - Lemma shiftr_spec_full a n m - : Z.testbit (a >> n) m = if Z_lt_dec m (-n) - then false - else if Z_le_dec 0 m - then Z.testbit a (m + n) - else false. - Proof. - rewrite <- Z.shiftl_opp_r, shiftl_spec_full, Z.sub_opp_r; reflexivity. - Qed. - Hint Rewrite shiftr_spec_full : Ztestbit_full. - - Lemma lnot_sub1 x : Z.lnot (x-1) = (-x). - Proof. - replace (-x) with (- (1) - (x - 1)) by omega. - rewrite <-(Z.add_lnot_diag (x-1)); omega. - Qed. - - Lemma lnot_opp x : Z.lnot (- x) = x-1. - Proof. - rewrite <-Z.lnot_involutive, lnot_sub1; reflexivity. - Qed. - - Lemma testbit_sub_pow2 n i x (i_range:0 <= i < n) (x_range:0 < x < 2 ^ n) : - Z.testbit (2 ^ n - x) i = negb (Z.testbit (x - 1) i). - Proof. - rewrite <-Z.lnot_spec, lnot_sub1 by omega. - rewrite <-(Z.mod_pow2_bits_low (-x) _ _ (proj2 i_range)). - f_equal. - rewrite Z.mod_opp_l_nz; autorewrite with zsimplify; omega. - Qed. - - Lemma ones_nonneg : forall i, (0 <= i) -> 0 <= Z.ones i. - Proof. - apply natlike_ind. - + unfold Z.ones. simpl; omega. - + intros. - rewrite Z.ones_succ by assumption. - Z.zero_bounds. - Qed. - Hint Resolve ones_nonneg : zarith. - - Lemma ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i. - Proof. - intros. - unfold Z.ones. - rewrite Z.shiftl_1_l. - apply Z.lt_succ_lt_pred. - apply Z.pow_gt_1; omega. - Qed. - Hint Resolve ones_pos_pos : zarith. - - Lemma pow2_mod_id_iff : forall a n, 0 <= n -> - (Z.pow2_mod a n = a <-> 0 <= a < 2 ^ n). - Proof. - intros a n H. - rewrite Z.pow2_mod_spec by assumption. - assert (0 < 2 ^ n) by Z.zero_bounds. - rewrite Z.mod_small_iff by omega. - split; intros; intuition omega. - Qed. - - Lemma testbit_false_bound : forall a x, 0 <= x -> - (forall n, ~ (n < x) -> Z.testbit a n = false) -> - a < 2 ^ x. - Proof. - intros a x H H0. - assert (H1 : a = Z.pow2_mod a x). { - apply Z.bits_inj'; intros. - rewrite Z.testbit_pow2_mod by omega; break_match; auto. - } - rewrite H1. - rewrite Z.pow2_mod_spec; try apply Z.mod_pos_bound; Z.zero_bounds. - Qed. - - Lemma lor_range : forall x y n, 0 <= x < 2 ^ n -> 0 <= y < 2 ^ n -> - 0 <= Z.lor x y < 2 ^ n. - Proof. - intros x y n H H0; assert (0 <= n) by auto with zarith omega. - repeat match goal with - | |- _ => progress intros - | |- _ => rewrite Z.lor_spec - | |- _ => rewrite Z.testbit_eqb by auto with zarith omega - | |- _ => rewrite !Z.div_small by (split; try omega; eapply Z.lt_le_trans; - [ intuition eassumption | apply Z.pow_le_mono_r; omega]) - | |- _ => split - | |- _ => apply testbit_false_bound - | |- _ => solve [auto with zarith] - | |- _ => solve [apply Z.lor_nonneg; intuition auto] - end. - Qed. - Hint Resolve lor_range : zarith. - - Lemma lor_shiftl_bounds : forall x y n m, - (0 <= n)%Z -> (0 <= m)%Z -> - (0 <= x < 2 ^ m)%Z -> - (0 <= y < 2 ^ n)%Z -> - (0 <= Z.lor y (Z.shiftl x n) < 2 ^ (n + m))%Z. - Proof. - intros x y n m H H0 H1 H2. - apply Z.lor_range. - { split; try omega. - apply Z.lt_le_trans with (m := (2 ^ n)%Z); try omega. - apply Z.pow_le_mono_r; omega. } - { rewrite Z.shiftl_mul_pow2 by omega. - rewrite Z.pow_add_r by omega. - split; Z.zero_bounds. - rewrite Z.mul_comm. - apply Z.mul_lt_mono_pos_l; omega. } - Qed. - - Lemma N_le_1_l : forall p, (1 <= N.pos p)%N. - Proof. - destruct p; cbv; congruence. - Qed. - - Lemma Pos_land_upper_bound_l : forall a b, (Pos.land a b <= N.pos a)%N. - Proof. - induction a as [a IHa|a IHa|]; destruct b as [b|b|]; try solve [cbv; congruence]; - simpl; specialize (IHa b); case_eq (Pos.land a b); intro p; simpl; - try (apply N_le_1_l || apply N.le_0_l); intro land_eq; - rewrite land_eq in *; unfold N.le, N.compare in *; - rewrite ?Pos.compare_xI_xI, ?Pos.compare_xO_xI, ?Pos.compare_xO_xO; - try assumption. - destruct (p ?=a)%positive; cbv; congruence. - Qed. - - Lemma land_upper_bound_l : forall a b, (0 <= a) -> (0 <= b) -> - Z.land a b <= a. - Proof. - intros a b H H0. - destruct a, b; try solve [exfalso; auto]; try solve [cbv; congruence]. - cbv [Z.land]. - rewrite <-N2Z.inj_pos, <-N2Z.inj_le. - auto using Pos_land_upper_bound_l. - Qed. - - Lemma land_upper_bound_r : forall a b, (0 <= a) -> (0 <= b) -> - Z.land a b <= b. - Proof. - intros. - rewrite Z.land_comm. - auto using Z.land_upper_bound_l. - Qed. - - Lemma le_fold_right_max : forall low l x, (forall y, In y l -> low <= y) -> - In x l -> x <= fold_right Z.max low l. - Proof. - induction l as [|a l IHl]; intros ? lower_bound In_list; [cbv [In] in *; intuition | ]. - simpl. - destruct (in_inv In_list); subst. - + apply Z.le_max_l. - + etransitivity. - - apply IHl; auto; intuition auto with datatypes. - - apply Z.le_max_r. - Qed. - - Lemma le_fold_right_max_initial : forall low l, low <= fold_right Z.max low l. - Proof. - induction l as [|a l IHl]; intros; try reflexivity. - etransitivity; [ apply IHl | apply Z.le_max_r ]. - Qed. - - Lemma add_compare_mono_r: forall n m p, (n + p ?= m + p) = (n ?= m). - Proof. - intros n m p. - rewrite <-!(Z.add_comm p). - apply Z.add_compare_mono_l. - Qed. - - Lemma compare_add_shiftl : forall x1 y1 x2 y2 n, 0 <= n -> - Z.pow2_mod x1 n = x1 -> Z.pow2_mod x2 n = x2 -> - x1 + (y1 << n) ?= x2 + (y2 << n) = - if Z.eq_dec y1 y2 - then x1 ?= x2 - else y1 ?= y2. - Proof. - repeat match goal with - | |- _ => progress intros - | |- _ => progress subst y1 - | |- _ => rewrite Z.shiftl_mul_pow2 by omega - | |- _ => rewrite add_compare_mono_r - | |- _ => rewrite <-Z.mul_sub_distr_r - | |- _ => break_innermost_match_step - | H : Z.pow2_mod _ _ = _ |- _ => rewrite pow2_mod_id_iff in H by omega - | H : ?a <> ?b |- _ = (?a ?= ?b) => - case_eq (a ?= b); rewrite ?Z.compare_eq_iff, ?Z.compare_gt_iff, ?Z.compare_lt_iff - | |- _ + (_ * _) > _ + (_ * _) => cbv [Z.gt] - | |- _ + (_ * ?x) < _ + (_ * ?x) => - apply Z.lt_sub_lt_add; apply Z.lt_le_trans with (m := 1 * x); [omega|] - | |- _ => apply Z.mul_le_mono_nonneg_r; omega - | |- _ => reflexivity - | |- _ => congruence - end. - Qed. - - Lemma ones_le x y : x <= y -> Z.ones x <= Z.ones y. - Proof. - rewrite !Z.ones_equiv; auto with zarith. - Qed. - Hint Resolve ones_le : zarith. - - Lemma mul_div_le x y z - (Hx : 0 <= x) (Hy : 0 <= y) (Hz : 0 < z) - (Hyz : y <= z) - : x * y / z <= x. - Proof. - transitivity (x * z / z); [ | rewrite Z.div_mul by lia; lia ]. - apply Z_div_le; nia. - Qed. - - Hint Resolve mul_div_le : zarith. - - Lemma div_mul_diff_exact a b c - (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) - : c * a / b = c * (a / b) + (c * (a mod b)) / b. - Proof. - rewrite (Z_div_mod_eq a b) at 1 by lia. - rewrite Z.mul_add_distr_l. - replace (c * (b * (a / b))) with ((c * (a / b)) * b) by lia. - rewrite Z.div_add_l by lia. - lia. - Qed. - - Lemma div_mul_diff_exact' a b c - (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) - : c * (a / b) = c * a / b - (c * (a mod b)) / b. - Proof. - rewrite div_mul_diff_exact by assumption; lia. - Qed. - - Lemma div_mul_diff_exact'' a b c - (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) - : a * c / b = (a / b) * c + (c * (a mod b)) / b. - Proof. - rewrite (Z.mul_comm a c), div_mul_diff_exact by lia; lia. - Qed. - - Lemma div_mul_diff_exact''' a b c - (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) - : (a / b) * c = a * c / b - (c * (a mod b)) / b. - Proof. - rewrite (Z.mul_comm a c), div_mul_diff_exact by lia; lia. - Qed. - - Lemma div_mul_diff a b c - (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) - : c * a / b - c * (a / b) <= c. - Proof. - rewrite div_mul_diff_exact by assumption. - ring_simplify; auto with zarith. - Qed. - - Lemma div_mul_le_le a b c - : 0 <= a -> 0 < b -> 0 <= c -> c * (a / b) <= c * a / b <= c * (a / b) + c. - Proof. - pose proof (Z.div_mul_diff a b c); split; try apply Z.div_mul_le; lia. - Qed. - - Lemma div_mul_le_le_offset a b c - : 0 <= a -> 0 < b -> 0 <= c -> c * a / b - c <= c * (a / b). - Proof. - pose proof (Z.div_mul_le_le a b c); lia. - Qed. - - Hint Resolve Zmult_le_compat_r Zmult_le_compat_l Z_div_le Z.div_mul_le_le_offset Z.add_le_mono Z.sub_le_mono : zarith. - - Lemma log2_nonneg' n a : n <= 0 -> n <= Z.log2 a. - Proof. - intros; transitivity 0; auto with zarith. - Qed. - - Hint Resolve log2_nonneg' : zarith. - - Lemma le_lt_to_log2 x y z : 0 <= z -> 0 < y -> 2^x <= y < 2^z -> x <= Z.log2 y < z. - Proof. - destruct (Z_le_gt_dec 0 x); auto with concl_log2 lia. - Qed. - - Lemma div_x_y_x x y : 0 < x -> 0 < y -> x / y / x = 1 / y. - Proof. - intros; rewrite Z.div_div, (Z.mul_comm y x), <- Z.div_div, Z.div_same by lia. - reflexivity. - Qed. - - Hint Rewrite div_x_y_x using zutil_arith : zsimplify. - - Lemma mod_opp_l_z_iff a b (H : b <> 0) : a mod b = 0 <-> (-a) mod b = 0. - Proof. - split; intro H'; apply Z.mod_opp_l_z in H'; rewrite ?Z.opp_involutive in H'; assumption. - Qed. - - Lemma opp_eq_0_iff a : -a = 0 <-> a = 0. - Proof. omega. Qed. - - Hint Rewrite <- mod_opp_l_z_iff using zutil_arith : zsimplify. - Hint Rewrite opp_eq_0_iff : zsimplify. - - Lemma sub_pos_bound a b X : 0 <= a < X -> 0 <= b < X -> -X < a - b < X. - Proof. lia. Qed. - - Lemma shiftl_opp_l a n - : Z.shiftl (-a) n = - Z.shiftl a n - (if Z_zerop (a mod 2 ^ (- n)) then 0 else 1). - Proof. - destruct (Z_dec 0 n) as [ [?|?] | ? ]; - subst; - rewrite ?Z.pow_neg_r by omega; - autorewrite with zsimplify_const; - [ | | simpl; omega ]. - { rewrite !Z.shiftl_mul_pow2 by omega. - nia. } - { rewrite !Z.shiftl_div_pow2 by omega. - rewrite Z.div_opp_l_complete by auto with zarith. - reflexivity. } - Qed. - Hint Rewrite shiftl_opp_l : push_Zshift. - Hint Rewrite <- shiftl_opp_l : pull_Zshift. - - Lemma shiftr_opp_l a n - : Z.shiftr (-a) n = - Z.shiftr a n - (if Z_zerop (a mod 2 ^ n) then 0 else 1). - Proof. - unfold Z.shiftr; rewrite shiftl_opp_l at 1; rewrite Z.opp_involutive. - reflexivity. - Qed. - Hint Rewrite shiftr_opp_l : push_Zshift. - Hint Rewrite <- shiftr_opp_l : pull_Zshift. - - Lemma sub_pos_bound_div a b X : 0 <= a < X -> 0 <= b < X -> -1 <= (a - b) / X <= 0. - Proof. - intros H0 H1; pose proof (Z.sub_pos_bound a b X H0 H1). - assert (Hn : -X <= a - b) by lia. - assert (Hp : a - b <= X - 1) by lia. - split; etransitivity; [ | apply Z_div_le, Hn; lia | apply Z_div_le, Hp; lia | ]; - instantiate; autorewrite with zsimplify; try reflexivity. - Qed. - - Hint Resolve (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) - (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) : zarith. - - Lemma sub_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (a - b) / X = if a <? b then -1 else 0. - Proof. - intros H0 H1; pose proof (Z.sub_pos_bound_div a b X H0 H1). - destruct (a <? b) eqn:?; Z.ltb_to_lt. - { cut ((a - b) / X <> 0); [ lia | ]. - autorewrite with zstrip_div; auto with zarith lia. } - { autorewrite with zstrip_div; auto with zarith lia. } - Qed. - - Lemma add_opp_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (-b + a) / X = if a <? b then -1 else 0. - Proof. - rewrite !(Z.add_comm (-_)), !Z.add_opp_r. - apply Z.sub_pos_bound_div_eq. - Qed. - - Hint Rewrite Z.sub_pos_bound_div_eq Z.add_opp_pos_bound_div_eq using zutil_arith : zstrip_div. - - Lemma div_small_sym a b : 0 <= a < b -> 0 = a / b. - Proof. intros; symmetry; apply Z.div_small; assumption. Qed. - - Lemma mod_small_sym a b : 0 <= a < b -> a = a mod b. - Proof. intros; symmetry; apply Z.mod_small; assumption. Qed. - - Hint Resolve div_small_sym mod_small_sym : zarith. - - Lemma mod_eq_le_to_eq a b : 0 < a <= b -> a mod b = 0 -> a = b. - Proof. - intros H H'. - assert (a = b * (a / b)) by auto with zarith lia. - assert (a / b = 1) by nia. - nia. - Qed. - Hint Resolve mod_eq_le_to_eq : zarith. - - Lemma mod_eq_le_div_1 a b : 0 < a <= b -> a mod b = 0 -> a / b = 1. - Proof. auto with zarith. Qed. - Hint Resolve mod_eq_le_div_1 : zarith. - Hint Rewrite mod_eq_le_div_1 using zutil_arith : zsimplify. - - Lemma mod_neq_0_le_to_neq a b : a mod b <> 0 -> a <> b. - Proof. repeat intro; subst; autorewrite with zsimplify in *; lia. Qed. - Hint Resolve mod_neq_0_le_to_neq : zarith. - - Lemma div_small_neg x y : 0 < -x <= y -> x / y = -1. - Proof. - intro H; rewrite <- (Z.opp_involutive x). - rewrite Z.div_opp_l_complete by lia. - generalize dependent (-x); clear x; intros x H. - pose proof (mod_neq_0_le_to_neq x y). - autorewrite with zsimplify; edestruct Z_zerop; autorewrite with zsimplify in *; lia. - Qed. - Hint Rewrite div_small_neg using zutil_arith : zsimplify. - - Lemma div_sub_small x y z : 0 <= x < z -> 0 <= y <= z -> (x - y) / z = if x <? y then -1 else 0. - Proof. - pose proof (Zlt_cases x y). - (destruct (x <? y) eqn:?); - intros; autorewrite with zsimplify; try lia. - Qed. - Hint Rewrite div_sub_small using zutil_arith : zsimplify. - - Lemma le_lt_trans n m p : n <= m -> m < p -> n < p. - Proof. lia. Qed. - - Lemma mul_div_lt_by_le x y z b : 0 <= y < z -> 0 <= x < b -> x * y / z < b. - Proof. - intros [? ?] [? ?]; eapply Z.le_lt_trans; [ | eassumption ]. - auto with zarith. - Qed. - Hint Resolve mul_div_lt_by_le : zarith. - - Definition pow_sub_r' - := fun a b c y H0 H1 => @Logic.eq_trans _ _ _ y (@Z.pow_sub_r a b c H0 H1). - Definition pow_sub_r'_sym - := fun a b c y p H0 H1 => Logic.eq_sym (@Logic.eq_trans _ y _ _ (Logic.eq_sym p) (@Z.pow_sub_r a b c H0 H1)). - Hint Resolve pow_sub_r' pow_sub_r'_sym Z.eq_le_incl : zarith. - Hint Resolve (fun b => f_equal (fun e => b ^ e)) (fun e => f_equal (fun b => b ^ e)) : zarith. - Definition mul_div_le' - := fun x y z w p H0 H1 H2 H3 => @Z.le_trans _ _ w (@Z.mul_div_le x y z H0 H1 H2 H3) p. - Hint Resolve mul_div_le' : zarith. - Lemma mul_div_le'' x y z w : y <= w -> 0 <= x -> 0 <= y -> 0 < z -> x <= z -> x * y / z <= w. - Proof. - rewrite (Z.mul_comm x y); intros; apply mul_div_le'; assumption. - Qed. - Hint Resolve mul_div_le'' : zarith. - - Lemma two_p_two_eq_four : 2^(2) = 4. - Proof. reflexivity. Qed. - Hint Rewrite <- two_p_two_eq_four : push_Zpow. - - Lemma base_pow_neg b n : n < 0 -> b^n = 0. - Proof. - destruct n; intro H; try reflexivity; compute in H; congruence. - Qed. - Hint Rewrite base_pow_neg using zutil_arith : zsimplify. - - Lemma div_mod' a b : b <> 0 -> a = (a / b) * b + a mod b. - Proof. intro; etransitivity; [ apply (Z.div_mod a b); assumption | lia ]. Qed. - Hint Rewrite <- div_mod' using zutil_arith : zsimplify. - - Lemma div_mod'' a b : b <> 0 -> a = a mod b + b * (a / b). - Proof. intro; etransitivity; [ apply (Z.div_mod a b); assumption | lia ]. Qed. - Hint Rewrite <- div_mod'' using zutil_arith : zsimplify. - - Lemma div_mod''' a b : b <> 0 -> a = a mod b + (a / b) * b. - Proof. intro; etransitivity; [ apply (Z.div_mod a b); assumption | lia ]. Qed. - Hint Rewrite <- div_mod''' using zutil_arith : zsimplify. - - Definition opp_distr_if (b : bool) x y : -(if b then x else y) = if b then -x else -y. - Proof. destruct b; reflexivity. Qed. - Hint Rewrite opp_distr_if : push_Zopp. - Hint Rewrite <- opp_distr_if : pull_Zopp. - - Lemma mul_r_distr_if (b : bool) x y z : z * (if b then x else y) = if b then z * x else z * y. - Proof. destruct b; reflexivity. Qed. - Hint Rewrite mul_r_distr_if : push_Zmul. - Hint Rewrite <- mul_r_distr_if : pull_Zmul. - - Lemma mul_l_distr_if (b : bool) x y z : (if b then x else y) * z = if b then x * z else y * z. - Proof. destruct b; reflexivity. Qed. - Hint Rewrite mul_l_distr_if : push_Zmul. - Hint Rewrite <- mul_l_distr_if : pull_Zmul. - - Lemma add_r_distr_if (b : bool) x y z : z + (if b then x else y) = if b then z + x else z + y. - Proof. destruct b; reflexivity. Qed. - Hint Rewrite add_r_distr_if : push_Zadd. - Hint Rewrite <- add_r_distr_if : pull_Zadd. - - Lemma add_l_distr_if (b : bool) x y z : (if b then x else y) + z = if b then x + z else y + z. - Proof. destruct b; reflexivity. Qed. - Hint Rewrite add_l_distr_if : push_Zadd. - Hint Rewrite <- add_l_distr_if : pull_Zadd. - - Lemma sub_r_distr_if (b : bool) x y z : z - (if b then x else y) = if b then z - x else z - y. - Proof. destruct b; reflexivity. Qed. - Hint Rewrite sub_r_distr_if : push_Zsub. - Hint Rewrite <- sub_r_distr_if : pull_Zsub. - - Lemma sub_l_distr_if (b : bool) x y z : (if b then x else y) - z = if b then x - z else y - z. - Proof. destruct b; reflexivity. Qed. - Hint Rewrite sub_l_distr_if : push_Zsub. - Hint Rewrite <- sub_l_distr_if : pull_Zsub. - - Lemma div_r_distr_if (b : bool) x y z : z / (if b then x else y) = if b then z / x else z / y. - Proof. destruct b; reflexivity. Qed. - Hint Rewrite div_r_distr_if : push_Zdiv. - Hint Rewrite <- div_r_distr_if : pull_Zdiv. - - Lemma div_l_distr_if (b : bool) x y z : (if b then x else y) / z = if b then x / z else y / z. - Proof. destruct b; reflexivity. Qed. - Hint Rewrite div_l_distr_if : push_Zdiv. - Hint Rewrite <- div_l_distr_if : pull_Zdiv. - - Lemma sub_mod_mod_0 x d : (x - x mod d) mod d = 0. - Proof. - destruct (Z_zerop d); subst; autorewrite with push_Zmod zsimplify; reflexivity. - Qed. - Hint Resolve sub_mod_mod_0 : zarith. - Hint Rewrite sub_mod_mod_0 : zsimplify. - - Lemma div_between n a b : 0 <= n -> b <> 0 -> n * b <= a < (1 + n) * b -> a / b = n. - Proof. intros; Z.div_mod_to_quot_rem_in_goal; nia. Qed. - Hint Rewrite div_between using zutil_arith : zsimplify. - - Lemma mod_small_n n a b : 0 <= n -> b <> 0 -> n * b <= a < (1 + n) * b -> a mod b = a - n * b. - Proof. intros; erewrite Zmod_eq_full, div_between by eassumption. reflexivity. Qed. - Hint Rewrite mod_small_n using zutil_arith : zsimplify. - - Lemma div_between_1 a b : b <> 0 -> b <= a < 2 * b -> a / b = 1. - Proof. intros; rewrite (div_between 1) by lia; reflexivity. Qed. - Hint Rewrite div_between_1 using zutil_arith : zsimplify. - - Lemma mod_small_1 a b : b <> 0 -> b <= a < 2 * b -> a mod b = a - b. - Proof. intros; rewrite (mod_small_n 1) by lia; lia. Qed. - Hint Rewrite mod_small_1 using zutil_arith : zsimplify. - - Lemma div_between_if n a b : 0 <= n -> b <> 0 -> n * b <= a < (2 + n) * b -> (a / b = if (1 + n) * b <=? a then 1 + n else n)%Z. - Proof. - intros. - break_match; Z.ltb_to_lt; - apply div_between; lia. - Qed. - - Lemma mod_small_n_if n a b : 0 <= n -> b <> 0 -> n * b <= a < (2 + n) * b -> a mod b = a - (if (1 + n) * b <=? a then (1 + n) else n) * b. - Proof. intros; erewrite Zmod_eq_full, div_between_if by eassumption; autorewrite with zsimplify_const. reflexivity. Qed. - - Lemma div_between_0_if a b : b <> 0 -> 0 <= a < 2 * b -> a / b = if b <=? a then 1 else 0. - Proof. intros; rewrite (div_between_if 0) by lia; autorewrite with zsimplify_const; reflexivity. Qed. - - Lemma mod_small_0_if a b : b <> 0 -> 0 <= a < 2 * b -> a mod b = a - if b <=? a then b else 0. - Proof. intros; rewrite (mod_small_n_if 0) by lia; autorewrite with zsimplify_const. break_match; lia. Qed. - - Lemma mul_mod_distr_r_full a b c : (a * c) mod (b * c) = (a mod b * c). - Proof. - destruct (Z_zerop b); [ | destruct (Z_zerop c) ]; subst; - autorewrite with zsimplify; auto using Z.mul_mod_distr_r. - Qed. - - Lemma mul_mod_distr_l_full a b c : (c * a) mod (c * b) = c * (a mod b). - Proof. - destruct (Z_zerop b); [ | destruct (Z_zerop c) ]; subst; - autorewrite with zsimplify; auto using Z.mul_mod_distr_l. - Qed. - - Lemma lt_mul_2_mod_sub : forall a b, b <> 0 -> b <= a < 2 * b -> a mod b = a - b. - Proof. - intros a b H H0. - replace (a mod b) with ((1 * b + (a - b)) mod b) by (f_equal; ring). - rewrite Z.mod_add_l by auto. - apply Z.mod_small. - omega. - Qed. - - - Lemma leb_add_same x y : (x <=? y + x) = (0 <=? y). - Proof. destruct (x <=? y + x) eqn:?, (0 <=? y) eqn:?; Z.ltb_to_lt; try reflexivity; omega. Qed. - Hint Rewrite leb_add_same : zsimplify. - - Lemma ltb_add_same x y : (x <? y + x) = (0 <? y). - Proof. destruct (x <? y + x) eqn:?, (0 <? y) eqn:?; Z.ltb_to_lt; try reflexivity; omega. Qed. - Hint Rewrite ltb_add_same : zsimplify. - - Lemma geb_add_same x y : (x >=? y + x) = (0 >=? y). - Proof. destruct (x >=? y + x) eqn:?, (0 >=? y) eqn:?; Z.ltb_to_lt; try reflexivity; omega. Qed. - Hint Rewrite geb_add_same : zsimplify. - - Lemma gtb_add_same x y : (x >? y + x) = (0 >? y). - Proof. destruct (x >? y + x) eqn:?, (0 >? y) eqn:?; Z.ltb_to_lt; try reflexivity; omega. Qed. - Hint Rewrite gtb_add_same : zsimplify. - - Lemma shiftl_add x y z : 0 <= z -> (x + y) << z = (x << z) + (y << z). - Proof. intros; autorewrite with Zshift_to_pow; lia. Qed. - Hint Rewrite shiftl_add using zutil_arith : push_Zshift. - Hint Rewrite <- shiftl_add using zutil_arith : pull_Zshift. - - Lemma shiftr_add x y z : z <= 0 -> (x + y) >> z = (x >> z) + (y >> z). - Proof. intros; autorewrite with Zshift_to_pow; lia. Qed. - Hint Rewrite shiftr_add using zutil_arith : push_Zshift. - Hint Rewrite <- shiftr_add using zutil_arith : pull_Zshift. - - Lemma shiftl_sub x y z : 0 <= z -> (x - y) << z = (x << z) - (y << z). - Proof. intros; autorewrite with Zshift_to_pow; lia. Qed. - Hint Rewrite shiftl_sub using zutil_arith : push_Zshift. - Hint Rewrite <- shiftl_sub using zutil_arith : pull_Zshift. - - Lemma shiftr_sub x y z : z <= 0 -> (x - y) >> z = (x >> z) - (y >> z). - Proof. intros; autorewrite with Zshift_to_pow; lia. Qed. - Hint Rewrite shiftr_sub using zutil_arith : push_Zshift. - Hint Rewrite <- shiftr_sub using zutil_arith : pull_Zshift. - - Lemma shl_shr_lt x y n m (Hx : 0 <= x < 2^n) (Hy : 0 <= y < 2^n) (Hm : 0 <= m <= n) - : 0 <= (x >> (n - m)) + ((y << m) mod 2^n) < 2^n. - Proof. - cut (0 <= (x >> (n - m)) + ((y << m) mod 2^n) <= 2^n - 1); [ omega | ]. - assert (0 <= x <= 2^n - 1) by omega. - assert (0 <= y <= 2^n - 1) by omega. - assert (0 < 2 ^ (n - m)) by auto with zarith. - assert (0 <= y mod 2 ^ (n - m) < 2^(n-m)) by auto with zarith. - assert (0 <= y mod 2 ^ (n - m) <= 2 ^ (n - m) - 1) by omega. - assert (0 <= (y mod 2 ^ (n - m)) * 2^m <= (2^(n-m) - 1)*2^m) by auto with zarith. - assert (0 <= x / 2^(n-m) < 2^n / 2^(n-m)). - { split; Z.zero_bounds. - apply Z.div_lt_upper_bound; autorewrite with pull_Zpow zsimplify; nia. } - autorewrite with Zshift_to_pow. - split; Z.zero_bounds. - replace (2^n) with (2^(n-m) * 2^m) by (autorewrite with pull_Zpow; f_equal; omega). - rewrite Zmult_mod_distr_r. - autorewrite with pull_Zpow zsimplify push_Zmul in * |- . - nia. - Qed. - - Lemma add_shift_mod x y n m - (Hx : 0 <= x < 2^n) (Hy : 0 <= y) - (Hn : 0 <= n) (Hm : 0 < m) - : (x + y << n) mod (m * 2^n) = x + (y mod m) << n. - Proof. - pose proof (Z.mod_bound_pos y m). - specialize_by omega. - assert (0 < 2^n) by auto with zarith. - autorewrite with Zshift_to_pow. - rewrite Zplus_mod, !Zmult_mod_distr_r. - rewrite Zplus_mod, !Zmod_mod, <- Zplus_mod. - rewrite !(Zmod_eq (_ + _)) by nia. - etransitivity; [ | apply Z.add_0_r ]. - rewrite <- !Z.add_opp_r, <- !Z.add_assoc. - repeat apply f_equal. - ring_simplify. - cut (((x + y mod m * 2 ^ n) / (m * 2 ^ n)) = 0); [ nia | ]. - apply Z.div_small; split; nia. - Qed. - - Lemma add_mul_mod x y n m - (Hx : 0 <= x < 2^n) (Hy : 0 <= y) - (Hn : 0 <= n) (Hm : 0 < m) - : (x + y * 2^n) mod (m * 2^n) = x + (y mod m) * 2^n. - Proof. - generalize (add_shift_mod x y n m). - autorewrite with Zshift_to_pow; auto. - Qed. - - Lemma lt_pow_2_shiftr : forall a n, 0 <= a < 2 ^ n -> a >> n = 0. - Proof. - intros a n H. - destruct (Z_le_dec 0 n). - + rewrite Z.shiftr_div_pow2 by assumption. - auto using Z.div_small. - + assert (2 ^ n = 0) by (apply Z.pow_neg_r; omega). - omega. - Qed. - - Hint Rewrite Z.pow2_bits_eqb using zutil_arith : Ztestbit. - Lemma pow_2_shiftr : forall n, 0 <= n -> (2 ^ n) >> n = 1. - Proof. - intros; apply Z.bits_inj'; intros. - replace 1 with (2 ^ 0) by ring. - repeat match goal with - | |- _ => progress intros - | |- _ => progress rewrite ?Z.eqb_eq, ?Z.eqb_neq in * - | |- _ => progress autorewrite with Ztestbit - | |- context[Z.eqb ?a ?b] => case_eq (Z.eqb a b) - | |- _ => reflexivity || omega - end. - Qed. - - Lemma lt_mul_2_pow_2_shiftr : forall a n, 0 <= a < 2 * 2 ^ n -> - a >> n = if Z_lt_dec a (2 ^ n) then 0 else 1. - Proof. - intros a n H; break_match; [ apply lt_pow_2_shiftr; omega | ]. - destruct (Z_le_dec 0 n). - + replace (2 * 2 ^ n) with (2 ^ (n + 1)) in * - by (rewrite Z.pow_add_r; try omega; ring). - pose proof (Z.shiftr_ones a (n + 1) n H). - pose proof (Z.shiftr_le (2 ^ n) a n). - specialize_by omega. - replace (n + 1 - n) with 1 in * by ring. - replace (Z.ones 1) with 1 in * by reflexivity. - rewrite pow_2_shiftr in * by omega. - omega. - + assert (2 ^ n = 0) by (apply Z.pow_neg_r; omega). - omega. - Qed. - - Lemma shiftr_nonneg_le : forall a n, 0 <= a -> 0 <= n -> a >> n <= a. - Proof. - intros. - repeat match goal with - | [ H : _ <= _ |- _ ] - => rewrite Z.lt_eq_cases in H - | [ H : _ \/ _ |- _ ] => destruct H - | _ => progress subst - | _ => progress autorewrite with zsimplify Zshift_to_pow - | _ => solve [ auto with zarith omega ] - end. - Qed. - Hint Resolve shiftr_nonneg_le : zarith. - - Lemma log2_pred_pow2_full a : Z.log2 (Z.pred (2^a)) = Z.max 0 (Z.pred a). - Proof. - destruct (Z_dec 0 a) as [ [?|?] | ?]. - { rewrite Z.log2_pred_pow2 by assumption. - apply Z.max_case_strong; omega. } - { autorewrite with zsimplify; simpl. - apply Z.max_case_strong; omega. } - { subst; compute; reflexivity. } - Qed. - Hint Rewrite log2_pred_pow2_full : zsimplify. - - Lemma log2_up_le_full a : a <= 2^Z.log2_up a. - Proof. - destruct (Z_dec 1 a) as [ [ ? | ? ] | ? ]; - first [ apply Z.log2_up_spec; assumption - | rewrite Z.log2_up_eqn0 by omega; simpl; omega ]. - Qed. - - Lemma log2_up_le_pow2_full : forall a b : Z, (0 <= b)%Z -> (a <= 2 ^ b)%Z <-> (Z.log2_up a <= b)%Z. - Proof. - intros a b H. - destruct (Z_lt_le_dec 0 a); [ apply Z.log2_up_le_pow2; assumption | ]. - split; transitivity 0%Z; try omega; auto with zarith. - rewrite Z.log2_up_eqn0 by omega. - reflexivity. - Qed. - - Lemma ones_lt_pow2 x y : 0 <= x <= y -> Z.ones x < 2^y. - Proof. - rewrite Z.ones_equiv, Z.lt_pred_le. - auto with zarith. - Qed. - Hint Resolve ones_lt_pow2 : zarith. - - Lemma log2_ones_full x : Z.log2 (Z.ones x) = Z.max 0 (Z.pred x). - Proof. - rewrite Z.ones_equiv, log2_pred_pow2_full; reflexivity. - Qed. - Hint Rewrite log2_ones_full : zsimplify. - - Lemma log2_ones_lt x y : 0 < x <= y -> Z.log2 (Z.ones x) < y. - Proof. - rewrite log2_ones_full; apply Z.max_case_strong; omega. - Qed. - Hint Resolve log2_ones_lt : zarith. - - Lemma log2_ones_le x y : 0 <= x <= y -> Z.log2 (Z.ones x) <= y. - Proof. - rewrite log2_ones_full; apply Z.max_case_strong; omega. - Qed. - Hint Resolve log2_ones_le : zarith. - - Lemma log2_ones_lt_nonneg x y : 0 < y -> x <= y -> Z.log2 (Z.ones x) < y. - Proof. - rewrite log2_ones_full; apply Z.max_case_strong; omega. - Qed. - Hint Resolve log2_ones_lt_nonneg : zarith. - - Lemma log2_lt_pow2_alt a b : 0 < b -> (a < 2^b <-> Z.log2 a < b). - Proof. - destruct (Z_lt_le_dec 0 a); auto using Z.log2_lt_pow2; []. - rewrite Z.log2_nonpos by omega. - split; auto with zarith; []. - intro; eapply le_lt_trans; [ eassumption | ]. - auto with zarith. - Qed. - - Section ZInequalities. - Lemma land_le : forall x y, (0 <= x)%Z -> (Z.land x y <= x)%Z. - Proof. - intros x y H; apply Z.ldiff_le; [assumption|]. - rewrite Z.ldiff_land, Z.land_comm, Z.land_assoc. - rewrite <- Z.land_0_l with (a := y); f_equal. - rewrite Z.land_comm, Z.land_lnot_diag. - reflexivity. - Qed. - - Lemma lor_lower : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> (x <= Z.lor x y)%Z. - Proof. - intros x y H H0; apply Z.ldiff_le; [apply Z.lor_nonneg; auto|]. - rewrite Z.ldiff_land. - apply Z.bits_inj_iff'; intros k Hpos; apply Z.le_ge in Hpos. - rewrite Z.testbit_0_l, Z.land_spec, Z.lnot_spec, Z.lor_spec; - [|apply Z.ge_le; assumption]. - induction (Z.testbit x k), (Z.testbit y k); cbv; reflexivity. - Qed. - - Lemma lor_le : forall x y z, - (0 <= x)%Z - -> (x <= y)%Z - -> (y <= z)%Z - -> (Z.lor x y <= (2 ^ Z.log2_up (z+1)) - 1)%Z. - Proof. - intros x y z H H0 H1; apply Z.ldiff_le. - - - apply Z.le_add_le_sub_r. - replace 1%Z with (2 ^ 0)%Z by (cbv; reflexivity). - rewrite Z.add_0_l. - apply Z.pow_le_mono_r; [cbv; reflexivity|]. - apply Z.log2_up_nonneg. - - - destruct (Z_lt_dec 0 z). - - + assert (forall a, a - 1 = Z.pred a)%Z as HP by (intro; omega); - rewrite HP, <- Z.ones_equiv; clear HP. - apply Z.ldiff_ones_r_low; [apply Z.lor_nonneg; split; omega|]. - rewrite Z.log2_up_eqn, Z.log2_lor; try omega. - apply Z.lt_succ_r. - apply Z.max_case_strong; intros; apply Z.log2_le_mono; omega. - - + replace z with 0%Z by omega. - replace y with 0%Z by omega. - replace x with 0%Z by omega. - cbv; reflexivity. - Qed. - - Lemma pow2_ge_0: forall a, (0 <= 2 ^ a)%Z. - Proof. - intros; apply Z.pow_nonneg; omega. - Qed. - - Lemma pow2_gt_0: forall a, (0 <= a)%Z -> (0 < 2 ^ a)%Z. - Proof. - intros; apply Z.pow_pos_nonneg; [|assumption]; omega. - Qed. - - Local Ltac solve_pow2 := - repeat match goal with - | [|- _ /\ _] => split - | [|- (0 < 2 ^ _)%Z] => apply pow2_gt_0 - | [|- (0 <= 2 ^ _)%Z] => apply pow2_ge_0 - | [|- (2 ^ _ <= 2 ^ _)%Z] => apply Z.pow_le_mono_r - | [|- (_ <= _)%Z] => omega - | [|- (_ < _)%Z] => omega - end. - - Lemma pow2_mod_range : forall a n m, - (0 <= n) -> - (n <= m) -> - (0 <= Z.pow2_mod a n < 2 ^ m). - Proof. - intros; unfold Z.pow2_mod. - rewrite Z.land_ones; [|assumption]. - split; [apply Z.mod_pos_bound, pow2_gt_0; assumption|]. - eapply Z.lt_le_trans; [apply Z.mod_pos_bound, pow2_gt_0; assumption|]. - apply Z.pow_le_mono; [|assumption]. - split; simpl; omega. - Qed. - - Lemma shiftr_range : forall a n m, - (0 <= n)%Z -> - (0 <= m)%Z -> - (0 <= a < 2 ^ (n + m))%Z -> - (0 <= Z.shiftr a n < 2 ^ m)%Z. - Proof. - intros a n m H0 H1 H2; destruct H2. - split; [apply Z.shiftr_nonneg; assumption|]. - rewrite Z.shiftr_div_pow2; [|assumption]. - apply Z.div_lt_upper_bound; [apply pow2_gt_0; assumption|]. - eapply Z.lt_le_trans; [eassumption|apply Z.eq_le_incl]. - apply Z.pow_add_r; omega. - Qed. - - - Lemma shiftr_le_mono: forall a b c d, - (0 <= a)%Z - -> (0 <= d)%Z - -> (a <= c)%Z - -> (d <= b)%Z - -> (Z.shiftr a b <= Z.shiftr c d)%Z. - Proof. - intros. - repeat rewrite Z.shiftr_div_pow2; [|omega|omega]. - etransitivity; [apply Z.div_le_compat_l | apply Z.div_le_mono]; solve_pow2. - Qed. - - Lemma shiftl_le_mono: forall a b c d, - (0 <= a)%Z - -> (0 <= b)%Z - -> (a <= c)%Z - -> (b <= d)%Z - -> (Z.shiftl a b <= Z.shiftl c d)%Z. - Proof. - intros. - repeat rewrite Z.shiftl_mul_pow2; [|omega|omega]. - etransitivity; [apply Z.mul_le_mono_nonneg_l|apply Z.mul_le_mono_nonneg_r]; solve_pow2. - Qed. - End ZInequalities. - - Lemma max_log2_up x y : Z.max (Z.log2_up x) (Z.log2_up y) = Z.log2_up (Z.max x y). - Proof. apply Z.max_monotone; intros ??; apply Z.log2_up_le_mono. Qed. - Hint Rewrite max_log2_up : push_Zmax. - Hint Rewrite <- max_log2_up : pull_Zmax. - - Lemma lor_bounds x y : 0 <= x -> 0 <= y - -> Z.max x y <= Z.lor x y <= 2^Z.log2_up (Z.max x y + 1) - 1. - Proof. - apply Z.max_case_strong; intros; split; - try solve [ eauto using lor_lower, Z.le_trans, lor_le with omega - | rewrite Z.lor_comm; eauto using lor_lower, Z.le_trans, lor_le with omega ]. - Qed. - Lemma lor_bounds_lower x y : 0 <= x -> 0 <= y - -> Z.max x y <= Z.lor x y. - Proof. intros; apply lor_bounds; assumption. Qed. - Lemma lor_bounds_upper x y : Z.lor x y <= 2^Z.log2_up (Z.max x y + 1) - 1. - Proof. - pose proof (proj2 (Z.lor_neg x y)). - destruct (Z_lt_le_dec x 0), (Z_lt_le_dec y 0); - try solve [ intros; apply lor_bounds; assumption ]; - transitivity (2^0-1); - try apply Z.sub_le_mono_r, Z.pow_le_mono_r, Z.log2_up_nonneg; - simpl; omega. - Qed. - Lemma lor_bounds_gen_lower x y l : 0 <= x -> 0 <= y -> l <= Z.max x y - -> l <= Z.lor x y. - Proof. - intros; etransitivity; - solve [ apply lor_bounds; auto - | eauto ]. - Qed. - Lemma lor_bounds_gen_upper x y u : x <= u -> y <= u - -> Z.lor x y <= 2^Z.log2_up (u + 1) - 1. - Proof. - intros; etransitivity; [ apply lor_bounds_upper | ]. - apply Z.sub_le_mono_r, Z.pow_le_mono_r, Z.log2_up_le_mono, Z.max_case_strong; - omega. - Qed. - Lemma lor_bounds_gen x y l u : 0 <= x -> 0 <= y -> l <= Z.max x y -> x <= u -> y <= u - -> l <= Z.lor x y <= 2^Z.log2_up (u + 1) - 1. - Proof. auto using lor_bounds_gen_lower, lor_bounds_gen_upper. Qed. - - Lemma log2_up_le_full_max a : Z.max a 1 <= 2^Z.log2_up a. - Proof. - apply Z.max_case_strong; auto using Z.log2_up_le_full. - intros; rewrite Z.log2_up_eqn0 by assumption; reflexivity. - Qed. - Lemma log2_up_le_1 a : Z.log2_up a <= 1 <-> a <= 2. - Proof. - pose proof (Z.log2_nonneg (Z.pred a)). - destruct (Z_dec a 2) as [ [ ? | ? ] | ? ]. - { rewrite (proj2 (Z.log2_up_null a)) by omega; split; omega. } - { rewrite Z.log2_up_eqn by omega. - split; try omega; intro. - assert (Z.log2 (Z.pred a) = 0) by omega. - assert (Z.pred a <= 1) by (apply Z.log2_null; omega). - omega. } - { subst; cbv -[Z.le]; split; omega. } - Qed. - Lemma log2_up_1_le a : 1 <= Z.log2_up a <-> 2 <= a. - Proof. - pose proof (Z.log2_nonneg (Z.pred a)). - destruct (Z_dec a 2) as [ [ ? | ? ] | ? ]. - { rewrite (proj2 (Z.log2_up_null a)) by omega; split; omega. } - { rewrite Z.log2_up_eqn by omega; omega. } - { subst; cbv -[Z.le]; split; omega. } - Qed. - - Lemma shiftl_le_Proper2 y - : Proper (Z.le ==> Z.le) (fun x => Z.shiftl x y). - Proof. - unfold Basics.flip in *. - pose proof (Zle_cases 0 y) as Hx. - intros x x' H. - pose proof (Zle_cases 0 x) as Hy. - pose proof (Zle_cases 0 x') as Hy'. - destruct (0 <=? y), (0 <=? x), (0 <=? x'); - autorewrite with Zshift_to_pow; - Z.replace_all_neg_with_pos; - autorewrite with pull_Zopp; - rewrite ?Z.div_opp_l_complete; - repeat destruct (Z_zerop _); - autorewrite with zsimplify_const pull_Zopp; - auto with zarith; - repeat match goal with - | [ |- context[-?x - ?y] ] - => replace (-x - y) with (-(x + y)) by omega - | _ => rewrite <- Z.opp_le_mono - | _ => rewrite <- Z.add_le_mono_r - | _ => solve [ auto with zarith ] - | [ |- ?x <= ?y + 1 ] - => cut (x <= y); [ omega | solve [ auto with zarith ] ] - | [ |- -_ <= _ ] - => solve [ transitivity (-0); auto with zarith ] - end. - { repeat match goal with H : context[_ mod _] |- _ => revert H end; - Z.div_mod_to_quot_rem_in_goal; nia. } - Qed. - - Lemma shiftl_le_Proper1 x - (R := fun b : bool => if b then Z.le else Basics.flip Z.le) - : Proper (R (0 <=? x) ==> Z.le) (Z.shiftl x). - Proof. - unfold Basics.flip in *. - pose proof (Zle_cases 0 x) as Hx. - intros y y' H. - pose proof (Zle_cases 0 y) as Hy. - pose proof (Zle_cases 0 y') as Hy'. - destruct (0 <=? x), (0 <=? y), (0 <=? y'); subst R; cbv beta iota in *; - autorewrite with Zshift_to_pow; - Z.replace_all_neg_with_pos; - autorewrite with pull_Zopp; - rewrite ?Z.div_opp_l_complete; - repeat destruct (Z_zerop _); - autorewrite with zsimplify_const pull_Zopp; - auto with zarith; - repeat match goal with - | [ |- context[-?x - ?y] ] - => replace (-x - y) with (-(x + y)) by omega - | _ => rewrite <- Z.opp_le_mono - | _ => rewrite <- Z.add_le_mono_r - | _ => solve [ auto with zarith ] - | [ |- ?x <= ?y + 1 ] - => cut (x <= y); [ omega | solve [ auto with zarith ] ] - | [ |- context[2^?x] ] - => lazymatch goal with - | [ H : 1 < 2^x |- _ ] => fail - | [ H : 0 < 2^x |- _ ] => fail - | [ H : 0 <= 2^x |- _ ] => fail - | _ => first [ assert (1 < 2^x) by auto with zarith - | assert (0 < 2^x) by auto with zarith - | assert (0 <= 2^x) by auto with zarith ] - end - | [ H : ?x <= ?y |- _ ] - => is_var x; is_var y; - lazymatch goal with - | [ H : 2^x <= 2^y |- _ ] => fail - | [ H : 2^x < 2^y |- _ ] => fail - | _ => assert (2^x <= 2^y) by auto with zarith - end - | [ H : ?x <= ?y, H' : ?f ?x = ?k, H'' : ?f ?y <> ?k |- _ ] - => let Hn := fresh in - assert (Hn : x <> y) by congruence; - assert (x < y) by omega; clear H Hn - | [ H : ?x <= ?y, H' : ?f ?x <> ?k, H'' : ?f ?y = ?k |- _ ] - => let Hn := fresh in - assert (Hn : x <> y) by congruence; - assert (x < y) by omega; clear H Hn - | _ => solve [ repeat match goal with H : context[_ mod _] |- _ => revert H end; - Z.div_mod_to_quot_rem_in_goal; subst; - lazymatch goal with - | [ |- _ <= (?a * ?q + ?r) * ?q' ] - => transitivity (q * (a * q') + r * q'); - [ assert (0 < a * q') by nia; nia - | nia ] - end ] - end. - { replace y' with (y + (y' - y)) by omega. - rewrite Z.pow_add_r, <- Zdiv_Zdiv by auto with zarith. - assert (y < y') by (assert (y <> y') by congruence; omega). - assert (1 < 2^(y'-y)) by auto with zarith. - assert (0 < x / 2^y) - by (repeat match goal with H : context[_ mod _] |- _ => revert H end; - Z.div_mod_to_quot_rem_in_goal; nia). - assert (2^y <= x) - by (repeat match goal with H : context[_ / _] |- _ => revert H end; - Z.div_mod_to_quot_rem_in_goal; nia). - match goal with - | [ |- ?x + 1 <= ?y ] => cut (x < y); [ omega | ] - end. - auto with zarith. } - Qed. - - Lemma shiftr_le_Proper2 y - : Proper (Z.le ==> Z.le) (fun x => Z.shiftr x y). - Proof. apply shiftl_le_Proper2. Qed. - - Lemma shiftr_le_Proper1 x - (R := fun b : bool => if b then Z.le else Basics.flip Z.le) - : Proper (R (x <? 0) ==> Z.le) (Z.shiftr x). - Proof. - subst R; intros y y' H'; unfold Z.shiftr; apply shiftl_le_Proper1. - unfold Basics.flip in *. - pose proof (Zle_cases 0 x). - pose proof (Zlt_cases x 0). - destruct (0 <=? x), (x <? 0); try omega. - Qed. -End Z. - -Module N2Z. - Lemma inj_land n m : Z.of_N (N.land n m) = Z.land (Z.of_N n) (Z.of_N m). - Proof. destruct n, m; reflexivity. Qed. - Hint Rewrite inj_land : push_Zof_N. - Hint Rewrite <- inj_land : pull_Zof_N. - - Lemma inj_lor n m : Z.of_N (N.lor n m) = Z.lor (Z.of_N n) (Z.of_N m). - Proof. destruct n, m; reflexivity. Qed. - Hint Rewrite inj_lor : push_Zof_N. - Hint Rewrite <- inj_lor : pull_Zof_N. - - Lemma inj_shiftl: forall x y, Z.of_N (N.shiftl x y) = Z.shiftl (Z.of_N x) (Z.of_N y). - Proof. - intros x y. - apply Z.bits_inj_iff'; intros k Hpos. - rewrite Z2N.inj_testbit; [|assumption]. - rewrite Z.shiftl_spec; [|assumption]. - - assert ((Z.to_N k) >= y \/ (Z.to_N k) < y)%N as g by ( - unfold N.ge, N.lt; induction (N.compare (Z.to_N k) y); [left|auto|left]; - intro H; inversion H). - - destruct g as [g|g]; - [ rewrite N.shiftl_spec_high; [|apply N2Z.inj_le; rewrite Z2N.id|apply N.ge_le] - | rewrite N.shiftl_spec_low]; try assumption. - - - rewrite <- N2Z.inj_testbit; f_equal. - rewrite N2Z.inj_sub, Z2N.id; [reflexivity|assumption|apply N.ge_le; assumption]. - - - apply N2Z.inj_lt in g. - rewrite Z2N.id in g; [symmetry|assumption]. - apply Z.testbit_neg_r; omega. - Qed. - Hint Rewrite inj_shiftl : push_Zof_N. - Hint Rewrite <- inj_shiftl : pull_Zof_N. - - Lemma inj_shiftr: forall x y, Z.of_N (N.shiftr x y) = Z.shiftr (Z.of_N x) (Z.of_N y). - Proof. - intros. - apply Z.bits_inj_iff'; intros k Hpos. - rewrite Z2N.inj_testbit; [|assumption]. - rewrite Z.shiftr_spec, N.shiftr_spec; [|apply N2Z.inj_le; rewrite Z2N.id|]; try assumption. - rewrite <- N2Z.inj_testbit; f_equal. - rewrite N2Z.inj_add; f_equal. - apply Z2N.id; assumption. - Qed. - Hint Rewrite inj_shiftr : push_Zof_N. - Hint Rewrite <- inj_shiftr : pull_Zof_N. -End N2Z. - -Module Export BoundsTactics. - Ltac prime_bound := Z.prime_bound. - Ltac zero_bounds := Z.zero_bounds. -End BoundsTactics. +Require Coq.ZArith.Zpower Coq.ZArith.Znumtheory Coq.ZArith.ZArith Coq.ZArith.Zdiv. +Require Coq.omega.Omega Coq.micromega.Psatz Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith. +Require Crypto.Util.ZUtil.AddGetCarry. +Require Crypto.Util.ZUtil.AddModulo. +Require Crypto.Util.ZUtil.CC. +Require Crypto.Util.ZUtil.CPS. +Require Crypto.Util.ZUtil.Definitions. +Require Crypto.Util.ZUtil.DistrIf. +Require Crypto.Util.ZUtil.Div. +Require Crypto.Util.ZUtil.Div.Bootstrap. +Require Crypto.Util.ZUtil.Divide. +Require Crypto.Util.ZUtil.EquivModulo. +Require Crypto.Util.ZUtil.Ge. +Require Crypto.Util.ZUtil.Hints. +Require Crypto.Util.ZUtil.Hints.Core. +Require Crypto.Util.ZUtil.Hints.PullPush. +Require Crypto.Util.ZUtil.Hints.ZArith. +Require Crypto.Util.ZUtil.Hints.Ztestbit. +Require Crypto.Util.ZUtil.Land. +Require Crypto.Util.ZUtil.LandLorBounds. +Require Crypto.Util.ZUtil.LandLorShiftBounds. +Require Crypto.Util.ZUtil.Le. +Require Crypto.Util.ZUtil.Lnot. +Require Crypto.Util.ZUtil.Log2. +Require Crypto.Util.ZUtil.ModInv. +Require Crypto.Util.ZUtil.Modulo. +Require Crypto.Util.ZUtil.Modulo.Bootstrap. +Require Crypto.Util.ZUtil.Modulo.PullPush. +Require Crypto.Util.ZUtil.Morphisms. +Require Crypto.Util.ZUtil.Mul. +Require Crypto.Util.ZUtil.MulSplit. +Require Crypto.Util.ZUtil.N2Z. +Require Crypto.Util.ZUtil.Notations. +Require Crypto.Util.ZUtil.Odd. +Require Crypto.Util.ZUtil.Ones. +Require Crypto.Util.ZUtil.Opp. +Require Crypto.Util.ZUtil.Peano. +Require Crypto.Util.ZUtil.Pow. +Require Crypto.Util.ZUtil.Pow2. +Require Crypto.Util.ZUtil.Pow2Mod. +Require Crypto.Util.ZUtil.Quot. +Require Crypto.Util.ZUtil.Rshi. +Require Crypto.Util.ZUtil.Sgn. +Require Crypto.Util.ZUtil.Shift. +Require Crypto.Util.ZUtil.Sorting. +Require Crypto.Util.ZUtil.Stabilization. +Require Crypto.Util.ZUtil.Tactics. +Require Crypto.Util.ZUtil.Tactics.CompareToSgn. +Require Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Crypto.Util.ZUtil.Tactics.DivideExistsMul. +Require Crypto.Util.ZUtil.Tactics.LinearSubstitute. +Require Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Crypto.Util.ZUtil.Tactics.PeelLe. +Require Crypto.Util.ZUtil.Tactics.PrimeBound. +Require Crypto.Util.ZUtil.Tactics.PullPush. +Require Crypto.Util.ZUtil.Tactics.PullPush.Modulo. +Require Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos. +Require Crypto.Util.ZUtil.Tactics.RewriteModSmall. +Require Crypto.Util.ZUtil.Tactics.SimplifyFractionsLe. +Require Crypto.Util.ZUtil.Tactics.SplitMinMax. +Require Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Crypto.Util.ZUtil.Tactics.Ztestbit. +Require Crypto.Util.ZUtil.Testbit. +Require Crypto.Util.ZUtil.Z2Nat. +Require Crypto.Util.ZUtil.ZSimplify. +Require Crypto.Util.ZUtil.ZSimplify.Autogenerated. +Require Crypto.Util.ZUtil.ZSimplify.Core. +Require Crypto.Util.ZUtil.ZSimplify.Simple. +Require Crypto.Util.ZUtil.Zselect. diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v index af2d8239e..4ef6b5403 100644 --- a/src/Util/ZUtil/Definitions.v +++ b/src/Util/ZUtil/Definitions.v @@ -84,4 +84,9 @@ Module Z. := if s =? 2^Z.log2 s then mul_split_at_bitwidth (Z.log2 s) x y else ((x * y) mod s, (x * y) / s). + + Definition round_lor_land_bound (x : Z) : Z + := if (0 <=? x)%Z + then 2^(Z.log2_up (x+1))-1 + else -2^(Z.log2_up (-x)). End Z. diff --git a/src/Util/ZUtil/DistrIf.v b/src/Util/ZUtil/DistrIf.v new file mode 100644 index 000000000..0d20fc1f4 --- /dev/null +++ b/src/Util/ZUtil/DistrIf.v @@ -0,0 +1,51 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints.Core. +Local Open Scope Z_scope. + +Module Z. + Definition opp_distr_if (b : bool) x y : -(if b then x else y) = if b then -x else -y. + Proof. destruct b; reflexivity. Qed. + Hint Rewrite opp_distr_if : push_Zopp. + Hint Rewrite <- opp_distr_if : pull_Zopp. + + Lemma mul_r_distr_if (b : bool) x y z : z * (if b then x else y) = if b then z * x else z * y. + Proof. destruct b; reflexivity. Qed. + Hint Rewrite mul_r_distr_if : push_Zmul. + Hint Rewrite <- mul_r_distr_if : pull_Zmul. + + Lemma mul_l_distr_if (b : bool) x y z : (if b then x else y) * z = if b then x * z else y * z. + Proof. destruct b; reflexivity. Qed. + Hint Rewrite mul_l_distr_if : push_Zmul. + Hint Rewrite <- mul_l_distr_if : pull_Zmul. + + Lemma add_r_distr_if (b : bool) x y z : z + (if b then x else y) = if b then z + x else z + y. + Proof. destruct b; reflexivity. Qed. + Hint Rewrite add_r_distr_if : push_Zadd. + Hint Rewrite <- add_r_distr_if : pull_Zadd. + + Lemma add_l_distr_if (b : bool) x y z : (if b then x else y) + z = if b then x + z else y + z. + Proof. destruct b; reflexivity. Qed. + Hint Rewrite add_l_distr_if : push_Zadd. + Hint Rewrite <- add_l_distr_if : pull_Zadd. + + Lemma sub_r_distr_if (b : bool) x y z : z - (if b then x else y) = if b then z - x else z - y. + Proof. destruct b; reflexivity. Qed. + Hint Rewrite sub_r_distr_if : push_Zsub. + Hint Rewrite <- sub_r_distr_if : pull_Zsub. + + Lemma sub_l_distr_if (b : bool) x y z : (if b then x else y) - z = if b then x - z else y - z. + Proof. destruct b; reflexivity. Qed. + Hint Rewrite sub_l_distr_if : push_Zsub. + Hint Rewrite <- sub_l_distr_if : pull_Zsub. + + Lemma div_r_distr_if (b : bool) x y z : z / (if b then x else y) = if b then z / x else z / y. + Proof. destruct b; reflexivity. Qed. + Hint Rewrite div_r_distr_if : push_Zdiv. + Hint Rewrite <- div_r_distr_if : pull_Zdiv. + + Lemma div_l_distr_if (b : bool) x y z : (if b then x else y) / z = if b then x / z else y / z. + Proof. destruct b; reflexivity. Qed. + Hint Rewrite div_l_distr_if : push_Zdiv. + Hint Rewrite <- div_l_distr_if : pull_Zdiv. +End Z. diff --git a/src/Util/ZUtil/Div.v b/src/Util/ZUtil/Div.v index 5ae17ad1a..7012f83c0 100644 --- a/src/Util/ZUtil/Div.v +++ b/src/Util/ZUtil/Div.v @@ -2,11 +2,14 @@ Require Import Coq.ZArith.ZArith Coq.micromega.Lia. Require Import Coq.ZArith.Znumtheory. Require Import Crypto.Util.ZUtil.Tactics.CompareToSgn. Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.ZUtil.Le. Require Import Crypto.Util.ZUtil.Hints.Core. Require Import Crypto.Util.ZUtil.Hints.ZArith. Require Import Crypto.Util.ZUtil.Hints.PullPush. +Require Import Crypto.Util.ZUtil.Hints. Require Import Crypto.Util.ZUtil.ZSimplify.Core. +Require Import Crypto.Util.Tactics.BreakMatch. Local Open Scope Z_scope. Module Z. @@ -262,4 +265,165 @@ Module Z. Lemma div_opp_r a b : a / (-b) = ((-a) / b). Proof. Z.div_mod_to_quot_rem; nia. Qed. Hint Resolve div_opp_r : zarith. + + Lemma div_floor : forall a b c, 0 < b -> a < b * (Z.succ c) -> a / b <= c. + Proof. + intros. + apply Z.lt_succ_r. + apply Z.div_lt_upper_bound; try omega. + Qed. + + Lemma mul_div_le x y z + (Hx : 0 <= x) (Hy : 0 <= y) (Hz : 0 < z) + (Hyz : y <= z) + : x * y / z <= x. + Proof. + transitivity (x * z / z); [ | rewrite Z.div_mul by lia; lia ]. + apply Z_div_le; nia. + Qed. + Hint Resolve mul_div_le : zarith. + + Lemma div_mul_diff_exact a b c + (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) + : c * a / b = c * (a / b) + (c * (a mod b)) / b. + Proof. + rewrite (Z_div_mod_eq a b) at 1 by lia. + rewrite Z.mul_add_distr_l. + replace (c * (b * (a / b))) with ((c * (a / b)) * b) by lia. + rewrite Z.div_add_l by lia. + lia. + Qed. + + Lemma div_mul_diff_exact' a b c + (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) + : c * (a / b) = c * a / b - (c * (a mod b)) / b. + Proof. + rewrite div_mul_diff_exact by assumption; lia. + Qed. + + Lemma div_mul_diff_exact'' a b c + (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) + : a * c / b = (a / b) * c + (c * (a mod b)) / b. + Proof. + rewrite (Z.mul_comm a c), div_mul_diff_exact by lia; lia. + Qed. + + Lemma div_mul_diff_exact''' a b c + (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) + : (a / b) * c = a * c / b - (c * (a mod b)) / b. + Proof. + rewrite (Z.mul_comm a c), div_mul_diff_exact by lia; lia. + Qed. + + Lemma div_mul_diff a b c + (Ha : 0 <= a) (Hb : 0 < b) (Hc : 0 <= c) + : c * a / b - c * (a / b) <= c. + Proof. + rewrite div_mul_diff_exact by assumption. + ring_simplify; auto with zarith. + Qed. + + Lemma div_mul_le_le a b c + : 0 <= a -> 0 < b -> 0 <= c -> c * (a / b) <= c * a / b <= c * (a / b) + c. + Proof. + pose proof (Z.div_mul_diff a b c); split; try apply Z.div_mul_le; lia. + Qed. + + Lemma div_mul_le_le_offset a b c + : 0 <= a -> 0 < b -> 0 <= c -> c * a / b - c <= c * (a / b). + Proof. + pose proof (Z.div_mul_le_le a b c); lia. + Qed. + Hint Resolve div_mul_le_le_offset : zarith. + + Lemma div_x_y_x x y : 0 < x -> 0 < y -> x / y / x = 1 / y. + Proof. + intros; rewrite Z.div_div, (Z.mul_comm y x), <- Z.div_div, Z.div_same by lia. + reflexivity. + Qed. + Hint Rewrite div_x_y_x using zutil_arith : zsimplify. + + Lemma sub_pos_bound_div a b X : 0 <= a < X -> 0 <= b < X -> -1 <= (a - b) / X <= 0. + Proof. + intros H0 H1; pose proof (Z.sub_pos_bound a b X H0 H1). + assert (Hn : -X <= a - b) by lia. + assert (Hp : a - b <= X - 1) by lia. + split; etransitivity; [ | apply Z_div_le, Hn; lia | apply Z_div_le, Hp; lia | ]; + instantiate; autorewrite with zsimplify; try reflexivity. + Qed. + + Hint Resolve (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) + (fun a b X H0 H1 => proj1 (Z.sub_pos_bound_div a b X H0 H1)) : zarith. + + Lemma sub_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (a - b) / X = if a <? b then -1 else 0. + Proof. + intros H0 H1; pose proof (Z.sub_pos_bound_div a b X H0 H1). + destruct (a <? b) eqn:?; Z.ltb_to_lt. + { cut ((a - b) / X <> 0); [ lia | ]. + autorewrite with zstrip_div; auto with zarith lia. } + { autorewrite with zstrip_div; auto with zarith lia. } + Qed. + + Lemma add_opp_pos_bound_div_eq a b X : 0 <= a < X -> 0 <= b < X -> (-b + a) / X = if a <? b then -1 else 0. + Proof. + rewrite !(Z.add_comm (-_)), !Z.add_opp_r. + apply Z.sub_pos_bound_div_eq. + Qed. + + Hint Rewrite Z.sub_pos_bound_div_eq Z.add_opp_pos_bound_div_eq using zutil_arith : zstrip_div. + + Lemma div_small_sym a b : 0 <= a < b -> 0 = a / b. + Proof. intros; symmetry; apply Z.div_small; assumption. Qed. + Hint Resolve div_small_sym : zarith. + + Lemma mod_eq_le_div_1 a b : 0 < a <= b -> a mod b = 0 -> a / b = 1. + Proof. intros; Z.div_mod_to_quot_rem; nia. Qed. + Hint Resolve mod_eq_le_div_1 : zarith. + Hint Rewrite mod_eq_le_div_1 using zutil_arith : zsimplify. + + Lemma div_small_neg x y : 0 < -x <= y -> x / y = -1. + Proof. intros; Z.div_mod_to_quot_rem; nia. Qed. + Hint Rewrite div_small_neg using zutil_arith : zsimplify. + + Lemma div_sub_small x y z : 0 <= x < z -> 0 <= y <= z -> (x - y) / z = if x <? y then -1 else 0. + Proof. + pose proof (Zlt_cases x y). + (destruct (x <? y) eqn:?); + intros; autorewrite with zsimplify; try lia. + Qed. + Hint Rewrite div_sub_small using zutil_arith : zsimplify. + + Lemma mul_div_lt_by_le x y z b : 0 <= y < z -> 0 <= x < b -> x * y / z < b. + Proof. + intros [? ?] [? ?]; eapply Z.le_lt_trans; [ | eassumption ]. + auto with zarith. + Qed. + Hint Resolve mul_div_lt_by_le : zarith. + + Definition mul_div_le' + := fun x y z w p H0 H1 H2 H3 => @Z.le_trans _ _ w (@Z.mul_div_le x y z H0 H1 H2 H3) p. + Hint Resolve mul_div_le' : zarith. + Lemma mul_div_le'' x y z w : y <= w -> 0 <= x -> 0 <= y -> 0 < z -> x <= z -> x * y / z <= w. + Proof. + rewrite (Z.mul_comm x y); intros; apply mul_div_le'; assumption. + Qed. + Hint Resolve mul_div_le'' : zarith. + + Lemma div_between n a b : 0 <= n -> b <> 0 -> n * b <= a < (1 + n) * b -> a / b = n. + Proof. intros; Z.div_mod_to_quot_rem_in_goal; nia. Qed. + Hint Rewrite div_between using zutil_arith : zsimplify. + + Lemma div_between_1 a b : b <> 0 -> b <= a < 2 * b -> a / b = 1. + Proof. intros; rewrite (div_between 1) by lia; reflexivity. Qed. + Hint Rewrite div_between_1 using zutil_arith : zsimplify. + + Lemma div_between_if n a b : 0 <= n -> b <> 0 -> n * b <= a < (2 + n) * b -> (a / b = if (1 + n) * b <=? a then 1 + n else n)%Z. + Proof. + intros. + break_match; Z.ltb_to_lt; + apply div_between; lia. + Qed. + + Lemma div_between_0_if a b : b <> 0 -> 0 <= a < 2 * b -> a / b = if b <=? a then 1 else 0. + Proof. intros; rewrite (div_between_if 0) by lia; autorewrite with zsimplify_const; reflexivity. Qed. End Z. diff --git a/src/Util/ZUtil/Divide.v b/src/Util/ZUtil/Divide.v new file mode 100644 index 000000000..8609db5ad --- /dev/null +++ b/src/Util/ZUtil/Divide.v @@ -0,0 +1,36 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.ZArith.Znumtheory. +Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Tactics.DivideExistsMul. +Local Open Scope Z_scope. + +Module Z. + Lemma divide_mul_div: forall a b c (a_nonzero : a <> 0) (c_nonzero : c <> 0), + (a | b * (a / c)) -> (c | a) -> (c | b). + Proof. + intros ? ? ? ? ? divide_a divide_c_a; do 2 Z.divide_exists_mul. + rewrite divide_c_a in divide_a. + rewrite Z.div_mul' in divide_a by auto. + replace (b * k) with (k * b) in divide_a by ring. + replace (c * k * k0) with (k * (k0 * c)) in divide_a by ring. + rewrite Z.mul_cancel_l in divide_a by (intuition auto with nia; rewrite H in divide_c_a; ring_simplify in divide_a; intuition). + eapply Zdivide_intro; eauto. + Qed. + + Lemma divide2_even_iff : forall n, (2 | n) <-> Z.even n = true. + Proof. + intros n; split. { + intro divide2_n. + Z.divide_exists_mul; [ | pose proof (Z.mod_pos_bound n 2); omega]. + rewrite divide2_n. + apply Z.even_mul. + } { + intro n_even. + pose proof (Zmod_even n) as H. + rewrite n_even in H. + apply Zmod_divide; omega || auto. + } + Qed. +End Z. diff --git a/src/Util/ZUtil/Hints/ZArith.v b/src/Util/ZUtil/Hints/ZArith.v index 17e56f9cf..2aa70dc97 100644 --- a/src/Util/ZUtil/Hints/ZArith.v +++ b/src/Util/ZUtil/Hints/ZArith.v @@ -6,3 +6,5 @@ Hint Resolve (fun a b H => proj1 (Z.mod_pos_bound a b H)) (fun a b H => proj2 (Z Hint Resolve (fun n m => proj1 (Z.opp_le_mono n m)) : zarith. Hint Resolve (fun n m => proj1 (Z.pred_le_mono n m)) : zarith. Hint Resolve (fun a b => proj2 (Z.lor_nonneg a b)) : zarith. + +Hint Resolve Zmult_le_compat_r Zmult_le_compat_l Z_div_le Z.add_le_mono Z.sub_le_mono : zarith. diff --git a/src/Util/ZUtil/Land.v b/src/Util/ZUtil/Land.v index f46d541e9..7f27f942d 100644 --- a/src/Util/ZUtil/Land.v +++ b/src/Util/ZUtil/Land.v @@ -1,6 +1,8 @@ Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. Require Import Crypto.Util.ZUtil.Notations. -Local Open Scope Z_scope. +Require Import Crypto.Util.ZUtil.Definitions. +Local Open Scope bool_scope. Local Open Scope Z_scope. Module Z. Lemma land_same_r : forall a b, (a &' b) &' b = a &' b. @@ -10,4 +12,15 @@ Module Z. case_eq (Z.testbit b n); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; reflexivity. Qed. + + Lemma land_m1'_l a : Z.land (-1) a = a. + Proof. apply Z.land_m1_l. Qed. + Hint Rewrite Z.land_m1_l land_m1'_l : zsimplify_const zsimplify zsimplify_fast. + + Lemma land_m1'_r a : Z.land a (-1) = a. + Proof. apply Z.land_m1_r. Qed. + Hint Rewrite Z.land_m1_r land_m1'_r : zsimplify_const zsimplify zsimplify_fast. + + Lemma sub_1_lt_le x y : (x - 1 < y) <-> (x <= y). + Proof. lia. Qed. End Z. diff --git a/src/Util/ZUtil/LandLorBounds.v b/src/Util/ZUtil/LandLorBounds.v new file mode 100644 index 000000000..1b10ecf97 --- /dev/null +++ b/src/Util/ZUtil/LandLorBounds.v @@ -0,0 +1,132 @@ +Require Import Coq.micromega.Lia. +Require Import Coq.ZArith.ZArith. +Require Import Coq.Classes.Morphisms. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Pow2. +Require Import Crypto.Util.ZUtil.Tactics.PeelLe. +Require Import Crypto.Util.ZUtil.Modulo.PullPush. +Require Import Crypto.Util.ZUtil.Ones. +Require Import Crypto.Util.ZUtil.Lnot. +Require Import Crypto.Util.ZUtil.Land. +Require Import Crypto.Util.Tactics.UniquePose. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.BreakMatch. +Local Open Scope Z_scope. + +Module Z. + Local Ltac saturate := + repeat first [ progress cbv [Z.round_lor_land_bound Proper respectful Basics.flip] in * + | progress cbn in * + | progress intros + | match goal with + | [ |- context[Z.log2_up ?x] ] + => unique pose proof (Z.log2_up_nonneg x) + | [ |- context[2^?x] ] + => unique assert (0 <= 2^x) by (apply Z.pow_nonneg; lia) + | [ H : 0 <= ?x |- context[2^?x] ] + => unique assert (0 < 2^x) by (apply Z.pow_pos_nonneg; lia) + | [ H : Pos.le ?x ?y |- context[Z.pos ?x] ] + => unique assert (Z.pos x <= Z.pos y) by lia + | [ H : Pos.le ?x ?y |- context[Z.pos (?x+1)] ] + => unique assert (Z.pos (x+1) <= Z.pos (y+1)) by lia + | [ H : Z.le ?x ?y |- context[2^Z.log2_up ?x] ] + => unique assert (2^Z.log2_up x <= 2^Z.log2_up y) by (Z.peel_le; lia) + end ]. + Local Ltac do_rewrites_step := + match goal with + | [ |- ?R ?x ?x ] => reflexivity + | [ |- context[Z.land (-2^_) (-2^_)] ] + => rewrite <- !Z.lnot_ones_equiv, <- !Z.lnot_lor, !Z.lor_ones_ones, !Z.lnot_ones_equiv + | [ |- context[Z.lor (-2^_) (-2^_)] ] + => rewrite <- !Z.lnot_ones_equiv, <- !Z.lnot_land, !Z.land_ones_ones, !Z.lnot_ones_equiv + | [ |- context[Z.land (2^_-1) (2^_-1)] ] + => rewrite !Z.sub_1_r, <- !Z.ones_equiv, !Z.land_ones_ones, !Z.ones_equiv, <- !Z.sub_1_r + | [ |- context[Z.lor (2^_-1) (2^_-1)] ] + => rewrite !Z.sub_1_r, <- !Z.ones_equiv, !Z.lor_ones_ones, !Z.ones_equiv, <- !Z.sub_1_r + | [ |- context[Z.land (2^?x-1) (-2^?y)] ] + => rewrite (@Z.land_comm (2^x-1) (-2^y)) + | [ |- context[Z.lor (2^?x-1) (-2^?y)] ] + => rewrite (@Z.lor_comm (2^x-1) (-2^y)) + | [ |- context[Z.land (-2^_) (2^_-1)] ] + => rewrite !Z.sub_1_r, <- !Z.ones_equiv, !Z.land_ones, ?Z.ones_equiv, <- ?Z.sub_1_r by lia + | [ |- context[Z.lor (-2^?x) (2^?y-1)] ] + => rewrite <- !Z.lnot_ones_equiv, <- (Z.lnot_involutive (2^y-1)), <- !Z.lnot_land, ?Z.lnot_ones_equiv, (Z.lnot_sub1 (2^y)), !Z.ones_equiv, ?Z.lnot_equiv, <- !Z.sub_1_r + | [ |- context[-?x mod ?y] ] + => rewrite (@Z.opp_mod_mod_push x y) by Z.NoZMod + | [ H : ?x <= ?x |- _ ] => clear H + | [ H : ?x < ?y, H' : ?y <= ?z |- _ ] => unique assert (x < z) by lia + | [ H : ?x < ?y, H' : ?a <= ?x |- _ ] => unique assert (a < y) by lia + | [ H : 2^?x < 2^?y |- context[2^?x mod 2^?y] ] + => repeat first [ rewrite (Z.mod_small (2^x) (2^y)) by lia + | rewrite !(@Z_mod_nz_opp_full (2^x) (2^y)) ] + | [ H : ?x < ?y, H' : context[?x mod ?y] |- _ ] => rewrite (Z.mod_small x y) in H' by lia + | [ |- context[2^?x mod 2^?y] ] + => let H := fresh in + destruct (@Z.pow2_lt_or_divides x y ltac:(lia)) as [H|H]; + [ repeat first [ rewrite (Z.mod_small (2^x) (2^y)) by lia + | rewrite !(@Z_mod_nz_opp_full (2^x) (2^y)) ] + | rewrite H ] + | _ => progress autorewrite with zsimplify_const + end. + Local Ltac do_rewrites := repeat do_rewrites_step. + Local Ltac fin_t := + repeat first [ progress destruct_head'_and + | match goal with + | [ H : orb _ _ = _ |- _ ] + => progress rewrite ?Bool.orb_true_iff, ?Bool.orb_false_iff, ?Z.ltb_lt, ?Z.ltb_ge in * + end + | break_innermost_match_step + | progress destruct_head'_or + | lia + | progress Z.peel_le ]. + Local Ltac t := + saturate; do_rewrites; fin_t. + + Local Instance land_round_Proper_pos_r x + : Proper (Pos.le ==> Z.le) + (fun y => + Z.land (Z.round_lor_land_bound x) (Z.round_lor_land_bound (Z.pos y))). + Proof. destruct x; t. Qed. + + Local Instance land_round_Proper_pos_l y + : Proper (Pos.le ==> Z.le) + (fun x => + Z.land (Z.round_lor_land_bound (Z.pos x)) (Z.round_lor_land_bound y)). + Proof. destruct y; t. Qed. + + Local Instance lor_round_Proper_pos_r x + : Proper (Pos.le ==> Z.le) + (fun y => + Z.lor (Z.round_lor_land_bound x) (Z.round_lor_land_bound (Z.pos y))). + Proof. destruct x; t. Qed. + + Local Instance lor_round_Proper_pos_l y + : Proper (Pos.le ==> Z.le) + (fun x => + Z.lor (Z.round_lor_land_bound (Z.pos x)) (Z.round_lor_land_bound y)). + Proof. destruct y; t. Qed. + + Local Instance land_round_Proper_neg_r x + : Proper (Basics.flip Pos.le ==> Z.le) + (fun y => + Z.land (Z.round_lor_land_bound x) (Z.round_lor_land_bound (Z.neg y))). + Proof. destruct x; t. Qed. + + Local Instance land_round_Proper_neg_l y + : Proper (Basics.flip Pos.le ==> Z.le) + (fun x => + Z.land (Z.round_lor_land_bound (Z.neg x)) (Z.round_lor_land_bound y)). + Proof. destruct y; t. Qed. + + Local Instance lor_round_Proper_neg_r x + : Proper (Basics.flip Pos.le ==> Z.le) + (fun y => + Z.lor (Z.round_lor_land_bound x) (Z.round_lor_land_bound (Z.neg y))). + Proof. destruct x; t. Qed. + + Local Instance lor_round_Proper_neg_l y + : Proper (Basics.flip Pos.le ==> Z.le) + (fun x => + Z.lor (Z.round_lor_land_bound (Z.neg x)) (Z.round_lor_land_bound y)). + Proof. destruct y; t. Qed. +End Z. diff --git a/src/Util/ZUtil/LandLorShiftBounds.v b/src/Util/ZUtil/LandLorShiftBounds.v new file mode 100644 index 000000000..e978ab6b0 --- /dev/null +++ b/src/Util/ZUtil/LandLorShiftBounds.v @@ -0,0 +1,340 @@ +Require Import Coq.Classes.Morphisms. +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Hints.ZArith. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Pow. +Require Import Crypto.Util.ZUtil.Pow2. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Testbit. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos. +Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. +Require Import Crypto.Util.NUtil.WithoutReferenceToZ. +Local Open Scope Z_scope. + +Module Z. + Lemma lor_range : forall x y n, 0 <= x < 2 ^ n -> 0 <= y < 2 ^ n -> + 0 <= Z.lor x y < 2 ^ n. + Proof. + intros x y n H H0; assert (0 <= n) by auto with zarith omega. + repeat match goal with + | |- _ => progress intros + | |- _ => rewrite Z.lor_spec + | |- _ => rewrite Z.testbit_eqb by auto with zarith omega + | |- _ => rewrite !Z.div_small by (split; try omega; eapply Z.lt_le_trans; + [ intuition eassumption | apply Z.pow_le_mono_r; omega]) + | |- _ => split + | |- _ => apply Z.testbit_false_bound + | |- _ => solve [auto with zarith] + | |- _ => solve [apply Z.lor_nonneg; intuition auto] + end. + Qed. + Hint Resolve lor_range : zarith. + + Lemma lor_shiftl_bounds : forall x y n m, + (0 <= n)%Z -> (0 <= m)%Z -> + (0 <= x < 2 ^ m)%Z -> + (0 <= y < 2 ^ n)%Z -> + (0 <= Z.lor y (Z.shiftl x n) < 2 ^ (n + m))%Z. + Proof. + intros x y n m H H0 H1 H2. + apply Z.lor_range. + { split; try omega. + apply Z.lt_le_trans with (m := (2 ^ n)%Z); try omega. + apply Z.pow_le_mono_r; omega. } + { rewrite Z.shiftl_mul_pow2 by omega. + rewrite Z.pow_add_r by omega. + split; Z.zero_bounds. + rewrite Z.mul_comm. + apply Z.mul_lt_mono_pos_l; omega. } + Qed. + + Lemma land_upper_bound_l : forall a b, (0 <= a) -> (0 <= b) -> + Z.land a b <= a. + Proof. + intros a b H H0. + destruct a, b; try solve [exfalso; auto]; try solve [cbv; congruence]. + cbv [Z.land]. + rewrite <-N2Z.inj_pos, <-N2Z.inj_le. + auto using N.Pos_land_upper_bound_l. + Qed. + + Lemma land_upper_bound_r : forall a b, (0 <= a) -> (0 <= b) -> + Z.land a b <= b. + Proof. + intros. + rewrite Z.land_comm. + auto using Z.land_upper_bound_l. + Qed. + + Section ZInequalities. + Lemma land_le : forall x y, (0 <= x)%Z -> (Z.land x y <= x)%Z. + Proof. + intros x y H; apply Z.ldiff_le; [assumption|]. + rewrite Z.ldiff_land, Z.land_comm, Z.land_assoc. + rewrite <- Z.land_0_l with (a := y); f_equal. + rewrite Z.land_comm, Z.land_lnot_diag. + reflexivity. + Qed. + + Lemma lor_lower : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> (x <= Z.lor x y)%Z. + Proof. + intros x y H H0; apply Z.ldiff_le; [apply Z.lor_nonneg; auto|]. + rewrite Z.ldiff_land. + apply Z.bits_inj_iff'; intros k Hpos; apply Z.le_ge in Hpos. + rewrite Z.testbit_0_l, Z.land_spec, Z.lnot_spec, Z.lor_spec; + [|apply Z.ge_le; assumption]. + induction (Z.testbit x k), (Z.testbit y k); cbv; reflexivity. + Qed. + + Lemma lor_le : forall x y z, + (0 <= x)%Z + -> (x <= y)%Z + -> (y <= z)%Z + -> (Z.lor x y <= (2 ^ Z.log2_up (z+1)) - 1)%Z. + Proof. + intros x y z H H0 H1; apply Z.ldiff_le. + + - apply Z.le_add_le_sub_r. + replace 1%Z with (2 ^ 0)%Z by (cbv; reflexivity). + rewrite Z.add_0_l. + apply Z.pow_le_mono_r; [cbv; reflexivity|]. + apply Z.log2_up_nonneg. + + - destruct (Z_lt_dec 0 z). + + + assert (forall a, a - 1 = Z.pred a)%Z as HP by (intro; omega); + rewrite HP, <- Z.ones_equiv; clear HP. + apply Z.ldiff_ones_r_low; [apply Z.lor_nonneg; split; omega|]. + rewrite Z.log2_up_eqn, Z.log2_lor; try omega. + apply Z.lt_succ_r. + apply Z.max_case_strong; intros; apply Z.log2_le_mono; omega. + + + replace z with 0%Z by omega. + replace y with 0%Z by omega. + replace x with 0%Z by omega. + cbv; reflexivity. + Qed. + + Local Ltac solve_pow2 := + repeat match goal with + | [|- _ /\ _] => split + | [|- (0 < 2 ^ _)%Z] => apply Z.pow2_gt_0 + | [|- (0 <= 2 ^ _)%Z] => apply Z.pow2_ge_0 + | [|- (2 ^ _ <= 2 ^ _)%Z] => apply Z.pow_le_mono_r + | [|- (_ <= _)%Z] => omega + | [|- (_ < _)%Z] => omega + end. + + Lemma pow2_mod_range : forall a n m, + (0 <= n) -> + (n <= m) -> + (0 <= Z.pow2_mod a n < 2 ^ m). + Proof. + intros; unfold Z.pow2_mod. + rewrite Z.land_ones; [|assumption]. + split; [apply Z.mod_pos_bound, Z.pow2_gt_0; assumption|]. + eapply Z.lt_le_trans; [apply Z.mod_pos_bound, Z.pow2_gt_0; assumption|]. + apply Z.pow_le_mono; [|assumption]. + split; simpl; omega. + Qed. + + Lemma shiftr_range : forall a n m, + (0 <= n)%Z -> + (0 <= m)%Z -> + (0 <= a < 2 ^ (n + m))%Z -> + (0 <= Z.shiftr a n < 2 ^ m)%Z. + Proof. + intros a n m H0 H1 H2; destruct H2. + split; [apply Z.shiftr_nonneg; assumption|]. + rewrite Z.shiftr_div_pow2; [|assumption]. + apply Z.div_lt_upper_bound; [apply Z.pow2_gt_0; assumption|]. + eapply Z.lt_le_trans; [eassumption|apply Z.eq_le_incl]. + apply Z.pow_add_r; omega. + Qed. + + + Lemma shiftr_le_mono: forall a b c d, + (0 <= a)%Z + -> (0 <= d)%Z + -> (a <= c)%Z + -> (d <= b)%Z + -> (Z.shiftr a b <= Z.shiftr c d)%Z. + Proof. + intros. + repeat rewrite Z.shiftr_div_pow2; [|omega|omega]. + etransitivity; [apply Z.div_le_compat_l | apply Z.div_le_mono]; solve_pow2. + Qed. + + Lemma shiftl_le_mono: forall a b c d, + (0 <= a)%Z + -> (0 <= b)%Z + -> (a <= c)%Z + -> (b <= d)%Z + -> (Z.shiftl a b <= Z.shiftl c d)%Z. + Proof. + intros. + repeat rewrite Z.shiftl_mul_pow2; [|omega|omega]. + etransitivity; [apply Z.mul_le_mono_nonneg_l|apply Z.mul_le_mono_nonneg_r]; solve_pow2. + Qed. + End ZInequalities. + + Lemma lor_bounds x y : 0 <= x -> 0 <= y + -> Z.max x y <= Z.lor x y <= 2^Z.log2_up (Z.max x y + 1) - 1. + Proof. + apply Z.max_case_strong; intros; split; + try solve [ eauto using lor_lower, Z.le_trans, lor_le with omega + | rewrite Z.lor_comm; eauto using lor_lower, Z.le_trans, lor_le with omega ]. + Qed. + Lemma lor_bounds_lower x y : 0 <= x -> 0 <= y + -> Z.max x y <= Z.lor x y. + Proof. intros; apply lor_bounds; assumption. Qed. + Lemma lor_bounds_upper x y : Z.lor x y <= 2^Z.log2_up (Z.max x y + 1) - 1. + Proof. + pose proof (proj2 (Z.lor_neg x y)). + destruct (Z_lt_le_dec x 0), (Z_lt_le_dec y 0); + try solve [ intros; apply lor_bounds; assumption ]; + transitivity (2^0-1); + try apply Z.sub_le_mono_r, Z.pow_le_mono_r, Z.log2_up_nonneg; + simpl; omega. + Qed. + Lemma lor_bounds_gen_lower x y l : 0 <= x -> 0 <= y -> l <= Z.max x y + -> l <= Z.lor x y. + Proof. + intros; etransitivity; + solve [ apply lor_bounds; auto + | eauto ]. + Qed. + Lemma lor_bounds_gen_upper x y u : x <= u -> y <= u + -> Z.lor x y <= 2^Z.log2_up (u + 1) - 1. + Proof. + intros; etransitivity; [ apply lor_bounds_upper | ]. + apply Z.sub_le_mono_r, Z.pow_le_mono_r, Z.log2_up_le_mono, Z.max_case_strong; + omega. + Qed. + Lemma lor_bounds_gen x y l u : 0 <= x -> 0 <= y -> l <= Z.max x y -> x <= u -> y <= u + -> l <= Z.lor x y <= 2^Z.log2_up (u + 1) - 1. + Proof. auto using lor_bounds_gen_lower, lor_bounds_gen_upper. Qed. + + Lemma shiftl_le_Proper2 y + : Proper (Z.le ==> Z.le) (fun x => Z.shiftl x y). + Proof. + unfold Basics.flip in *. + pose proof (Zle_cases 0 y) as Hx. + intros x x' H. + pose proof (Zle_cases 0 x) as Hy. + pose proof (Zle_cases 0 x') as Hy'. + destruct (0 <=? y), (0 <=? x), (0 <=? x'); + autorewrite with Zshift_to_pow; + Z.replace_all_neg_with_pos; + autorewrite with pull_Zopp; + rewrite ?Z.div_opp_l_complete; + repeat destruct (Z_zerop _); + autorewrite with zsimplify_const pull_Zopp; + auto with zarith; + repeat match goal with + | [ |- context[-?x - ?y] ] + => replace (-x - y) with (-(x + y)) by omega + | _ => rewrite <- Z.opp_le_mono + | _ => rewrite <- Z.add_le_mono_r + | _ => solve [ auto with zarith ] + | [ |- ?x <= ?y + 1 ] + => cut (x <= y); [ omega | solve [ auto with zarith ] ] + | [ |- -_ <= _ ] + => solve [ transitivity (-0); auto with zarith ] + end. + { repeat match goal with H : context[_ mod _] |- _ => revert H end; + Z.div_mod_to_quot_rem_in_goal; nia. } + Qed. + + Lemma shiftl_le_Proper1 x + (R := fun b : bool => if b then Z.le else Basics.flip Z.le) + : Proper (R (0 <=? x) ==> Z.le) (Z.shiftl x). + Proof. + unfold Basics.flip in *. + pose proof (Zle_cases 0 x) as Hx. + intros y y' H. + pose proof (Zle_cases 0 y) as Hy. + pose proof (Zle_cases 0 y') as Hy'. + destruct (0 <=? x), (0 <=? y), (0 <=? y'); subst R; cbv beta iota in *; + autorewrite with Zshift_to_pow; + Z.replace_all_neg_with_pos; + autorewrite with pull_Zopp; + rewrite ?Z.div_opp_l_complete; + repeat destruct (Z_zerop _); + autorewrite with zsimplify_const pull_Zopp; + auto with zarith; + repeat match goal with + | [ |- context[-?x - ?y] ] + => replace (-x - y) with (-(x + y)) by omega + | _ => rewrite <- Z.opp_le_mono + | _ => rewrite <- Z.add_le_mono_r + | _ => solve [ auto with zarith ] + | [ |- ?x <= ?y + 1 ] + => cut (x <= y); [ omega | solve [ auto with zarith ] ] + | [ |- context[2^?x] ] + => lazymatch goal with + | [ H : 1 < 2^x |- _ ] => fail + | [ H : 0 < 2^x |- _ ] => fail + | [ H : 0 <= 2^x |- _ ] => fail + | _ => first [ assert (1 < 2^x) by auto with zarith + | assert (0 < 2^x) by auto with zarith + | assert (0 <= 2^x) by auto with zarith ] + end + | [ H : ?x <= ?y |- _ ] + => is_var x; is_var y; + lazymatch goal with + | [ H : 2^x <= 2^y |- _ ] => fail + | [ H : 2^x < 2^y |- _ ] => fail + | _ => assert (2^x <= 2^y) by auto with zarith + end + | [ H : ?x <= ?y, H' : ?f ?x = ?k, H'' : ?f ?y <> ?k |- _ ] + => let Hn := fresh in + assert (Hn : x <> y) by congruence; + assert (x < y) by omega; clear H Hn + | [ H : ?x <= ?y, H' : ?f ?x <> ?k, H'' : ?f ?y = ?k |- _ ] + => let Hn := fresh in + assert (Hn : x <> y) by congruence; + assert (x < y) by omega; clear H Hn + | _ => solve [ repeat match goal with H : context[_ mod _] |- _ => revert H end; + Z.div_mod_to_quot_rem_in_goal; subst; + lazymatch goal with + | [ |- _ <= (?a * ?q + ?r) * ?q' ] + => transitivity (q * (a * q') + r * q'); + [ assert (0 < a * q') by nia; nia + | nia ] + end ] + end. + { replace y' with (y + (y' - y)) by omega. + rewrite Z.pow_add_r, <- Zdiv_Zdiv by auto with zarith. + assert (y < y') by (assert (y <> y') by congruence; omega). + assert (1 < 2^(y'-y)) by auto with zarith. + assert (0 < x / 2^y) + by (repeat match goal with H : context[_ mod _] |- _ => revert H end; + Z.div_mod_to_quot_rem_in_goal; nia). + assert (2^y <= x) + by (repeat match goal with H : context[_ / _] |- _ => revert H end; + Z.div_mod_to_quot_rem_in_goal; nia). + match goal with + | [ |- ?x + 1 <= ?y ] => cut (x < y); [ omega | ] + end. + auto with zarith. } + Qed. + + Lemma shiftr_le_Proper2 y + : Proper (Z.le ==> Z.le) (fun x => Z.shiftr x y). + Proof. apply shiftl_le_Proper2. Qed. + + Lemma shiftr_le_Proper1 x + (R := fun b : bool => if b then Z.le else Basics.flip Z.le) + : Proper (R (x <? 0) ==> Z.le) (Z.shiftr x). + Proof. + subst R; intros y y' H'; unfold Z.shiftr; apply shiftl_le_Proper1. + unfold Basics.flip in *. + pose proof (Zle_cases 0 x). + pose proof (Zlt_cases x 0). + destruct (0 <=? x), (x <? 0); try omega. + Qed. +End Z. diff --git a/src/Util/ZUtil/Le.v b/src/Util/ZUtil/Le.v index ab7767de7..ca180c556 100644 --- a/src/Util/ZUtil/Le.v +++ b/src/Util/ZUtil/Le.v @@ -1,9 +1,58 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Local Open Scope Z_scope. Module Z. Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0. Proof. intros; omega. Qed. Hint Resolve positive_is_nonzero : zarith. + + Lemma le_lt_trans n m p : n <= m -> m < p -> n < p. + Proof. lia. Qed. + + Lemma le_fold_right_max : forall low l x, (forall y, List.In y l -> low <= y) -> + List.In x l -> x <= List.fold_right Z.max low l. + Proof. + induction l as [|a l IHl]; intros ? lower_bound In_list; [cbv [List.In] in *; intuition | ]. + simpl. + destruct (List.in_inv In_list); subst. + + apply Z.le_max_l. + + etransitivity. + - apply IHl; auto; intuition auto with datatypes. + - apply Z.le_max_r. + Qed. + + Lemma le_fold_right_max_initial : forall low l, low <= List.fold_right Z.max low l. + Proof. + induction l as [|a l IHl]; intros; try reflexivity. + etransitivity; [ apply IHl | apply Z.le_max_r ]. + Qed. + + Lemma add_compare_mono_r: forall n m p, (n + p ?= m + p) = (n ?= m). + Proof. + intros n m p. + rewrite <-!(Z.add_comm p). + apply Z.add_compare_mono_l. + Qed. + + Lemma leb_add_same x y : (x <=? y + x) = (0 <=? y). + Proof. destruct (x <=? y + x) eqn:?, (0 <=? y) eqn:?; Z.ltb_to_lt; try reflexivity; omega. Qed. + Hint Rewrite leb_add_same : zsimplify. + + Lemma ltb_add_same x y : (x <? y + x) = (0 <? y). + Proof. destruct (x <? y + x) eqn:?, (0 <? y) eqn:?; Z.ltb_to_lt; try reflexivity; omega. Qed. + Hint Rewrite ltb_add_same : zsimplify. + + Lemma geb_add_same x y : (x >=? y + x) = (0 >=? y). + Proof. destruct (x >=? y + x) eqn:?, (0 >=? y) eqn:?; Z.ltb_to_lt; try reflexivity; omega. Qed. + Hint Rewrite geb_add_same : zsimplify. + + Lemma gtb_add_same x y : (x >? y + x) = (0 >? y). + Proof. destruct (x >? y + x) eqn:?, (0 >? y) eqn:?; Z.ltb_to_lt; try reflexivity; omega. Qed. + Hint Rewrite gtb_add_same : zsimplify. + + Lemma sub_pos_bound a b X : 0 <= a < X -> 0 <= b < X -> -X < a - b < X. + Proof. lia. Qed. End Z. diff --git a/src/Util/ZUtil/Lnot.v b/src/Util/ZUtil/Lnot.v new file mode 100644 index 000000000..c4c747c76 --- /dev/null +++ b/src/Util/ZUtil/Lnot.v @@ -0,0 +1,16 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Local Open Scope Z_scope. + +Module Z. + Lemma lnot_equiv n : Z.lnot n = Z.pred (-n). + Proof. reflexivity. Qed. + + Lemma lnot_sub1 n : Z.lnot (n-1) = -n. + Proof. rewrite lnot_equiv; lia. Qed. + + Lemma lnot_opp x : Z.lnot (- x) = x-1. + Proof. + rewrite <-Z.lnot_involutive, lnot_sub1; reflexivity. + Qed. +End Z. diff --git a/src/Util/ZUtil/Log2.v b/src/Util/ZUtil/Log2.v new file mode 100644 index 000000000..90c43b7fb --- /dev/null +++ b/src/Util/ZUtil/Log2.v @@ -0,0 +1,90 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Hints.ZArith. +Require Import Crypto.Util.ZUtil.Pow. +Require Import Crypto.Util.ZUtil.ZSimplify.Core. +Require Import Crypto.Util.ZUtil.ZSimplify.Simple. +Local Open Scope Z_scope. + +Module Z. + Lemma log2_nonneg' n a : n <= 0 -> n <= Z.log2 a. + Proof. + intros; transitivity 0; auto with zarith. + Qed. + Hint Resolve log2_nonneg' : zarith. + + Lemma le_lt_to_log2 x y z : 0 <= z -> 0 < y -> 2^x <= y < 2^z -> x <= Z.log2 y < z. + Proof. + destruct (Z_le_gt_dec 0 x); auto with concl_log2 lia. + Qed. + + Lemma log2_pred_pow2_full a : Z.log2 (Z.pred (2^a)) = Z.max 0 (Z.pred a). + Proof. + destruct (Z_dec 0 a) as [ [?|?] | ?]. + { rewrite Z.log2_pred_pow2 by assumption; lia. } + { autorewrite with zsimplify; simpl. + apply Z.max_case_strong; try omega. + + } + { subst; compute; reflexivity. } + Qed. + Hint Rewrite log2_pred_pow2_full : zsimplify. + + Lemma log2_up_le_full a : a <= 2^Z.log2_up a. + Proof. + destruct (Z_dec 1 a) as [ [ ? | ? ] | ? ]; + first [ apply Z.log2_up_spec; assumption + | rewrite Z.log2_up_eqn0 by omega; simpl; omega ]. + Qed. + + Lemma log2_up_le_pow2_full : forall a b : Z, (0 <= b)%Z -> (a <= 2 ^ b)%Z <-> (Z.log2_up a <= b)%Z. + Proof. + intros a b H. + destruct (Z_lt_le_dec 0 a); [ apply Z.log2_up_le_pow2; assumption | ]. + split; transitivity 0%Z; try omega; auto with zarith. + rewrite Z.log2_up_eqn0 by omega. + reflexivity. + Qed. + + Lemma log2_lt_pow2_alt a b : 0 < b -> (a < 2^b <-> Z.log2 a < b). + Proof. + destruct (Z_lt_le_dec 0 a); auto using Z.log2_lt_pow2; []. + rewrite Z.log2_nonpos by omega. + split; auto with zarith; []. + intro; eapply Z.le_lt_trans; [ eassumption | ]. + auto with zarith. + Qed. + + Lemma max_log2_up x y : Z.max (Z.log2_up x) (Z.log2_up y) = Z.log2_up (Z.max x y). + Proof. apply Z.max_monotone; intros ??; apply Z.log2_up_le_mono. Qed. + Hint Rewrite max_log2_up : push_Zmax. + Hint Rewrite <- max_log2_up : pull_Zmax. + + Lemma log2_up_le_full_max a : Z.max a 1 <= 2^Z.log2_up a. + Proof. + apply Z.max_case_strong; auto using Z.log2_up_le_full. + intros; rewrite Z.log2_up_eqn0 by assumption; reflexivity. + Qed. + Lemma log2_up_le_1 a : Z.log2_up a <= 1 <-> a <= 2. + Proof. + pose proof (Z.log2_nonneg (Z.pred a)). + destruct (Z_dec a 2) as [ [ ? | ? ] | ? ]. + { rewrite (proj2 (Z.log2_up_null a)) by omega; split; omega. } + { rewrite Z.log2_up_eqn by omega. + split; try omega; intro. + assert (Z.log2 (Z.pred a) = 0) by omega. + assert (Z.pred a <= 1) by (apply Z.log2_null; omega). + omega. } + { subst; cbv -[Z.le]; split; omega. } + Qed. + Lemma log2_up_1_le a : 1 <= Z.log2_up a <-> 2 <= a. + Proof. + pose proof (Z.log2_nonneg (Z.pred a)). + destruct (Z_dec a 2) as [ [ ? | ? ] | ? ]. + { rewrite (proj2 (Z.log2_up_null a)) by omega; split; omega. } + { rewrite Z.log2_up_eqn by omega; omega. } + { subst; cbv -[Z.le]; split; omega. } + Qed. +End Z. diff --git a/src/Util/ZUtil/Modulo.v b/src/Util/ZUtil/Modulo.v index 84917a454..567d106e3 100644 --- a/src/Util/ZUtil/Modulo.v +++ b/src/Util/ZUtil/Modulo.v @@ -4,6 +4,7 @@ Require Import Crypto.Util.ZUtil.ZSimplify.Core. Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos. +Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo. Require Import Crypto.Util.ZUtil.Div. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.DestructHead. @@ -287,4 +288,85 @@ Module Z. Lemma mod_opp_r a b : a mod (-b) = -((-a) mod b). Proof. pose proof (Z.div_opp_r a b); Z.div_mod_to_quot_rem; nia. Qed. Hint Resolve mod_opp_r : zarith. + + Lemma mod_same_pow : forall a b c, 0 <= c <= b -> a ^ b mod a ^ c = 0. + Proof. + intros a b c H. + replace b with (b - c + c) by ring. + rewrite Z.pow_add_r by omega. + apply Z_mod_mult. + Qed. + Hint Rewrite mod_same_pow using zutil_arith : zsimplify. + + Lemma mod_opp_l_z_iff a b (H : b <> 0) : a mod b = 0 <-> (-a) mod b = 0. + Proof. + split; intro H'; apply Z.mod_opp_l_z in H'; rewrite ?Z.opp_involutive in H'; assumption. + Qed. + Hint Rewrite <- mod_opp_l_z_iff using zutil_arith : zsimplify. + + Lemma mod_small_sym a b : 0 <= a < b -> a = a mod b. + Proof. intros; symmetry; apply Z.mod_small; assumption. Qed. + Hint Resolve mod_small_sym : zarith. + + Lemma mod_eq_le_to_eq a b : 0 < a <= b -> a mod b = 0 -> a = b. + Proof. pose proof (Z.mod_eq_le_div_1 a b); intros; Z.div_mod_to_quot_rem; nia. Qed. + Hint Resolve mod_eq_le_to_eq : zarith. + + Lemma mod_neq_0_le_to_neq a b : a mod b <> 0 -> a <> b. + Proof. repeat intro; subst; autorewrite with zsimplify in *; lia. Qed. + Hint Resolve mod_neq_0_le_to_neq : zarith. + + Lemma div_mod' a b : b <> 0 -> a = (a / b) * b + a mod b. + Proof. intro; etransitivity; [ apply (Z.div_mod a b); assumption | lia ]. Qed. + Hint Rewrite <- div_mod' using zutil_arith : zsimplify. + + Lemma div_mod'' a b : b <> 0 -> a = a mod b + b * (a / b). + Proof. intro; etransitivity; [ apply (Z.div_mod a b); assumption | lia ]. Qed. + Hint Rewrite <- div_mod'' using zutil_arith : zsimplify. + + Lemma div_mod''' a b : b <> 0 -> a = a mod b + (a / b) * b. + Proof. intro; etransitivity; [ apply (Z.div_mod a b); assumption | lia ]. Qed. + Hint Rewrite <- div_mod''' using zutil_arith : zsimplify. + + Lemma sub_mod_mod_0 x d : (x - x mod d) mod d = 0. + Proof. + destruct (Z_zerop d); subst; push_Zmod; autorewrite with zsimplify; reflexivity. + Qed. + Hint Resolve sub_mod_mod_0 : zarith. + Hint Rewrite sub_mod_mod_0 : zsimplify. + + Lemma mod_small_n n a b : 0 <= n -> b <> 0 -> n * b <= a < (1 + n) * b -> a mod b = a - n * b. + Proof. intros; erewrite Zmod_eq_full, Z.div_between by eassumption. reflexivity. Qed. + Hint Rewrite mod_small_n using zutil_arith : zsimplify. + + Lemma mod_small_1 a b : b <> 0 -> b <= a < 2 * b -> a mod b = a - b. + Proof. intros; rewrite (mod_small_n 1) by lia; lia. Qed. + Hint Rewrite mod_small_1 using zutil_arith : zsimplify. + + Lemma mod_small_n_if n a b : 0 <= n -> b <> 0 -> n * b <= a < (2 + n) * b -> a mod b = a - (if (1 + n) * b <=? a then (1 + n) else n) * b. + Proof. intros; erewrite Zmod_eq_full, Z.div_between_if by eassumption; autorewrite with zsimplify_const. reflexivity. Qed. + + Lemma mod_small_0_if a b : b <> 0 -> 0 <= a < 2 * b -> a mod b = a - if b <=? a then b else 0. + Proof. intros; rewrite (mod_small_n_if 0) by lia; autorewrite with zsimplify_const. break_match; lia. Qed. + + Lemma mul_mod_distr_r_full a b c : (a * c) mod (b * c) = (a mod b * c). + Proof. + destruct (Z_zerop b); [ | destruct (Z_zerop c) ]; subst; + autorewrite with zsimplify; auto using Z.mul_mod_distr_r. + Qed. + + Lemma mul_mod_distr_l_full a b c : (c * a) mod (c * b) = c * (a mod b). + Proof. + destruct (Z_zerop b); [ | destruct (Z_zerop c) ]; subst; + autorewrite with zsimplify; auto using Z.mul_mod_distr_l. + Qed. + + Lemma lt_mul_2_mod_sub : forall a b, b <> 0 -> b <= a < 2 * b -> a mod b = a - b. + Proof. + intros a b H H0. + replace (a mod b) with ((1 * b + (a - b)) mod b) by (f_equal; ring). + rewrite Z.mod_add_l by auto. + apply Z.mod_small. + omega. + Qed. End Z. diff --git a/src/Util/ZUtil/Morphisms.v b/src/Util/ZUtil/Morphisms.v index 91f3dff3c..15a9fcf1a 100644 --- a/src/Util/ZUtil/Morphisms.v +++ b/src/Util/ZUtil/Morphisms.v @@ -6,6 +6,7 @@ Require Import Coq.Classes.Morphisms. Require Import Coq.Classes.RelationPairs. Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.LandLorBounds. Require Import Crypto.Util.ZUtil.Tactics.PeelLe. Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem. Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. @@ -279,4 +280,13 @@ Module Z. Lemma shiftl_Zneg_Zneg_le_Proper_r x : Proper (Basics.flip Pos.le ==> Z.le) (fun p => Z.shiftl (Zneg p) (Zneg x)). Proof. shift_Proper_t'. Qed. Hint Resolve shiftl_Zneg_Zneg_le_Proper_r : zarith. + + Hint Resolve Z.land_round_Proper_pos_r : zarith. + Hint Resolve Z.land_round_Proper_pos_l : zarith. + Hint Resolve Z.lor_round_Proper_pos_r : zarith. + Hint Resolve Z.lor_round_Proper_pos_l : zarith. + Hint Resolve Z.land_round_Proper_neg_r : zarith. + Hint Resolve Z.land_round_Proper_neg_l : zarith. + Hint Resolve Z.lor_round_Proper_neg_r : zarith. + Hint Resolve Z.lor_round_Proper_neg_l : zarith. End Z. diff --git a/src/Util/ZUtil/Mul.v b/src/Util/ZUtil/Mul.v new file mode 100644 index 000000000..6cf851e4e --- /dev/null +++ b/src/Util/ZUtil/Mul.v @@ -0,0 +1,8 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Local Open Scope Z_scope. + +Module Z. + Lemma mul_comm3 x y z : x * (y * z) = y * (x * z). + Proof. lia. Qed. +End Z. diff --git a/src/Util/ZUtil/N2Z.v b/src/Util/ZUtil/N2Z.v new file mode 100644 index 000000000..928f0b334 --- /dev/null +++ b/src/Util/ZUtil/N2Z.v @@ -0,0 +1,53 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.ZUtil.Hints.Core. +Local Open Scope Z_scope. + +Module N2Z. + Lemma inj_land n m : Z.of_N (N.land n m) = Z.land (Z.of_N n) (Z.of_N m). + Proof. destruct n, m; reflexivity. Qed. + Hint Rewrite inj_land : push_Zof_N. + Hint Rewrite <- inj_land : pull_Zof_N. + + Lemma inj_lor n m : Z.of_N (N.lor n m) = Z.lor (Z.of_N n) (Z.of_N m). + Proof. destruct n, m; reflexivity. Qed. + Hint Rewrite inj_lor : push_Zof_N. + Hint Rewrite <- inj_lor : pull_Zof_N. + + Lemma inj_shiftl: forall x y, Z.of_N (N.shiftl x y) = Z.shiftl (Z.of_N x) (Z.of_N y). + Proof. + intros x y. + apply Z.bits_inj_iff'; intros k Hpos. + rewrite Z2N.inj_testbit; [|assumption]. + rewrite Z.shiftl_spec; [|assumption]. + + assert ((Z.to_N k) >= y \/ (Z.to_N k) < y)%N as g by ( + unfold N.ge, N.lt; induction (N.compare (Z.to_N k) y); [left|auto|left]; + intro H; inversion H). + + destruct g as [g|g]; + [ rewrite N.shiftl_spec_high; [|apply N2Z.inj_le; rewrite Z2N.id|apply N.ge_le] + | rewrite N.shiftl_spec_low]; try assumption. + + - rewrite <- N2Z.inj_testbit; f_equal. + rewrite N2Z.inj_sub, Z2N.id; [reflexivity|assumption|apply N.ge_le; assumption]. + + - apply N2Z.inj_lt in g. + rewrite Z2N.id in g; [symmetry|assumption]. + apply Z.testbit_neg_r; omega. + Qed. + Hint Rewrite inj_shiftl : push_Zof_N. + Hint Rewrite <- inj_shiftl : pull_Zof_N. + + Lemma inj_shiftr: forall x y, Z.of_N (N.shiftr x y) = Z.shiftr (Z.of_N x) (Z.of_N y). + Proof. + intros. + apply Z.bits_inj_iff'; intros k Hpos. + rewrite Z2N.inj_testbit; [|assumption]. + rewrite Z.shiftr_spec, N.shiftr_spec; [|apply N2Z.inj_le; rewrite Z2N.id|]; try assumption. + rewrite <- N2Z.inj_testbit; f_equal. + rewrite N2Z.inj_add; f_equal. + apply Z2N.id; assumption. + Qed. + Hint Rewrite inj_shiftr : push_Zof_N. + Hint Rewrite <- inj_shiftr : pull_Zof_N. +End N2Z. diff --git a/src/Util/ZUtil/Odd.v b/src/Util/ZUtil/Odd.v new file mode 100644 index 000000000..37b8bd443 --- /dev/null +++ b/src/Util/ZUtil/Odd.v @@ -0,0 +1,32 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.ZArith.Znumtheory. +Require Import Coq.micromega.Lia. +Local Open Scope Z_scope. + +Module Z. + Lemma prime_odd_or_2 : forall p (prime_p : prime p), p = 2 \/ Z.odd p = true. + Proof. + intros p prime_p. + apply Decidable.imp_not_l; try apply Z.eq_decidable. + intros p_neq2. + pose proof (Zmod_odd p) as mod_odd. + destruct (Sumbool.sumbool_of_bool (Z.odd p)) as [? | p_not_odd]; auto. + rewrite p_not_odd in mod_odd. + apply Zmod_divides in mod_odd; try omega. + destruct mod_odd as [c c_id]. + rewrite Z.mul_comm in c_id. + apply Zdivide_intro in c_id. + apply prime_divisors in c_id; auto. + destruct c_id; [omega | destruct H; [omega | destruct H; auto] ]. + pose proof (prime_ge_2 p prime_p); omega. + Qed. + + Lemma odd_mod : forall a b, (b <> 0)%Z -> + Z.odd (a mod b) = if Z.odd b then xorb (Z.odd a) (Z.odd (a / b)) else Z.odd a. + Proof. + intros a b H. + rewrite Zmod_eq_full by assumption. + rewrite <-Z.add_opp_r, Z.odd_add, Z.odd_opp, Z.odd_mul. + case_eq (Z.odd b); intros; rewrite ?Bool.andb_true_r, ?Bool.andb_false_r; auto using Bool.xorb_false_r. + Qed. +End Z. diff --git a/src/Util/ZUtil/Ones.v b/src/Util/ZUtil/Ones.v new file mode 100644 index 000000000..e856f23a0 --- /dev/null +++ b/src/Util/ZUtil/Ones.v @@ -0,0 +1,177 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Pow2. +Require Import Crypto.Util.ZUtil.Log2. +Require Import Crypto.Util.ZUtil.Lnot. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Hints.ZArith. +Require Import Crypto.Util.ZUtil.ZSimplify.Simple. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.UniquePose. +Local Open Scope bool_scope. Local Open Scope Z_scope. + +Module Z. + Lemma ones_le x y : x <= y -> Z.ones x <= Z.ones y. + Proof. + rewrite !Z.ones_equiv; auto with zarith. + Qed. + Hint Resolve ones_le : zarith. + + Lemma ones_lt_pow2 x y : 0 <= x <= y -> Z.ones x < 2^y. + Proof. + rewrite Z.ones_equiv, Z.lt_pred_le. + auto with zarith. + Qed. + Hint Resolve ones_lt_pow2 : zarith. + + Lemma log2_ones_full x : Z.log2 (Z.ones x) = Z.max 0 (Z.pred x). + Proof. + rewrite Z.ones_equiv, Z.log2_pred_pow2_full; reflexivity. + Qed. + Hint Rewrite log2_ones_full : zsimplify. + + Lemma log2_ones_lt x y : 0 < x <= y -> Z.log2 (Z.ones x) < y. + Proof. + rewrite log2_ones_full; apply Z.max_case_strong; omega. + Qed. + Hint Resolve log2_ones_lt : zarith. + + Lemma log2_ones_le x y : 0 <= x <= y -> Z.log2 (Z.ones x) <= y. + Proof. + rewrite log2_ones_full; apply Z.max_case_strong; omega. + Qed. + Hint Resolve log2_ones_le : zarith. + + Lemma log2_ones_lt_nonneg x y : 0 < y -> x <= y -> Z.log2 (Z.ones x) < y. + Proof. + rewrite log2_ones_full; apply Z.max_case_strong; omega. + Qed. + Hint Resolve log2_ones_lt_nonneg : zarith. + + Lemma ones_pred : forall i, 0 < i -> Z.ones (Z.pred i) = Z.shiftr (Z.ones i) 1. + Proof. + induction i as [|p|p]; [ | | pose proof (Pos2Z.neg_is_neg p) ]; try omega. + intros. + unfold Z.ones. + rewrite !Z.shiftl_1_l, Z.shiftr_div_pow2, <-!Z.sub_1_r, Z.pow_1_r, <-!Z.add_opp_r by omega. + replace (2 ^ (Z.pos p)) with (2 ^ (Z.pos p - 1)* 2). + rewrite Z.div_add_l by omega. + reflexivity. + change 2 with (2 ^ 1) at 2. + rewrite <-Z.pow_add_r by (pose proof (Pos2Z.is_pos p); omega). + f_equal. omega. + Qed. + Hint Rewrite <- ones_pred using zutil_arith : push_Zshift. + + Lemma ones_succ : forall x, (0 <= x) -> + Z.ones (Z.succ x) = 2 ^ x + Z.ones x. + Proof. + unfold Z.ones; intros. + rewrite !Z.shiftl_1_l. + rewrite Z.add_pred_r. + apply Z.succ_inj. + rewrite !Z.succ_pred. + rewrite Z.pow_succ_r; omega. + Qed. + + Lemma ones_nonneg : forall i, (0 <= i) -> 0 <= Z.ones i. + Proof. + apply natlike_ind. + + unfold Z.ones. simpl; omega. + + intros. + rewrite Z.ones_succ by assumption. + Z.zero_bounds. + Qed. + Hint Resolve ones_nonneg : zarith. + + Lemma ones_pos_pos : forall i, (0 < i) -> 0 < Z.ones i. + Proof. + intros. + unfold Z.ones. + rewrite Z.shiftl_1_l. + apply Z.lt_succ_lt_pred. + apply Z.pow_gt_1; omega. + Qed. + Hint Resolve ones_pos_pos : zarith. + + Lemma lnot_ones_equiv n : Z.lnot (Z.ones n) = -2^n. + Proof. rewrite Z.ones_equiv, Z.lnot_equiv, <- ?Z.sub_1_r; lia. Qed. + + Lemma land_ones_ones n m + : Z.land (Z.ones n) (Z.ones m) + = Z.ones (if ((n <? 0) || (m <? 0)) + then Z.max n m + else Z.min n m). + Proof. + repeat first [ reflexivity + | break_innermost_match_step + | progress rewrite ?Bool.orb_true_iff in * + | progress rewrite ?Bool.orb_false_iff in * + | progress rewrite ?Z.ltb_lt, ?Z.ltb_ge in * + | progress destruct_head'_and + | apply Z.min_case_strong + | apply Z.max_case_strong + | progress intros + | progress destruct_head'_or + | rewrite !Z.pow_r_Zneg + | rewrite !Z.land_m1_l + | rewrite !Z.land_m1_r + | progress change (Z.pred 0) with (-1) + | rewrite Z.mod_small by lia + | match goal with + | [ H : ?x < 0 |- _ ] => is_var x; destruct x; try lia + | [ H : ?x <= Z.neg _ |- _ ] => is_var x; destruct x; try lia + | [ |- context[Z.ones (Z.neg ?x)] ] => rewrite (Z.ones_equiv (Z.neg x)) + | [ H : ?n <= ?m |- Z.land (Z.ones ?m) (Z.ones ?n) = _ ] + => rewrite (Z.land_comm (Z.ones m) (Z.ones n)) + | [ H : ?n <= ?m |- Z.land (Z.ones ?n) (Z.ones ?m) = _ ] + => progress rewrite ?Z.land_ones, ?Z.ones_equiv, <- ?Z.sub_1_r by auto + | [ H : ?n <= ?m |- _ ] + => is_var n; is_var m; unique pose proof (Z.pow_le_mono_r 2 n m ltac:(lia) H) + | [ |- context[2^?x] ] => unique pose proof (Z.pow2_gt_0 x ltac:(lia)) + end ]. + Qed. + Hint Rewrite land_ones_ones : zsimplify. + + Lemma lor_ones_ones n m + : Z.lor (Z.ones n) (Z.ones m) + = Z.ones (if ((n <? 0) || (m <? 0)) + then Z.min n m + else Z.max n m). + Proof. + destruct (Z_zerop n), (Z_zerop m); subst; + repeat first [ reflexivity + | break_innermost_match_step + | progress rewrite ?Bool.orb_true_iff in * + | progress rewrite ?Bool.orb_false_iff in * + | progress rewrite ?Z.ltb_lt, ?Z.ltb_ge in * + | progress destruct_head'_and + | apply Z.min_case_strong + | apply Z.max_case_strong + | progress intros + | progress destruct_head'_or + | rewrite !Z.pow_r_Zneg + | rewrite !Z.lor_m1_l + | rewrite !Z.lor_m1_r + | progress change (Z.pred 0) with (-1) + | rewrite Z.mod_small by lia + | lia + | match goal with + | [ H : ?x < 0 |- _ ] => is_var x; destruct x; try lia + | [ H : ?x <= Z.neg _ |- _ ] => is_var x; destruct x; try lia + | [ |- context[Z.ones (Z.neg ?x)] ] => rewrite (Z.ones_equiv (Z.neg x)) + | [ H : ?n <= ?m |- Z.lor (Z.ones ?m) (Z.ones ?n) = _ ] + => rewrite (Z.lor_comm (Z.ones m) (Z.ones n)) + | [ H : ?n <= ?m |- Z.lor (Z.ones ?n) (Z.ones ?m) = _ ] + => progress rewrite ?Z.lor_ones_low; try apply Z.log2_ones_lt_nonneg; rewrite ?Z.ones_equiv, <- ?Z.sub_1_r + | [ H : ?n <= ?m |- _ ] + => is_var n; is_var m; unique pose proof (Z.pow_le_mono_r 2 n m ltac:(lia) H) + | [ |- context[2^?x] ] => unique pose proof (Z.pow2_gt_0 x ltac:(lia)) + end ]. + Qed. + Hint Rewrite lor_ones_ones : zsimplify. +End Z. diff --git a/src/Util/ZUtil/Opp.v b/src/Util/ZUtil/Opp.v new file mode 100644 index 000000000..3cc18241b --- /dev/null +++ b/src/Util/ZUtil/Opp.v @@ -0,0 +1,11 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.ZSimplify.Core. +Local Open Scope Z_scope. + +Module Z. + Lemma opp_eq_0_iff a : -a = 0 <-> a = 0. + Proof. omega. Qed. + Hint Rewrite opp_eq_0_iff : zsimplify. +End Z. diff --git a/src/Util/ZUtil/Pow.v b/src/Util/ZUtil/Pow.v new file mode 100644 index 000000000..06ce2187b --- /dev/null +++ b/src/Util/ZUtil/Pow.v @@ -0,0 +1,44 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints.Core. +Local Open Scope Z_scope. + +Module Z. + Lemma base_pow_neg b n : n < 0 -> b^n = 0. + Proof. + destruct n; intro H; try reflexivity; compute in H; congruence. + Qed. + Hint Rewrite base_pow_neg using zutil_arith : zsimplify. + + Lemma nonneg_pow_pos a b : 0 < a -> 0 < a^b -> 0 <= b. + Proof. + destruct (Z_lt_le_dec b 0); intros; auto. + erewrite Z.pow_neg_r in * by eassumption. + omega. + Qed. + Hint Resolve nonneg_pow_pos (fun n => nonneg_pow_pos 2 n Z.lt_0_2) : zarith. + Lemma nonneg_pow_pos_helper a b dummy : 0 < a -> 0 <= dummy < a^b -> 0 <= b. + Proof. eauto with zarith omega. Qed. + Hint Resolve nonneg_pow_pos_helper (fun n dummy => nonneg_pow_pos_helper 2 n dummy Z.lt_0_2) : zarith. + + Lemma div_pow2succ : forall n x, (0 <= x) -> + n / 2 ^ Z.succ x = Z.div2 (n / 2 ^ x). + Proof. + intros. + rewrite Z.pow_succ_r, Z.mul_comm by auto. + rewrite <- Z.div_div by (try apply Z.pow_nonzero; omega). + rewrite Zdiv2_div. + reflexivity. + Qed. + + Definition pow_sub_r' + := fun a b c y H0 H1 => @Logic.eq_trans _ _ _ y (@Z.pow_sub_r a b c H0 H1). + Definition pow_sub_r'_sym + := fun a b c y p H0 H1 => Logic.eq_sym (@Logic.eq_trans _ y _ _ (Logic.eq_sym p) (@Z.pow_sub_r a b c H0 H1)). + Hint Resolve pow_sub_r' pow_sub_r'_sym Z.eq_le_incl : zarith. + Hint Resolve (fun b => f_equal (fun e => b ^ e)) (fun e => f_equal (fun b => b ^ e)) : zarith. + + Lemma two_p_two_eq_four : 2^(2) = 4. + Proof. reflexivity. Qed. + Hint Rewrite <- two_p_two_eq_four : push_Zpow. +End Z. diff --git a/src/Util/ZUtil/Pow2.v b/src/Util/ZUtil/Pow2.v new file mode 100644 index 000000000..bc3b01225 --- /dev/null +++ b/src/Util/ZUtil/Pow2.v @@ -0,0 +1,26 @@ +Require Import Coq.micromega.Lia. +Require Import Coq.ZArith.ZArith. +Local Open Scope Z_scope. + +Module Z. + Lemma pow2_ge_0: forall a, (0 <= 2 ^ a)%Z. + Proof. + intros; apply Z.pow_nonneg; omega. + Qed. + + Lemma pow2_gt_0: forall a, (0 <= a)%Z -> (0 < 2 ^ a)%Z. + Proof. + intros; apply Z.pow_pos_nonneg; [|assumption]; omega. + Qed. + + Lemma pow2_lt_or_divides : forall a b, 0 <= b -> + 2 ^ a < 2 ^ b \/ (2 ^ a) mod 2 ^ b = 0. + Proof. + intros a b H. + destruct (Z_lt_dec a b); [left|right]. + { apply Z.pow_lt_mono_r; auto; omega. } + { replace a with (a - b + b) by ring. + rewrite Z.pow_add_r by omega. + apply Z.mod_mul, Z.pow_nonzero; omega. } + Qed. +End Z. diff --git a/src/Util/ZUtil/Pow2Mod.v b/src/Util/ZUtil/Pow2Mod.v index 237ca19dc..74c22394a 100644 --- a/src/Util/ZUtil/Pow2Mod.v +++ b/src/Util/ZUtil/Pow2Mod.v @@ -3,6 +3,7 @@ Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.Notations. Require Import Crypto.Util.ZUtil.Hints.Core. Require Import Crypto.Util.ZUtil.Hints.Ztestbit. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. Require Import Crypto.Util.ZUtil.Testbit. Require Import Crypto.Util.Tactics.BreakMatch. Local Open Scope Z_scope. @@ -51,4 +52,14 @@ Module Z. auto with zarith. Qed. Hint Resolve pow2_mod_pos_bound : zarith. + + Lemma pow2_mod_id_iff : forall a n, 0 <= n -> + (Z.pow2_mod a n = a <-> 0 <= a < 2 ^ n). + Proof. + intros a n H. + rewrite Z.pow2_mod_spec by assumption. + assert (0 < 2 ^ n) by Z.zero_bounds. + rewrite Z.mod_small_iff by omega. + split; intros; intuition omega. + Qed. End Z. diff --git a/src/Util/ZUtil/Shift.v b/src/Util/ZUtil/Shift.v new file mode 100644 index 000000000..b5fb79c13 --- /dev/null +++ b/src/Util/ZUtil/Shift.v @@ -0,0 +1,393 @@ +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Ones. +Require Import Crypto.Util.ZUtil.Definitions. +Require Import Crypto.Util.ZUtil.Testbit. +Require Import Crypto.Util.ZUtil.Pow2Mod. +Require Import Crypto.Util.ZUtil.Le. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Tactics.SpecializeBy. +Local Open Scope Z_scope. + +Module Z. + Lemma shiftr_add_shiftl_high : forall n m a b, 0 <= n <= m -> 0 <= a < 2 ^ n -> + Z.shiftr (a + (Z.shiftl b n)) m = Z.shiftr b (m - n). + Proof. + intros n m a b H H0. + rewrite !Z.shiftr_div_pow2, Z.shiftl_mul_pow2 by omega. + replace (2 ^ m) with (2 ^ n * 2 ^ (m - n)) by + (rewrite <-Z.pow_add_r by omega; f_equal; ring). + rewrite <-Z.div_div, Z.div_add, (Z.div_small a) ; try solve + [assumption || apply Z.pow_nonzero || apply Z.pow_pos_nonneg; omega]. + f_equal; ring. + Qed. + Hint Rewrite Z.shiftr_add_shiftl_high using zutil_arith : pull_Zshift. + Hint Rewrite <- Z.shiftr_add_shiftl_high using zutil_arith : push_Zshift. + + Lemma shiftr_add_shiftl_low : forall n m a b, 0 <= m <= n -> 0 <= a < 2 ^ n -> + Z.shiftr (a + (Z.shiftl b n)) m = Z.shiftr a m + Z.shiftr b (m - n). + Proof. + intros n m a b H H0. + rewrite !Z.shiftr_div_pow2, Z.shiftl_mul_pow2, Z.shiftr_mul_pow2 by omega. + replace (2 ^ n) with (2 ^ (n - m) * 2 ^ m) by + (rewrite <-Z.pow_add_r by omega; f_equal; ring). + rewrite Z.mul_assoc, Z.div_add by (apply Z.pow_nonzero; omega). + repeat f_equal; ring. + Qed. + Hint Rewrite Z.shiftr_add_shiftl_low using zutil_arith : pull_Zshift. + Hint Rewrite <- Z.shiftr_add_shiftl_low using zutil_arith : push_Zshift. + + Lemma testbit_add_shiftl_high : forall i, (0 <= i) -> forall a b n, (0 <= n <= i) -> + 0 <= a < 2 ^ n -> + Z.testbit (a + Z.shiftl b n) i = Z.testbit b (i - n). + Proof. + intros i ?. + apply natlike_ind with (x := i); [ intros a b n | intros x H0 H1 a b n | ]; intros; try assumption; + (destruct (Z.eq_dec 0 n); [ subst; rewrite Z.pow_0_r in *; + replace a with 0 by omega; f_equal; ring | ]); try omega. + rewrite <-Z.add_1_r at 1. rewrite <-Z.shiftr_spec by assumption. + replace (Z.succ x - n) with (x - (n - 1)) by ring. + rewrite shiftr_add_shiftl_low, <-Z.shiftl_opp_r with (a := b) by omega. + rewrite <-H1 with (a := Z.shiftr a 1); try omega; [ repeat f_equal; ring | ]. + rewrite Z.shiftr_div_pow2 by omega. + split; apply Z.div_pos || apply Z.div_lt_upper_bound; + try solve [rewrite ?Z.pow_1_r; omega]. + rewrite <-Z.pow_add_r by omega. + replace (1 + (n - 1)) with n by ring; omega. + Qed. + Hint Rewrite testbit_add_shiftl_high using zutil_arith : Ztestbit. + + Lemma shiftr_succ : forall n x, + Z.shiftr n (Z.succ x) = Z.shiftr (Z.shiftr n x) 1. + Proof. + intros. + rewrite Z.shiftr_shiftr by omega. + reflexivity. + Qed. + Hint Rewrite Z.shiftr_succ using zutil_arith : push_Zshift. + Hint Rewrite <- Z.shiftr_succ using zutil_arith : pull_Zshift. + + Lemma shiftr_1_r_le : forall a b, a <= b -> + Z.shiftr a 1 <= Z.shiftr b 1. + Proof. + intros. + rewrite !Z.shiftr_div_pow2, Z.pow_1_r by omega. + apply Z.div_le_mono; omega. + Qed. + Hint Resolve shiftr_1_r_le : zarith. + + Lemma shiftr_le : forall a b i : Z, 0 <= i -> a <= b -> a >> i <= b >> i. + Proof. + intros a b i ?; revert a b. apply natlike_ind with (x := i); intros; auto. + rewrite !shiftr_succ, shiftr_1_r_le; eauto. reflexivity. + Qed. + Hint Resolve shiftr_le : zarith. + + Lemma shiftr_ones' : forall a n, 0 <= a < 2 ^ n -> forall i, (0 <= i) -> + Z.shiftr a i <= Z.ones (n - i) \/ n <= i. + Proof. + intros a n H. + apply natlike_ind. + + unfold Z.ones. + rewrite Z.shiftr_0_r, Z.shiftl_1_l, Z.sub_0_r. + omega. + + intros x H0 H1. + destruct (Z_lt_le_dec x n); try omega. + intuition auto with zarith lia. + left. + rewrite shiftr_succ. + replace (n - Z.succ x) with (Z.pred (n - x)) by omega. + rewrite Z.ones_pred by omega. + apply Z.shiftr_1_r_le. + assumption. + Qed. + + Lemma shiftr_ones : forall a n i, 0 <= a < 2 ^ n -> (0 <= i) -> (i <= n) -> + Z.shiftr a i <= Z.ones (n - i) . + Proof. + intros a n i G G0 G1. + destruct (Z_le_lt_eq_dec i n G1). + + destruct (Z.shiftr_ones' a n G i G0); omega. + + subst; rewrite Z.sub_diag. + destruct (Z.eq_dec a 0). + - subst; rewrite Z.shiftr_0_l; reflexivity. + - rewrite Z.shiftr_eq_0; try omega; try reflexivity. + apply Z.log2_lt_pow2; omega. + Qed. + Hint Resolve shiftr_ones : zarith. + + Lemma shiftr_upper_bound : forall a n, 0 <= n -> 0 <= a <= 2 ^ n -> Z.shiftr a n <= 1. + Proof. + intros a ? ? [a_nonneg a_upper_bound]. + apply Z_le_lt_eq_dec in a_upper_bound. + destruct a_upper_bound. + + destruct (Z.eq_dec 0 a). + - subst; rewrite Z.shiftr_0_l; omega. + - rewrite Z.shiftr_eq_0; auto; try omega. + apply Z.log2_lt_pow2; auto; omega. + + subst. + rewrite Z.shiftr_div_pow2 by assumption. + rewrite Z.div_same; try omega. + assert (0 < 2 ^ n) by (apply Z.pow_pos_nonneg; omega). + omega. + Qed. + Hint Resolve shiftr_upper_bound : zarith. + + Lemma lor_shiftl : forall a b n, 0 <= n -> 0 <= a < 2 ^ n -> + Z.lor a (Z.shiftl b n) = a + (Z.shiftl b n). + Proof. + intros a b n H H0. + apply Z.bits_inj'; intros t ?. + rewrite Z.lor_spec, Z.shiftl_spec by assumption. + destruct (Z_lt_dec t n). + + rewrite Z.testbit_add_shiftl_low by omega. + rewrite Z.testbit_neg_r with (n := t - n) by omega. + apply Bool.orb_false_r. + + rewrite testbit_add_shiftl_high by omega. + replace (Z.testbit a t) with false; [ apply Bool.orb_false_l | ]. + symmetry. + apply Z.testbit_false; try omega. + rewrite Z.div_small; try reflexivity. + split; try eapply Z.lt_le_trans with (m := 2 ^ n); try omega. + apply Z.pow_le_mono_r; omega. + Qed. + Hint Rewrite <- Z.lor_shiftl using zutil_arith : convert_to_Ztestbit. + + Lemma lor_shiftl' : forall a b n, 0 <= n -> 0 <= a < 2 ^ n -> + Z.lor (Z.shiftl b n) a = (Z.shiftl b n) + a. + Proof. + intros; rewrite Z.lor_comm, Z.add_comm; apply lor_shiftl; assumption. + Qed. + Hint Rewrite <- Z.lor_shiftl' using zutil_arith : convert_to_Ztestbit. + + Lemma shiftl_spec_full a n m + : Z.testbit (a << n) m = if Z_lt_dec m n + then false + else if Z_le_dec 0 m + then Z.testbit a (m - n) + else false. + Proof. + repeat break_match; auto using Z.shiftl_spec_low, Z.shiftl_spec, Z.testbit_neg_r with omega. + Qed. + Hint Rewrite shiftl_spec_full : Ztestbit_full. + + Lemma shiftr_spec_full a n m + : Z.testbit (a >> n) m = if Z_lt_dec m (-n) + then false + else if Z_le_dec 0 m + then Z.testbit a (m + n) + else false. + Proof. + rewrite <- Z.shiftl_opp_r, shiftl_spec_full, Z.sub_opp_r; reflexivity. + Qed. + Hint Rewrite shiftr_spec_full : Ztestbit_full. + + Lemma testbit_add_shiftl_full i (Hi : 0 <= i) a b n (Ha : 0 <= a < 2^n) + : Z.testbit (a + b << n) i + = if (i <? n) then Z.testbit a i else Z.testbit b (i - n). + Proof. + assert (0 < 2^n) by omega. + assert (0 <= n) by eauto 2 with zarith. + pose proof (Zlt_cases i n); break_match; autorewrite with Ztestbit; reflexivity. + Qed. + Hint Rewrite testbit_add_shiftl_full using zutil_arith : Ztestbit. + + Lemma land_add_land : forall n m a b, (m <= n)%nat -> + Z.land ((Z.land a (Z.ones (Z.of_nat n))) + (Z.shiftl b (Z.of_nat n))) (Z.ones (Z.of_nat m)) = Z.land a (Z.ones (Z.of_nat m)). + Proof. + intros n m a b H. + rewrite !Z.land_ones by apply Nat2Z.is_nonneg. + rewrite Z.shiftl_mul_pow2 by apply Nat2Z.is_nonneg. + replace (b * 2 ^ Z.of_nat n) with + ((b * 2 ^ Z.of_nat (n - m)) * 2 ^ Z.of_nat m) by + (rewrite (le_plus_minus m n) at 2; try assumption; + rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg; ring). + rewrite Z.mod_add by (pose proof (Z.pow_pos_nonneg 2 (Z.of_nat m)); omega). + symmetry. apply Znumtheory.Zmod_div_mod; try (apply Z.pow_pos_nonneg; omega). + rewrite (le_plus_minus m n) by assumption. + rewrite Nat2Z.inj_add, Z.pow_add_r by apply Nat2Z.is_nonneg. + apply Z.divide_factor_l. + Qed. + + Lemma shiftl_add x y z : 0 <= z -> (x + y) << z = (x << z) + (y << z). + Proof. intros; autorewrite with Zshift_to_pow; lia. Qed. + Hint Rewrite shiftl_add using zutil_arith : push_Zshift. + Hint Rewrite <- shiftl_add using zutil_arith : pull_Zshift. + + Lemma shiftr_add x y z : z <= 0 -> (x + y) >> z = (x >> z) + (y >> z). + Proof. intros; autorewrite with Zshift_to_pow; lia. Qed. + Hint Rewrite shiftr_add using zutil_arith : push_Zshift. + Hint Rewrite <- shiftr_add using zutil_arith : pull_Zshift. + + Lemma shiftl_sub x y z : 0 <= z -> (x - y) << z = (x << z) - (y << z). + Proof. intros; autorewrite with Zshift_to_pow; lia. Qed. + Hint Rewrite shiftl_sub using zutil_arith : push_Zshift. + Hint Rewrite <- shiftl_sub using zutil_arith : pull_Zshift. + + Lemma shiftr_sub x y z : z <= 0 -> (x - y) >> z = (x >> z) - (y >> z). + Proof. intros; autorewrite with Zshift_to_pow; lia. Qed. + Hint Rewrite shiftr_sub using zutil_arith : push_Zshift. + Hint Rewrite <- shiftr_sub using zutil_arith : pull_Zshift. + + Lemma compare_add_shiftl : forall x1 y1 x2 y2 n, 0 <= n -> + Z.pow2_mod x1 n = x1 -> Z.pow2_mod x2 n = x2 -> + x1 + (y1 << n) ?= x2 + (y2 << n) = + if Z.eq_dec y1 y2 + then x1 ?= x2 + else y1 ?= y2. + Proof. + repeat match goal with + | |- _ => progress intros + | |- _ => progress subst y1 + | |- _ => rewrite Z.shiftl_mul_pow2 by omega + | |- _ => rewrite Z.add_compare_mono_r + | |- _ => rewrite <-Z.mul_sub_distr_r + | |- _ => break_innermost_match_step + | H : Z.pow2_mod _ _ = _ |- _ => rewrite Z.pow2_mod_id_iff in H by omega + | H : ?a <> ?b |- _ = (?a ?= ?b) => + case_eq (a ?= b); rewrite ?Z.compare_eq_iff, ?Z.compare_gt_iff, ?Z.compare_lt_iff + | |- _ + (_ * _) > _ + (_ * _) => cbv [Z.gt] + | |- _ + (_ * ?x) < _ + (_ * ?x) => + apply Z.lt_sub_lt_add; apply Z.lt_le_trans with (m := 1 * x); [omega|] + | |- _ => apply Z.mul_le_mono_nonneg_r; omega + | |- _ => reflexivity + | |- _ => congruence + end. + Qed. + + Lemma shiftl_opp_l a n + : Z.shiftl (-a) n = - Z.shiftl a n - (if Z_zerop (a mod 2 ^ (- n)) then 0 else 1). + Proof. + destruct (Z_dec 0 n) as [ [?|?] | ? ]; + subst; + rewrite ?Z.pow_neg_r by omega; + autorewrite with zsimplify_const; + [ | | simpl; omega ]. + { rewrite !Z.shiftl_mul_pow2 by omega. + nia. } + { rewrite !Z.shiftl_div_pow2 by omega. + rewrite Z.div_opp_l_complete by auto with zarith. + reflexivity. } + Qed. + Hint Rewrite shiftl_opp_l : push_Zshift. + Hint Rewrite <- shiftl_opp_l : pull_Zshift. + + Lemma shiftr_opp_l a n + : Z.shiftr (-a) n = - Z.shiftr a n - (if Z_zerop (a mod 2 ^ n) then 0 else 1). + Proof. + unfold Z.shiftr; rewrite shiftl_opp_l at 1; rewrite Z.opp_involutive. + reflexivity. + Qed. + Hint Rewrite shiftr_opp_l : push_Zshift. + Hint Rewrite <- shiftr_opp_l : pull_Zshift. + + Lemma shl_shr_lt x y n m (Hx : 0 <= x < 2^n) (Hy : 0 <= y < 2^n) (Hm : 0 <= m <= n) + : 0 <= (x >> (n - m)) + ((y << m) mod 2^n) < 2^n. + Proof. + cut (0 <= (x >> (n - m)) + ((y << m) mod 2^n) <= 2^n - 1); [ omega | ]. + assert (0 <= x <= 2^n - 1) by omega. + assert (0 <= y <= 2^n - 1) by omega. + assert (0 < 2 ^ (n - m)) by auto with zarith. + assert (0 <= y mod 2 ^ (n - m) < 2^(n-m)) by auto with zarith. + assert (0 <= y mod 2 ^ (n - m) <= 2 ^ (n - m) - 1) by omega. + assert (0 <= (y mod 2 ^ (n - m)) * 2^m <= (2^(n-m) - 1)*2^m) by auto with zarith. + assert (0 <= x / 2^(n-m) < 2^n / 2^(n-m)). + { split; Z.zero_bounds. + apply Z.div_lt_upper_bound; autorewrite with pull_Zpow zsimplify; nia. } + autorewrite with Zshift_to_pow. + split; Z.zero_bounds. + replace (2^n) with (2^(n-m) * 2^m) by (autorewrite with pull_Zpow; f_equal; omega). + rewrite Zmult_mod_distr_r. + autorewrite with pull_Zpow zsimplify push_Zmul in * |- . + nia. + Qed. + + Lemma add_shift_mod x y n m + (Hx : 0 <= x < 2^n) (Hy : 0 <= y) + (Hn : 0 <= n) (Hm : 0 < m) + : (x + y << n) mod (m * 2^n) = x + (y mod m) << n. + Proof. + pose proof (Z.mod_bound_pos y m). + specialize_by omega. + assert (0 < 2^n) by auto with zarith. + autorewrite with Zshift_to_pow. + rewrite Zplus_mod, !Zmult_mod_distr_r. + rewrite Zplus_mod, !Zmod_mod, <- Zplus_mod. + rewrite !(Zmod_eq (_ + _)) by nia. + etransitivity; [ | apply Z.add_0_r ]. + rewrite <- !Z.add_opp_r, <- !Z.add_assoc. + repeat apply f_equal. + ring_simplify. + cut (((x + y mod m * 2 ^ n) / (m * 2 ^ n)) = 0); [ nia | ]. + apply Z.div_small; split; nia. + Qed. + + Lemma add_mul_mod x y n m + (Hx : 0 <= x < 2^n) (Hy : 0 <= y) + (Hn : 0 <= n) (Hm : 0 < m) + : (x + y * 2^n) mod (m * 2^n) = x + (y mod m) * 2^n. + Proof. + generalize (add_shift_mod x y n m). + autorewrite with Zshift_to_pow; auto. + Qed. + + Lemma lt_pow_2_shiftr : forall a n, 0 <= a < 2 ^ n -> a >> n = 0. + Proof. + intros a n H. + destruct (Z_le_dec 0 n). + + rewrite Z.shiftr_div_pow2 by assumption. + auto using Z.div_small. + + assert (2 ^ n = 0) by (apply Z.pow_neg_r; omega). + omega. + Qed. + + Hint Rewrite Z.pow2_bits_eqb using zutil_arith : Ztestbit. + Lemma pow_2_shiftr : forall n, 0 <= n -> (2 ^ n) >> n = 1. + Proof. + intros; apply Z.bits_inj'; intros. + replace 1 with (2 ^ 0) by ring. + repeat match goal with + | |- _ => progress intros + | |- _ => progress rewrite ?Z.eqb_eq, ?Z.eqb_neq in * + | |- _ => progress autorewrite with Ztestbit + | |- context[Z.eqb ?a ?b] => case_eq (Z.eqb a b) + | |- _ => reflexivity || omega + end. + Qed. + + Lemma lt_mul_2_pow_2_shiftr : forall a n, 0 <= a < 2 * 2 ^ n -> + a >> n = if Z_lt_dec a (2 ^ n) then 0 else 1. + Proof. + intros a n H; break_match; [ apply lt_pow_2_shiftr; omega | ]. + destruct (Z_le_dec 0 n). + + replace (2 * 2 ^ n) with (2 ^ (n + 1)) in * + by (rewrite Z.pow_add_r; try omega; ring). + pose proof (Z.shiftr_ones a (n + 1) n H). + pose proof (Z.shiftr_le (2 ^ n) a n). + specialize_by omega. + replace (n + 1 - n) with 1 in * by ring. + replace (Z.ones 1) with 1 in * by reflexivity. + rewrite pow_2_shiftr in * by omega. + omega. + + assert (2 ^ n = 0) by (apply Z.pow_neg_r; omega). + omega. + Qed. + + Lemma shiftr_nonneg_le : forall a n, 0 <= a -> 0 <= n -> a >> n <= a. + Proof. + intros. + repeat match goal with + | [ H : _ <= _ |- _ ] + => rewrite Z.lt_eq_cases in H + | [ H : _ \/ _ |- _ ] => destruct H + | _ => progress subst + | _ => progress autorewrite with zsimplify Zshift_to_pow + | _ => solve [ auto with zarith omega ] + end. + Qed. + Hint Resolve shiftr_nonneg_le : zarith. +End Z. diff --git a/src/Util/ZUtil/Stabilization.v b/src/Util/ZUtil/Stabilization.v index 4df0300da..7e89ea1b4 100644 --- a/src/Util/ZUtil/Stabilization.v +++ b/src/Util/ZUtil/Stabilization.v @@ -1,7 +1,10 @@ Require Import Coq.ZArith.ZArith. Require Import Coq.micromega.Lia. Require Import Coq.Classes.Morphisms. -Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.Hints.Core. +Require Import Crypto.Util.ZUtil.Hints.ZArith. +Require Import Crypto.Util.ZUtil.Tactics.ReplaceNegWithPos. +Require Import Crypto.Util.ZUtil.Testbit. Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.Tactics.SpecializeBy. diff --git a/src/Util/ZUtil/Tactics/PullPush/Modulo.v b/src/Util/ZUtil/Tactics/PullPush/Modulo.v index 55889cbf0..fe0c3224c 100644 --- a/src/Util/ZUtil/Tactics/PullPush/Modulo.v +++ b/src/Util/ZUtil/Tactics/PullPush/Modulo.v @@ -3,89 +3,92 @@ Require Import Crypto.Util.ZUtil.Hints.Core. Require Import Crypto.Util.ZUtil.Modulo.PullPush. Local Open Scope Z_scope. -Ltac push_Zmod := - repeat match goal with - | _ => progress autorewrite with push_Zmod - | [ |- context[(?x * ?y) mod ?z] ] - => first [ rewrite (Z.mul_mod_push x y z) by Z.NoZMod - | rewrite (Z.mul_mod_l_push x y z) by Z.NoZMod - | rewrite (Z.mul_mod_r_push x y z) by Z.NoZMod ] - | [ |- context[(?x + ?y) mod ?z] ] - => first [ rewrite (Z.add_mod_push x y z) by Z.NoZMod - | rewrite (Z.add_mod_l_push x y z) by Z.NoZMod - | rewrite (Z.add_mod_r_push x y z) by Z.NoZMod ] - | [ |- context[(?x - ?y) mod ?z] ] - => first [ rewrite (Z.sub_mod_push x y z) by Z.NoZMod - | rewrite (Z.sub_mod_l_push x y z) by Z.NoZMod - | rewrite (Z.sub_mod_r_push x y z) by Z.NoZMod ] - | [ |- context[(-?y) mod ?z] ] - => rewrite (Z.opp_mod_mod_push y z) by Z.NoZMod - | [ |- context[(?p^?q) mod ?z] ] - => rewrite (Z.pow_mod_push p q z) by Z.NoZMod - end. +Ltac push_Zmod_step := + match goal with + | _ => progress autorewrite with push_Zmod + | [ |- context[(?x * ?y) mod ?z] ] + => first [ rewrite (Z.mul_mod_push x y z) by Z.NoZMod + | rewrite (Z.mul_mod_l_push x y z) by Z.NoZMod + | rewrite (Z.mul_mod_r_push x y z) by Z.NoZMod ] + | [ |- context[(?x + ?y) mod ?z] ] + => first [ rewrite (Z.add_mod_push x y z) by Z.NoZMod + | rewrite (Z.add_mod_l_push x y z) by Z.NoZMod + | rewrite (Z.add_mod_r_push x y z) by Z.NoZMod ] + | [ |- context[(?x - ?y) mod ?z] ] + => first [ rewrite (Z.sub_mod_push x y z) by Z.NoZMod + | rewrite (Z.sub_mod_l_push x y z) by Z.NoZMod + | rewrite (Z.sub_mod_r_push x y z) by Z.NoZMod ] + | [ |- context[(-?y) mod ?z] ] + => rewrite (Z.opp_mod_mod_push y z) by Z.NoZMod + | [ |- context[(?p^?q) mod ?z] ] + => rewrite (Z.pow_mod_push p q z) by Z.NoZMod + end. +Ltac push_Zmod := repeat push_Zmod_step. -Ltac push_Zmod_hyps := - repeat match goal with - | _ => progress autorewrite with push_Zmod in * |- - | [ H : context[(?x * ?y) mod ?z] |- _ ] - => first [ rewrite (Z.mul_mod_push x y z) in H by Z.NoZMod - | rewrite (Z.mul_mod_l_push x y z) in H by Z.NoZMod - | rewrite (Z.mul_mod_r_push x y z) in H by Z.NoZMod ] - | [ H : context[(?x + ?y) mod ?z] |- _ ] - => first [ rewrite (Z.add_mod_push x y z) in H by Z.NoZMod - | rewrite (Z.add_mod_l_push x y z) in H by Z.NoZMod - | rewrite (Z.add_mod_r_push x y z) in H by Z.NoZMod ] - | [ H : context[(?x - ?y) mod ?z] |- _ ] - => first [ rewrite (Z.sub_mod_push x y z) in H by Z.NoZMod - | rewrite (Z.sub_mod_l_push x y z) in H by Z.NoZMod - | rewrite (Z.sub_mod_r_push x y z) in H by Z.NoZMod ] - | [ H : context[(-?y) mod ?z] |- _ ] - => rewrite (Z.opp_mod_mod_push y z) in H by Z.NoZMod - | [ H : context[(?p^?q) mod ?z] |- _ ] - => rewrite (Z.pow_mod_push p q z) in H by Z.NoZMod - end. +Ltac push_Zmod_hyps_step := + match goal with + | _ => progress autorewrite with push_Zmod in * |- + | [ H : context[(?x * ?y) mod ?z] |- _ ] + => first [ rewrite (Z.mul_mod_push x y z) in H by Z.NoZMod + | rewrite (Z.mul_mod_l_push x y z) in H by Z.NoZMod + | rewrite (Z.mul_mod_r_push x y z) in H by Z.NoZMod ] + | [ H : context[(?x + ?y) mod ?z] |- _ ] + => first [ rewrite (Z.add_mod_push x y z) in H by Z.NoZMod + | rewrite (Z.add_mod_l_push x y z) in H by Z.NoZMod + | rewrite (Z.add_mod_r_push x y z) in H by Z.NoZMod ] + | [ H : context[(?x - ?y) mod ?z] |- _ ] + => first [ rewrite (Z.sub_mod_push x y z) in H by Z.NoZMod + | rewrite (Z.sub_mod_l_push x y z) in H by Z.NoZMod + | rewrite (Z.sub_mod_r_push x y z) in H by Z.NoZMod ] + | [ H : context[(-?y) mod ?z] |- _ ] + => rewrite (Z.opp_mod_mod_push y z) in H by Z.NoZMod + | [ H : context[(?p^?q) mod ?z] |- _ ] + => rewrite (Z.pow_mod_push p q z) in H by Z.NoZMod + end. +Ltac push_Zmod_hyps := repeat push_Zmod_hyps_step. Ltac has_no_mod x z := lazymatch x with | context[_ mod z] => fail | _ => idtac end. -Ltac pull_Zmod := - repeat match goal with - | [ |- context[((?x mod ?z) * (?y mod ?z)) mod ?z] ] - => has_no_mod x z; has_no_mod y z; - rewrite <- (Z.mul_mod_full x y z) - | [ |- context[((?x mod ?z) * ?y) mod ?z] ] - => has_no_mod x z; has_no_mod y z; - rewrite <- (Z.mul_mod_l x y z) - | [ |- context[(?x * (?y mod ?z)) mod ?z] ] - => has_no_mod x z; has_no_mod y z; - rewrite <- (Z.mul_mod_r x y z) - | [ |- context[((?x mod ?z) + (?y mod ?z)) mod ?z] ] - => has_no_mod x z; has_no_mod y z; - rewrite <- (Z.add_mod_full x y z) - | [ |- context[((?x mod ?z) + ?y) mod ?z] ] - => has_no_mod x z; has_no_mod y z; - rewrite <- (Z.add_mod_l x y z) - | [ |- context[(?x + (?y mod ?z)) mod ?z] ] - => has_no_mod x z; has_no_mod y z; - rewrite <- (Z.add_mod_r x y z) - | [ |- context[((?x mod ?z) - (?y mod ?z)) mod ?z] ] - => has_no_mod x z; has_no_mod y z; - rewrite <- (Z.sub_mod_full x y z) - | [ |- context[((?x mod ?z) - ?y) mod ?z] ] - => has_no_mod x z; has_no_mod y z; - rewrite <- (Z.sub_mod_l x y z) - | [ |- context[(?x - (?y mod ?z)) mod ?z] ] - => has_no_mod x z; has_no_mod y z; - rewrite <- (Z.sub_mod_r x y z) - | [ |- context[(((-?y) mod ?z)) mod ?z] ] - => has_no_mod y z; - rewrite <- (Z.opp_mod_mod y z) - | [ |- context[((?x mod ?z)^?y) mod ?z] ] - => has_no_mod x z; - rewrite <- (Z.pow_mod_full x y z) - | [ |- context[(?x mod ?z) mod ?z] ] - => rewrite (Zmod_mod x z) - | _ => progress autorewrite with pull_Zmod - end. +Ltac pull_Zmod_step := + match goal with + | [ |- context[((?x mod ?z) * (?y mod ?z)) mod ?z] ] + => has_no_mod x z; has_no_mod y z; + rewrite <- (Z.mul_mod_full x y z) + | [ |- context[((?x mod ?z) * ?y) mod ?z] ] + => has_no_mod x z; has_no_mod y z; + rewrite <- (Z.mul_mod_l x y z) + | [ |- context[(?x * (?y mod ?z)) mod ?z] ] + => has_no_mod x z; has_no_mod y z; + rewrite <- (Z.mul_mod_r x y z) + | [ |- context[((?x mod ?z) + (?y mod ?z)) mod ?z] ] + => has_no_mod x z; has_no_mod y z; + rewrite <- (Z.add_mod_full x y z) + | [ |- context[((?x mod ?z) + ?y) mod ?z] ] + => has_no_mod x z; has_no_mod y z; + rewrite <- (Z.add_mod_l x y z) + | [ |- context[(?x + (?y mod ?z)) mod ?z] ] + => has_no_mod x z; has_no_mod y z; + rewrite <- (Z.add_mod_r x y z) + | [ |- context[((?x mod ?z) - (?y mod ?z)) mod ?z] ] + => has_no_mod x z; has_no_mod y z; + rewrite <- (Z.sub_mod_full x y z) + | [ |- context[((?x mod ?z) - ?y) mod ?z] ] + => has_no_mod x z; has_no_mod y z; + rewrite <- (Z.sub_mod_l x y z) + | [ |- context[(?x - (?y mod ?z)) mod ?z] ] + => has_no_mod x z; has_no_mod y z; + rewrite <- (Z.sub_mod_r x y z) + | [ |- context[(-(?y mod ?z)) mod ?z] ] + => has_no_mod y z; + rewrite <- (Z.opp_mod_mod y z) + | [ |- context[((?x mod ?z)^?y) mod ?z] ] + => has_no_mod x z; + rewrite <- (Z.pow_mod_full x y z) + | [ |- context[(?x mod ?z) mod ?z] ] + => rewrite (Zmod_mod x z) + | _ => progress autorewrite with pull_Zmod + end. +Ltac pull_Zmod := repeat pull_Zmod_step. diff --git a/src/Util/ZUtil/Testbit.v b/src/Util/ZUtil/Testbit.v index 175d07b02..f8ef5465a 100644 --- a/src/Util/ZUtil/Testbit.v +++ b/src/Util/ZUtil/Testbit.v @@ -1,7 +1,12 @@ +Require Import Coq.micromega.Lia. Require Import Coq.ZArith.ZArith. Require Import Crypto.Util.ZUtil.Definitions. Require Import Crypto.Util.ZUtil.Hints. Require Import Crypto.Util.ZUtil.Notations. +Require Import Crypto.Util.ZUtil.Lnot. +Require Import Crypto.Util.ZUtil.Div. +Require Import Crypto.Util.ZUtil.Tactics.ZeroBounds. +Require Import Crypto.Util.ZUtil.Tactics.LtbToLt. Require Import Crypto.Util.Tactics.BreakMatch. Local Open Scope Z_scope. @@ -87,4 +92,39 @@ Module Z. auto using Z.mod_pow2_bits_low. Qed. Hint Rewrite testbit_add_shiftl_low using zutil_arith : Ztestbit. + + Lemma testbit_sub_pow2 n i x (i_range:0 <= i < n) (x_range:0 < x < 2 ^ n) : + Z.testbit (2 ^ n - x) i = negb (Z.testbit (x - 1) i). + Proof. + rewrite <-Z.lnot_spec, Z.lnot_sub1 by omega. + rewrite <-(Z.mod_pow2_bits_low (-x) _ _ (proj2 i_range)). + f_equal. + rewrite Z.mod_opp_l_nz; autorewrite with zsimplify; omega. + Qed. + + Lemma testbit_false_bound : forall a x, 0 <= x -> + (forall n, ~ (n < x) -> Z.testbit a n = false) -> + a < 2 ^ x. + Proof. + intros a x H H0. + assert (H1 : a = Z.pow2_mod a x). { + apply Z.bits_inj'; intros. + rewrite Z.testbit_pow2_mod by omega; break_match; auto. + } + rewrite H1. + cbv [Z.pow2_mod]; rewrite Z.land_ones by auto. + try apply Z.mod_pos_bound; Z.zero_bounds. + Qed. + + Lemma testbit_neg_eq_if x n : + 0 <= n -> + - (2 ^ n) <= x < 2 ^ n -> + Z.b2z (if x <? 0 then true else Z.testbit x n) = - (x / 2 ^ n) mod 2. + Proof. + intros. break_match; Z.ltb_to_lt. + { autorewrite with zsimplify. reflexivity. } + { autorewrite with zsimplify. + rewrite Z.bits_above_pow2 by omega. + reflexivity. } + Qed. End Z. diff --git a/src/Util/ZUtil/Z2Nat.v b/src/Util/ZUtil/Z2Nat.v index d6dd49a41..75d27dcaf 100644 --- a/src/Util/ZUtil/Z2Nat.v +++ b/src/Util/ZUtil/Z2Nat.v @@ -7,3 +7,41 @@ Module Z2Nat. destruct n; try reflexivity; lia. Qed. End Z2Nat. + +Module Z. + Lemma pos_pow_nat_pos : forall x n, + Z.pos x ^ Z.of_nat n > 0. + Proof. intros; apply Z.lt_gt, Z.pow_pos_nonneg; lia. Qed. + + Lemma pow_Z2N_Zpow : forall a n, 0 <= a -> + ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat. + Proof. + intros a n H; induction n as [|n IHn]; try reflexivity. + rewrite Nat2Z.inj_succ. + rewrite Nat.pow_succ_r by apply le_0_n. + rewrite Z.pow_succ_r by apply Zle_0_nat. + rewrite IHn. + rewrite Z2Nat.inj_mul; auto using Z.pow_nonneg. + Qed. + + Lemma pow_Zpow : forall a n : nat, Z.of_nat (a ^ n) = Z.of_nat a ^ Z.of_nat n. + Proof with auto using Zle_0_nat, Z.pow_nonneg. + intros; apply Z2Nat.inj... + rewrite <- pow_Z2N_Zpow, !Nat2Z.id... + Qed. + Hint Rewrite pow_Zpow : push_Zof_nat. + Hint Rewrite <- pow_Zpow : pull_Zof_nat. + + Lemma Zpow_sub_1_nat_pow a v + : (Z.pos a^Z.of_nat v - 1 = Z.of_nat (Z.to_nat (Z.pos a)^v - 1))%Z. + Proof. + rewrite <- (Z2Nat.id (Z.pos a)) at 1 by lia. + change 2%Z with (Z.of_nat 2); change 1%Z with (Z.of_nat 1); + autorewrite with pull_Zof_nat. + rewrite Nat2Z.inj_sub + by (change 1%nat with (Z.to_nat (Z.pos a)^0)%nat; apply Nat.pow_le_mono_r; simpl; lia). + reflexivity. + Qed. + Hint Rewrite Zpow_sub_1_nat_pow : pull_Zof_nat. + Hint Rewrite <- Zpow_sub_1_nat_pow : push_Zof_nat. +End Z. |