implement F_opp

3 files changed, 54 insertions, 7 deletions

diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index 6c79e6891..e23288e49 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -6,6 +6,13 @@ Require Import BinInt Zdiv Znumtheory NArith. (* import Zdiv before Znumtheory *
 Require Import Coq.Classes.Morphisms Setoid.
 Require Export Ring_theory Field_theory Field_tac.
 
+Lemma F_opp_spec : forall {m} (a:F m), add a (opp a) = ZToField 0.
+  intros m a.
+  pose (@opp_with_spec m) as H.
+  change (@opp m) with (proj1_sig H). 
+  destruct H; eauto.
+Qed.
+
 Theorem F_eq: forall {m} (x y : F m), x = y <-> FieldToZ x = FieldToZ y.
 Proof.
   destruct x, y; intuition; simpl in *; try congruence.
@@ -173,14 +180,23 @@ 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.
+    replace (x + (m - y))%Z with (m+(x-y))%Z by omega.
+    rewrite Zplus_mod.
+    rewrite Z_mod_same_full; simpl Z.add.
+    rewrite Zmod_mod.
+    reflexivity.
+  Qed.
 
   (* Compatibility between inject and subtraction *)
   Lemma ZToField_sub : forall (x y : Z),
       @ZToField m (x - y) = ZToField x - ZToField y.
   Proof.
-    repeat progress Fdefn.
-    rewrite Zplus_mod, FieldToZ_opp', FieldToZ_ZToField.
-    demod; reflexivity.
+    Fdefn.
+    apply sub_intersperse_modulus.
   Qed.
 
   (* Compatibility between inject and multiplication *)
@@ -286,8 +302,8 @@ Section RingModuloPre.
     constructor; intros; try Fdefn; unfold id, unfoldFm;
       try (apply gf_eq; simpl; intuition).
 
-    - rewrite FieldToZ_opp, FieldToZ_ZToField; demod; trivial.
-    - rewrite FieldToZ_opp, FieldToZ_ZToField, Z_mod_opp; trivial.
+    - apply sub_intersperse_modulus.
+    - rewrite Zminus_mod, Z_mod_same_full; simpl. apply Z_mod_opp.
     - rewrite (proj1 (Z.eqb_eq x y)); trivial.
   Qed.
 
diff --git a/src/ModularArithmetic/Pre.v b/src/ModularArithmetic/Pre.v
index 2c111be32..c313bfcea 100644
--- a/src/ModularArithmetic/Pre.v
+++ b/src/ModularArithmetic/Pre.v
@@ -1,4 +1,6 @@
 Require Import Znumtheory BinInt BinNums.
+Require Import Eqdep_dec.
+Require Import EqdepFacts.
 
 Lemma Z_mod_mod x m : x mod m = (x mod m) mod m.
   symmetry.
@@ -6,3 +8,32 @@ Lemma Z_mod_mod x m : x mod m = (x mod m) mod m.
   - subst; rewrite !Zdiv.Zmod_0_r; reflexivity.
   - apply BinInt.Z.mod_mod; assumption.
 Qed.
+
+Lemma exist_reduced_eq: forall (m : Z) (a b : Z), a = b -> forall pfa pfb,
+    exist (fun z : Z => z = z mod m) a pfa =
+    exist (fun z : Z => z = z mod m) b pfb.
+Proof.
+Admitted.
+
+Definition opp_impl:
+  forall {m : BinNums.Z},
+    {opp0 : {z : BinNums.Z | z = z mod m} -> {z : BinNums.Z | z = z mod m} |
+     forall x : {z : BinNums.Z | z = z mod m},
+       exist (fun z : BinNums.Z => z = z mod m)
+             ((proj1_sig x + proj1_sig (opp0 x)) mod m)
+             (Z_mod_mod (proj1_sig x + proj1_sig (opp0 x)) m) =
+       exist (fun z : BinNums.Z => z = z mod m) (0 mod m) (Z_mod_mod 0 m)}.
+  intro m.
+  refine (exist _ (fun x => exist _ ((m-proj1_sig x) mod m) _) _); intros.
+
+  destruct x;
+  simpl;
+  apply exist_reduced_eq;
+  rewrite Zdiv.Zplus_mod_idemp_r;
+  replace (x + (m - x)) with m by omega;
+  apply Zdiv.Z_mod_same_full.
+
+  Grab Existential Variables.
+  destruct x; simpl.
+  rewrite Zdiv.Zmod_mod; reflexivity.
+Defined.
\ No newline at end of file
diff --git a/src/Spec/ModularArithmetic.v b/src/Spec/ModularArithmetic.v
index e2243dfff..2f887548f 100644
--- a/src/Spec/ModularArithmetic.v
+++ b/src/Spec/ModularArithmetic.v
@@ -31,8 +31,8 @@ Section FieldOperations.
   Definition add (a b:Fm) : Fm := ZToField (a + b).
   Definition mul (a b:Fm) : Fm := ZToField (a * b).
 
-  Parameter opp : Fm -> Fm. 
-  Axiom F_opp_spec : forall (a:Fm), add a (opp a) = 0.
+  Definition opp_with_spec : { opp | forall x, add x (opp x) = 0 } := Pre.opp_impl.
+  Definition opp : F m -> F m := Eval hnf in proj1_sig opp_with_spec.
   Definition sub (a b:Fm) : Fm := add a (opp b).
 
   Parameter inv : Fm -> Fm.