Refactor ModularArithmetic into Zmod, expand Decidable

ModularArithmetic now uses Algebra lemmas in various places instead of
custom manual proofs. Similarly, Util.Decidable is used to state and
prove the relevant decidability results.

Backwards-incompatible changes:

F_some_lemma -> Zmod.some_lemma
Arguments ZToField _%Z _%Z : clear implicits.
inv_spec says inv x * x = 1, not x * inv x = 1

2 files changed, 28 insertions, 34 deletions

diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v
index 3ae1daa75..de5e0191f 100644
--- a/src/Experiments/DerivationsOptionRectLetInEncoding.v
+++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v
@@ -267,7 +267,7 @@ Lemma unfoldDiv : forall {m} (x y:F m), (x/y = x * inv y)%F. Proof. unfold div.
 Definition FieldToN {m} (x:F m) := Z.to_N (FieldToZ x).
 Lemma FieldToN_correct {m} (x:F m) : FieldToN (m:=m) x = Z.to_N (FieldToZ x). reflexivity. Qed.
 
-Definition natToField {m} x : F m := ZToField (Z.of_nat x).
+Definition natToField {m} x : F m := ZToField _ (Z.of_nat x).
 Definition FieldToNat {m} (x:F m) : nat := Z.to_nat (FieldToZ x).
 
 Section with_unqualified_modulo2.
@@ -275,11 +275,6 @@ Import NPeano Nat.
 Local Infix "mod" := modulo : nat_scope.
 Lemma FieldToNat_natToField {m} : m <> 0 -> forall x, x mod m = FieldToNat (natToField (m:=Z.of_nat m) x).
   unfold natToField, FieldToNat; intros.
-  rewrite (FieldToZ_ZToField), <-mod_Zmod, Nat2Z.id; trivial.
-Qed.
-End with_unqualified_modulo2.
-
-Lemma F_eqb_iff {q} : forall x y : F q, F_eqb x y = true <-> x = y.
-Proof.
-  split; eauto using F_eqb_eq, F_eqb_complete.
+  rewrite (Zmod.FieldToZ_ZToField), <-mod_Zmod, Nat2Z.id; trivial.
 Qed.
+End with_unqualified_modulo2.
\ No newline at end of file
diff --git a/src/Experiments/SpecEd25519.v b/src/Experiments/SpecEd25519.v
index f107e4497..6d6de9dcb 100644
--- a/src/Experiments/SpecEd25519.v
+++ b/src/Experiments/SpecEd25519.v
@@ -8,44 +8,43 @@ Require Import Crypto.ModularArithmetic.PrimeFieldTheorems Crypto.ModularArithme
 Require Import Crypto.Util.NatUtil Crypto.Util.ZUtil Crypto.Util.WordUtil Crypto.Util.NumTheoryUtil.
 Require Import Bedrock.Word.
 Require Import Crypto.Tactics.VerdiTactics.
-Require Import Coq.Logic.Decidable.
+Require Import Coq.Logic.Decidable Crypto.Util.Decidable.
 Require Import Coq.omega.Omega.
 
 (* TODO: move to PrimeFieldTheorems *)
-Lemma minus1_is_square {q} :  prime q -> (q mod 4)%Z = 1%Z -> isSquare (opp 1 : F q)%F.
+Lemma minus1_is_square {q} :  prime q -> (q mod 4)%Z = 1%Z -> (exists y, y*y  = opp (ZToField q 1))%F.
   intros; pose proof prime_ge_2 q _.
-  apply square_Zmod_F.
-  destruct (minus1_square_1mod4 q) as [b b_id]; trivial.
-  exists b; rewrite b_id.
-  rewrite opp_ZToField, !FieldToZ_ZToField, !Z.mod_small; omega.
-Qed.
-
-Lemma euler_criterion_nonsquare {q} (prime_q:prime q) (two_lt_q:(2<q)%Z) (d:F q) : 
-  ((d =? 0)%Z || (Pre.powmod q d (Z.to_N (q / 2)) =? 1)%Z)%bool = false -> 
-   forall x : F q, (x ^ 2)%F <> d.
-Proof.
-  pose proof @euler_criterion_if q prime_q d two_lt_q;
-    break_if; intros; try discriminate; eauto.
+  rewrite Zmod.square_iff.
+  destruct (minus1_square_1mod4 q) as [b b_id]; trivial; exists b.
+  rewrite b_id, Zmod.FieldToZ_opp, Zmod.FieldToZ_ZToField, Z.mod_opp_l_nz, !Zmod_small;
+    (repeat (omega || rewrite Zmod_small)).
 Qed.
 
 Definition q : Z := (2 ^ 255 - 19)%Z.
 Global Instance prime_q : prime q. Admitted.
 Lemma two_lt_q : (2 < q)%Z. Proof. reflexivity. Qed.
-Lemma char_gt_2 : (1 + 1 <> (0:F q))%F. Proof. rewrite F_eq; compute; discriminate. Qed.
+Lemma char_gt_2 : (1 + 1 <> (0:F q))%F. vm_decide_no_check. Qed.
 
 Definition a : F q := opp 1%F.
-Lemma nonzero_a : a <> 0%F. Proof. rewrite F_eq; compute; discriminate. Qed.
+Lemma nonzero_a : a <> 0%F. Proof. vm_decide_no_check. Qed.
 Lemma square_a : exists b, (b*b=a)%F.
-Proof. setoid_rewrite <-F_pow_2_r. apply (minus1_is_square _); reflexivity. Qed.
+Proof. pose (@Zmod.Decidable_square q _ two_lt_q a); vm_decide_no_check. Qed.
+Definition d : F q := (opp (ZToField _ 121665) / (ZToField _ 121666))%F.
+
+(* TODO: move to Decidable *)
+Lemma not_not P {d:Decidable P} : not (not P) <-> P.
+Proof. destruct (dec P); intuition. Qed.
+  
+Global Instance dec_ex_forall_not T (P:T->Prop) {d:Decidable (exists b, P b)} : Decidable (forall b, ~ P b).
+Proof.
+  destruct (dec (~ exists b, P b)) as [Hd|Hd]; [left|right];
+    [abstract eauto | abstract (rewrite not_not in Hd by eauto; destruct Hd; eauto) ].
+Defined.
 
-Definition d : F q := (opp (ZToField 121665) / (ZToField 121666))%F.
 Lemma nonsquare_d : forall x, (x*x <> d)%F.
-Proof.
-  intros; rewrite <-F_pow_2_r.
-  apply (euler_criterion_nonsquare prime_q two_lt_q); vm_cast_no_check (eq_refl false).
-Qed. (* 3s *)
+Proof. pose (@Zmod.Decidable_square q _ two_lt_q d). vm_decide_no_check. Qed.
 
-Instance curve25519params : @E.twisted_edwards_params (F q) eq (ZToField 0) (ZToField 1) add mul a d :=
+Instance curve25519params : @E.twisted_edwards_params (F q) eq 0%F 1%F add mul a d :=
   {
     nonzero_a := nonzero_a;
     char_gt_2 := char_gt_2;
@@ -112,10 +111,10 @@ Definition FlEncoding : canonical encoding of F (Z.of_nat l) as word b :=
 Lemma q_5mod8 : (q mod 8 = 5)%Z. cbv; reflexivity. Qed.
 
 Lemma sqrt_minus1_valid : ((@ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1)%F.
-Proof. apply F_eq; vm_compute; reflexivity. Qed.
+Proof. vm_decide_no_check. Qed.
 
-Local Notation point := (@E.point (F q) eq (ZToField 1) add mul a d).
-Local Notation zero := (E.zero(H:=field_modulo)).
+Local Notation point := (@E.point (F q) eq 1%F add mul a d).
+Local Notation zero := (E.zero(H:=Zmod.field_modulo q)).
 Local Notation add := (E.add(H0:=curve25519params)).
 Local Infix "*" := (E.mul(H0:=curve25519params)).
 Axiom H : forall n : nat, word n -> word (b + b).