diff options
| author |  Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:59:13 -0400 |
|---|---|---|
| committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:59:13 -0400 |
| commit | 9b3c0e79384ab9c997a45f7d0bc38ec54e1412c6 (patch) | |
| tree | 25e986ef13b3fcfd4765168a80e6f0520084b4c4 /src | |
| parent | b942db6abaac7243c3901785bde0f3c4c1f46e6d (diff) | |
| parent | 2e566c32baf2a140cd7820c4f06437ee5c43ac44 (diff) | |
squash commits + revert makefile
Diffstat (limited to 'src')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystem.v | 12 | ||||
| -rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 4 |
2 files changed, 10 insertions, 6 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v index c77f8c273..558b9a5a2 100644 --- a/src/ModularArithmetic/ModularBaseSystem.v +++ b/src/ModularArithmetic/ModularBaseSystem.v @@ -1,8 +1,12 @@ -Require Import Zpower ZArith. -Require Import List. -Require Import Crypto.Util.ListUtil. +Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith. +Require Import Coq.Lists.List. +Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Crypto.BaseSystem Crypto.ModularArithmetic.PseudoMersenneBaseParams Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs Crypto.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.BaseSystem. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams. +Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs. +Require Import Crypto.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.Tactics.VerdiTactics. Local Open Scope Z_scope. Section PseudoMersenneBase. diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 8835a5d6e..70a2c4a87 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -410,7 +410,7 @@ Section SquareRootsPrime5Mod8. (* This is only the square root of -1 if q mod 8 is 3 or 5 *) Definition sqrt_minus1 : F q := ZToField 2 ^ Z.to_N (q / 4). - Lemma two_lt_q : 2 < q. + Lemma two_lt_q_5mod8 : 2 < q. Proof. pose proof (prime_ge_2 q _) as two_le_q. apply Zle_lt_or_eq in two_le_q. @@ -466,7 +466,7 @@ Section SquareRootsPrime5Mod8. replace (Z.to_N 2) with 2%N by auto. ring. - symmetry; apply euler_criterion_F; auto using two_lt_q. + symmetry; apply euler_criterion_F; auto using two_lt_q_5mod8. } Qed. |