3 files changed, 58 insertions, 22 deletions
diff --git a/src/Galois/GaloisExamples.v b/src/Galois/GaloisExamples.v
index 35faf3f03..f649701b7 100644
--- a/src/Galois/GaloisExamples.v
+++ b/src/Galois/GaloisExamples.v
@@ -1,8 +1,7 @@
 
 Require Import Zpower ZArith Znumtheory.
 Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory.
-Require Import Crypto.Galois.ComputationalGaloisField.
-Require Import Crypto.Galois.AbstractGaloisField.
+Require Import Crypto.Galois.ZGaloisField.
 
 Definition two_5_1 := (two_p 5) - 1.
 Lemma two_5_1_prime : prime two_5_1.
@@ -21,9 +20,8 @@ Module Modulus127_1 <: Modulus.
 End Modulus127_1.
 
 Module Example31.
-  Module Field := Galois Modulus31.
-  Module Theory := ComputationalGaloisField Modulus31.
-  Import Modulus31 Theory Field.
+  Module Theory := ZGaloisField Modulus31.
+  Import Theory.
   Local Open Scope GF_scope.
 
   Lemma example1: forall x y z: GF, z <> 0 -> x * (y / z) / z = x * y / (z ^ 2).
@@ -32,13 +30,13 @@ Module Example31.
     field; trivial.
   Qed.
 
-  Lemma example2: forall x: GF, x * (ZToGF 2) = x + x.
+  Lemma example2: forall x: GF, x * (inject 2) = x + x.
   Proof.
     intros; simpl.
     field.
   Qed.
 
-  Lemma example3: forall x: GF, x ^ 2 + (ZToGF 2) * x + (ZToGF 1) = (x + (ZToGF 1)) ^ 2.
+  Lemma example3: forall x: GF, x ^ 2 + (inject 2) * x + (inject 1) = (x + (inject 1)) ^ 2.
   Proof.
     intros; simpl.
     field; trivial.
@@ -47,8 +45,8 @@ Module Example31.
 End Example31.
 
 Module TimesZeroTransparentTestModule.
-  Module Theory := ComputationalGaloisField Modulus127_1.
-  Import Modulus127_1 Theory Theory.Field.
+  Module Theory := ZGaloisField Modulus127_1.
+  Import Theory.
   Local Open Scope GF_scope.
 
   Lemma timesZero : forall a, a*0 = 0.
@@ -58,13 +56,12 @@ Module TimesZeroTransparentTestModule.
 End TimesZeroTransparentTestModule.
 
 Module TimesZeroParametricTestModule (M: Modulus).
-  Module Theory := AbstractGaloisField M.
-  Import M Theory Theory.Field.
+  Module Theory := ZGaloisField M.
+  Import Theory.
   Local Open Scope GF_scope.
 
   Lemma timesZero : forall a, a*0 = 0.
     intros.
     field.
-    ring. (* field doesn't work but ring does :) *)
   Qed.
 End TimesZeroParametricTestModule.
diff --git a/src/Galois/GaloisTheory.v b/src/Galois/GaloisTheory.v
index e95eed864..8fa1b4113 100644
--- a/src/Galois/GaloisTheory.v
+++ b/src/Galois/GaloisTheory.v
@@ -158,14 +158,7 @@ Module GaloisTheory (M: Modulus).
 
   (* Ring properties *)
 
-  Ltac GFexp_tac t :=
-    match t with
-    | Z0 => N0
-    | Zpos ?n => Ncst (Npos n)
-    | Z_of_N ?n => Ncst n
-    | NtoZ ?n => Ncst n
-    | _ => NotConstant
-    end.
+  Ltac GFexp_tac t := Ncst t.
 
   Lemma GFdecidable : forall (x y: GF), Zeq_bool x y = true -> x = y.
   Proof.
diff --git a/src/Galois/ZGaloisField.v b/src/Galois/ZGaloisField.v
index 23b1c8dd8..bf9efa964 100644
--- a/src/Galois/ZGaloisField.v
+++ b/src/Galois/ZGaloisField.v
@@ -1,6 +1,6 @@
 
 Require Import BinInt BinNat ZArith Znumtheory.
-Require Import BoolEq.
+Require Import BoolEq Field_theory.
 Require Import Galois GaloisTheory.
 
 Module ZGaloisField (M: Modulus).
@@ -26,13 +26,59 @@ Module ZGaloisField (M: Modulus).
       symmetry; apply Zeq_bool_eq; trivial.
   Qed.
 
+  Lemma GFmorph_div_theory: 
+      div_theory eq Zplus Zmult inject Z.quotrem.
+  Proof.
+    constructor; intros; intuition.
+    replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b);
+      try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial).
+
+    eq_remove_proofs; demod;
+      rewrite <- (Z.quot_rem' a b);
+      destruct a; simpl; trivial.
+  Qed.
+
+  Lemma injectZeroIsGFZero :
+    GFzero = inject 0.
+  Proof.
+    apply gf_eq; simpl; trivial.
+  Qed.
+
+  Lemma injectOneIsGFOne :
+    GFone = inject 1.
+  Proof.
+    apply gf_eq; simpl; intuition.
+    symmetry; apply Zmod_small; destruct modulus; simpl;
+      apply prime_ge_2 in p; intuition.
+  Qed.
+
+  Ltac GFpreprocess :=
+    repeat rewrite injectZeroIsGFZero;
+    repeat rewrite injectOneIsGFOne.
+
+  Ltac GFpostprocess :=
+    repeat rewrite <- injectZeroIsGFZero;
+    repeat rewrite <- injectOneIsGFOne.
+
+  Ltac GFconstant t :=
+    match t with
+    | inject ?x => x
+    | _ => NotConstant
+    end.
+
   Add Ring GFring_Z : GFring_theory
     (morphism GFring_morph,
+     constants [GFconstant],
+     div GFmorph_div_theory,
      power_tac GFpower_theory [GFexp_tac]).
 
   Add Field GFfield_Z : GFfield_theory
     (morphism GFring_morph,
-     power_tac GFpower_theory [GFexp_tac]).
+     preprocess [GFpreprocess],
+     postprocess [GFpostprocess],
+     constants [GFconstant],
+     div GFmorph_div_theory,
+     power_tac GFpower_theory [GFexp_tac]). 
 
 End ZGaloisField.