remove eq_dec from Monoid

9 files changed, 92 insertions, 93 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index 5601b9d28..04598989a 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -1,11 +1,11 @@
 Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid.
 Require Import Crypto.Util.Tactics.
-Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.Notations.
 Require Coq.Numbers.Natural.Peano.NPeano.
 Local Close Scope nat_scope. Local Close Scope type_scope. Local Close Scope core_scope.
 Require Crypto.Tactics.Algebra_syntax.Nsatz.
 Require Export Crypto.Util.FixCoqMistakes.
+Require Export Crypto.Util.Decidable.
 
 Module Import ModuloCoq8485.
   Import NPeano Nat.
@@ -33,14 +33,12 @@ Section Algebra.
         monoid_is_right_identity : is_right_identity;
 
         monoid_op_Proper: Proper (respectful eq (respectful eq eq)) op;
-        monoid_Equivalence : Equivalence eq;
-        monoid_is_eq_dec : DecidableRel eq
+        monoid_Equivalence : Equivalence eq
       }.
     Global Existing Instance monoid_is_associative.
     Global Existing Instance monoid_is_left_identity.
     Global Existing Instance monoid_is_right_identity.
     Global Existing Instance monoid_Equivalence.
-    Global Existing Instance monoid_is_eq_dec.
     Global Existing Instance monoid_op_Proper.
 
     Context {inv:T->T}.
@@ -109,18 +107,19 @@ Section Algebra.
     Global Existing Instance commutative_ring_ring.
     Global Existing Instance commutative_ring_is_commutative.
 
-    Class is_mul_nonzero_nonzero := { mul_nonzero_nonzero : forall x y, x<>0 -> y<>0 -> x*y<>0 }.
+    Class is_zero_product_zero_factor :=
+      { zero_product_zero_factor : forall x y, x*y = 0 -> x = 0 \/ y = 0 }.
 
     Class is_zero_neq_one := { zero_neq_one : zero <> one }.
 
     Class integral_domain :=
       {
         integral_domain_commutative_ring : commutative_ring;
-        integral_domain_is_mul_nonzero_nonzero : is_mul_nonzero_nonzero;
+        integral_domain_is_zero_product_zero_factor : is_zero_product_zero_factor;
         integral_domain_is_zero_neq_one : is_zero_neq_one
       }.
     Global Existing Instance integral_domain_commutative_ring.
-    Global Existing Instance integral_domain_is_mul_nonzero_nonzero.
+    Global Existing Instance integral_domain_is_zero_product_zero_factor.
     Global Existing Instance integral_domain_is_zero_neq_one.
 
     Context {inv:T->T} {div:T->T->T}.
@@ -130,7 +129,7 @@ Section Algebra.
       {
         field_commutative_ring : commutative_ring;
         field_is_left_multiplicative_inverse : is_left_multiplicative_inverse;
-        field_domain_is_zero_neq_one : is_zero_neq_one;
+        field_is_zero_neq_one : is_zero_neq_one;
 
         field_div_definition : forall x y , div x y = x * inv y;
 
@@ -139,7 +138,7 @@ Section Algebra.
       }.
     Global Existing Instance field_commutative_ring.
     Global Existing Instance field_is_left_multiplicative_inverse.
-    Global Existing Instance field_domain_is_zero_neq_one.
+    Global Existing Instance field_is_zero_neq_one.
     Global Existing Instance field_inv_Proper.
     Global Existing Instance field_div_Proper.
   End AddMul.
@@ -505,6 +504,13 @@ Module Ring.
       eapply Group.cancel_left, mul_opp_l.
     Qed.
 
+    Lemma zero_product_iff_zero_factor {Hzpzf:@is_zero_product_zero_factor T eq zero mul} :
+      forall x y : T, eq (mul x y) zero <-> eq x zero \/ eq y zero.
+    Proof.
+      split; eauto using zero_product_zero_factor; [].
+      intros [Hz|Hz]; rewrite Hz; eauto using mul_0_l, mul_0_r.
+    Qed.
+
     Global Instance Ncring_Ring_ops : @Ncring.Ring_ops T zero one add mul sub opp eq.
     Global Instance Ncring_Ring : @Ncring.Ring T zero one add mul sub opp eq Ncring_Ring_ops.
     Proof.
@@ -600,31 +606,14 @@ Module IntegralDomain.
   Section IntegralDomain.
     Context {T eq zero one opp add sub mul} `{@integral_domain T eq zero one opp add sub mul}.
 
-    Lemma mul_nonzero_nonzero_cases (x y : T)
-      : eq (mul x y) zero -> eq x zero \/ eq y zero.
-    Proof.
-      pose proof mul_nonzero_nonzero x y.
-      destruct (dec (eq x zero)); destruct (dec (eq y zero)); intuition.
-    Qed.
-
-    Lemma mul_nonzero_nonzero_iff (x y : T)
-      : ~eq (mul x y) zero <-> ~eq x zero /\ ~eq y zero.
-    Proof.
-      split.
-      { intro H0; split; intro H1; apply H0; rewrite H1.
-        { apply Ring.mul_0_l. }
-        { apply Ring.mul_0_r. } }
-      { intros [? ?] ?; edestruct mul_nonzero_nonzero_cases; eauto with nocore. }
-    Qed.
+    Lemma nonzero_product_iff_nonzero_factors :
+      forall x y : T, ~ eq (mul x y) zero <-> ~ eq x zero /\ ~ eq y zero.
+    Proof. setoid_rewrite Ring.zero_product_iff_zero_factor; intuition. Qed.
 
     Global Instance Integral_domain :
       @Integral_domain.Integral_domain T zero one add mul sub opp eq Ring.Ncring_Ring_ops
                                        Ring.Ncring_Ring Ring.Cring_Cring_commutative_ring.
-    Proof.
-      split; dropRingSyntax.
-      - auto using mul_nonzero_nonzero_cases.
-      - intro bad; symmetry in bad; auto using zero_neq_one.
-    Qed.
+    Proof. split; dropRingSyntax; eauto using zero_product_zero_factor, one_neq_zero. Qed.
   End IntegralDomain.
 End IntegralDomain.
 
@@ -640,21 +629,6 @@ Module Field.
       intros. rewrite commutative. auto using left_multiplicative_inverse.
     Qed.
 
-    Global Instance is_mul_nonzero_nonzero : @is_mul_nonzero_nonzero T eq 0 mul.
-    Proof.
-      constructor. intros x y Hx Hy Hxy.
-      assert (0 = (inv y * (inv x * x)) * y) as H00. (rewrite <-!associative, Hxy, !Ring.mul_0_r; reflexivity).
-      rewrite left_multiplicative_inverse in H00 by assumption.
-      rewrite right_identity in H00.
-      rewrite left_multiplicative_inverse in H00 by assumption.
-      auto using zero_neq_one.
-    Qed.
-
-    Global Instance integral_domain : @integral_domain T eq zero one opp add sub mul.
-    Proof.
-      split; auto using field_commutative_ring, field_domain_is_zero_neq_one, is_mul_nonzero_nonzero.
-    Qed.
-
     Lemma inv_unique x ix : ix * x = one -> ix = inv x.
     Proof.
       intro Hix.
@@ -675,11 +649,27 @@ Module Field.
       { apply left_multiplicative_inverse. }
     Qed.
 
+    Context (eq_dec:DecidableRel eq).
+
+    Global Instance is_mul_nonzero_nonzero : @is_zero_product_zero_factor T eq 0 mul.
+    Proof.
+      split. intros x y Hxy.
+      eapply not_not; try typeclasses eauto; []; intuition idtac; eapply zero_neq_one.
+      transitivity ((inv y * (inv x * x)) * y).
+      - rewrite <-!associative, Hxy, !Ring.mul_0_r; reflexivity.
+      - rewrite left_multiplicative_inverse, right_identity, left_multiplicative_inverse by trivial.
+        reflexivity.
+    Qed.
+
+    Global Instance integral_domain : @integral_domain T eq zero one opp add sub mul.
+    Proof.
+      split; auto using field_commutative_ring, field_is_zero_neq_one, is_mul_nonzero_nonzero.
+    Qed.
   End Field.
 
   Lemma isomorphism_to_subfield_field
         {T EQ ZERO ONE OPP ADD SUB MUL INV DIV}
-        {Equivalence_EQ: @Equivalence T EQ} {eq_dec: DecidableRel EQ}
+        {Equivalence_EQ: @Equivalence T EQ}
         {Proper_OPP:Proper(EQ==>EQ)OPP}
         {Proper_ADD:Proper(EQ==>EQ==>EQ)ADD}
         {Proper_SUB:Proper(EQ==>EQ==>EQ)SUB}
@@ -754,7 +744,7 @@ Module Field.
           field_inv_Proper, field_div_Proper].
       + apply left_multiplicative_inverse.
         symmetry in EQ_zero. rewrite EQ_zero. assumption.
-      + eapply field_domain_is_zero_neq_one; eauto.
+      + eapply field_is_zero_neq_one; eauto.
   Qed.
 
   Section Homomorphism.
@@ -764,39 +754,41 @@ Module Field.
     Local Infix "=" := eq. Local Infix "=" := eq : type_scope.
     Context `{@Ring.is_homomorphism F EQ ONE ADD MUL K eq one add mul phi}.
 
-    Lemma homomorphism_multiplicative_inverse_complete
-       : forall x, (EQ x ZERO -> phi (INV x) = inv (phi x))
-       -> phi (INV x) = inv (phi x).
+    Lemma homomorphism_multiplicative_inverse
+      : forall x, not (EQ x ZERO)
+      -> phi (INV x) = inv (phi x).
     Proof.
       intros.
-      destruct (dec (EQ x ZERO)); auto.
-      assert (phi (MUL (INV x) x) = one) as A. {
-        rewrite left_multiplicative_inverse; auto using Ring.homomorphism_one.
-      }
-      rewrite Ring.homomorphism_mul in A.
-      apply inv_unique in A. assumption.
+      eapply inv_unique.
+      rewrite <-Ring.homomorphism_mul.
+      rewrite left_multiplicative_inverse; auto using Ring.homomorphism_one.
     Qed.
 
-    Lemma homomorphism_multiplicative_inverse
-      : forall x, not (EQ x ZERO)
-      -> phi (INV x) = inv (phi x).
+    Lemma homomorphism_multiplicative_inverse_complete
+          { EQ_dec : DecidableRel EQ }
+       : forall x, (EQ x ZERO -> phi (INV x) = inv (phi x))
+       -> phi (INV x) = inv (phi x).
     Proof.
-      intros. apply homomorphism_multiplicative_inverse_complete. contradiction.
+      intros x ?; destruct (dec (EQ x ZERO)); auto using homomorphism_multiplicative_inverse.
     Qed.
 
-    Lemma homomorphism_div_complete
-      : forall x y, (EQ y ZERO -> phi (INV y) = inv (phi y))
+    Lemma homomorphism_div
+      : forall x y, not (EQ y ZERO)
       -> phi (DIV x y) = div (phi x) (phi y).
     Proof.
       intros. rewrite !field_div_definition.
-      rewrite Ring.homomorphism_mul, homomorphism_multiplicative_inverse_complete. reflexivity. trivial.
+      rewrite Ring.homomorphism_mul, homomorphism_multiplicative_inverse;
+        (eauto || reflexivity).
     Qed.
 
-    Lemma homomorphism_div
-      : forall x y, not (EQ y ZERO)
+    Lemma homomorphism_div_complete
+          { EQ_dec : DecidableRel EQ }
+      : forall x y, (EQ y ZERO -> phi (INV y) = inv (phi y))
       -> phi (DIV x y) = div (phi x) (phi y).
     Proof.
-      intros. apply homomorphism_div_complete. contradiction.
+      intros. rewrite !field_div_definition.
+      rewrite Ring.homomorphism_mul, homomorphism_multiplicative_inverse_complete;
+        (eauto || reflexivity).
     Qed.
   End Homomorphism.
 End Field.
@@ -824,11 +816,11 @@ Ltac guess_field :=
 Ltac field_nonzero_mul_split :=
   repeat match goal with
          | [ H : ?R (?mul ?x ?y) ?zero |- _ ]
-           => apply IntegralDomain.mul_nonzero_nonzero_cases in H; destruct H
+           => apply zero_product_zero_factor in H; destruct H
          | [ |- not (?R (?mul ?x ?y) ?zero) ]
-           => apply IntegralDomain.mul_nonzero_nonzero_iff; split
+           => apply IntegralDomain.nonzero_product_iff_nonzero_factors; split
          | [ H : not (?R (?mul ?x ?y) ?zero) |- _ ]
-           => apply IntegralDomain.mul_nonzero_nonzero_iff in H; destruct H
+           => apply IntegralDomain.nonzero_product_iff_nonzero_factors in H; destruct H
          end.
 
 Ltac field_simplify_eq_if_div :=
@@ -1146,7 +1138,7 @@ Ltac neq01 :=
 Ltac combine_field_inequalities_step :=
   match goal with
   | [ H : not (?R ?x ?zero), H' : not (?R ?x' ?zero) |- _ ]
-    => pose proof (mul_nonzero_nonzero x x' H H'); clear H H'
+    => pose proof (proj2 (IntegralDomain.nonzero_product_iff_nonzero_factors x x') (conj H H')); clear H H'
   | [ H : (?X -> False)%type |- _ ]
     => change (not X) in H
   end.
@@ -1158,7 +1150,7 @@ Ltac combine_field_inequalities_step :=
 Ltac split_field_inequalities_step :=
   match goal with
   | [ H : not (?R (?mul ?x ?y) ?zero) |- _ ]
-    => apply IntegralDomain.mul_nonzero_nonzero_iff in H; destruct H
+    => apply IntegralDomain.nonzero_product_iff_nonzero_factors in H; destruct H
   end.
 Ltac split_field_inequalities :=
   canonicalize_field_inequalities;
@@ -1220,7 +1212,7 @@ Ltac super_nsatz :=
           super_nsatz_internal idtac).
 
 Section ExtraLemmas.
-  Context {F eq zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}.
+  Context {F eq zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div} {eq_dec:DecidableRel eq}.
   Local Infix "+" := add. Local Infix "*" := mul. Local Infix "-" := sub. Local Infix "/" := div.
   Local Notation "0" := zero. Local Notation "1" := one.
   Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
@@ -1331,7 +1323,7 @@ Hint Extern 1 => progress ring_simplify_subterms_in_all : ring_simplify_subterms
 
 
 Section Example.
-  Context {F zero one opp add sub mul inv div} `{F_field:field F eq zero one opp add sub mul inv div}.
+  Context {F zero one opp add sub mul inv div} {F_field:@field F eq zero one opp add sub mul inv div} {eq_dec : DecidableRel (@eq F)}.
   Local Infix "+" := add. Local Infix "*" := mul. Local Infix "-" := sub. Local Infix "/" := div.
   Local Notation "0" := zero. Local Notation "1" := one.
 
@@ -1359,8 +1351,8 @@ Section Z.
   Proof.
     split.
     { apply commutative_ring_Z. }
-    { constructor. intros. apply Z.neq_mul_0; auto. }
-    { constructor. discriminate. }
+    { split. intros. eapply Z.eq_mul_0; assumption. }
+    { split. discriminate. }
   Qed.
 
   Example _example_nonzero_nsatz_contradict_Z x y : Z.mul x y = (Zpos xH) -> not (x = Z0).
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index 4a443fd77..be0a80d1f 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -14,7 +14,8 @@ Module E.
   Section CompleteEdwardsCurveTheorems.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv a d}
             {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {prm:@twisted_edwards_params F Feq Fzero Fone Fadd Fmul a d}.
+            {prm:@twisted_edwards_params F Feq Fzero Fone Fadd Fmul a d}
+            {Feq_dec:DecidableRel Feq}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Notation "0" := Fzero.  Local Notation "1" := Fone.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
@@ -128,10 +129,12 @@ Module E.
   Section Homomorphism.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv Fa Fd}
             {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {Fprm:@twisted_edwards_params F Feq Fzero Fone Fadd Fmul Fa Fd}.
+            {Fprm:@twisted_edwards_params F Feq Fzero Fone Fadd Fmul Fa Fd}
+            {Feq_dec:DecidableRel Feq}.
     Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv Ka Kd}
             {fieldK: @Algebra.field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv}
-            {Kprm:@twisted_edwards_params K Keq Kzero Kone Kadd Kmul Ka Kd}.
+            {Kprm:@twisted_edwards_params K Keq Kzero Kone Kadd Kmul Ka Kd}
+            {Keq_dec:DecidableRel Keq}.
     Context {phi:F->K} {Hphi:@Ring.is_homomorphism F Feq Fone Fadd Fmul
                                                    K Keq Kone Kadd Kmul phi}.
     Context {Ha:Keq (phi Fa) Ka} {Hd:Keq (phi Fd) Kd}.
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index 6b28173e3..189c4d08b 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -15,7 +15,8 @@ Module Extended.
     Import Group Ring Field.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv a d}
             {field:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {prm:@E.twisted_edwards_params F Feq Fzero Fone Fadd Fmul a d}.
+            {prm:@E.twisted_edwards_params F Feq Fzero Fone Fadd Fmul a d}
+            {Feq_dec:DecidableRel Feq}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Notation "0" := Fzero.  Local Notation "1" := Fone.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
@@ -47,7 +48,7 @@ Module Extended.
              | _ => solve [eauto]
              | _ => solve [intuition eauto]
              | _ => solve [etransitivity; eauto]
-             | |- _*_ <> 0 => apply mul_nonzero_nonzero
+             | |- _*_ <> 0 => apply Ring.zero_product_iff_zero_factor
              | [H: _ |- _ ] => solve [intro; apply H; super_nsatz]
              | |- Feq _ _ => super_nsatz
              end.
@@ -195,10 +196,12 @@ Module Extended.
     Import Group Ring Field.
     Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv Fa Fd}
             {fieldF:@field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}
-            {Fprm:@E.twisted_edwards_params F Feq Fzero Fone Fadd Fmul Fa Fd}.
+            {Fprm:@E.twisted_edwards_params F Feq Fzero Fone Fadd Fmul Fa Fd}
+            {Feq_dec:DecidableRel Feq}.
     Context {K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv Ka Kd}
             {fieldK:@field K Keq Kzero Kone Kopp Kadd Ksub Kmul Kinv Kdiv}
-            {Kprm:@E.twisted_edwards_params K Keq Kzero Kone Kadd Kmul Ka Kd}.
+            {Kprm:@E.twisted_edwards_params K Keq Kzero Kone Kadd Kmul Ka Kd}
+            {Keq_dec:DecidableRel Keq}.
     Context {phi:F->K} {Hphi:@Ring.is_homomorphism F Feq Fone Fadd Fmul
                                                    K Keq Kone Kadd Kmul phi}.
     Context {phi_nonzero : forall x, ~ Feq x Fzero -> ~ Keq (phi x) Kzero}.
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
index 705597e15..fe98f5dcc 100644
--- a/src/CompleteEdwardsCurve/Pre.v
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -5,7 +5,7 @@ Require Import Crypto.Util.Notations Crypto.Util.Decidable.
 Generalizable All Variables.
 Section Pre.
   Context {F eq zero one opp add sub mul inv div}
-         `{field F eq zero one opp add sub mul inv div}.
+         `{field F eq zero one opp add sub mul inv div} {eq_dec:DecidableRel eq}.
 
   Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)).
   Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v
index f9eb96072..00fb98133 100644
--- a/src/Encoding/PointEncodingPre.v
+++ b/src/Encoding/PointEncodingPre.v
@@ -16,7 +16,7 @@ Require Export Crypto.Util.FixCoqMistakes.
 
 Generalizable All Variables.
 Section PointEncodingPre.
-  Context {F eq zero one opp add sub mul inv div} `{field F eq zero one opp add sub mul inv div}.
+  Context {F eq zero one opp add sub mul inv div} `{field F eq zero one opp add sub mul inv div} {eq_dec:DecidableRel eq}.
   Local Infix "==" := eq : type_scope.
   Local Notation "a !== b" := (not (a == b)): type_scope.
   Local Notation "0" := zero.  Local Notation "1" := one.
@@ -26,7 +26,6 @@ Section PointEncodingPre.
 
   Add Field EdwardsCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)).
 
-  Context {eq_dec:forall x y : F, {x==y}+{x==y->False} }.
   Definition F_eqb x y := if eq_dec x y then true else false.
   Lemma F_eqb_iff : forall x y, F_eqb x y = true <-> x == y.
   Proof.
@@ -62,10 +61,10 @@ Section PointEncodingPre.
     onCurve (sqrt (solve_for_x2 y), y).
   Proof.
     intros.
-    apply E.solve_correct.
+    eapply E.solve_correct.
     eapply square_sqrt.
     symmetry.
-    apply E.solve_correct; eassumption.
+    eapply E.solve_correct. eassumption.
   Qed.
 
   (* TODO : move? *)
@@ -239,6 +238,7 @@ Section PointEncodingPre.
     edestruct dec; [ | congruence_option_coord ].
     break_if; [ | congruence_option_coord].
     break_if; [ congruence_option_coord | ].
+    repeat match goal with [H:  _ = _ :> Decidable _ |- _ ] => clear H end.
     apply E.solve_correct in e.
     break_if; eapply prod_eq_onCurve;
       eauto using inversion_option_coordinates_eq, solve_onCurve, solve_opp_onCurve.
diff --git a/src/Experiments/SpecEd25519.v b/src/Experiments/SpecEd25519.v
index 1299ad650..692254512 100644
--- a/src/Experiments/SpecEd25519.v
+++ b/src/Experiments/SpecEd25519.v
@@ -104,9 +104,9 @@ Lemma sqrt_minus1_valid : ((F.of_Z q 2 ^ Z.to_N (q / 4)) ^ 2 = F.opp 1)%F.
 Proof. vm_decide_no_check. Qed.
 
 Local Notation point := (@E.point (F q) eq 1%F F.add F.mul a d).
-Local Notation zero := (E.zero(H:=F.field_modulo q)).
-Local Notation add := (E.add(H0:=curve25519params)).
-Local Infix "*" := (E.mul(H0:=curve25519params)).
+Local Notation zero := (E.zero(field:=F.field_modulo q)).
+Local Notation add := (E.add(H:=curve25519params)).
+Local Infix "*" := (E.mul(H:=curve25519params)).
 Axiom H : forall n : nat, word n -> word (b + b).
 Axiom B : point. (* TODO: B = decodePoint (y=4/5, x="positive") *)
 Axiom B_nonzero : B <> zero.
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index 16a1217ce..584013015 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -1,4 +1,5 @@
 Require Crypto.CompleteEdwardsCurve.Pre.
+Require Crypto.Util.Decidable.
 
 Module E.
   Section TwistedEdwardsCurves.
@@ -8,7 +9,7 @@ Module E.
     * <https://eprint.iacr.org/2015/677.pdf>
     *)
 
-    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} `{Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} `{field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
     Local Notation "0" := Fzero.  Local Notation "1" := Fone.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
diff --git a/src/Spec/WeierstrassCurve.v b/src/Spec/WeierstrassCurve.v
index e2c99a8fe..484a67c89 100644
--- a/src/Spec/WeierstrassCurve.v
+++ b/src/Spec/WeierstrassCurve.v
@@ -9,7 +9,7 @@ Module E.
      * <http://cs.ucsb.edu/~koc/ccs130h/2013/EllipticHyperelliptic-CohenFrey.pdf> (page 79)
      *)
 
-    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} `{Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {field:@Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} {Feq_dec:Decidable.DecidableRel Feq}.
     Local Infix "=" := Feq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_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.
diff --git a/src/WeierstrassCurve/Pre.v b/src/WeierstrassCurve/Pre.v
index aeffc3a2b..039ffad8a 100644
--- a/src/WeierstrassCurve/Pre.v
+++ b/src/WeierstrassCurve/Pre.v
@@ -8,7 +8,7 @@ Local Open Scope core_scope.
 
 Generalizable All Variables.
 Section Pre.
-  Context {F eq zero one opp add sub mul inv div} `{field F eq zero one opp add sub mul inv div}.
+  Context {F eq zero one opp add sub mul inv div} {field:@field F eq zero one opp add sub mul inv div} {eq_dec: DecidableRel eq}.
   Local Infix "=" := eq. Local Notation "a <> b" := (not (a = b)).
   Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
   Local Notation "0" := zero.  Local Notation "1" := one.