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

5 files changed, 114 insertions, 218 deletions

diff --git a/src/Experiments/SpecEd25519.v b/src/Experiments/SpecEd25519.v
index 30d8ce13d..f107e4497 100644
--- a/src/Experiments/SpecEd25519.v
+++ b/src/Experiments/SpecEd25519.v
@@ -11,102 +11,79 @@ Require Import Crypto.Tactics.VerdiTactics.
 Require Import Coq.Logic.Decidable.
 Require Import Coq.omega.Omega.
 
-Local Open Scope nat_scope.
-Definition q : Z := (2 ^ 255 - 19)%Z.
-Global Instance prime_q : prime q. Admitted.
-Lemma two_lt_q : (2 < q)%Z. reflexivity. Qed.
-
-Definition a : F q := opp 1%F.
-
-(* TODO (jadep) : make the proofs about a and d more general *)
-Lemma nonzero_a : a <> 0%F.
-Proof.
-  unfold a.
-  intro eq_opp1_0.
-  apply (@Fq_1_neq_0 q prime_q).
-  rewrite <- (F_opp_spec 1%F).
-  rewrite eq_opp1_0.
-  symmetry; apply F_add_0_r.
+(* TODO: move to PrimeFieldTheorems *)
+Lemma minus1_is_square {q} :  prime q -> (q mod 4)%Z = 1%Z -> isSquare (opp 1 : F q)%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.
 
-Ltac q_bound := pose proof two_lt_q; omega.
-Lemma square_a : isSquare a.
+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.
-  assert (q_1mod4 : (q mod 4 = 1)%Z) by abstract reflexivity.
-  intros.
-  pose proof (minus1_square_1mod4 q prime_q q_1mod4) as minus1_square.
-  destruct minus1_square as [b b_id].
-  apply square_Zmod_F.
-  exists b; rewrite b_id.
-  unfold a.
-  rewrite opp_ZToField.
-  rewrite FieldToZ_ZToField.
-  rewrite Z.mod_small; q_bound.
+  pose proof @euler_criterion_if q prime_q d two_lt_q;
+    break_if; intros; try discriminate; eauto.
 Qed.
 
-Hint Rewrite
- @FieldToZ_add
- @FieldToZ_mul
- @FieldToZ_opp
- @FieldToZ_inv_efficient
- @FieldToZ_pow_efficient
- @FieldToZ_ZToField
- @Zmod_mod
- : ZToField.
+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.
+
+Definition a : F q := opp 1%F.
+Lemma nonzero_a : a <> 0%F. Proof. rewrite F_eq; compute; discriminate. Qed.
+Lemma square_a : exists b, (b*b=a)%F.
+Proof. setoid_rewrite <-F_pow_2_r. apply (minus1_is_square _); reflexivity. Qed.
 
 Definition d : F q := (opp (ZToField 121665) / (ZToField 121666))%F.
-Lemma nonsquare_d : forall x, (x^2 <> d)%F.
-  pose proof @euler_criterion_if q prime_q d two_lt_q.
-  match goal with
-    [H: if ?b then ?x else ?y |- ?y ] => replace b with false in H; [exact H|clear H]
-  end.
-  unfold d, div. autorewrite with ZToField; [|eauto using prime_q, two_lt_q..].
-  vm_compute. (* 10s *)
-  exact eq_refl.
-Qed. (* 10s *)
+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 *)
 
 Instance curve25519params : @E.twisted_edwards_params (F q) eq (ZToField 0) (ZToField 1) add mul a d :=
   {
-    nonzero_a := nonzero_a
-                   (* TODO:port
-    char_gt_2 : ~ Feq (Fadd Fone Fone) Fzero;
-    nonzero_a : ~ Feq a Fzero;
-    nonsquare_d : forall x : F, ~ Feq (Fmul x x) d }
-                    *)
+    nonzero_a := nonzero_a;
+    char_gt_2 := char_gt_2;
+    square_a := square_a;
+    nonsquare_d := nonsquare_d
   }.
-Admitted.
 
-Lemma two_power_nat_Z2Nat : forall n, Z.to_nat (two_power_nat n) = 2 ^ n.
+Lemma two_power_nat_Z2Nat : forall n, Z.to_nat (two_power_nat n) = (2 ^ n)%nat.
 Admitted.
 
-Definition b := 256.
+Definition b := 256%nat.
 Lemma b_valid : (2 ^ (b - 1) > Z.to_nat q)%nat.
 Proof.
   unfold q, gt.
-  replace (2 ^ (b - 1)) with (Z.to_nat (2 ^ (Z.of_nat (b - 1))))
+  replace (2 ^ (b - 1))%nat with (Z.to_nat (2 ^ (Z.of_nat (b - 1))))
     by (rewrite <- two_power_nat_equiv; apply two_power_nat_Z2Nat).
   rewrite <- Z2Nat.inj_lt; compute; congruence.
 Qed.
 
-Definition c := 3.
-Lemma c_valid : c = 2 \/ c = 3.
+Definition c := 3%nat.
+Lemma c_valid : (c = 2 \/ c = 3)%nat.
 Proof.
   right; auto.
 Qed.
 
-Definition n := b - 2.
-Lemma n_ge_c : n >= c.
+Definition n := (b - 2)%nat.
+Lemma n_ge_c : (n >= c)%nat.
 Proof.
   unfold n, c, b; omega.
 Qed.
-Lemma n_le_b : n <= b.
+Lemma n_le_b : (n <= b)%nat.
 Proof.
   unfold n, b; omega.
 Qed.
 
 Definition l : nat := Z.to_nat (252 + 27742317777372353535851937790883648493)%Z.
 Lemma prime_l : prime (Z.of_nat l). Admitted.
-Lemma l_odd : l > 2.
+Lemma l_odd : (l > 2)%nat.
 Proof.
   unfold l, proj1_sig.
   rewrite Z2Nat.inj_add; try omega.
@@ -116,12 +93,12 @@ Qed.
 
 Require Import Crypto.Spec.Encoding.
 
-Lemma q_pos : (0 < q)%Z. q_bound. Qed.
+Lemma q_pos : (0 < q)%Z. pose proof prime_ge_2 q _; omega. Qed.
 Definition FqEncoding : canonical encoding of (F q) as word (b-1) :=
   @modular_word_encoding q (b - 1) q_pos b_valid.
 
 Lemma l_pos : (0 < Z.of_nat l)%Z. pose proof prime_l; prime_bound. Qed.
-Lemma l_bound : Z.to_nat (Z.of_nat l) < 2 ^ b.
+Lemma l_bound : (Z.to_nat (Z.of_nat l) < 2 ^ b)%nat.
 Proof.
   rewrite Nat2Z.id.
   rewrite <- pow2_id.
@@ -135,12 +112,7 @@ 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.
-  autorewrite with ZToField.
-  vm_compute.
-  reflexivity.
-Qed.
+Proof. apply F_eq; vm_compute; reflexivity. Qed.
 
 Local Notation point := (@E.point (F q) eq (ZToField 1) add mul a d).
 Local Notation zero := (E.zero(H:=field_modulo)).
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index 951f848bf..a1d47ae8f 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -21,13 +21,6 @@ Section ModularArithmeticPreliminaries.
     eapply UIP_dec, Z.eq_dec.
   Qed.
 
-  Lemma F_opp_spec : forall (a:F m), add a (opp a) = 0.
-    intros a.
-    pose (@opp_with_spec m) as H.
-    change (@opp m) with (proj1_sig H).
-    destruct H; eauto.
-  Qed.
-
   Lemma F_pow_spec : forall (a:F m),
       pow a 0%N = 1%F /\ forall x, pow a (1 + x)%N = mul a (pow a x).
   Proof.
@@ -85,7 +78,6 @@ end.
 
 Ltac Fdefn :=
   intros;
-  rewrite ?F_opp_spec;
   repeat match goal with [ x : F _ |- _ ] => destruct x end;
   try eq_remove_proofs;
   demod;
@@ -155,10 +147,13 @@ Section FandZ.
   Proof.
     repeat split; Fdefn; try apply F_eq_dec.
     { rewrite Z.add_0_r. auto. }
-    { rewrite <-Z.add_sub_swap, <-Z.add_sub_assoc, Z.sub_diag, Z.add_0_r. apply Z_mod_same_full. }
     { rewrite Z.mul_1_r. auto. }
   Qed.
 
+  Lemma F_opp_spec : forall (a:F m), add a (opp a) = 0.
+    Fdefn.
+  Qed.
+
   Lemma ZToField_0 : @ZToField m 0 = 0.
   Proof.
     Fdefn.
@@ -270,7 +265,6 @@ Section FandZ.
       @ZToField m (x - y) = ZToField x - ZToField y.
   Proof.
     Fdefn.
-    apply sub_intersperse_modulus.
   Qed.
 
   (* Compatibility between inject and multiplication *)
@@ -412,13 +406,30 @@ Section RingModuloPre.
     Fdefn; rewrite <-Z.quot_rem'; trivial.
   Qed.
 
+  Lemma Z_mul_mod_modulus_r : forall x m, ((x*m) mod m = 0)%Z.
+    intros.
+    rewrite Zmult_mod, Z_mod_same_full.
+    rewrite Z.mul_0_r, Zmod_0_l.
+    reflexivity.
+  Qed.
+
+  Lemma Z_mod_opp_equiv : forall x y m,  x  mod m = (-y) mod m ->
+                                       (-x) mod m =   y  mod m.
+  Proof.
+    intros.
+    rewrite <-Z.sub_0_l.
+    rewrite Zminus_mod. rewrite H.
+    rewrite ?Zminus_mod_idemp_l, ?Zminus_mod_idemp_r; f_equal.
+    destruct y; auto.
+  Qed.
+
   Lemma Z_opp_opp : forall x : Z, (-(-x)) = x.
     destruct x; auto.
   Qed.
 
   Lemma Z_mod_opp : forall x m, (- x) mod m = (- (x mod m)) mod m.
     intros.
-    apply Pre.mod_opp_equiv.
+    apply Z_mod_opp_equiv.
     rewrite Z_opp_opp.
     demod; auto.
   Qed.
@@ -437,9 +448,7 @@ Section RingModuloPre.
   Proof.
     constructor; intros; try Fdefn; unfold id;
       try (apply gf_eq; simpl; intuition).
-
-    - apply sub_intersperse_modulus.
-    - rewrite Zminus_mod, Z_mod_same_full; simpl. apply Z_mod_opp.
+    - apply Z_mod_opp_equiv; rewrite Z_opp_opp, Zmod_mod; reflexivity.
     - rewrite (proj1 (Z.eqb_eq x y)); trivial.
   Qed.
 
@@ -620,6 +629,7 @@ Section VariousModulo.
   Lemma opp_ZToField : forall x : Z, opp (ZToField x) = @ZToField m (m - x).
   Proof.
     Fdefn.
+    rewrite Zminus_mod, Z_mod_same_full, (Z.sub_0_l (x mod m)); reflexivity.
   Qed.
 
   Lemma F_pow_2_r : forall x : F m, x^2 = x*x.
diff --git a/src/ModularArithmetic/Pre.v b/src/ModularArithmetic/Pre.v
index fca5576b7..5e61278f6 100644
--- a/src/ModularArithmetic/Pre.v
+++ b/src/ModularArithmetic/Pre.v
@@ -3,6 +3,8 @@ Require Import Coq.Logic.Eqdep_dec.
 Require Import Coq.Logic.EqdepFacts.
 Require Import Crypto.Tactics.VerdiTactics.
 Require Import Coq.omega.Omega.
+Require Import Crypto.Util.NumTheoryUtil.
+Require Import Crypto.Tactics.VerdiTactics.
 
 Lemma Z_mod_mod x m : x mod m = (x mod m) mod m.
   symmetry.
@@ -21,29 +23,6 @@ Proof.
   eapply UIP_dec, Z.eq_dec.
 Qed.
 
-Definition opp_impl:
-  forall {m : BinNums.Z},
-    {opp0 : {z : BinNums.Z | z = z mod m} -> {z : BinNums.Z | z = z mod m} |
-     forall x : {z : BinNums.Z | z = z mod m},
-       exist (fun z : BinNums.Z => z = z mod m)
-             ((proj1_sig x + proj1_sig (opp0 x)) mod m)
-             (Z_mod_mod (proj1_sig x + proj1_sig (opp0 x)) m) =
-       exist (fun z : BinNums.Z => z = z mod m) (0 mod m) (Z_mod_mod 0 m)}.
-  intro m.
-  refine (exist _ (fun x => exist _ ((m-proj1_sig x) mod m) _) _); intros.
-
-  destruct x;
-  simpl;
-  apply exist_reduced_eq;
-  rewrite Zdiv.Zplus_mod_idemp_r;
-  replace (x + (m - x)) with m by omega;
-  apply Zdiv.Z_mod_same_full.
-
-  Grab Existential Variables.
-  destruct x; simpl.
-  rewrite Zdiv.Zmod_mod; reflexivity.
-Defined.
-
 Definition mulmod m := fun a b => a * b mod m.
 Definition powmod_pos m := Pos.iter_op (mulmod m).
 Definition powmod m a x := match x with N0 => 1 mod m | Npos p => powmod_pos m p (a mod m) end.
@@ -93,17 +72,18 @@ Proof.
   rewrite ?Zdiv.Zmult_mod_idemp_l, ?Zdiv.Zmult_mod_idemp_r; f_equal.
 Qed.
 
-Definition pow_impl_sig {m} : {z : Z | z = z mod m} -> N -> {z : Z | z = z mod m}.
-  intros a x.
-  exists (powmod m (proj1_sig a) x).
-  destruct x; [simpl; rewrite Zmod_mod; reflexivity|].
+Local Obligation Tactic := idtac.
+
+Program Definition pow_impl_sig {m} (a:{z : Z | z = z mod m}) (x:N) : {z : Z | z = z mod m}
+  := powmod m (proj1_sig a) x.
+Next Obligation.
+  intros; destruct x; [simpl; rewrite Zmod_mod; reflexivity|].
   rewrite N_pos_1plus.
   rewrite powmod_1plus.
   rewrite Zmod_mod; reflexivity.
-Defined.
+Qed.
 
-Definition pow_impl:
-   forall {m : BinNums.Z},
+Program Definition pow_impl {m} :
    {pow0
    : {z : BinNums.Z | z = z mod m} -> BinNums.N -> {z : BinNums.Z | z = z mod m}
    |
@@ -114,85 +94,23 @@ Definition pow_impl:
     pow0 a (1 + x)%N =
     exist (fun z : BinNums.Z => z = z mod m)
       ((proj1_sig a * proj1_sig (pow0 a x)) mod m)
-      (Z_mod_mod (proj1_sig a * proj1_sig (pow0 a x)) m))}.
-  intros m. exists pow_impl_sig.
-  split; [eauto using exist_reduced_eq|]; intros.
-  apply exist_reduced_eq.
-  rewrite powmod_1plus.
-  rewrite ?Zdiv.Zmult_mod_idemp_l, ?Zdiv.Zmult_mod_idemp_r; f_equal.
+      (Z_mod_mod (proj1_sig a * proj1_sig (pow0 a x)) m))} := pow_impl_sig.
+Next Obligation.
+  split; intros; apply exist_reduced_eq;
+    rewrite ?powmod_1plus, ?Zdiv.Zmult_mod_idemp_l, ?Zdiv.Zmult_mod_idemp_r; reflexivity.
 Qed.
 
-Lemma mul_mod_modulus_r : forall x m, (x*m) mod m = 0.
-  intros.
-  rewrite Zmult_mod, Z_mod_same_full.
-  rewrite Z.mul_0_r, Zmod_0_l.
-  reflexivity.
+Program Definition mod_inv_sig {m} (a:{z : Z | z = z mod m}) : {z : Z | z = z mod m} :=
+  let (a, _) := a in
+  match a return _ with
+  | 0%Z => 0 (* m = 2 *)
+  | _ => powmod m a (Z.to_N (m-2))
+  end.
+Next Obligation.
+  intros; break_match; rewrite ?powmod_Zpow_mod, ?Zmod_mod, ?Zmod_0_l; reflexivity.
 Qed.
 
-Lemma mod_opp_equiv : forall x y m,  x  mod m = (-y) mod m ->
-                              (-x) mod m =   y  mod m.
-Proof.
-  intros.
-  rewrite <-Z.sub_0_l.
-  rewrite Zminus_mod. rewrite H.
-  rewrite ?Zminus_mod_idemp_l, ?Zminus_mod_idemp_r; f_equal.
-  destruct y; auto.
-Qed.
-
-Definition mod_inv_eucl (a m:Z) : Z.
-  destruct (euclid a m). (* [euclid] is opaque. TODO: reimplement? *)
-  exact ((match a with Z0 => Z0 | _ =>
-                                 (match d with Z.pos _ =>  u | _ => -u end)
-          end) mod m).
-Defined.
-
-Lemma reduced_nonzero_pos:
-  forall a m : Z, m > 0 -> a <> 0 -> a = a mod m -> 0 < a.
-Proof.
-  intros a m m_pos a_nonzero pfa.
-  destruct (Z.eq_dec 0 m); subst_max; try omega.
-  pose proof (Z_mod_lt a m) as H.
-  destruct (Z.eq_dec 0 a); subst_max; try omega.
-Qed.
-
-Lemma mod_inv_eucl_correct : forall a m, a <> 0 -> a = a mod m -> prime m ->
-                                    ((mod_inv_eucl a m) * a) mod m = 1 mod m.
-Proof.
-  intros a m a_nonzero pfa prime_m.
-  pose proof (prime_ge_2 _ prime_m).
-  assert (0 < m) as m_pos by omega.
-  assert (0 <= m) as m_nonneg by omega.
-  assert (0 < a) as a_pos by (eapply reduced_nonzero_pos; eauto; omega).
-  unfold mod_inv_eucl.
-  destruct a as [|a'|a'] eqn:ha; try pose proof (Zlt_neg_0 a') as nnn; try omega; clear nnn.
-  rewrite<- ha in *.
-  lazymatch goal with [ |- context [euclid ?a ?b] ] => destruct (euclid a b) end.
-  lazymatch goal with [H: Zis_gcd _ _ _ |- _ ] => destruct H end.
-  rewrite Z.add_move_r in e.
-  destruct (Z_mod_lt a m ); try omega; rewrite <- pfa in *.
-  destruct (prime_divisors _ prime_m _ H1) as [Ha|[Hb|[Hc|Hd]]]; subst d.
-  + assert ((u * a) mod m = (-1 - v * m) mod m) as Hx by (f_equal; trivial).
-    rewrite Zminus_mod, mul_mod_modulus_r, Z.sub_0_r, Zmod_mod in Hx.
-    rewrite Zmult_mod_idemp_l.
-    rewrite <-Zopp_mult_distr_l.
-    eauto using mod_opp_equiv.
-  + rewrite Zmult_mod_idemp_l.
-    rewrite e, Zminus_mod, mul_mod_modulus_r, Z.sub_0_r, Zmod_mod; reflexivity.
-  + pose proof (Zdivide_le _ _ m_nonneg a_pos H0); omega.
-  + apply Zdivide_opp_l_rev in H0.
-    pose proof (Zdivide_le _ _ m_nonneg a_pos H0); omega.
-Qed.
-
-Lemma mod_inv_eucl_sig : forall {m}, {z : Z | z = z mod m} -> {z : Z | z = z mod m}.
-  intros m a.
-  exists (mod_inv_eucl (proj1_sig a) m).
-  destruct a; unfold mod_inv_eucl.
-  lazymatch goal with [ |- context [euclid ?a ?b] ] => destruct (euclid a b) end.
-  rewrite Zmod_mod; reflexivity.
-Defined.
-
-Definition inv_impl :
-   forall {m : BinNums.Z},
+Program Definition inv_impl {m : BinNums.Z} :
    {inv0 : {z : BinNums.Z | z = z mod m} -> {z : BinNums.Z | z = z mod m} |
    inv0 (exist (fun z : BinNums.Z => z = z mod m) (0 mod m) (Z_mod_mod 0 m)) =
    exist (fun z : BinNums.Z => z = z mod m) (0 mod m) (Z_mod_mod 0 m) /\
@@ -202,20 +120,21 @@ Definition inv_impl :
     exist (fun z : BinNums.Z => z = z mod m)
       ((proj1_sig a * proj1_sig (inv0 a)) mod m)
       (Z_mod_mod (proj1_sig a * proj1_sig (inv0 a)) m) =
-    exist (fun z : BinNums.Z => z = z mod m) (1 mod m) (Z_mod_mod 1 m))}.
-Proof.
-  intros m. exists mod_inv_eucl_sig. split; intros.
-  - simpl.
-    apply exist_reduced_eq; simpl.
-    unfold mod_inv_eucl; simpl.
-    lazymatch goal with [ |- context [euclid ?a ?b] ] => destruct (euclid a b) end.
-    auto.
-  -
-    destruct a.
-    cbv [proj1_sig mod_inv_eucl_sig].
-    rewrite Z.mul_comm.
-    eapply exist_reduced_eq.
-    rewrite mod_inv_eucl_correct; eauto.
-    intro; destruct H0.
-    eapply exist_reduced_eq. congruence.
+    exist (fun z : BinNums.Z => z = z mod m) (1 mod m) (Z_mod_mod 1 m))}
+     := mod_inv_sig.
+Next Obligation.
+  split.
+  { apply exist_reduced_eq; rewrite Zmod_0_l; reflexivity. }
+  intros Hm [a pfa] Ha'. apply exist_reduced_eq.
+  assert (Hm':0 <= m - 2) by (pose proof prime_ge_2 m Hm; omega).
+  assert (Ha:a mod m<>0) by (intro; apply Ha', exist_reduced_eq; congruence).
+  cbv [proj1_sig mod_inv_sig].
+  transitivity ((a*powmod m a (Z.to_N (m - 2))) mod m); [destruct a; congruence|].
+  rewrite !powmod_Zpow_mod.
+  rewrite Z2N.id by assumption.
+  rewrite Zmult_mod_idemp_r.
+  rewrite <-Z.pow_succ_r by assumption.
+  replace (Z.succ (m - 2)) with (m-1) by omega.
+  rewrite (Zmod_small 1) by omega.
+  apply (fermat_little m Hm a Ha).
 Qed.
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index a2f606f30..8d594e8ce 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -346,8 +346,8 @@ Section VariousModPrime.
   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.
+    unfold F_eqb in H.
+    rewrite !FieldToZ_ZToField, !@FieldToZ_pow_efficient, !Zmod_small in H by omega; assumption.
   Qed.
 
   Lemma sqrt_solutions : forall x y : F q, y ^ 2 = x ^ 2 -> y = x \/ y = opp x.
diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v
index 8ee07fe5d..fc506f61d 100644
--- a/src/Spec/ModularArithmetic.v
+++ b/src/Spec/ModularArithmetic.v
@@ -24,29 +24,24 @@ Coercion FieldToZ {m} (a:F m) : BinNums.Z := proj1_sig a.
 
 Section FieldOperations.
   Context {m : BinInt.Z}.
-
-  (* Coercion without Context {m} --> non-uniform inheritance --> Anomalies *)
-  Let ZToFm := ZToField : BinNums.Z -> F m. Local Coercion ZToFm : BinNums.Z >-> F.
+  Definition zero : F m := ZToField 0.
+  Definition one : F m := ZToField 1.
 
   Definition add (a b:F m) : F m := ZToField (a + b).
   Definition mul (a b:F m) : F m := ZToField (a * b).
-
-  Definition opp_with_spec : { opp : F m -> F m
-                             | forall x, add x (opp x) = 0
-                             } := Pre.opp_impl.
-  Definition opp : F m -> F m := Eval hnf in proj1_sig opp_with_spec.
+  Definition opp (a : F m) : F m := ZToField (0 - a).
   Definition sub (a b:F m) : F m := add a (opp b).
 
   Definition inv_with_spec : { inv : F m -> F m
-                             | inv 0 = 0
+                             | inv zero = zero
                              /\ ( Znumtheory.prime m ->
-                                 forall (a:F m), a <> 0 -> mul a (inv a) = 1 )
+                                 forall a, a <> zero -> mul a (inv 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).
 
   Definition pow_with_spec : { pow : F m -> BinNums.N -> F m
-                             | forall a, pow a 0%N = 1
+                             | forall a, pow a 0%N = one
                              /\ forall x, pow a (1 + x)%N = mul a (pow a x)
                              } := Pre.pow_impl.
   Definition pow : F m -> BinNums.N -> F m := Eval hnf in proj1_sig pow_with_spec.