ModularArithmetic: [field] tactic that respects opacity, prettify ExtendedCoordinates, outline Edwards curve associativity

2 files changed, 204 insertions, 90 deletions

diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index dd40a4510..5e6fd7b42 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -1,5 +1,6 @@
 Require Export Crypto.Spec.CompleteEdwardsCurve.
 
+Require Import Crypto.ModularArithmetic.FField.
 Require Import Crypto.CompleteEdwardsCurve.Pre.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Eqdep_dec.
@@ -7,15 +8,21 @@ Require Import Crypto.Tactics.VerdiTactics.
 
 Section CompleteEdwardsCurveTheorems.
   Context {prm:TwistedEdwardsParams}.
+  Local Opaque q a d prime_q two_lt_q nonzero_a square_a nonsquare_d. (* [F_field] calls [compute] *)
   Existing Instance prime_q.
-  Add Field Ffield_Z : (@Ffield_theory q _)
+
+  Add Field Ffield_p' : (@Ffield_theory q _)
     (morphism (@Fring_morph q),
-     preprocess [idtac],
-     postprocess [try exact Fq_1_neq_0; try assumption],
+     preprocess [Fpreprocess],
+     postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
      constants [Fconstant],
      div (@Fmorph_div_theory q),
      power_tac (@Fpower_theory q) [Fexp_tac]). 
 
+  Add Field Ffield_notConstant : (OpaqueFieldTheory q)
+    (constants [notConstant]). 
+
+
   Lemma point_eq : forall p1 p2, p1 = p2 -> forall pf1 pf2,
     mkPoint p1 pf1 = mkPoint p2 pf2.
   Proof.
@@ -36,12 +43,162 @@ Section CompleteEdwardsCurveTheorems.
   end.
   Lemma twistedAddComm : forall A B, (A+B = B+A)%E.
   Proof.
-    Edefn; apply f_equal2; ring.
+    Edefn; apply (f_equal2 div); ring.
   Qed.
 
   Lemma twistedAddAssoc : forall A B C, (A+(B+C) = (A+B)+C)%E.
   Proof.
-    (* http://math.rice.edu/~friedl/papers/AAELLIPTIC.PDF *)
+    intros; Edefn; F_field_simplify_eq.
+    - (* nsatz. *) (* requires IntegralDomain (F q), then gives stack overflow *)
+      admit. (*sage -c "
+R.<d,a,xA,yA,xB,yB,xC,yC> = PolynomialRing(QQ,8,order='invlex')
+I = R.ideal([
+  (a * (xA * xA) + yA * yA) - (1 + d * (xA * xA) * (yA * yA)),
+  (a * (xB * xB) + yB * yB) - (1 + d * (xB * xB) * (yB * yB)),
+  (a * (xC * xC) + yC * yC) - (1 + d * (xC * xC) * (yC * yC))
+])
+
+print ((- xA * xA * xA * yB * yB * yB * yB * yC * yC * xB * xB * xB * xC * d * d * d * yA * yA -
+    xA * xA * xA * yB * yB * yB * yC * yC * yC * a * xB * xB * xC * xC * d * d +
+    xA * xA * xA * yB * yB * yB * yC * a * xB * xB * xB * xB * xC * xC * d * d * d * yA * yA -
+    xA * xA * xA * yB * yB * yB * yC * xB * xB * d * d * yA * yA +
+    xA * xA * xA * yB * yB * yC * yC * a * a * xB * xB * xB * xC * xC * xC * d * d -
+    xA * xA * xA * yB * yB * yC * yC * a * xB * xC * d +
+    xA * xA * xA * yB * yB * a * xB * xB * xB * xC * d * d * yA * yA +
+    xA * xA * xA * yB * yC * a * a * xB * xB * xC * xC * d +
+    xA * xA * yB * yB * yB * yB * yC * yC * yC * xB * xC * xC * d * d * yA +
+    xA * xA * yB * yB * yB * yB * yC * xB * xB * xB * xC * xC * d * d * d * yA * yA * yA +
+    xA * xA * yB * yB * yB * yC * yC * xB * xB * xB * xB * xC * d * d * d * yA * yA * yA +
+    xA * xA * yB * yB * yB * yC * yC * xC * d * yA -
+    xA * xA * yB * yB * yB * xB * xB * xC * d * d * yA * yA * yA -
+    (1 + 1) * xA * xA * yB * yB * yC * a * xB * xC * xC * d * yA -
+    xA * xA * yB * yB * yC * xB * xB * xB * d * d * yA * yA * yA +
+    xA * xA * yB * yC * yC * a * a * xB * xB * xB * xB * xC * xC * xC * d * d * yA -
+    (1 + 1) * xA * xA * yB * yC * yC * a * xB * xB * xC * d * yA +
+    xA * xA * yC * a * a * xB * xB * xB * xC * xC * d * yA -
+    xA * yB * yB * yB * yB * yC * yC * xB * xC * xC * xC * d * d * yA * yA +
+    xA * yB * yB * yB * yC * xC * xC * d * yA * yA +
+    xA * yB * yB * yC * yC * xB * xC * d + (1 + 1) * xA * yB * yB * yC * yC * xB * xC * d * yA * yA +
+    xA * yB * yC * yC * yC * a * xB * xB * xB * xB * xC * xC * d * d * yA * yA -
+    xA * yB * yC * a * xB * xB * xC * xC * d - (1 + 1) * xA * yB * yC * a * xB * xB * xC * xC * d * yA * yA +
+    xA * yB * yC - xA * yC * yC * a * xB * xB * xB * xC * d * yA * yA -
+    xA * a * xB * xC - yB * yB * yB * yC * yC * xB * xB * xC * xC * xC * d * d * yA * yA * yA -
+    yB * yB * yC * yC * yC * xB * xB * xB * xC * xC * d * d * yA * yA * yA -
+    yB * yB * yC * xB * xC * xC * d * yA + yB * yB * yC * xB * xC * xC * d * yA * yA * yA -
+                                           yB * yC * yC * xB * xB * xC * d * yA + yB * yC * yC * xB * xB * xC * d * yA * yA * yA +
+    yB * xC * yA + yC * xB * yA - (
+    - xA * xA * xA * yB * yB * yB * yB * yC * yC * xB * xC * d * d * yA * yA -
+    xA * xA * xA * yB * yB * yB * yC * yC * yC * xB * xB * d * d * yA * yA +
+    xA * xA * xA * yB * yB * a * a * xB * xB * xB * xC * xC * xC * d * d * yA * yA +
+    xA * xA * xA * yB * yC * a * a * xB * xB * xB * xB * xC * xC * d * d * yA * yA +
+    xA * xA * yB * yB * yB * yB * yC * yC * yC * xB * xB * xB * xC * xC * d * d * d * yA +
+    xA * xA * yB * yB * yB * yB * yC * xB * xC * xC * d * d * yA * yA * yA +
+    xA * xA * yB * yB * yB * yC * yC * a * xB * xB * xB * xB * xC * xC * xC * d * d * d * yA +
+    xA * xA * yB * yB * yB * yC * yC * xC * d * yA -
+    xA * xA * yB * yB * yB * a * xB * xB * xC * xC * xC * d * d * yA * yA * yA -
+    xA * xA * yB * yB * yC * yC * yC * xB * xB * xB * d * d * yA * yA * yA +
+    xA * xA * yB * yB * yC * yC * yC * xB * d * yA -
+    (1 + 1) * xA * xA * yB * yB * yC * a * xB * xC * xC * d * yA -
+    xA * xA * yB * yB * yC * xB * d * yA +
+    xA * xA * yB * yC * yC * a * xB * xB * xB * xB * xC * d * d * yA * yA * yA -
+    (1 + 1) * xA * xA * yB * yC * yC * a * xB * xB * xC * d * yA +
+    xA * xA * yB * a * a * xB * xB * xC * xC * xC * d * yA -
+    xA * xA * yB * a * xB * xB * xC * d * yA + xA * xA * yC * a * a * xB * xB * xB * xC * xC * d * yA -
+                                               xA * yB * yB * yB * yB * yC * yC * xB * xB * xB * xC * xC * xC * d * d * d * yA * yA +
+    xA * yB * yB * yB * yC * yC * yC * xB * xB * xB * xB * xC * xC * d * d * d * yA * yA -
+    xA * yB * yB * yB * yC * yC * yC * xB * xB * xC * xC * d * d +
+    xA * yB * yB * yB * yC * xC * xC * d * yA * yA +
+    xA * yB * yB * yC * yC * a * xB * xB * xB * xC * xC * xC * d * d +
+    (1 + 1) * xA * yB * yB * yC * yC * xB * xC * d * yA * yA -
+    xA * yB * yB * a * xB * xC * xC * xC * d * yA * yA +
+    xA * yB * yB * xB * xC * d * yA * yA + xA * yB * yC * yC * yC * xB * xB * d * yA * yA -
+                                           (1 + 1) * xA * yB * yC * a * xB * xB * xC * xC * d * yA * yA -
+                                           xA * yB * yC * xB * xB * d * yA * yA + xA * yB * yC -
+                                                                                  xA * yC * yC * a * xB * xB * xB * xC * d * yA * yA -
+                                                                                  xA * a * xB * xC - yB * yB * yB * yC * yC * xB * xB * xC * xC * xC * d * d * yA -
+                                                                                  yB * yB * yC * yC * yC * xB * xB * xB * xC * xC * d * d * yA +
+    yB * xC * yA + yC * xB * yA))
+    in I)"*)
+    - admit. (* nonzero demonimator conditions, to be resolved as in ExtendedCoordinates.v *)
+    - (* nsatz. *) (* requires IntegralDomain (F q), then gives stack overflow *)
+      admit. (* sage -c "
+R.<d,a,xA,yA,xB,yB,xC,yC> = PolynomialRing(QQ,8,order='invlex')
+I = R.ideal([
+  (a * (xA * xA) + yA * yA) - (1 + d * (xA * xA) * (yA * yA)),
+  (a * (xB * xB) + yB * yB) - (1 + d * (xB * xB) * (yB * yB)),
+  (a * (xC * xC) + yC * yC) - (1 + d * (xC * xC) * (yC * yC))
+])
+
+print (((- yA * yA * yA * yB * yB * yB * yB * yC * yC * xB * xB * xB * xC * 1 * d * d * d * xA * xA -
+    yA * yA * yA * yB * yB * yB * yC * yC * yC * xB * xB * xC * xC * d * d +
+    yA * yA * yA * yB * yB * yB * yC * a * xB * xB * xB * xB * xC * xC * 1 * d * d * d * xA * xA -
+    yA * yA * yA * yB * yB * yB * yC * xB * xB * 1 * 1 * d * d * xA * xA +
+    yA * yA * yA * yB * yB * yC * yC * a * xB * xB * xB * xC * xC * xC * d * d -
+    yA * yA * yA * yB * yB * yC * yC * xB * xC * 1 * d +
+    yA * yA * yA * yB * yB * a * xB * xB * xB * xC * 1 * 1 * d * d * xA * xA +
+    yA * yA * yA * yB * yC * a * xB * xB * xC * xC * 1 * d -
+    yA * yA * yB * yB * yB * yB * yC * yC * yC * xB * xC * xC * d * d * xA -
+    yA * yA * yB * yB * yB * yB * yC * a * xB * xB * xB * xC * xC * 1 * d * d * d * xA * xA * xA -
+    yA * yA * yB * yB * yB * yC * yC * a * xB * xB * xB * xB * xC * 1 * d * d * d * xA * xA * xA -
+    yA * yA * yB * yB * yB * yC * yC * xC * 1 * d * xA +
+    yA * yA * yB * yB * yB * a * xB * xB * xC * 1 * 1 * d * d * xA * xA * xA +
+    yA * yA * yB * yB * yC * a * xB * xB * xB * 1 * 1 * d * d * xA * xA * xA +
+    (1 + 1) * yA * yA * yB * yB * yC * a * xB * xC * xC * 1 * d * xA -
+    yA * yA * yB * yC * yC * a * a * xB * xB * xB * xB * xC * xC * xC * d * d * xA +
+    (1 + 1) * yA * yA * yB * yC * yC * a * xB * xB * xC * 1 * d * xA -
+    yA * yA * yC * a * a * xB * xB * xB * xC * xC * 1 * d * xA -
+    yA * yB * yB * yB * yB * yC * yC * a * xB * xC * xC * xC * d * d * xA * xA +
+    yA * yB * yB * yB * yC * a * xC * xC * 1 * d * xA * xA +
+    (1 + 1) * yA * yB * yB * yC * yC * a * xB * xC * 1 * d * xA * xA +
+    yA * yB * yB * yC * yC * xB * xC * 1 * 1 * 1 * d +
+    yA * yB * yC * yC * yC * a * a * xB * xB * xB * xB * xC * xC * d * d * xA * xA -
+    (1 + 1) * yA * yB * yC * a * a * xB * xB * xC * xC * 1 * d * xA * xA -
+    yA * yB * yC * a * xB * xB * xC * xC * 1 * 1 * 1 * d + 
+    yA * yB * yC * 1 * 1 * 1 * 1 - yA * yC * yC * a * a * xB * xB * xB * xC * 1 * d * xA * xA -
+    yA * a * xB * xC * 1 * 1 * 1 * 1 +
+    yB * yB * yB * yC * yC * a * a * xB * xB * xC * xC * xC * d * d * xA * xA * xA +
+    yB * yB * yC * yC * yC * a * a * xB * xB * xB * xC * xC * d * d * xA * xA * xA -
+    yB * yB * yC * a * a * xB * xC * xC * 1 * d * xA * xA * xA +
+    yB * yB * yC * a * xB * xC * xC * 1 * 1 * 1 * d * xA -
+    yB * yC * yC * a * a * xB * xB * xC * 1 * d * xA * xA * xA +
+    yB * yC * yC * a * xB * xB * xC * 1 * 1 * 1 * d * xA - 
+    yB * a * xC * 1 * 1 * 1 * 1 * xA - yC * a * xB * 1 * 1 * 1 * 1 * xA) -
+   (- yA * yA * yA * yB * yB * yB * yB * yC * yC * xB * xC * d * d * xA * xA -
+    yA * yA * yA * yB * yB * yB * yC * yC * yC * xB * xB * d * d * xA * xA +
+    yA * yA * yA * yB * yB * a * a * xB * xB * xB * xC * xC * xC * d * d * xA * xA +
+    yA * yA * yA * yB * yC * a * a * xB * xB * xB * xB * xC * xC * d * d * xA * xA -
+    yA * yA * yB * yB * yB * yB * yC * yC * yC * xB * xB * xB * xC * xC * 1 * d * d * d * xA -
+    yA * yA * yB * yB * yB * yB * yC * a * xB * xC * xC * d * d * xA * xA * xA -
+    yA * yA * yB * yB * yB * yC * yC * a * xB * xB * xB * xB * xC * xC * xC * 1 * d * d * d * xA -
+    yA * yA * yB * yB * yB * yC * yC * xC * 1 * d * xA +
+    yA * yA * yB * yB * yB * a * a * xB * xB * xC * xC * xC * d * d * xA * xA * xA +
+    yA * yA * yB * yB * yC * yC * yC * a * xB * xB * xB * d * d * xA * xA * xA -
+    yA * yA * yB * yB * yC * yC * yC * xB * 1 * d * xA +
+    (1 + 1) * yA * yA * yB * yB * yC * a * xB * xC * xC * 1 * d * xA +
+    yA * yA * yB * yB * yC * xB * 1 * 1 * 1 * d * xA -
+    yA * yA * yB * yC * yC * a * a * xB * xB * xB * xB * xC * d * d * xA * xA * xA +
+    (1 + 1) * yA * yA * yB * yC * yC * a * xB * xB * xC * 1 * d * xA -
+    yA * yA * yB * a * a * xB * xB * xC * xC * xC * 1 * d * xA +
+    yA * yA * yB * a * xB * xB * xC * 1 * 1 * 1 * d * xA -
+    yA * yA * yC * a * a * xB * xB * xB * xC * xC * 1 * d * xA -
+    yA * yB * yB * yB * yB * yC * yC * a * xB * xB * xB * xC * xC * xC * 1 * d * d * d * xA * xA +
+    yA * yB * yB * yB * yC * yC * yC * a * xB * xB * xB * xB * xC * xC * 1 * d * d * d * xA * xA -
+    yA * yB * yB * yB * yC * yC * yC * xB * xB * xC * xC * 1 * 1 * d * d +
+    yA * yB * yB * yB * yC * a * xC * xC * 1 * d * xA * xA +
+    yA * yB * yB * yC * yC * a * xB * xB * xB * xC * xC * xC * 1 * 1 * d * d +
+    (1 + 1) * yA * yB * yB * yC * yC * a * xB * xC * 1 * d * xA * xA -
+    yA * yB * yB * a * a * xB * xC * xC * xC * 1 * d * xA * xA +
+    yA * yB * yB * a * xB * xC * 1 * 1 * 1 * d * xA * xA +
+    yA * yB * yC * yC * yC * a * xB * xB * 1 * d * xA * xA -
+    (1 + 1) * yA * yB * yC * a * a * xB * xB * xC * xC * 1 * d * xA * xA -
+    yA * yB * yC * a * xB * xB * 1 * 1 * 1 * d * xA * xA + 
+    yA * yB * yC * 1 * 1 * 1 * 1 - yA * yC * yC * a * a * xB * xB * xB * xC * 1 * d * xA * xA -
+    yA * a * xB * xC * 1 * 1 * 1 * 1 +
+    yB * yB * yB * yC * yC * a * xB * xB * xC * xC * xC * 1 * 1 * d * d * xA +
+    yB * yB * yC * yC * yC * a * xB * xB * xB * xC * xC * 1 * 1 * d * d * xA -
+    yB * a * xC * 1 * 1 * 1 * 1 * xA - yC * a * xB * 1 * 1 * 1 * 1 * xA)) in I)"
+*)
+    - admit. (* nonzero demonimator conditions, to be resolved as in ExtendedCoordinates.v *)
   Admitted.
 
   Lemma zeroIsIdentity : forall P, (P + zero = P)%E.
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index f2eba81eb..226600428 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -1,94 +1,25 @@
 Require Import Crypto.CompleteEdwardsCurve.Pre.
 Require Import Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Import Crypto.ModularArithmetic.FField.
 Require Import Crypto.Tactics.VerdiTactics.
 Local Open Scope F_scope.
 
-Section ExtendedCoordinatesFieldProofs.
-  (* If [field] worked on (F q) when Definition q := someProj someRecord, we
-     could inline this proof into unifiedAdd_repM1 *)
-  Context p (prime_p : Znumtheory.prime p) (two_lt_p : BinInt.Z.lt 2 p).
-  Existing Instance prime_p.
+Section ExtendedCoordinates.
+  Context {prm:TwistedEdwardsParams}.
+  Local Opaque q a d prime_q two_lt_q nonzero_a square_a nonsquare_d. (* [F_field] calls [compute] *)
+  Existing Instance prime_q.
 
-  Add Field GFfield_Z : (@Ffield_theory p _)
-    (morphism (@Fring_morph p),
+  Add Field Ffield_p' : (@Ffield_theory q _)
+    (morphism (@Fring_morph q),
      preprocess [Fpreprocess],
-     postprocess [Fpostprocess],
+     postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
      constants [Fconstant],
-     div (@Fmorph_div_theory p),
-     power_tac (@Fpower_theory p) [Fexp_tac]). 
-  
-  Lemma unifiedAdd_repM1_fieldproof:
-  forall (d XP YP ZP XQ YQ ZQ : F p)
-  (HZP : ZP <> 0)
-  (HZQ : ZQ <> 0)
-  (HoRp : forall x1 y1 x2 y2 : F p,
-    opp 1 * x1 ^ 2 + y1 ^ 2 = 1 + d * x1 ^ 2 * y1 ^ 2 ->
-    opp 1 * x2 ^ 2 + y2 ^ 2 = 1 + d * x2 ^ 2 * y2 ^ 2 ->
-    1 + d * x1 * x2 * y1 * y2 <> 0)
-  (HoRm : forall x1 y1 x2 y2 : F p,
-    opp 1 * x1 ^ 2 + y1 ^ 2 = 1 + d * x1 ^ 2 * y1 ^ 2 ->
-    opp 1 * x2 ^ 2 + y2 ^ 2 = 1 + d * x2 ^ 2 * y2 ^ 2 ->
-    1 - d * x1 * x2 * y1 * y2 <> 0)
-  (HoQ: opp 1 * (XQ / ZQ) ^ 2 + (YQ / ZQ) ^ 2 = 1 + d * (XQ / ZQ) ^ 2 * (YQ / ZQ) ^ 2)
-  (HoP : opp 1 * (XP / ZP) ^ 2 + (YP / ZP) ^ 2 = 1 + d * (XP / ZP) ^ 2 * (YP / ZP) ^ 2),
-      (((YP + XP) * (YQ + XQ) - (YP - XP) * (YQ - XQ)) *
-      (ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) /
-                                                                              ((ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) *
-                                                                              (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ))),
-      (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) *
-      ((YP + XP) * (YQ + XQ) + (YP - XP) * (YQ - XQ)) /
-                                                      ((ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) *
-                                                      (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)))) =
-      ((XP / ZP * (YQ / ZQ) + YP / ZP * (XQ / ZQ)) /
-                                                  (1 + d * (XP / ZP) * (XQ / ZQ) * (YP / ZP) * (YQ / ZQ)),
-      (YP / ZP * (YQ / ZQ) - opp 1 * (XP / ZP) * (XQ / ZQ)) /
-                                                              (1 - d * (XP / ZP) * (XQ / ZQ) * (YP / ZP) * (YQ / ZQ))) /\
-      ((ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) *
-      (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) = 0 ->
-      False) /\
-      ((YP + XP) * (YQ + XQ) - (YP - XP) * (YQ - XQ)) *
-      ((YP + XP) * (YQ + XQ) + (YP - XP) * (YQ - XQ)) =
-      ((YP + XP) * (YQ + XQ) - (YP - XP) * (YQ - XQ)) *
-      (ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) *
-      ((ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) *
-      ((YP + XP) * (YQ + XQ) + (YP - XP) * (YQ - XQ))) /
-                                                      ((ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ)) *
-                                                          (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ))).
-  Proof.
-    intros; repeat split; try apply (f_equal2 pair); try field; auto.
+     div (@Fmorph_div_theory q),
+     power_tac (@Fpower_theory q) [Fexp_tac]). 
 
-    Ltac tnz := eauto 10 using Fq_mul_nonzero_nonzero, (@char_gt_2 p two_lt_p).
-    (* If we we had reasoning modulo associativity and commutativity,
-    *  the following tactic would probably solve all 10 goals here:
-    repeat match goal with [H1: @eq (F p) _ _, H2: @eq (F p) _ _ |- _ ] =>
-      let H := fresh "H" in ( 
-        pose proof (edwardsAddCompletePlus _ _ _ _ H1 H2) as H;
-        match type of H with ?xs <> 0 => ac_rewrite (eq_refl xs) end
-      ) || (
-        pose proof (edwardsAddCompleteMinus _ _ _ _ H1 H2) as H;
-        match type of H with ?xs <> 0 => ac_rewrite (eq_refl xs) end
-      ); tnz
-    end. *)
-
-      - replace (ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ) with (ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ) * (XP / ZP) * (YQ / ZQ) * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  + XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  - XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZQ * ZP * ZQ - d * XP * XQ * YP * YQ) with (ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  + XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  - XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZQ * ZP * ZQ - d * XP * XQ * YP * YQ) with (ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz).
-      repeat apply Fq_mul_nonzero_nonzero.
-        + replace (ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ) ) with (ZToField 2*ZQ*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-        + replace (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ) ) with (ZToField 2*ZQ*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  + XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  - XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
-    Qed.
-End ExtendedCoordinatesFieldProofs.
-
-Section ExtendedCoordinates.
-  Context {prm:TwistedEdwardsParams}.
-  Existing Instance prime_q.
+  Add Field Ffield_notConstant : (OpaqueFieldTheory q)
+    (constants [notConstant]). 
 
   (** [extended] represents a point on an elliptic curve using extended projective
   * Edwards coordinates with twist a=-1 (see <https://eprint.iacr.org/2008/522.pdf>). *)
@@ -174,10 +105,36 @@ Section ExtendedCoordinates.
       P ~= rP -> Q ~= rQ -> (unifiedAddM1 P Q) ~= (unifiedAdd' rP rQ).
     Proof.
       intros P Q rP rQ HoP HoQ HrP HrQ.
-      pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d) as HoRp; simpl in HoRp.
-      pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d) as HoRm; simpl in HoRm.
-      unfoldExtended; rewrite a_eq_minus1 in *.
-      apply unifiedAdd_repM1_fieldproof; auto using prime_q, two_lt_q.
+      pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d).
+      pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d).
+      unfoldExtended; rewrite a_eq_minus1 in *; simpl in *.
+        repeat split; repeat apply (f_equal2 pair); try F_field; repeat split; auto;
+        repeat rewrite ?F_add_0_r, ?F_add_0_l, ?F_sub_0_l, ?F_sub_0_r,
+           ?F_mul_0_r, ?F_mul_0_l, ?F_mul_1_l, ?F_mul_1_r, ?F_div_1_r.
+
+    Ltac tnz := repeat apply Fq_mul_nonzero_nonzero; auto using (@char_gt_2 q two_lt_q).
+    (* If we we had reasoning modulo associativity and commutativity,
+    *  the following tactic would probably solve all remaining goals here:
+    repeat match goal with [H1: @eq (F p) _ _, H2: @eq (F p) _ _ |- _ ] =>
+      let H := fresh "H" in ( 
+        pose proof (edwardsAddCompletePlus _ _ _ _ H1 H2) as H;
+        match type of H with ?xs <> 0 => ac_rewrite (eq_refl xs) end
+      ) || (
+        pose proof (edwardsAddCompleteMinus _ _ _ _ H1 H2) as H;
+        match type of H with ?xs <> 0 => ac_rewrite (eq_refl xs) end
+      ); tnz
+    end. *)
+
+      - replace (ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ) with (ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ) * (XP / ZP) * (YQ / ZQ) * (YP / ZP))) by (field; tnz); tnz.
+      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  + XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
+      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  - XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
+      - replace (ZP * ZQ * ZP * ZQ - d * XP * XQ * YP * YQ) with (ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
+      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  + XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
+      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  - XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
+      - replace (ZP * ZToField 2 * ZQ - XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ) ) with (ZToField 2*ZQ*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
+        replace (ZP * ZToField 2 * ZQ + XP * YP / ZP * ZToField 2 * d * (XQ * YQ / ZQ) ) with (ZToField 2*ZQ*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
+      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  + XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 + d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
+      - replace (ZP * ZToField 2 * ZQ * (ZP * ZQ)  - XP * YP * ZToField 2 * d * (XQ * YQ)) with (ZToField 2*ZQ*ZQ*ZP*ZP* (1 - d * (XQ / ZQ)  * (XP / ZP) * (YQ / ZQ)  * (YP / ZP))) by (field; tnz); tnz.
     Qed.
   End TwistMinus1.
 End ExtendedCoordinates.
\ No newline at end of file