From 969cb56234750c320768ae39e934b18ce2883aef Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 10 Jun 2016 16:43:21 -0400
Subject: 8.5 fixes

---
 src/ModularArithmetic/ModularArithmeticTheorems.v | 53 ++++++++++++-----------
 1 file changed, 27 insertions(+), 26 deletions(-)

(limited to 'src/ModularArithmetic/ModularArithmeticTheorems.v')

diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index dabfcf883..8566177a1 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -1,3 +1,4 @@
+Require Import Coq.omega.Omega.
 Require Import Crypto.Spec.ModularArithmetic.
 Require Import Crypto.ModularArithmetic.Pre.
 
@@ -19,20 +20,20 @@ Section ModularArithmeticPreliminaries.
     f_equal.
     eapply UIP_dec, Z.eq_dec.
   Qed.
-  
+
   Lemma F_opp_spec : forall (a:F m), add a (opp a) = 0.
     intros a.
     pose (@opp_with_spec m) as H.
-    change (@opp m) with (proj1_sig H). 
+    change (@opp m) with (proj1_sig H).
     destruct H; eauto.
   Qed.
-  
+
   Lemma F_pow_spec : forall (a:F m),
       pow a 0%N = 1%F /\ forall x, pow a (1 + x)%N = mul a (pow a x).
   Proof.
     intros a.
     pose (@pow_with_spec m) as H.
-    change (@pow m) with (proj1_sig H). 
+    change (@pow m) with (proj1_sig H).
     destruct H; eauto.
   Qed.
 End ModularArithmeticPreliminaries.
@@ -81,7 +82,7 @@ Ltac eq_remove_proofs := lazymatch goal with
     assert (Q := F_eq a b);
     simpl in *; apply Q; clear Q
 end.
-            
+
 Ltac Fdefn :=
   intros;
   rewrite ?F_opp_spec;
@@ -217,7 +218,7 @@ Section FandZ.
       rewrite ?N2Nat.inj_succ, ?pow_0, <-?N.add_1_l, ?pow_succ;
       simpl; congruence.
   Qed.
-  
+
   Lemma mod_plus_zero_subproof a b : 0 mod m = (a + b) mod m ->
                                      b mod m =  (- a)  mod m.
   Proof.
@@ -244,7 +245,7 @@ Section FandZ.
     intros.
     pose proof (FieldToZ_opp' x) as H; rewrite mod_FieldToZ in H; trivial.
   Qed.
-  
+
   Lemma sub_intersperse_modulus : forall x y, ((x - y) mod m = (x + (m - y)) mod m)%Z.
   Proof.
     intros.
@@ -282,7 +283,7 @@ Section FandZ.
   Proof.
     Fdefn.
   Qed.
- 
+
   (* Compatibility between inject and pow *)
   Lemma ZToField_pow : forall x n,
     @ZToField m x ^ n = ZToField (x ^ (Z.of_N n) mod m).
@@ -317,7 +318,7 @@ End FandZ.
 
 Section RingModuloPre.
   Context {m:Z}.
-  Local Coercion ZToFm := ZToField : Z -> F m. Hint Unfold ZToFm.
+  Local Coercion ZToFm' := ZToField : Z -> F m. Hint Unfold ZToFm'.
   (* Substitution to prove all Compats *)
   Ltac compat := repeat intro; subst; trivial.
 
@@ -362,12 +363,12 @@ Section RingModuloPre.
   Proof.
     Fdefn; rewrite Z.mul_1_r; auto.
   Qed.
-    
+
   Lemma F_mul_assoc:
     forall x y z : F m, x * (y * z) = x * y * z.
   Proof.
     Fdefn.
-  Qed.  
+  Qed.
 
   Lemma F_pow_pow_N (x : F m) : forall (n : N), (x ^ id n)%F = pow_N 1%F mul x n.
   Proof.
@@ -390,7 +391,7 @@ Section RingModuloPre.
   Qed.
 
   (***** Division Theory *****)
-  Definition Fquotrem(a b: F m): F m * F m := 
+  Definition Fquotrem(a b: F m): F m * F m :=
     let '(q, r) := (Z.quotrem a b) in (q : F m, r : F m).
   Lemma Fdiv_theory : div_theory eq (@add m) (@mul m) (@id _) Fquotrem.
   Proof.
@@ -434,7 +435,7 @@ Section RingModuloPre.
   Qed.
 
   (* Redefine our division theory under the ring morphism *)
-  Lemma Fmorph_div_theory: 
+  Lemma Fmorph_div_theory:
       div_theory eq Zplus Zmult (@ZToField m) Z.quotrem.
   Proof.
     constructor; intros; intuition.
@@ -451,7 +452,7 @@ Section RingModuloPre.
     Fdefn.
   Qed.
 End RingModuloPre.
-  
+
 Ltac Fconstant t := match t with @ZToField _ ?x => x | _ => NotConstant end.
 Ltac Fexp_tac t := Ncst t.
 Ltac Fpreprocess := rewrite <-?ZToField_0, ?ZToField_1.
@@ -470,49 +471,49 @@ Module RingModulo (Export M : Modulus).
   Definition ring_morph_modulo := @Fring_morph modulus.
   Definition morph_div_theory_modulo := @Fmorph_div_theory modulus.
   Definition power_theory_modulo := @Fpower_theory modulus.
-  
+
   Add Ring GFring_Z : ring_theory_modulo
     (morphism ring_morph_modulo,
      constants [Fconstant],
      div morph_div_theory_modulo,
-     power_tac power_theory_modulo [Fexp_tac]). 
+     power_tac power_theory_modulo [Fexp_tac]).
 End RingModulo.
 
 Section VariousModulo.
   Context {m:Z}.
-  
+
   Add Ring GFring_Z : (@Fring_theory m)
     (morphism (@Fring_morph m),
      constants [Fconstant],
      div (@Fmorph_div_theory m),
-     power_tac (@Fpower_theory m) [Fexp_tac]). 
+     power_tac (@Fpower_theory m) [Fexp_tac]).
 
   Lemma F_mul_0_l : forall x : F m, 0 * x = 0.
   Proof.
     intros; ring.
   Qed.
-  
+
   Lemma F_mul_0_r : forall x : F m, x * 0 = 0.
   Proof.
     intros; ring.
   Qed.
-  
+
   Lemma F_mul_nonzero_l : forall a b : F m, a*b <> 0 -> a <> 0.
     intros; intuition; subst.
     assert (0 * b = 0) by ring; intuition.
   Qed.
-  
+
   Lemma F_mul_nonzero_r : forall a b : F m, a*b <> 0 -> b <> 0.
     intros; intuition; subst.
     assert (a * 0 = 0) by ring; intuition.
   Qed.
-  
+
   Lemma F_pow_distr_mul : forall (x y:F m) z, (0 <= z)%N ->
     (x ^ z) * (y ^ z) = (x * y) ^ z.
   Proof.
     intros.
     replace z with (Z.to_N (Z.of_N z)) by apply N2Z.id.
-    apply natlike_ind with (x := Z.of_N z); simpl; [ ring | | 
+    apply natlike_ind with (x := Z.of_N z); simpl; [ ring | |
       replace 0%Z with (Z.of_N 0%N) by auto; apply N2Z.inj_le; auto].
     intros z' z'_nonneg IHz'.
     rewrite Z2N.inj_succ by auto.
@@ -521,7 +522,7 @@ Section VariousModulo.
     rewrite <- IHz'.
     ring.
   Qed.
-  
+
   Lemma F_opp_0 : opp (0 : F m) = 0%F.
   Proof.
     intros; ring.
@@ -563,7 +564,7 @@ Section VariousModulo.
   Proof.
     intros; ring.
   Qed.
-  
+
   Lemma F_add_reg_r : forall x y z : F m, y + x = z + x -> y = z.
   Proof.
     intros ? ? ? A.
@@ -653,7 +654,7 @@ Section VariousModulo.
   Proof.
     split; intro A;
       [ replace w with (w - x + x) by ring
-      | replace w with (w + z - z) by ring ]; rewrite A; ring. 
+      | replace w with (w + z - z) by ring ]; rewrite A; ring.
   Qed.
 
   Definition isSquare (x : F m) := exists sqrt_x, sqrt_x ^ 2 = x.
-- 
cgit v1.2.3


From 7129157393f420268c9399dc9b4119469994bf63 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 10 Jun 2016 17:25:28 -0400
Subject: More changes for 8.5

[Local Coercion :=] changed meanings.  Use [Let] and [Local Coercion] for consistent behavior
---
 src/CompleteEdwardsCurve/Pre.v                    | 46 ++++++++++++-----------
 src/ModularArithmetic/ModularArithmeticTheorems.v |  4 +-
 src/ModularArithmetic/Tutorial.v                  | 15 ++++----
 src/Spec/ModularArithmetic.v                      |  6 +--
 4 files changed, 36 insertions(+), 35 deletions(-)

(limited to 'src/ModularArithmetic/ModularArithmeticTheorems.v')

diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
index fea4a99b3..322db1792 100644
--- a/src/CompleteEdwardsCurve/Pre.v
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -1,9 +1,11 @@
 Require Import Coq.ZArith.BinInt Coq.ZArith.Znumtheory Crypto.Tactics.VerdiTactics.
+Require Import Coq.omega.Omega.
 
 Require Import Crypto.Spec.ModularArithmetic.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
+Local Open Scope Z_scope.
 Local Open Scope F_scope.
-  
+
 Section Pre.
   Context {q : BinInt.Z}.
   Context {a : F q}.
@@ -20,8 +22,8 @@ Section Pre.
      postprocess [Fpostprocess],
      constants [Fconstant],
      div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]). 
-  
+     power_tac (@Fpower_theory q) [Fexp_tac]).
+
   (* the canonical definitions are in Spec *)
   Local Notation onCurve P := (let '(x, y) := P in a*x^2 + y^2 = 1 + d*x^2*y^2).
   Local Notation unifiedAdd' P1' P2' := (
@@ -29,7 +31,7 @@ Section Pre.
     let '(x2, y2) := P2' in
     (((x1*y2  +  y1*x2)/(1 + d*x1*x2*y1*y2)) , ((y1*y2 - a*x1*x2)/(1 - d*x1*x2*y1*y2)))
   ).
-  
+
   Lemma char_gt_2 : ZToField 2 <> (0: F q).
     intro; find_injection.
     pose proof two_lt_q.
@@ -38,7 +40,7 @@ Section Pre.
 
   Ltac rewriteAny := match goal with [H: _ = _ |- _ ] => rewrite H end.
   Ltac rewriteLeftAny := match goal with [H: _ = _ |- _ ] => rewrite <- H end.
-  
+
   Ltac whatsNotZero :=
     repeat match goal with
     | [H: ?lhs = ?rhs |- _ ] =>
@@ -67,11 +69,11 @@ Section Pre.
     (d*x1*x2*y1*y2)^2 <> 1.
   Proof.
     intros Hc1 Hc2 Hcontra; simpl in Hc1, Hc2; whatsNotZero.
-  
-    pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero. 
+
+    pose proof char_gt_2. pose proof a_nonzero as Ha_nonzero.
     destruct a_square as [sqrt_a a_square'].
     rewrite <-a_square' in *.
-  
+
     (* Furthermore... *)
     pose proof (eq_refl (d*x1^2*y1^2*(sqrt_a^2*x2^2 + y2^2))) as Heqt.
     rewrite Hc2 in Heqt at 2.
@@ -80,7 +82,7 @@ Section Pre.
     rewrite Hcontra in Heqt.
     replace (d * x1 ^ 2 * y1 ^ 2 + 1) with (1 + d * x1 ^ 2 * y1 ^ 2) in Heqt by field.
     rewrite <-Hc1 in Heqt.
-  
+
     (* main equation for both potentially nonzero denominators *)
     destruct (F_eq_dec (sqrt_a*x2 + y2) 0); destruct (F_eq_dec (sqrt_a*x2 - y2) 0);
       try lazymatch goal with [H: ?f (sqrt_a * x2)  y2 <> 0 |- _ ] =>
@@ -97,11 +99,11 @@ Section Pre.
             destruct (d_nonsquare (n/l)); (remember n; rewriteAny; field; auto)
         end
       end.
-  
+
     assert (Hc: (sqrt_a * x2 + y2) + (sqrt_a * x2 - y2) = 0) by (repeat rewriteAny; field).
-  
+
     replace (sqrt_a * x2 + y2 + (sqrt_a * x2 - y2)) with (ZToField 2 * sqrt_a * x2) in Hc by field.
-  
+
     (* contradiction: product of nonzero things is zero *)
     destruct (Fq_mul_zero_why _ _ Hc) as [Hcc|Hcc]; subst; intuition.
     destruct (Fq_mul_zero_why _ _ Hcc) as [Hccc|Hccc]; subst; intuition.
@@ -119,7 +121,7 @@ Section Pre.
     - replace (d * x1 * x2 * y1 * y2) with (1+d * x1 * x2 * y1 * y2-1) in H by field.
       intro Hz; rewrite Hz in H; intuition.
   Qed.
-  
+
   Lemma edwardsAddCompleteMinus x1 y1 x2 y2 :
     onCurve (x1, y1) ->
     onCurve (x2, y2) ->
@@ -130,27 +132,27 @@ Section Pre.
     - replace (d * x1 * x2 * y1 * y2) with ((1-(1-d * x1 * x2 * y1 * y2))) in H by field.
       intro Hz; rewrite Hz in H; apply H; field.
   Qed.
-  
+
   Definition zeroOnCurve : onCurve (0, 1).
     simpl. field.
   Qed.
-  
+
   Lemma unifiedAdd'_onCurve' x1 y1 x2 y2 x3 y3
     (H: (x3, y3) = unifiedAdd' (x1, y1) (x2, y2)) :
     onCurve (x1, y1) -> onCurve (x2, y2) -> onCurve (x3, y3).
   Proof.
     (* https://eprint.iacr.org/2007/286.pdf Theorem 3.1;
-      * c=1 and an extra a in front of x^2 *) 
-  
+      * c=1 and an extra a in front of x^2 *)
+
     injection H; clear H; intros.
-  
+
     Ltac t x1 y1 x2 y2 :=
       assert ((a*x2^2 + y2^2)*d*x1^2*y1^2
              = (1 + d*x2^2*y2^2) * d*x1^2*y1^2) by (rewriteAny; auto);
       assert (a*x1^2 + y1^2 - (a*x2^2 + y2^2)*d*x1^2*y1^2
              = 1 - d^2*x1^2*x2^2*y1^2*y2^2) by (repeat rewriteAny; field).
     t x1 y1 x2 y2; t x2 y2 x1 y1.
-  
+
     remember ((a*x1^2 + y1^2 - (a*x2^2+y2^2)*d*x1^2*y1^2)*(a*x2^2 + y2^2 -
       (a*x1^2 + y1^2)*d*x2^2*y2^2)) as T.
     assert (HT1: T = (1 - d^2*x1^2*x2^2*y1^2*y2^2)^2) by (repeat rewriteAny; field).
@@ -158,7 +160,7 @@ Section Pre.
     (y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -d * ((x1 *
      y2 + y1 * x2)* (y1 * y2 - a * x1 * x2))^2)) by (subst; field).
     replace (1:F q) with (a*x3^2 + y3^2 -d*x3^2*y3^2); [field|]; subst x3 y3.
-  
+
     match goal with [ |- ?x = 1 ] => replace x with
     ((a * ((x1 * y2 + y1 * x2) * (1 - d * x1 * x2 * y1 * y2)) ^ 2 +
      ((y1 * y2 - a * x1 * x2) * (1 + d * x1 * x2 * y1 * y2)) ^ 2 -
@@ -175,7 +177,7 @@ Section Pre.
       auto using Fq_pow_nonzero, Fq_mul_nonzero_nonzero,
         edwardsAddCompleteMinus, edwardsAddCompletePlus.
   Qed.
-  
+
   Lemma unifiedAdd'_onCurve : forall P1 P2, onCurve P1 -> onCurve P2 ->
     onCurve (unifiedAdd' P1 P2).
   Proof.
@@ -183,4 +185,4 @@ Section Pre.
     remember (unifiedAdd' (f, f0) (f1, f2)) as r; destruct r.
     eapply unifiedAdd'_onCurve'; eauto.
   Qed.
-End Pre.
\ No newline at end of file
+End Pre.
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index 8566177a1..6168f88bd 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -11,7 +11,7 @@ Require Export Crypto.Util.IterAssocOp.
 
 Section ModularArithmeticPreliminaries.
   Context {m:Z}.
-  Local Coercion ZToFm := ZToField : BinNums.Z -> F m. Hint Unfold ZToFm.
+  Let ZToFm := ZToField : BinNums.Z -> F m. Hint Unfold ZToFm. Local Coercion ZToFm : Z >-> F.
 
   Theorem F_eq: forall (x y : F m), x = y <-> FieldToZ x = FieldToZ y.
   Proof.
@@ -318,7 +318,7 @@ End FandZ.
 
 Section RingModuloPre.
   Context {m:Z}.
-  Local Coercion ZToFm' := ZToField : Z -> F m. Hint Unfold ZToFm'.
+  Let ZToFm := ZToField : Z -> F m. Hint Unfold ZToFm. Local Coercion ZToFm : Z >-> F.
   (* Substitution to prove all Compats *)
   Ltac compat := repeat intro; subst; trivial.
 
diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v
index d6c7fa4b8..7d354ab3e 100644
--- a/src/ModularArithmetic/Tutorial.v
+++ b/src/ModularArithmetic/Tutorial.v
@@ -9,9 +9,9 @@ Section Mod24.
 
   (* Specify modulus *)
   Let q := 24.
-  
+
   (* Boilerplate for letting Z numbers be interpreted as field elements *)
-  Local Coercion ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq.
+  Let ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq. Local Coercion ZToFq : Z >-> F.
 
   (* Boilerplate for [ring]. Similar boilerplate works for [field] if
   the modulus is prime . *)
@@ -21,7 +21,7 @@ Section Mod24.
      postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
      constants [Fconstant],
      div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]). 
+     power_tac (@Fpower_theory q) [Fexp_tac]).
 
   Lemma sumOfSquares : forall a b: F q, (a+b)^2 = a^2 + 2*a*b + b^2.
   Proof.
@@ -37,9 +37,9 @@ Section Modq.
 
   (* Set notations + - * / refer to F operations *)
   Local Open Scope F_scope.
-  
+
   (* Boilerplate for letting Z numbers be interpreted as field elements *)
-  Local Coercion ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq.
+  Let ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq. Local Coercion ZToFq : Z >-> F.
 
   (* Boilerplate for [field]. Similar boilerplate works for [ring] if
   the modulus is not prime . *)
@@ -49,7 +49,7 @@ Section Modq.
      postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
      constants [Fconstant],
      div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]). 
+     power_tac (@Fpower_theory q) [Fexp_tac]).
 
   Lemma sumOfSquares' : forall a b c: F q, c <> 0 -> ((a+b)/c)^2 = a^2/c^2 + ZToField 2*(a/c)*(b/c) + b^2/c^2.
   Proof.
@@ -170,7 +170,7 @@ Module TimesZeroParametricTestModule (M: PrimeModulus).
     field; try exact Fq_1_neq_0.
   Qed.
 
-  Lemma biggerFraction : forall XP YP ZP TP XQ YQ ZQ TQ d : F modulus, 
+  Lemma biggerFraction : forall XP YP ZP TP XQ YQ ZQ TQ d : F modulus,
    ZQ <> 0 ->
    ZP <> 0 ->
    ZP * ZQ * ZP * ZQ + d * XP * XQ * YP * YQ <> 0 ->
@@ -187,4 +187,3 @@ Module TimesZeroParametricTestModule (M: PrimeModulus).
     field; assumption.
   Qed.
 End TimesZeroParametricTestModule.
-
diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v
index 76efe3d79..8ee07fe5d 100644
--- a/src/Spec/ModularArithmetic.v
+++ b/src/Spec/ModularArithmetic.v
@@ -26,8 +26,8 @@ Section FieldOperations.
   Context {m : BinInt.Z}.
 
   (* Coercion without Context {m} --> non-uniform inheritance --> Anomalies *)
-  Local Coercion ZToFm := ZToField : BinNums.Z -> F m.
-  
+  Let ZToFm := ZToField : BinNums.Z -> F m. Local Coercion ZToFm : BinNums.Z >-> F.
+
   Definition add (a b:F m) : F m := ZToField (a + b).
   Definition mul (a b:F m) : F m := ZToField (a * b).
 
@@ -69,4 +69,4 @@ Infix "-" := sub : F_scope.
 Infix "/" := div : F_scope.
 Infix "^" := pow : F_scope.
 Notation "0" := (ZToField 0) : F_scope.
-Notation "1" := (ZToField 1) : F_scope.
\ No newline at end of file
+Notation "1" := (ZToField 1) : F_scope.
-- 
cgit v1.2.3


From 26640780a5cdce3aed531c1bf7cdaa692244edc7 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Thu, 16 Jun 2016 15:51:26 -0400
Subject: Z is integral domain

---
 src/Algebra.v                                     | 29 +++++++++++++++++++----
 src/ModularArithmetic/ModularArithmeticTheorems.v | 10 ++++++++
 2 files changed, 35 insertions(+), 4 deletions(-)

(limited to 'src/ModularArithmetic/ModularArithmeticTheorems.v')

diff --git a/src/Algebra.v b/src/Algebra.v
index 43aac8e4a..b5eb4a7f5 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -527,7 +527,8 @@ Ltac nsatz_rewrite_and_revert domain :=
 Ltac nsatz_nonzero := 
   try solve [apply Integral_domain.integral_domain_one_zero
             |apply Integral_domain.integral_domain_minus_one_zero
-            |trivial].
+            |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 *)
@@ -585,8 +586,8 @@ Ltac field_algebra :=
   try (nsatz; dropRingSyntax);
   repeat (apply conj);
   try solve
-      [unfold not; intro; nsatz_contradict
-      |nsatz_nonzero].
+      [nsatz_nonzero
+      |unfold not; intro; nsatz_contradict].
 
 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}.
@@ -603,4 +604,24 @@ Section Example.
 
   Example _example_nonzero_nsatz_contradict x y : x * y = 1 -> not (x = 0).
   Proof. intros. intro. nsatz_contradict. Qed.
-End Example.
\ No newline at end of file
+End Example.
+
+Section Z.
+  Require Import ZArith.
+  Global Instance ring_Z : @ring Z Logic.eq 0%Z 1%Z Z.opp Z.add Z.sub Z.mul.
+  Proof. repeat split; auto using Z.eq_dec with zarith typeclass_instances. Qed.
+
+  Global Instance commutative_ring_Z : @commutative_ring Z Logic.eq 0%Z 1%Z Z.opp Z.add Z.sub Z.mul.
+  Proof. eauto using @commutative_ring, @is_commutative, ring_Z with zarith. Qed.
+
+  Global Instance integral_domain_Z : @integral_domain Z Logic.eq 0%Z 1%Z Z.opp Z.add Z.sub Z.mul.
+  Proof.
+    split.
+    { apply commutative_ring_Z. }
+    { constructor. intros. apply Z.neq_mul_0; auto. }
+    { constructor. discriminate. }
+  Qed.
+
+  Example _example_nonzero_nsatz_contradict_Z x y : Z.mul x y = (Zpos xH) -> not (x = Z0).
+  Proof. intros. intro. nsatz_contradict. Qed.
+End Z.
\ No newline at end of file
diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index dabfcf883..fe7600784 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -149,6 +149,16 @@ Section FandZ.
     intuition; find_inversion; rewrite ?Z.mod_0_l, ?Z.mod_small in *; intuition.
   Qed.
 
+  Require Crypto.Algebra.
+  Global Instance ring_modulo : @Algebra.ring (F m) Logic.eq (ZToField 0) (ZToField 1) opp add sub mul.
+  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.mul_1_r. auto. }
+  Qed.
+
   Lemma ZToField_0 : @ZToField m 0 = 0.
   Proof.
     Fdefn.
-- 
cgit v1.2.3


From 39ec94341fa3a30d97d4462e9c9d481ada2c8d3d Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Fri, 17 Jun 2016 13:33:17 -0400
Subject: move nsatz out of algebra, improve algebra, port
 CompleteEdwardsCurveTheorems

---
 _CoqProject                                        |   1 +
 src/Algebra.v                                      | 267 +++++++-----------
 .../CompleteEdwardsCurveTheorems.v                 | 314 ++++++---------------
 src/ModularArithmetic/ModularArithmeticTheorems.v  |   3 +-
 src/Nsatz.v                                        | 119 ++++++++
 src/Spec/CompleteEdwardsCurve.v                    |   8 +-
 6 files changed, 318 insertions(+), 394 deletions(-)
 create mode 100644 src/Nsatz.v

(limited to 'src/ModularArithmetic/ModularArithmeticTheorems.v')

diff --git a/_CoqProject b/_CoqProject
index 2fc5b1b90..a0fbc5401 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -4,6 +4,7 @@ src/BaseSystem.v
 src/BaseSystemProofs.v
 src/EdDSAProofs.v
 src/Field.v
+src/Nsatz.v
 src/Rep.v
 src/Testbit.v
 src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
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}.
-- 
cgit v1.2.3


From b41ac7998a11354618b122874c03bc68c2833a94 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Mon, 20 Jun 2016 02:26:56 -0400
Subject: [F q] is [Algebra.field]

---
 src/ModularArithmetic/ModularArithmeticTheorems.v | 6 ++----
 src/ModularArithmetic/PrimeFieldTheorems.v        | 9 +++++++++
 2 files changed, 11 insertions(+), 4 deletions(-)

(limited to 'src/ModularArithmetic/ModularArithmeticTheorems.v')

diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index 4e0ba461e..5a84d80b7 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -150,14 +150,12 @@ Section FandZ.
   Qed.
 
   Require Crypto.Algebra.
-  Global Instance ring_modulo : @Algebra.ring (F m) Logic.eq (ZToField 0) (ZToField 1) opp add sub mul.
+  Global Instance commutative_ring_modulo : @Algebra.commutative_ring (F m) Logic.eq (ZToField 0) (ZToField 1) opp add sub mul.
   Proof.
-    repeat split; Fdefn.
+    repeat split; Fdefn; try apply F_eq_dec.
     { rewrite Z.add_0_r. auto. }
-    { 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/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index 70a2c4a87..2021e8514 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -10,6 +10,7 @@ Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.ZArith.ZArith Coq.ZArith.
 Require Import Coq.Logic.Eqdep_dec.
 Require Import Crypto.Util.NumTheoryUtil Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.
+Require Crypto.Algebra.
 
 Existing Class prime.
 
@@ -51,6 +52,14 @@ Section FieldModuloPre.
   Proof.
     constructor; auto using Fring_theory, Fq_1_neq_0, F_mul_inv_l.
   Qed.
+
+  Global Instance field_modulo : @Algebra.field (F q) Logic.eq (ZToField 0) (ZToField 1) opp add sub mul inv div.
+  Proof.
+    constructor; try solve_proper.
+    - apply commutative_ring_modulo.
+    - split. auto using F_mul_inv_l.
+    - split. auto using Fq_1_neq_0.
+  Qed.
 End FieldModuloPre.
 
 Module Type PrimeModulus.
-- 
cgit v1.2.3