move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems

5 files changed, 317 insertions, 394 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index b5eb4a7f5..f6b2fa330 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -1,6 +1,6 @@
 Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid.
-Require Import Util.Tactics.
-Close Scope nat_scope. Close Scope type_scope. Close Scope core_scope.
+Require Import Crypto.Util.Tactics Crypto.Nsatz.
+Local Close Scope nat_scope. Local Close Scope type_scope. Local Close Scope core_scope.
 
 Section Algebra.
   Context {T:Type} {eq:T->T->Prop}.
@@ -22,11 +22,18 @@ Section Algebra.
       {
         monoid_is_associative : is_associative;
         monoid_is_left_identity : is_left_identity;
-        monoid_is_right_identity : is_right_identity
+        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 : is_eq_dec
       }.
     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}.
     Class is_left_inverse := { left_inverse : forall x, op (inv x) x = id }.
@@ -38,17 +45,11 @@ Section Algebra.
         group_is_left_inverse : is_left_inverse;
         group_is_right_inverse : is_right_inverse;
 
-        group_Equivalence : Equivalence eq;
-        group_is_eq_dec : is_eq_dec;
-        group_op_Proper: Proper (respectful eq (respectful eq eq)) op;
         group_inv_Proper: Proper (respectful eq eq) inv
       }.
     Global Existing Instance group_monoid.
     Global Existing Instance group_is_left_inverse.
     Global Existing Instance group_is_right_inverse.
-    Global Existing Instance group_Equivalence.
-    Global Existing Instance group_is_eq_dec.
-    Global Existing Instance group_op_Proper.
     Global Existing Instance group_inv_Proper.
 
     Class is_commutative := { commutative : forall x y, op x y = op y x }.
@@ -137,45 +138,63 @@ Section Algebra.
 End Algebra.
 
 
-Section GenericCancellation.
-  Context {T:Type} {eq:T->T->Prop} {Equivalence_eq : Equivalence eq}.
-  Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
-  Context {op:T->T->T} {Proper_op : Proper(respectful eq (respectful eq eq)) op}.
-  Context {id:T}.
-  
-  Context {Hassoc: is_associative (op:=op) (eq:=eq)}.
-  Context {Hrid: is_right_identity (op:=op) (eq:=eq) (id := id)}.
-  Context {Hlid: is_left_identity (op:=op) (eq:=eq) (id:=id) }.
+Module Monoid.
+  Section Monoid.
+    Context {T eq op id} {monoid:@monoid T eq op id}.
+    Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
+    Local Infix "*" := op.
 
-  Lemma cancel_right z iz (Hinv:op z iz = id) :
-    forall x y, op x z = op y z <-> x = y.
-  Proof.
-    split; intros.
-    { assert (op (op x z) iz = op (op y z) iz) as Hcut by (f_equiv; assumption).
-      rewrite <-associative in Hcut.
-      rewrite <-!associative, !Hinv, !right_identity in Hcut; exact Hcut. }
-    { f_equiv; assumption. }
-  Qed.
+    Lemma cancel_right z iz (Hinv:op z iz = id) :
+      forall x y, x * z = y * z <-> x = y.
+    Proof.
+      split; intros.
+      { assert (op (op x z) iz = op (op y z) iz) as Hcut by (f_equiv; assumption).
+        rewrite <-associative in Hcut.
+        rewrite <-!associative, !Hinv, !right_identity in Hcut; exact Hcut. }
+      { f_equiv; assumption. }
+    Qed.
 
-  Lemma cancel_left z iz (Hinv:op iz z = id) :
-    forall x y, op z x = op z y <-> x = y.
-  Proof.
-    split; intros.
-    { assert (op iz (op z x) = op iz (op z y)) as Hcut by (f_equiv; assumption).
-      rewrite !associative, !Hinv, !left_identity in Hcut; exact Hcut. }
-    { f_equiv; assumption. }
-  Qed.
-End GenericCancellation.
+    Lemma cancel_left z iz (Hinv:op iz z = id) :
+      forall x y, z * x = z * y <-> x = y.
+    Proof.
+      split; intros.
+      { assert (op iz (op z x) = op iz (op z y)) as Hcut by (f_equiv; assumption).
+        rewrite !associative, !Hinv, !left_identity in Hcut; exact Hcut. }
+      { f_equiv; assumption. }
+    Qed.
+
+    Lemma inv_inv x ix iix : ix*x = id -> iix*ix = id -> iix = x. 
+    Proof.
+      intros Hi Hii.
+      assert (H:op iix id = op iix (op ix x)) by (rewrite Hi; reflexivity).
+      rewrite associative, Hii, left_identity, right_identity in H; exact H.
+    Qed.
+
+    Lemma inv_op x y ix iy : ix*x = id -> iy*y = id -> (iy*ix)*(x*y) =id.
+    Proof.
+      intros Hx Hy.
+      cut (iy * (ix*x) * y = id); try intro H.
+      { rewrite <-!associative; rewrite <-!associative in H; exact H. }
+      rewrite Hx, right_identity, Hy. reflexivity.
+    Qed.
+    
+  End Monoid.
+End Monoid.
 
 Module Group.
   Section BasicProperties.
     Context {T eq op id inv} `{@group T eq op id inv}.
     Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
-
-    Lemma cancel_left : forall z x y, op z x = op z y <-> x = y.
-    Proof. eauto using cancel_left, left_inverse. Qed.
-    Lemma cancel_right : forall z x y, op x z = op y z <-> x = y.
-    Proof. eauto using cancel_right, right_inverse. Qed.
+    Local Infix "*" := op.
+
+    Lemma cancel_left : forall z x y, z*x = z*y <-> x = y.
+    Proof. eauto using Monoid.cancel_left, left_inverse. Qed.
+    Lemma cancel_right : forall z x y, x*z = y*z <-> x = y.
+    Proof. eauto using Monoid.cancel_right, right_inverse. Qed.
+    Lemma inv_inv x : inv(inv(x)) = x.
+    Proof. eauto using Monoid.inv_inv, left_inverse. Qed.
+    Lemma inv_op x y : (inv y*inv x)*(x*y) =id.
+    Proof. eauto using Monoid.inv_op, left_inverse. Qed.
   End BasicProperties.
 
   Section Homomorphism.
@@ -240,12 +259,12 @@ Module Ring.
     Local Notation "0" := zero. Local Notation "1" := one.
     Local Infix "+" := add. Local Infix "-" := sub. Local Infix "*" := mul.
 
-    Lemma mul_0_r : forall x, x * 0 = 0.
+    Lemma mul_0_r : forall x, 0 * x = 0.
     Proof.
       intros.
-      assert (x*0 = x*0) as Hx by reflexivity.
-      rewrite <-(left_identity 0), left_distributive in Hx at 1.
-      assert (x*0 + x*0 - x*0 = x*0 - x*0) as Hxx by (f_equiv; exact Hx).
+      assert (0*x = 0*x) as Hx by reflexivity.
+      rewrite <-(right_identity 0), right_distributive in Hx at 1.
+      assert (0*x + 0*x - 0*x = 0*x - 0*x) as Hxx by (f_equiv; exact Hx).
       rewrite !ring_sub_definition, <-associative, right_inverse, right_identity in Hxx; exact Hxx.
     Qed.
 
@@ -258,6 +277,37 @@ Module Ring.
       rewrite associative, left_inverse, left_identity in Hxx; exact Hxx.
     Qed.
 
+    Lemma sub_0_l x : 0 - x = opp x.
+    Proof. rewrite ring_sub_definition. rewrite left_identity. reflexivity. Qed.
+
+    Lemma mul_opp_r x y : x * opp y = opp (x * y).
+    Proof.
+      assert (Ho:x*(opp y) + x*y = 0)
+        by (rewrite <-left_distributive, left_inverse, mul_0_l; reflexivity).
+      rewrite <-(left_identity (opp (x*y))), <-Ho; clear Ho.
+      rewrite <-!associative, right_inverse, right_identity; reflexivity.
+    Qed.
+
+    Lemma mul_opp_l x y : opp x * y = opp (x * y).
+    Proof.
+      assert (Ho:opp x*y + x*y = 0)
+        by (rewrite <-right_distributive, left_inverse, mul_0_r; reflexivity).
+      rewrite <-(left_identity (opp (x*y))), <-Ho; clear Ho.
+      rewrite <-!associative, right_inverse, right_identity; reflexivity.
+    Qed.
+
+    Global Instance is_left_distributive_sub : is_left_distributive (eq:=eq)(add:=sub)(mul:=mul).
+    Proof.
+      split; intros. rewrite !ring_sub_definition, left_distributive.
+      eapply Group.cancel_left, mul_opp_r.
+    Qed.
+
+    Global Instance is_right_distributive_sub : is_right_distributive (eq:=eq)(add:=sub)(mul:=mul).
+    Proof.
+      split; intros. rewrite !ring_sub_definition, right_distributive.
+      eapply Group.cancel_left, mul_opp_l.
+    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.
@@ -266,6 +316,8 @@ Module Ring.
         eapply @left_identity; eauto with typeclass_instances.
       - eapply @right_identity; eauto with typeclass_instances.
       - eapply associative.
+      - intros; eapply right_distributive.
+      - intros; eapply left_distributive.
     Qed.
     
     Lemma opp_nonzero_nonzero : forall x, x <> 0 -> opp x <> 0.
@@ -361,7 +413,7 @@ Module Field.
     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 by (rewrite <-!associative, Hxy, !Ring.mul_0_r; reflexivity).
+      assert (0 = (inv y * (inv x * x)) * y) as H00. (rewrite <-!associative, Hxy, !Ring.mul_0_l; reflexivity).
       rewrite left_multiplicative_inverse in H00 by assumption.
       rewrite right_identity in H00.
       rewrite left_multiplicative_inverse in H00 by assumption.
@@ -456,128 +508,6 @@ Ltac field_simplify_eq_hyps :=
 Ltac field_simplify_eq_all := field_simplify_eq_hyps; try field_simplify_eq.
 
 
-(*** Tactics for manipulating polynomial equations *)
-Require Nsatz.
-Require Import List.
-Open Scope core_scope.
-
-Generalizable All Variables.
-Lemma cring_sub_diag_iff {R zero eq sub} `{cring:Cring.Cring (R:=R) (ring0:=zero) (ring_eq:=eq) (sub:=sub)}
-  : forall x y, eq (sub x y) zero <-> eq x y.
-Proof.
-  split;intros Hx.
-  { eapply Nsatz.psos_r1b. eapply Hx. }
-  { eapply Nsatz.psos_r1. eapply Hx. }
-Qed.
-
-Ltac get_goal := lazymatch goal with |- ?g => g end.
-
-Ltac nsatz_equation_implications_to_list eq zero g :=
-  lazymatch g with
-  | eq ?p zero => constr:(p::nil)
-  | eq ?p zero -> ?g => let l := nsatz_equation_implications_to_list eq zero g in constr:(p::l)
-  end.
-
-Ltac nsatz_reify_equations eq zero :=
-  let g := get_goal in
-  let lb := nsatz_equation_implications_to_list eq zero g in
-  lazymatch (eval red in (Ncring_tac.list_reifyl (lterm:=lb))) with
-    (?variables, ?le) =>
-    lazymatch (eval compute in (List.rev le)) with
-    | ?reified_goal::?reified_givens => constr:(variables, reified_givens, reified_goal)
-    end
-  end.
-
-Ltac nsatz_get_free_variables reified_package :=
-  lazymatch reified_package with (?fv, _, _) => fv end.
-
-Ltac nsatz_get_reified_givens reified_package :=
-  lazymatch reified_package with (_, ?givens, _) => givens end.
-
-Ltac nsatz_get_reified_goal reified_package :=
-  lazymatch reified_package with (_, _, ?goal) => goal end.
-
-Require Import Coq.setoid_ring.Ring_polynom.
-Ltac nsatz_compute_to_goal sugar nparams reified_goal power reified_givens :=
-  nsatz_compute (PEc sugar :: PEc nparams :: PEpow reified_goal power :: reified_givens).
-
-Ltac nsatz_compute_get_leading_coefficient :=
-  lazymatch goal with
-    |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => a
-  end.
-
-Ltac nsatz_compute_get_certificate :=
-  lazymatch goal with
-    |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => constr:(c,b)
-  end.
-
-Ltac nsatz_rewrite_and_revert domain :=
-  lazymatch type of domain with
-  | @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
-    lazymatch goal with
-    | |- eq _ zero => idtac
-    | |- eq _ _ => rewrite <-(cring_sub_diag_iff (cring:=FCring))
-    end;
-    repeat match goal with
-           | [H : eq _ zero |- _ ] => revert H
-           | [H : eq _ _ |- _ ] => rewrite <-(cring_sub_diag_iff (cring:=FCring)) in H; revert H
-           end
-  end.
-  
-Ltac nsatz_nonzero := 
-  try solve [apply Integral_domain.integral_domain_one_zero
-            |apply Integral_domain.integral_domain_minus_one_zero
-            |trivial
-            |apply Ring.opp_nonzero_nonzero;trivial].
-
-Ltac nsatz_domain_sugar_power domain sugar power := 
-  let nparams := constr:(BinInt.Zneg BinPos.xH) in (* some symbols can be "parameters", treated as coefficients *)
-  lazymatch type of domain with
-  | @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
-    nsatz_rewrite_and_revert domain;
-    let reified_package := nsatz_reify_equations eq zero in
-    let fv := nsatz_get_free_variables reified_package in
-    let interp := constr:(@Nsatz.PEevalR _ _ _ _ _ _ _ _ Fops fv) in
-    let reified_givens := nsatz_get_reified_givens reified_package in
-    let reified_goal := nsatz_get_reified_goal reified_package in
-    nsatz_compute_to_goal sugar nparams reified_goal power reified_givens;
-    let a := nsatz_compute_get_leading_coefficient in
-    let crt := nsatz_compute_get_certificate in
-    intros _ (* discard [nsatz_compute] output *); intros;
-    apply (fun Haa refl cond => @Integral_domain.Rintegral_domain_pow _ _ _ _ _ _ _ _ _ _ _ domain (interp a) _ (BinNat.N.to_nat power) Haa (@Nsatz.check_correct _ _ _ _ _ _ _ _ _ _ FCring fv reified_givens (PEmul a (PEpow reified_goal power)) crt refl cond));
-    [ nsatz_nonzero; cbv iota beta delta [Nsatz.PEevalR PEeval InitialRing.gen_phiZ InitialRing.gen_phiPOS]
-    | solve [vm_compute; exact (eq_refl true)] (* exact_no_check (eq_refl true) *)
-    | solve [repeat (split; [assumption|]); exact I] ]
-  end.
-
-Ltac nsatz_guess_domain :=
-  match goal with
-  | |- ?eq _ _ => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
-  | |- not (?eq _ _) =>  constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
-  | [H: ?eq _ _ |- _ ] =>  constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
-  | [H: not (?eq _ _) |- _] =>  constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
-  end.
-
-Ltac nsatz_sugar_power sugar power :=
-  let domain := nsatz_guess_domain in
-  nsatz_domain_sugar_power domain sugar power.
-
-Tactic Notation "nsatz" constr(n) :=
-  let nn := (eval compute in (BinNat.N.of_nat n)) in
-  nsatz_sugar_power BinInt.Z0 nn.
-
-Tactic Notation "nsatz" := nsatz 1%nat || nsatz 2%nat || nsatz 3%nat || nsatz 4%nat || nsatz 5%nat.
-
-Ltac nsatz_contradict :=
-  intros;
-  let domain := nsatz_guess_domain in
-  lazymatch type of domain with
-  | @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
-    assert (eq one zero) as Hbad;
-    [nsatz; nsatz_nonzero
-    |destruct (Integral_domain.integral_domain_one_zero (Integral_domain:=domain) Hbad)]
-  end.
-
 (*** Polynomial equations over fields *)
 
 Ltac field_algebra :=
@@ -587,6 +517,7 @@ Ltac field_algebra :=
   repeat (apply conj);
   try solve
       [nsatz_nonzero
+      |apply Ring.opp_nonzero_nonzero;trivial
       |unfold not; intro; nsatz_contradict].
 
 Section Example.
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index 88ae9578c..4ad76856e 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -1,47 +1,32 @@
 Require Export Crypto.Spec.CompleteEdwardsCurve.
 
-Require Import Crypto.ModularArithmetic.FField.
-Require Import Crypto.ModularArithmetic.FNsatz.
+Require Import Crypto.Algebra Crypto.Nsatz.
 Require Import Crypto.CompleteEdwardsCurve.Pre.
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Coq.Logic.Eqdep_dec.
 Require Import Crypto.Tactics.VerdiTactics.
 
 Module E.
+  Import Group Ring Field CompleteEdwardsCurve.E.
   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_p' : (@Ffield_theory q _)
-      (morphism (@Fring_morph q),
-       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]).
-  
-    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 xy1 xy2 pf1 pf2,
-      xy1 = xy2 -> exist E.onCurve xy1 pf1 = exist E.onCurve xy2 pf2.
-    Proof.
-      destruct xy1, xy2; intros; find_injection; intros; subst. apply f_equal.
-      apply UIP_dec, F_eq_dec. (* this is a hack. We actually don't care about the equality of the proofs. However, we *can* prove it, and knowing it lets us use the universal equality instead of a type-specific equivalence, which makes many things nicer. *)
-    Qed. Hint Resolve point_eq.
+    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}.
+    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.
+    Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
+    Local Notation "x ^2" := (x*x) (at level 30).
+    Local Notation point := (@point F Feq Fone Fadd Fmul a d).
+    Local Notation onCurve := (@onCurve F Feq Fone Fadd Fmul a d).
+
+    Add Field _edwards_curve_theorems_field : (field_theory_for_stdlib_tactic (H:=field)).
   
-    Definition point_eqb (p1 p2:E.point) : bool := andb
-        (F_eqb (fst (proj1_sig p1)) (fst (proj1_sig p2)))
-        (F_eqb (snd (proj1_sig p1)) (snd (proj1_sig p2))).
+    Definition eq (P Q:point) :=
+      let Feq2 (ab xy:F*F) := fst ab = fst xy /\ snd ab = snd xy in
+      Feq2 (coordinates P) (coordinates Q).
+    Infix "=" := eq : E_scope.
   
+    (* TODO:port
     Local Ltac t :=
       unfold point_eqb;
         repeat match goal with
@@ -94,207 +79,94 @@ Module E.
     Proof.
       intros. destruct (point_eq_dec p1 p2); eauto using point_eqb_complete, point_eqb_neq_complete.
     Qed.
-  
-    Ltac Edefn := unfold E.add, E.add', E.zero; intros;
-                    repeat match goal with
-                           | [ p : E.point |- _ ] =>
-                             let x := fresh "x" p in
-                             let y := fresh "y" p in
-                             let pf := fresh "pf" p in
-                             destruct p as [[x y] pf]; unfold E.onCurve in pf
-                    | _ => eapply point_eq, (f_equal2 pair)
-                    | _ => eapply point_eq
-    end.
-    Lemma add_comm : forall A B, (A+B = B+A)%E.
-    Proof.
-      Edefn; apply (f_equal2 div); ring.
-    Qed.
-  
-    Ltac unifiedAdd_nonzero := match goal with
-    | [ |- (?op 1 (d * _ * _ * _ * _ *
-      inv (1 - d * ?xA * ?xB * ?yA * ?yB) * inv (1 + d * ?xA * ?xB * ?yA * ?yB)))%F <> 0%F]
-      => let Hadd := fresh "Hadd" in
-       pose proof (@unifiedAdd'_onCurve _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d (xA, yA) (xB, yB)) as Hadd;
-       simpl in Hadd;
-       match goal with
-       | [H : (1 - d * ?xC * xB * ?yC * yB)%F <> 0%F |- (?op 1 ?other)%F <> 0%F] =>
-         replace other with
-          (d * xC * ((xA * yB + yA * xB) / (1 + d * xA * xB * yA * yB)) 
-          * yC * ((yA * yB - a * xA * xB) / (1 - d * xA * xB * yA * yB)))%F by (subst; unfold div; ring);
-          auto
-      end
-    end.
-  
-    Lemma add_assoc : forall A B C, (A+(B+C) = (A+B)+C)%E.
-    Proof.
-      Edefn; F_field_simplify_eq; try abstract (rewrite ?@F_pow_2_r in *; clear_prm; F_nsatz);
-        pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d);
-        pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d);
-        cbv beta iota in *;
-        repeat split; field_nonzero idtac; unifiedAdd_nonzero.
-    Qed.
-  
-    Lemma add_0_r : forall P, (P + E.zero = P)%E.
-    Proof.
-      Edefn; 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; exact eq_refl.
-    Qed.
+    *)
 
-    Lemma add_0_l : forall P, (E.zero + P)%E = P.
-    Proof.
-      intros; rewrite add_comm. apply add_0_r.
-    Qed.
+    (* TODO: move to util *)
+    Lemma decide_and  : forall P Q, {P}+{not P} -> {Q}+{not Q} -> {P/\Q}+{not(P/\Q)}.
+    Proof. intros; repeat match goal with [H:{_}+{_}|-_] => destruct H end; intuition. Qed.
 
-    Lemma mul_0_l : forall P, (0 * P = E.zero)%E.
-    Proof.
-      auto.
-    Qed.
+    Ltac destruct_points := 
+      repeat match goal with
+             | [ p : point |- _ ] =>
+               let x := fresh "x" p in
+               let y := fresh "y" p in
+               let pf := fresh "pf" p in
+               destruct p as [[x y] pf]
+             end.
 
-    Lemma mul_S_l : forall n P, (S n * P)%E = (P + n * P)%E.
-    Proof.
-      auto.
-    Qed.
+    Ltac expand_opp :=
+      rewrite ?mul_opp_r, ?mul_opp_l, ?ring_sub_definition, ?inv_inv, <-?ring_sub_definition.
 
-    Lemma mul_add_l : forall a b P, ((a + b)%nat * P)%E = E.add (a * P)%E (b * P)%E.
-    Proof.
-      induction a; intros; rewrite ?plus_Sn_m, ?plus_O_n, ?mul_S_l, ?mul_0_l, ?add_0_l, ?mul_S_, ?IHa, ?add_assoc; auto.
-    Qed.
+    Local Hint Resolve char_gt_2.
+    Local Hint Resolve nonzero_a.
+    Local Hint Resolve square_a.
+    Local Hint Resolve nonsquare_d.
+    Local Hint Resolve @edwardsAddCompletePlus.
+    Local Hint Resolve @edwardsAddCompleteMinus.
+  
+    Program Definition opp (P:point) : point :=
+      exist _ (let '(x, y) := coordinates P in (Fopp x, y) ) _.
+    Solve All Obligations using intros; destruct_points; simpl; field_algebra.
 
-    Lemma mul_assoc : forall (n m : nat) P, (n * (m * P) = (n * m)%nat * P)%E.
+    Global Instance edwards_acurve_abelian_group : abelian_group (eq:=eq)(op:=add)(id:=zero)(inv:=opp).
     Proof.
-      induction n; intros; auto.
-      rewrite ?mul_S_l, ?Mult.mult_succ_l, ?mul_add_l, ?IHn, add_comm. reflexivity.
+        repeat match goal with
+               | |- _ => progress intros
+               | [H: _ /\ _ |- _ ] => destruct H
+               | |- _ => progress destruct_points
+               | |- _ => progress cbv [fst snd coordinates proj1_sig eq add zero opp] in *
+               | |- _ => split
+               | |- Feq _ _ => common_denominator_all; try nsatz
+               | |- _ <> 0 => expand_opp; solve [nsatz_nonzero|eauto]
+               | |- {_}+{_} => eauto 15 using decide_and, @eq_dec with typeclass_instances
+               end.
+        (* TODO: port denominator-nonzero proofs for associativity *)
+        match goal with | |- _ <> 0 => admit end.
+        match goal with | |- _ <> 0 => admit end.
+        match goal with | |- _ <> 0 => admit end.
+        match goal with | |- _ <> 0 => admit end.
     Qed.
 
-    Lemma mul_zero_r : forall m, (m * E.zero = E.zero)%E.
-    Proof.
-      induction m; rewrite ?mul_S_l, ?add_0_l; auto.
-    Qed.
-  
-    (* solve for x ^ 2 *)
-    Definition solve_for_x2 (y : F q) := ((y ^ 2 - 1) / (d * (y ^ 2) - a))%F.
-  
-    Lemma d_y2_a_nonzero : (forall y, 0 <> d * y ^ 2 - a)%F.
-      intros ? eq_zero.
-      pose proof prime_q.
-      destruct square_a as [sqrt_a sqrt_a_id].
-      rewrite <- sqrt_a_id in eq_zero.
-      destruct (Fq_square_mul_sub _ _ _ eq_zero) as [ [sqrt_d sqrt_d_id] | a_zero].
-      + pose proof (nonsquare_d sqrt_d); auto.
-      + subst.
-        rewrite Fq_pow_zero in sqrt_a_id by congruence.
-        auto using nonzero_a.
-    Qed.
-  
-    Lemma a_d_y2_nonzero : (forall y, a - d * y ^ 2 <> 0)%F.
-    Proof.
-      intros y eq_zero.
-      pose proof prime_q.
-      eapply F_minus_swap in eq_zero.
-      eauto using (d_y2_a_nonzero y).
-    Qed.
-  
-    Lemma solve_correct : forall x y, E.onCurve (x, y) <->
-      (x ^ 2 = solve_for_x2 y)%F.
+    (* TODO: move to [Group] and [AbelianGroup] as appropriate *)
+    Lemma mul_0_l : forall P, (0 * P = zero)%E.
+    Proof. intros; reflexivity. Qed.
+    Lemma mul_S_l : forall n P, (S n * P = P + n * P)%E.
+    Proof. intros; reflexivity. Qed.
+    Lemma mul_add_l : forall (n m:nat) (P:point), ((n + m)%nat * P = n * P + m * P)%E.
     Proof.
-      split.
-      + intro onCurve_x_y.
-        pose proof prime_q.
-        unfold E.onCurve in onCurve_x_y.
-        eapply F_div_mul; auto using (d_y2_a_nonzero y).
-        replace (x ^ 2 * (d * y ^ 2 - a))%F with ((d * x ^ 2 * y ^ 2) - (a * x ^ 2))%F by ring.
-        rewrite F_sub_add_swap.
-        replace (y ^ 2 + a * x ^ 2)%F with (a * x ^ 2 + y ^ 2)%F by ring.
-        rewrite onCurve_x_y.
-        ring.
-      + intro x2_eq.
-        unfold E.onCurve, solve_for_x2 in *.
-        rewrite x2_eq.
-        field.
-        auto using d_y2_a_nonzero.
+      induction n; intros;
+        rewrite ?plus_Sn_m, ?plus_O_n, ?mul_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity.
     Qed.
-  
-  
-    Definition opp' (xy:(F q*F q)) : (F q * F q) := let '(x, y) := xy in (opp x, y).
-    Definition opp (P:E.point) : E.point. exists (opp' (proj1_sig P)).
-    Proof.
-      destruct P as [[]]; simpl; rewrite F_square_opp; trivial.
-    Defined.
-    
-    Definition sub P Q := (P + opp Q)%E.
-    
-    Lemma opp_zero : opp E.zero = E.zero.
-    Proof.
-      pose proof @F_opp_0.
-      unfold opp, opp', E.zero; simpl; eapply point_eq; congruence.
-    Qed.
-  
-    Lemma add_opp_r : forall P, (P + opp P = E.zero)%E.
-    Proof.
-      unfold opp, opp'; Edefn; rewrite ?@F_pow_2_r in *; (F_field_simplify_eq; [clear_prm; F_nsatz|..]);
-        rewrite <-?@F_pow_2_r in *;
-        pose proof (@edwardsAddCompletePlus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d _ _ _ _ pfP pfP);
-        pose proof (@edwardsAddCompleteMinus _ _ _ _ two_lt_q nonzero_a square_a nonsquare_d _ _ _ _ pfP pfP);
-        field_nonzero idtac.
-    Qed.
-  
-    Lemma add_opp_l : forall P, (opp P + P = E.zero)%E.
+    Lemma mul_assoc : forall (n m : nat) P, (n * (m * P) = (n * m)%nat * P)%E.
     Proof.
-      intros. rewrite add_comm. eapply add_opp_r.
+      induction n; intros; [reflexivity|].
+      rewrite ?mul_S_l, ?Mult.mult_succ_l, ?mul_add_l, ?IHn, commutative; reflexivity.
     Qed.
-  
-    Lemma add_cancel_r : forall A B C, (B+A = C+A -> B = C)%E.
+    Lemma mul_zero_r : forall m, (m * E.zero = E.zero)%E.
+    Proof. induction m; rewrite ?mul_S_l, ?left_identity, ?IHm; try reflexivity. Qed.
+    (*
+    Lemma opp_mul : forall n P, (opp (n * P) = n * (opp P))%E.
     Proof.
-      intros.
-      assert ((B + A) + opp A = (C + A) + opp A)%E as Hc by congruence.
-      rewrite <-!add_assoc, !add_opp_r, !add_0_r in Hc; exact Hc.
+      induction n. intros. simpl. admit.
     Qed.
+     *)
   
-    Lemma add_cancel_l : forall A B C, (A+B = A+C -> B = C)%E.
-    Proof.
-      intros.
-      rewrite (add_comm A C) in H.
-      rewrite (add_comm A B) in H.
-      eauto using add_cancel_r.
-    Qed.
-    
-    Lemma shuffle_eq_add_opp : forall P Q R, (P + Q = R <-> Q = opp P + R)%E.
-    Proof.
-      split; intros.
-      { assert (opp P + (P + Q) = opp P + R)%E as Hc by congruence.
-        rewrite add_assoc, add_opp_l, add_comm, add_0_r in Hc; exact Hc. }
-      { subst. rewrite add_assoc, add_opp_r, add_comm, add_0_r; reflexivity. }
-    Qed.
-        
-    Lemma opp_opp : forall P, opp (opp P) = P.
-    Proof.
-      intros.
-      pose proof (add_opp_r P%E) as H.
-      rewrite add_comm in H.
-      rewrite shuffle_eq_add_opp in H.
-      rewrite add_0_r in H.
-      congruence.
-    Qed.
-    
-    Lemma opp_add : forall P Q, opp (P + Q)%E = (opp P + opp Q)%E.
-    Proof.
-      intros.
-      pose proof (add_opp_r (P+Q)%E) as H.
-      rewrite <-!add_assoc in H.
-      rewrite add_comm in H.
-      rewrite <-!add_assoc in H.
-      rewrite shuffle_eq_add_opp in H.
-      rewrite add_comm in H.
-      rewrite shuffle_eq_add_opp in H.
-      rewrite add_0_r in H.
-      assumption.
-    Qed.
+
+    Section PointCompression.
+      Local Notation "x ^2" := (x*x).
+      Definition solve_for_x2 (y : F) := ((y^2 - 1) / (d * (y^2) - a)).
       
-    Lemma opp_mul : forall n P, opp (E.mul n P) = E.mul n (opp P).
-    Proof.
-      pose proof opp_add; pose proof opp_zero.
-      induction n; trivial; intros; rewrite !mul_S_l, opp_add; congruence.
-    Qed.
+      Lemma a_d_y2_nonzero : forall y, d * y^2 - a <> 0.
+      Proof.
+        intros ? eq_zero.
+        destruct square_a as [sqrt_a sqrt_a_id]; rewrite <- sqrt_a_id in eq_zero.
+        destruct (eq_dec y 0); [apply nonzero_a|apply nonsquare_d with (sqrt_a/y)]; field_algebra.
+      Qed.
+      
+      Lemma solve_correct : forall x y, onCurve (x, y) <-> (x^2 = solve_for_x2 y).
+      Proof.
+        unfold solve_for_x2; simpl; split; intros; field_algebra; auto using a_d_y2_nonzero.
+      Qed.
+    End PointCompression.
   End CompleteEdwardsCurveTheorems.
-End E.
-Infix "-" := E.sub : E_scope.
\ No newline at end of file
+End E.
\ No newline at end of file
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index fe7600784..4e0ba461e 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -154,9 +154,10 @@ Section FandZ.
   Proof.
     repeat split; Fdefn.
     { 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. }
     { apply F_eq_dec. }
+    { 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. }
+    { apply F_eq_dec. }
   Qed.
 
   Lemma ZToField_0 : @ZToField m 0 = 0.
diff --git a/src/Nsatz.v b/src/Nsatz.v
new file mode 100644
index 000000000..c8a648626
--- /dev/null
+++ b/src/Nsatz.v
@@ -0,0 +1,119 @@
+(*** Tactics for manipulating polynomial equations *)
+Require Nsatz.
+Require Import List.
+
+Generalizable All Variables.
+Lemma cring_sub_diag_iff {R zero eq sub} `{cring:Cring.Cring (R:=R) (ring0:=zero) (ring_eq:=eq) (sub:=sub)}
+  : forall x y, eq (sub x y) zero <-> eq x y.
+Proof.
+  split;intros Hx.
+  { eapply Nsatz.psos_r1b. eapply Hx. }
+  { eapply Nsatz.psos_r1. eapply Hx. }
+Qed.
+
+Ltac get_goal := lazymatch goal with |- ?g => g end.
+
+Ltac nsatz_equation_implications_to_list eq zero g :=
+  lazymatch g with
+  | eq ?p zero => constr:(p::nil)
+  | eq ?p zero -> ?g => let l := nsatz_equation_implications_to_list eq zero g in constr:(p::l)
+  end.
+
+Ltac nsatz_reify_equations eq zero :=
+  let g := get_goal in
+  let lb := nsatz_equation_implications_to_list eq zero g in
+  lazymatch (eval red in (Ncring_tac.list_reifyl (lterm:=lb))) with
+    (?variables, ?le) =>
+    lazymatch (eval compute in (List.rev le)) with
+    | ?reified_goal::?reified_givens => constr:(variables, reified_givens, reified_goal)
+    end
+  end.
+
+Ltac nsatz_get_free_variables reified_package :=
+  lazymatch reified_package with (?fv, _, _) => fv end.
+
+Ltac nsatz_get_reified_givens reified_package :=
+  lazymatch reified_package with (_, ?givens, _) => givens end.
+
+Ltac nsatz_get_reified_goal reified_package :=
+  lazymatch reified_package with (_, _, ?goal) => goal end.
+
+Require Import Coq.setoid_ring.Ring_polynom.
+Ltac nsatz_compute_to_goal sugar nparams reified_goal power reified_givens :=
+  nsatz_compute (PEc sugar :: PEc nparams :: PEpow reified_goal power :: reified_givens).
+
+Ltac nsatz_compute_get_leading_coefficient :=
+  lazymatch goal with
+    |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => a
+  end.
+
+Ltac nsatz_compute_get_certificate :=
+  lazymatch goal with
+    |- Logic.eq ((?a :: _ :: ?b) :: ?c) _ -> _ => constr:(c,b)
+  end.
+
+Ltac nsatz_rewrite_and_revert domain :=
+  lazymatch type of domain with
+  | @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
+    lazymatch goal with
+    | |- eq _ zero => idtac
+    | |- eq _ _ => rewrite <-(cring_sub_diag_iff (cring:=FCring))
+    end;
+    repeat match goal with
+           | [H : eq _ zero |- _ ] => revert H
+           | [H : eq _ _ |- _ ] => rewrite <-(cring_sub_diag_iff (cring:=FCring)) in H; revert H
+           end
+  end.
+  
+Ltac nsatz_nonzero := 
+  try solve [apply Integral_domain.integral_domain_one_zero
+            |apply Integral_domain.integral_domain_minus_one_zero
+            |trivial].
+
+Ltac nsatz_domain_sugar_power domain sugar power := 
+  let nparams := constr:(BinInt.Zneg BinPos.xH) in (* some symbols can be "parameters", treated as coefficients *)
+  lazymatch type of domain with
+  | @Integral_domain.Integral_domain ?F ?zero _ _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
+    nsatz_rewrite_and_revert domain;
+    let reified_package := nsatz_reify_equations eq zero in
+    let fv := nsatz_get_free_variables reified_package in
+    let interp := constr:(@Nsatz.PEevalR _ _ _ _ _ _ _ _ Fops fv) in
+    let reified_givens := nsatz_get_reified_givens reified_package in
+    let reified_goal := nsatz_get_reified_goal reified_package in
+    nsatz_compute_to_goal sugar nparams reified_goal power reified_givens;
+    let a := nsatz_compute_get_leading_coefficient in
+    let crt := nsatz_compute_get_certificate in
+    intros _ (* discard [nsatz_compute] output *); intros;
+    apply (fun Haa refl cond => @Integral_domain.Rintegral_domain_pow _ _ _ _ _ _ _ _ _ _ _ domain (interp a) _ (BinNat.N.to_nat power) Haa (@Nsatz.check_correct _ _ _ _ _ _ _ _ _ _ FCring fv reified_givens (PEmul a (PEpow reified_goal power)) crt refl cond));
+    [ nsatz_nonzero; cbv iota beta delta [Nsatz.PEevalR PEeval InitialRing.gen_phiZ InitialRing.gen_phiPOS]
+    | solve [vm_compute; exact (eq_refl true)] (* exact_no_check (eq_refl true) *)
+    | solve [repeat (split; [assumption|]); exact I] ]
+  end.
+
+Ltac nsatz_guess_domain :=
+  match goal with
+  | |- ?eq _ _ => constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
+  | |- not (?eq _ _) =>  constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
+  | [H: ?eq _ _ |- _ ] =>  constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
+  | [H: not (?eq _ _) |- _] =>  constr:(_:Integral_domain.Integral_domain (ring_eq:=eq))
+  end.
+
+Ltac nsatz_sugar_power sugar power :=
+  let domain := nsatz_guess_domain in
+  nsatz_domain_sugar_power domain sugar power.
+
+Tactic Notation "nsatz" constr(n) :=
+  let nn := (eval compute in (BinNat.N.of_nat n)) in
+  nsatz_sugar_power BinInt.Z0 nn.
+
+Tactic Notation "nsatz" := nsatz 1%nat || nsatz 2%nat || nsatz 3%nat || nsatz 4%nat || nsatz 5%nat.
+
+Ltac nsatz_contradict :=
+  intros;
+  let domain := nsatz_guess_domain in
+  lazymatch type of domain with
+  | @Integral_domain.Integral_domain _ ?zero ?one _ _ _ _ ?eq ?Fops ?FRing ?FCring =>
+    assert (eq one zero) as Hbad;
+    [nsatz; nsatz_nonzero
+    |destruct (Integral_domain.integral_domain_one_zero (Integral_domain:=domain) Hbad)]
+  end.
\ No newline at end of file
diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
index 518d3d551..5df36e295 100644
--- a/src/Spec/CompleteEdwardsCurve.v
+++ b/src/Spec/CompleteEdwardsCurve.v
@@ -8,11 +8,11 @@ Module E.
     * <https://eprint.iacr.org/2015/677.pdf>
     *)
 
-    Context {F eq Fzero one opp Fadd sub Fmul inv div} `{Algebra.field F eq Fzero one opp Fadd sub Fmul inv div}.
-    Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
-    Local Notation "0" := Fzero.  Local Notation "1" := one.
+    Context {F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv} `{Algebra.field F Feq Fzero Fone Fopp Fadd Fsub Fmul Finv Fdiv}.
+    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.
-    Local Infix "-" := sub. Local Infix "/" := div.
+    Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
     Local Notation "x ^2" := (x*x) (at level 30).
 
     Context {a d: F}.