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

3 files changed, 8 insertions, 9 deletions

diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v
index fc506f61d..16584c683 100644
--- a/src/Spec/ModularArithmetic.v
+++ b/src/Spec/ModularArithmetic.v
@@ -35,7 +35,7 @@ Section FieldOperations.
   Definition inv_with_spec : { inv : F m -> F m
                              | inv zero = zero
                              /\ ( Znumtheory.prime m ->
-                                 forall a, a <> zero -> mul a (inv a) = one )
+                                 forall a, a <> zero -> mul (inv a) a = one )
                              } := Pre.inv_impl.
   Definition inv : F m -> F m := Eval hnf in proj1_sig inv_with_spec.
   Definition div (a b:F m) : F m := mul a (inv b).
@@ -49,7 +49,7 @@ End FieldOperations.
 
 Delimit Scope F_scope with F.
 Arguments F _%Z.
-Arguments ZToField {_} _%Z : simpl never.
+Arguments ZToField _%Z _%Z : simpl never, clear implicits.
 Arguments add {_} _%F _%F : simpl never.
 Arguments mul {_} _%F _%F : simpl never.
 Arguments sub {_} _%F _%F : simpl never.
@@ -57,11 +57,10 @@ Arguments div {_} _%F _%F : simpl never.
 Arguments pow {_} _%F _%N : simpl never.
 Arguments inv {_} _%F : simpl never.
 Arguments opp {_} _%F : simpl never.
-Local Open Scope F_scope.
 Infix "+" := add : F_scope.
 Infix "*" := mul : F_scope.
 Infix "-" := sub : F_scope.
 Infix "/" := div : F_scope.
 Infix "^" := pow : F_scope.
-Notation "0" := (ZToField 0) : F_scope.
-Notation "1" := (ZToField 1) : F_scope.
+Notation "0" := (ZToField _ 0) : F_scope.
+Notation "1" := (ZToField _ 1) : F_scope.
\ No newline at end of file
diff --git a/src/Spec/ModularWordEncoding.v b/src/Spec/ModularWordEncoding.v
index acd2bedbd..86546a22f 100644
--- a/src/Spec/ModularWordEncoding.v
+++ b/src/Spec/ModularWordEncoding.v
@@ -18,7 +18,7 @@ Section ModularWordEncoding.
   Definition Fm_dec (x_ : word sz) : option (F m) :=
     let z := Z.of_N (wordToN (x_)) in
     if Z_lt_dec z m
-      then Some (ZToField z)
+      then Some (ZToField m z)
       else None
   .
 
@@ -37,4 +37,4 @@ Section ModularWordEncoding.
       @ModularWordEncodingPre.Fm_encoding_canonical m sz bound_check
   }.
 
-End ModularWordEncoding.
+End ModularWordEncoding.
\ No newline at end of file
diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v
index 7ec5d99ec..e2c99a8fe 100644
--- a/src/Spec/WeierstrassCurve.v
+++ b/src/Spec/WeierstrassCurve.v
@@ -11,8 +11,8 @@ Module E.
 
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} `{Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
-    Local Infix "=?" := Algebra.eq_dec (at level 70, no associativity) : type_scope.
-    Local Notation "x =? y" := (Sumbool.bool_of_sumbool (Algebra.eq_dec x y)) : bool_scope.
+    Local Notation "x =? y" := (Decidable.dec (Feq x y)) (at level 70, no associativity) : type_scope.
+    Local Notation "x =? y" := (Sumbool.bool_of_sumbool (Decidable.dec (Feq x y))) : bool_scope.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
     Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
     Local Notation "- x" := (Fopp x).