diff options
Diffstat (limited to 'src/Arithmetic/PrimeFieldTheorems.v')
| -rw-r--r-- | src/Arithmetic/PrimeFieldTheorems.v | 23 |
1 files changed, 13 insertions, 10 deletions
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; |