1 files changed, 48 insertions, 2 deletions
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.