generic field definition

3 files changed, 57 insertions, 20 deletions

diff --git a/_CoqProject b/_CoqProject
index 416b29176..de22ff9d4 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -2,6 +2,7 @@
 src/BaseSystem.v
 src/BaseSystemProofs.v
 src/EdDSAProofs.v
+src/Field.v
 src/Rep.v
 src/Testbit.v
 src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
index fea4a99b3..318b05f50 100644
--- a/src/CompleteEdwardsCurve/Pre.v
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -1,26 +1,17 @@
-Require Import Coq.ZArith.BinInt Coq.ZArith.Znumtheory Crypto.Tactics.VerdiTactics.
+Require Import Crypto.Field.
+Require Import Coq.setoid_ring.Cring.
+
+Import Field.
 
-Require Import Crypto.Spec.ModularArithmetic.
-Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
-Local Open Scope F_scope.
-  
 Section Pre.
-  Context {q : BinInt.Z}.
-  Context {a : F q}.
-  Context {d : F q}.
-  Context {prime_q : Znumtheory.prime q}.
-  Context {two_lt_q : 2 < q}.
-  Context {a_nonzero : a <> 0}.
-  Context {a_square : exists sqrt_a, sqrt_a^2 = a}.
-  Context {d_nonsquare : forall x, x^2 <> d}.
+  Context F `{Field F}.
+
+  Context {a:F} {a_nonzero : a <> 0} {a_square : exists sqrt_a, sqrt_a^2%Z = a}.
+  Context {d:F} {d_nonsquare : forall x, x^2%Z <> d}.
+  Context {char_gt_2 : 1+1 == 0 -> False}.
 
-  Add Field Ffield_Z : (@Ffield_theory q _)
-    (morphism (@Fring_morph q),
-     preprocess [Fpreprocess],
-     postprocess [Fpostprocess],
-     constants [Fconstant],
-     div (@Fmorph_div_theory q),
-     power_tac (@Fpower_theory q) [Fexp_tac]). 
+  Require Import Coq.setoid_ring.Field_tac.
+  Add Field EdwardsCurveField : (Field_theory_for_tactic F).
   
   (* 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).
diff --git a/src/Field.v b/src/Field.v
new file mode 100644
index 000000000..2a2907088
--- /dev/null
+++ b/src/Field.v
@@ -0,0 +1,45 @@
+Require Import Coq.setoid_ring.Cring.
+Generalizable All Variables.
+
+Class Field_ops (F:Type)
+      `{Ring_ops F}
+      {inv:F->F} := {}.
+
+Class Division (A B:Type) := division : A -> B -> A.
+
+Notation "_/_" := division.
+Notation "n / d" := (division n d).
+
+Module Field.
+
+  Definition div `{Field_ops F} n d := mul n (inv d).
+  Global Instance div_notation `{Field_ops F} : @Division F F := div.
+
+  Class Field {F inv} `{FieldCring:Cring (R:=F)} {Fo:Field_ops F (inv:=inv)} :=
+    {
+      field_inv_comp : Proper (_==_ ==> _==_) inv;
+      field_inv_def : forall x, (x == 0 -> False) -> inv x * x == 1;
+      field_zero_neq_one : 0 == 1 -> False
+    }.
+  Global Existing Instance field_inv_comp.
+
+  Definition powZ `{Field_ops F} (x:F) (n:Z) :=
+    match n with
+      | Z0 => 1
+      | Zpos p => pow_pos x p
+      | Zneg p => inv (pow_pos x p)
+    end.
+  Global Instance power_field `{Field_ops F} : Power | 5 := { power := powZ }.
+
+  Section FieldProofs.
+    Context F `{Field F}.
+    Require Import Coq.setoid_ring.Field_theory.
+    Lemma Field_theory_for_tactic : field_theory 0 1 _+_ _*_ _-_ -_ _/_ inv _==_.
+    Proof.
+      split; repeat constructor; repeat intro; gen_rewrite; try cring.
+      { apply field_zero_neq_one. symmetry; assumption. }
+      { apply field_inv_def. assumption. }
+    Qed.
+
+  End FieldProofs.
+End Field.
\ No newline at end of file