remove field_algebra

2 files changed, 13 insertions, 16 deletions

diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index 263582508..d8efb82f3 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -33,6 +33,7 @@ Module Extended.
     Create HintDb bash discriminated.
     Local Hint Unfold E.eq fst snd fieldwise fieldwise' coordinates E.coordinates proj1_sig Pre.onCurve : bash.
     Ltac bash :=
+      pose proof E.char_gt_2;
       repeat match goal with
              | |- Proper _ _ => intro
              | _ => progress intros
@@ -43,15 +44,11 @@ Module Extended.
              | |- _ /\ _ => split
              | _ => solve [neq01]
              | _ => solve [eauto]
-             | _ => solve [intuition]
+             | _ => solve [intuition eauto]
              | _ => solve [etransitivity; eauto]
-             | |- Feq _ _ => field_algebra
-             | |- _ <> 0 => apply mul_nonzero_nonzero
-             | [ H : _ <> 0 |- _ <> 0 ] =>
-               intro; apply H;
-               field_algebra;
-               solve [ apply Ring.opp_nonzero_nonzero, E.char_gt_2
-                     | apply E.char_gt_2]
+             | |- _*_ <> 0 => apply mul_nonzero_nonzero
+             | [H: _ |- _ ] => solve [intro; apply H; super_nsatz]
+             | |- Feq _ _ => super_nsatz
              end.
 
     Obligation Tactic := bash.
@@ -63,8 +60,7 @@ Module Extended.
       (let '(X,Y,Z,T) := coordinates P in ((X/Z), (Y/Z))) _.
 
     Definition eq (P Q:point) := E.eq (to_twisted P) (to_twisted Q).
-    Global Instance DecidableRel_eq : Decidable.DecidableRel eq.
-    Proof. typeclasses eauto. Qed.
+    Global Instance DecidableRel_eq : Decidable.DecidableRel eq := _.
 
     Local Hint Unfold from_twisted to_twisted eq : bash.
 
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
index 432e834aa..a83c85b02 100644
--- a/src/CompleteEdwardsCurve/Pre.v
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -50,24 +50,25 @@ Section Pre.
         => apply d_nonsquare with (sqrt_d:= (f (sqrt_a * x1) (d * x1 * x2 * y1 * y2 * y1))
                                            /(f (sqrt_a * x2) y2   *   x1 * y1           ))
       | _ => apply a_nonzero
-      end; field_algebra; auto using Ring.opp_nonzero_nonzero; nsatz_contradict.
+      end; super_nsatz.
   Qed.
 
   Lemma edwardsAddCompletePlus x1 y1 x2 y2 :
     onCurve (x1, y1) -> onCurve (x2, y2) -> (1 + d*x1*x2*y1*y2) <> 0.
-  Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); field_algebra. Qed.
+  Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); super_nsatz. Qed.
 
   Lemma edwardsAddCompleteMinus x1 y1 x2 y2 :
     onCurve (x1, y1) -> onCurve (x2, y2) -> (1 - d*x1*x2*y1*y2) <> 0.
-  Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); field_algebra. Qed.
+  Proof. intros H1 H2 ?. apply (edwardsAddComplete' _ _ _ _ H1 H2); super_nsatz. Qed.
 
-  Lemma zeroOnCurve : onCurve (0, 1). Proof. simpl. field_algebra. Qed.
+  Lemma zeroOnCurve : onCurve (0, 1). Proof. simpl. super_nsatz. Qed.
 
   Lemma unifiedAdd'_onCurve : forall P1 P2,
     onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2).
   Proof.
-    unfold onCurve, unifiedAdd'; intros [x1 y1] [x2 y2] H1 H2.
-    field_algebra; auto using edwardsAddCompleteMinus, edwardsAddCompletePlus.
+    unfold onCurve, unifiedAdd'; intros [x1 y1] [x2 y2] ? ?.
+    conservative_common_denominator; [ | auto using edwardsAddCompleteMinus, edwardsAddCompletePlus..].
+    nsatz.
   Qed.
 End Pre.