Merge branch 'master' of github.mit.edu:plv/fiat-crypto

7 files changed, 47 insertions, 32 deletions

diff --git a/src/ModularArithmetic/FField.v b/src/ModularArithmetic/FField.v
index cd293056f..4f2b623e0 100644
--- a/src/ModularArithmetic/FField.v
+++ b/src/ModularArithmetic/FField.v
@@ -1,5 +1,5 @@
 Require Export Crypto.Spec.ModularArithmetic.
-Require Export Field.
+Require Export Coq.setoid_ring.Field.
 
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 
@@ -14,6 +14,10 @@ Definition Opaquediv {p} : OpaqueF p -> OpaqueF p -> OpaqueF p := @div p.
 Definition Opaqueopp {p} : OpaqueF p -> OpaqueF p := @opp p.
 Definition Opaqueinv {p} : OpaqueF p -> OpaqueF p := @inv p.
 Definition OpaqueZToField {p} : BinInt.Z -> OpaqueF p := @ZToField p.
+Definition Opaqueadd_correct {p} : @Opaqueadd p = @add p := eq_refl.
+Definition Opaquesub_correct {p} : @Opaquesub p = @sub p := eq_refl.
+Definition Opaquemul_correct {p} : @Opaquemul p = @mul p := eq_refl.
+Definition Opaquediv_correct {p} : @Opaquediv p = @div p := eq_refl.
 Global Opaque F OpaqueZmodulo Opaqueadd Opaquemul Opaquesub Opaquediv Opaqueopp Opaqueinv OpaqueZToField.
 
 Definition OpaqueFieldTheory p {prime_p} : @field_theory (OpaqueF p) (OpaqueZToField 0%Z) (OpaqueZToField 1%Z) Opaqueadd Opaquemul Opaquesub Opaqueopp Opaquediv Opaqueinv eq := Eval hnf in @Ffield_theory p prime_p.
@@ -26,7 +30,7 @@ Ltac FIELD_SIMPL_idtac FLD lH rl :=
   get_FldPost FLD ().
 Ltac field_simplify_eq_idtac := let G := Get_goal in field_lookup (PackField FIELD_SIMPL_idtac) [] G.
 
-Ltac F_to_Opaque := 
+Ltac F_to_Opaque :=
   change F with OpaqueF in *;
   change BinInt.Z.modulo with OpaqueZmodulo in *;
   change @add with @Opaqueadd in *;
@@ -41,13 +45,10 @@ Ltac F_from_Opaque p :=
   change OpaqueF with F in *;
   change (@sig BinNums.Z (fun z : BinNums.Z => @eq BinNums.Z z (BinInt.Z.modulo z p))) with (F p) in *;
   change OpaqueZmodulo with BinInt.Z.modulo in *;
-  change @Opaqueadd with @add in *;
-  change @Opaquemul with @mul in *;
-  change @Opaquesub with @sub in *;
-  change @Opaquediv with @div in *;
   change @Opaqueopp with @opp in *;
   change @Opaqueinv with @inv in *;
-  change @OpaqueZToField with @ZToField in *.
+  change @OpaqueZToField with @ZToField in *;
+  rewrite ?@Opaqueadd_correct, ?@Opaquesub_correct, ?@Opaquemul_correct, ?@Opaquediv_correct in *.
 
 Ltac F_field_simplify_eq :=
   lazymatch goal with |- @eq (F ?p) _ _ =>
@@ -59,4 +60,4 @@ Ltac F_field_simplify_eq :=
 
 Ltac F_field := F_field_simplify_eq; [ring|..].
 
-Ltac notConstant t := constr:NotConstant.
\ No newline at end of file
+Ltac notConstant t := constr:NotConstant.
diff --git a/src/ModularArithmetic/FNsatz.v b/src/ModularArithmetic/FNsatz.v
index a0f34073d..221b8d799 100644
--- a/src/ModularArithmetic/FNsatz.v
+++ b/src/ModularArithmetic/FNsatz.v
@@ -1,6 +1,6 @@
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Export Crypto.ModularArithmetic.FField.
-Require Import Nsatz.
+Require Import Coq.nsatz.Nsatz.
 
 Ltac FqAsIntegralDomain :=
   lazymatch goal with [H:Znumtheory.prime ?q |- _ ] =>
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index f39cc4176..ddb689547 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -1,11 +1,11 @@
 Require Import Crypto.Spec.ModularArithmetic.
 Require Import Crypto.ModularArithmetic.Pre.
 
-Require Import Eqdep_dec.
-Require Import Tactics.VerdiTactics.
-Require Import BinInt Zdiv Znumtheory NArith. (* import Zdiv before Znumtheory *)
-Require Import Coq.Classes.Morphisms Setoid.
-Require Export Ring_theory Field_theory Field_tac.
+Require Import Coq.Logic.Eqdep_dec.
+Require Import Crypto.Tactics.VerdiTactics.
+Require Import Coq.ZArith.BinInt Coq.ZArith.Zdiv Coq.ZArith.Znumtheory Coq.NArith.NArith. (* import Zdiv before Znumtheory *)
+Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid.
+Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac.
 
 Section ModularArithmeticPreliminaries.
   Context {m:Z}.
diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v
index 2bfcdcf0b..f63bfbb1c 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/Pre.v b/src/ModularArithmetic/Pre.v
index 3432488c4..2978fdd42 100644
--- a/src/ModularArithmetic/Pre.v
+++ b/src/ModularArithmetic/Pre.v
@@ -1,6 +1,6 @@
-Require Import BinInt BinNat BinNums Zdiv Znumtheory.
-Require Import Eqdep_dec.
-Require Import EqdepFacts.
+Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.Numbers.BinNums Coq.ZArith.Zdiv Coq.ZArith.Znumtheory.
+Require Import Coq.Logic.Eqdep_dec.
+Require Import Coq.Logic.EqdepFacts.
 Require Import Crypto.Tactics.VerdiTactics.
 
 Lemma Z_mod_mod x m : x mod m = (x mod m) mod m.
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index 40af15dac..77d84c455 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -1,13 +1,13 @@
-Require Export Spec.ModularArithmetic ModularArithmetic.ModularArithmeticTheorems.
-Require Export Ring_theory Field_theory Field_tac.
+Require Export Crypto.Spec.ModularArithmetic Crypto.ModularArithmetic.ModularArithmeticTheorems.
+Require Export Coq.setoid_ring.Ring_theory Coq.setoid_ring.Field_theory Coq.setoid_ring.Field_tac.
 
-Require Import Nsatz.
+Require Import Coq.nsatz.Nsatz.
 Require Import Crypto.ModularArithmetic.Pre.
-Require Import Util.NumTheoryUtil.
-Require Import Tactics.VerdiTactics.
-Require Import Coq.Classes.Morphisms Setoid.
-Require Import BinInt BinNat ZArith Znumtheory NArith. (* import Zdiv before Znumtheory *)
-Require Import Eqdep_dec.
+Require Import Crypto.Util.NumTheoryUtil.
+Require Import Crypto.Tactics.VerdiTactics.
+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.
 
 Existing Class prime.
@@ -294,7 +294,7 @@ Section VariousModPrime.
     }
   Qed.
 
-  Lemma euler_criterion_if : forall (a : F q) (q_odd : 2 < q),
+  Lemma euler_criterion_if' : forall (a : F q) (q_odd : 2 < q),
     if (orb (F_eqb a 0) (F_eqb (a ^ (Z.to_N (q / 2))) 1))
     then (isSquare a) else (forall b, b ^ 2 <> a).
   Proof.
@@ -309,6 +309,16 @@ Section VariousModPrime.
       apply euler_criterion_F in a_square; auto.
   Qed.
 
+  Lemma euler_criterion_if : forall (a : F q) (q_odd : 2 < q),
+    if (a =? 0) || (powmod q a (Z.to_N (q / 2)) =? 1)
+    then (isSquare a) else (forall b, b ^ 2 <> a).
+  Proof.
+    intros.
+    pose proof (euler_criterion_if' a q_odd) as H.
+    unfold F_eqb in *; simpl in *.
+    rewrite !Zmod_small, !@FieldToZ_pow_efficient in H by omega; eauto.
+  Qed.
+
   Lemma sqrt_solutions : forall x y : F q, y ^ 2 = x ^ 2 -> y = x \/ y = opp x.
   Proof.
     intros ? ? squares_eq.
diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v
index 425816f9e..d6c7fa4b8 100644
--- a/src/ModularArithmetic/Tutorial.v
+++ b/src/ModularArithmetic/Tutorial.v
@@ -1,5 +1,5 @@
-Require Import BinInt Zpower ZArith Znumtheory.
-Require Import Spec.ModularArithmetic ModularArithmetic.PrimeFieldTheorems.
+Require Import Coq.ZArith.BinInt Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory.
+Require Import Crypto.Spec.ModularArithmetic Crypto.ModularArithmetic.PrimeFieldTheorems.
 
 
 (* Example for modular arithmetic with a concrete modulus in a section *)