fix field for division by constant (by dmz@mit.edu)

2 files changed, 16 insertions, 3 deletions

diff --git a/src/Galois/GaloisExamples.v b/src/Galois/GaloisExamples.v
index f649701b7..12bcfa2c8 100644
--- a/src/Galois/GaloisExamples.v
+++ b/src/Galois/GaloisExamples.v
@@ -42,6 +42,12 @@ Module Example31.
     field; trivial.
   Qed.
 
+  Lemma example4: forall x: GF, x/(inject 1) = x.
+  Proof.
+    intros; field.
+    discriminate.
+  Qed.
+
 End Example31.
 
 Module TimesZeroTransparentTestModule.
diff --git a/src/Galois/ZGaloisField.v b/src/Galois/ZGaloisField.v
index bf9efa964..a554e826a 100644
--- a/src/Galois/ZGaloisField.v
+++ b/src/Galois/ZGaloisField.v
@@ -1,7 +1,7 @@
-
 Require Import BinInt BinNat ZArith Znumtheory.
 Require Import BoolEq Field_theory.
 Require Import Galois GaloisTheory.
+Require Import Tactics.VerdiTactics.
 
 Module ZGaloisField (M: Modulus).
   Module G := Galois M.
@@ -52,11 +52,20 @@ Module ZGaloisField (M: Modulus).
       apply prime_ge_2 in p; intuition.
   Qed.
 
+  Lemma exist_neq: forall A (P: A -> Prop) x y Px Py, x <> y -> exist P x Px <> exist P y Py.
+  Proof.
+    intuition; solve_by_inversion.
+  Qed.
+
   Ltac GFpreprocess :=
     repeat rewrite injectZeroIsGFZero;
     repeat rewrite injectOneIsGFOne.
 
   Ltac GFpostprocess :=
+    repeat split;
+		repeat match goal with [ |- context[exist ?a ?b (inject_subproof ?x)] ] =>
+			replace (exist a b (inject_subproof x)) with (inject x%Z) by reflexivity
+		end;
     repeat rewrite <- injectZeroIsGFZero;
     repeat rewrite <- injectOneIsGFOne.
 
@@ -79,6 +88,4 @@ Module ZGaloisField (M: Modulus).
      constants [GFconstant],
      div GFmorph_div_theory,
      power_tac GFpower_theory [GFexp_tac]). 
-
 End ZGaloisField.
-