CompleteEdwardsCurveTheorems: associativity proof that times out on Qed

4 files changed, 65 insertions, 155 deletions

diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index 5e6fd7b42..01b3584c0 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -1,6 +1,7 @@
 Require Export Crypto.Spec.CompleteEdwardsCurve.
 
 Require Import Crypto.ModularArithmetic.FField.
+Require Import Crypto.ModularArithmetic.FNsatz.
 Require Import Crypto.CompleteEdwardsCurve.Pre.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Eqdep_dec.
@@ -22,6 +23,12 @@ Section CompleteEdwardsCurveTheorems.
   Add Field Ffield_notConstant : (OpaqueFieldTheory q)
     (constants [notConstant]). 
 
+  Ltac clear_prm :=
+    generalize dependent a; intro a; intros;
+    generalize dependent d; intro d; intros;
+    generalize dependent prime_q; intro prime_q; intros;
+    generalize dependent q; intro q; intros;
+    clear prm.
 
   Lemma point_eq : forall p1 p2, p1 = p2 -> forall pf1 pf2,
     mkPoint p1 pf1 = mkPoint p2 pf2.
@@ -48,157 +55,10 @@ Section CompleteEdwardsCurveTheorems.
 
   Lemma twistedAddAssoc : forall A B C, (A+(B+C) = (A+B)+C)%E.
   Proof.
-    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 *)
+    (* The Ltac takes ~15s, the Qed takes longer than I have had patience for *)
+    Edefn; F_field_simplify_eq; try abstract (rewrite ?@F_pow_2_r in *; clear_prm; F_nsatz);
+      repeat split; match goal with [ |- _ = 0%F -> False ] => admit end;
+        fail "unreachable".
   Admitted.
 
   Lemma zeroIsIdentity : forall P, (P + zero = P)%E.
diff --git a/src/ModularArithmetic/FNsatz.v b/src/ModularArithmetic/FNsatz.v
new file mode 100644
index 000000000..a0f34073d
--- /dev/null
+++ b/src/ModularArithmetic/FNsatz.v
@@ -0,0 +1,40 @@
+Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Require Export Crypto.ModularArithmetic.FField.
+Require Import Nsatz.
+
+Ltac FqAsIntegralDomain :=
+  lazymatch goal with [H:Znumtheory.prime ?q |- _ ] =>
+    pose proof (_:@Integral_domain.Integral_domain (F q) _ _ _ _ _ _ _ _ _ _) as FqIntegralDomain;
+    lazymatch type of FqIntegralDomain with @Integral_domain.Integral_domain _ _ _ _ _ _ _ _ ?ringOps ?ringOk ?ringComm =>
+      generalize dependent ringComm; intro Cring;
+      generalize dependent ringOk; intro Ring;
+      generalize dependent ringOps; intro RingOps;
+      lazymatch type of RingOps with @Ncring.Ring_ops ?t ?z ?o ?a ?m ?s ?p ?e =>
+        generalize dependent e; intro equiv;
+        generalize dependent p; intro opp;
+        generalize dependent s; intro sub;
+        generalize dependent m; intro mul;
+        generalize dependent a; intro add;
+        generalize dependent o; intro one;
+        generalize dependent z; intro zero;
+        generalize dependent t; intro R
+      end
+    end; intros;
+    clear q H
+  end.
+
+Ltac fixed_equality_to_goal H x y := generalize (psos_r1 x y H); clear H.
+Ltac fixed_equalities_to_goal :=
+  match goal with
+  | H:?x == ?y |- _ => fixed_equality_to_goal H x y
+  | H:_ ?x ?y |- _ => fixed_equality_to_goal H x y
+  | H:_ _ ?x ?y |- _ => fixed_equality_to_goal H x y
+  | H:_ _ _ ?x ?y |- _ => fixed_equality_to_goal H x y
+  | H:_ _ _ _ ?x ?y |- _ => fixed_equality_to_goal H x y
+  end.
+Ltac fixed_nsatz :=
+  intros; try apply psos_r1b;
+   lazymatch goal with
+   | |- @equality ?T _ _ _ => repeat fixed_equalities_to_goal; nsatz_generic 6%N 1%Z (@nil T) (@nil T)
+  end.
+Ltac F_nsatz := abstract (FqAsIntegralDomain; fixed_nsatz).
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index 4602e8781..f39cc4176 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -581,6 +581,16 @@ Section VariousModulo.
     Fdefn.
   Qed.
 
+  Lemma F_pow_2_r : forall x : F m, x^2 = x*x.
+  Proof.
+    intros. ring.
+  Qed.
+
+  Lemma F_pow_3_r : forall x : F m, x^3 = x*x*x.
+  Proof.
+    intros. ring.
+  Qed.
+
   Lemma F_pow_add : forall (x : F m) k j, x ^ j * x ^ k = x ^ (j + k).
   Proof.
     intros.
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index e32b4b093..40af15dac 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -324,8 +324,8 @@ Section VariousModPrime.
     apply F_add_reg_l in opp_spec; auto.
   Qed.
 
-  Instance Fq_Ring_ops : @Ring_ops (F q) 0 1 add mul sub opp eq.
-  Instance Fq_Ring: @Ring (F q) 0 1 add mul sub opp eq Fq_Ring_ops.
+  Global Instance Fq_Ring_ops : @Ring_ops (F q) 0 1 add mul sub opp eq.
+  Global Instance Fq_Ring: @Ring (F q) 0 1 add mul sub opp eq Fq_Ring_ops.
   Proof.
     econstructor; eauto with typeclass_instances;
       unfold R2, equality, eq_notation, addition, add_notation, one, one_notation,
@@ -333,12 +333,12 @@ Section VariousModPrime.
       sub_notation, opposite, opp_notation; intros; ring.
     Qed.
 
-  Instance Fq_Cring: @Cring (F q) 0 1 add mul sub opp eq Fq_Ring_ops Fq_Ring.
+  Global Instance Fq_Cring: @Cring (F q) 0 1 add mul sub opp eq Fq_Ring_ops Fq_Ring.
   Proof.
     repeat intro. apply F_mul_comm.
   Qed.
 
-  Instance Fq_Integral_domain : @Integral_domain (F q) 0 1 add mul sub opp eq Fq_Ring_ops Fq_Ring Fq_Cring.
+  Global Instance Fq_Integral_domain : @Integral_domain (F q) 0 1 add mul sub opp eq Fq_Ring_ops Fq_Ring Fq_Cring.
   Proof.
     econstructor; eauto using Fq_mul_zero_why, Fq_1_neq_0.
   Qed.