Refactor ModularArithmetic into Zmod, expand Decidable

ModularArithmetic now uses Algebra lemmas in various places instead of
custom manual proofs. Similarly, Util.Decidable is used to state and
prove the relevant decidability results.

Backwards-incompatible changes:

F_some_lemma -> Zmod.some_lemma
Arguments ZToField _%Z _%Z : clear implicits.
inv_spec says inv x * x = 1, not x * inv x = 1

1 files changed, 28 insertions, 14 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index 9bd3cac5e..adbf5b86b 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -12,17 +12,10 @@ Module Import ModuloCoq8485.
   Infix "mod" := modulo.
 End ModuloCoq8485.
 
-Notation is_eq_dec := (DecidableRel _) (only parsing).
-Notation "@ 'is_eq_dec' T R" := (DecidableRel (R:T->T->Prop)) (only parsing).
-Notation eq_dec x y := (@dec (_ x y) _) (only parsing).
-Notation "x =? y" := (eq_dec x y) : type_scope.
-
 Section Algebra.
   Context {T:Type} {eq:T->T->Prop}.
   Local Infix "=" := eq : type_scope. Local Notation "a <> b" := (not (a = b)) : type_scope.
 
-  Local Notation is_eq_dec := (@is_eq_dec T eq).
-
   Section SingleOperation.
     Context {op:T->T->T}.
 
@@ -41,7 +34,7 @@ Section Algebra.
 
         monoid_op_Proper: Proper (respectful eq (respectful eq eq)) op;
         monoid_Equivalence : Equivalence eq;
-        monoid_is_eq_dec : is_eq_dec
+        monoid_is_eq_dec : DecidableRel eq
       }.
     Global Existing Instance monoid_is_associative.
     Global Existing Instance monoid_is_left_identity.
@@ -364,6 +357,23 @@ Module ScalarMult.
     Global Existing Instance scalarmult_Proper.
     Context `{is_scalarmult}.
 
+    Fixpoint scalarmult_ref (n:nat) (P:G) {struct n} :=
+      match n with
+      | O => zero
+      | S n' => add P (scalarmult_ref n' P)
+      end.
+
+    Global Instance Proper_scalarmult_ref : Proper (Logic.eq==>eq==>eq) scalarmult_ref.
+    Proof.
+      repeat intro; subst.
+      match goal with [n:nat |- _ ] => induction n; simpl @scalarmult_ref; [reflexivity|] end.
+      repeat match goal with [H:_ |- _ ] => rewrite H end; reflexivity.
+    Qed.
+
+    Lemma scalarmult_ext : forall n P, mul n P = scalarmult_ref n P.
+      induction n; simpl @scalarmult_ref; intros; rewrite <-?IHn; (apply scalarmult_0_l || apply scalarmult_S_l).
+    Qed.
+
     Lemma scalarmult_1_l : forall P, 1*P = P.
     Proof. intros. rewrite scalarmult_S_l, scalarmult_0_l, right_identity; reflexivity. Qed.
 
@@ -402,6 +412,10 @@ Module ScalarMult.
         rewrite scalarmult_add_l, scalarmult_1_l, Group.inv_op, scalarmult_S_l, Group.cancel_left; eauto. }
     Qed.
   End ScalarMultProperties.
+
+  Global Instance scalarmult_ref_is_scalarmult {G eq add zero} `{@monoid G eq add zero}
+    : @is_scalarmult G eq add zero (@scalarmult_ref G add zero).
+  Proof. split; try exact _; intros; reflexivity. Qed.
 End ScalarMult.
 
 Require Coq.nsatz.Nsatz.
@@ -588,7 +602,7 @@ Module IntegralDomain.
       : eq (mul x y) zero -> eq x zero \/ eq y zero.
     Proof.
       pose proof mul_nonzero_nonzero x y.
-      destruct (eq_dec x zero); destruct (eq_dec y zero); intuition.
+      destruct (dec (eq x zero)); destruct (dec (eq y zero)); intuition.
     Qed.
 
     Lemma mul_nonzero_nonzero_iff (x y : T)
@@ -663,7 +677,7 @@ Module Field.
 
   Lemma isomorphism_to_subfield_field
         {T EQ ZERO ONE OPP ADD SUB MUL INV DIV}
-        {Equivalence_EQ: @Equivalence T EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y} }
+        {Equivalence_EQ: @Equivalence T EQ} {eq_dec: DecidableRel EQ}
         {Proper_OPP:Proper(EQ==>EQ)OPP}
         {Proper_ADD:Proper(EQ==>EQ==>EQ)ADD}
         {Proper_SUB:Proper(EQ==>EQ==>EQ)SUB}
@@ -673,7 +687,7 @@ Module Field.
         {R eq zero one opp add sub mul inv div} {fieldR:@field R eq zero one opp add sub mul inv div}
         {phi}
         {eq_phi_EQ: forall x y, eq (phi x) (phi y) -> EQ x y}
-        {neq_zero_one : (EQ ZERO ONE -> False)}
+        {neq_zero_one : (not (EQ ZERO ONE))}
         {phi_opp : forall a, eq (phi (OPP a)) (opp (phi a))}
         {phi_add : forall a b, eq (phi (ADD a b)) (add (phi a) (phi b))}
         {phi_sub : forall a b, eq (phi (SUB a b)) (sub (phi a) (phi b))}
@@ -753,7 +767,7 @@ Module Field.
        -> phi (INV x) = inv (phi x).
     Proof.
       intros.
-      destruct (eq_dec x ZERO); auto.
+      destruct (dec (EQ x ZERO)); auto.
       assert (phi (MUL (INV x) x) = one) as A. {
         rewrite left_multiplicative_inverse; auto using Ring.homomorphism_one.
       }
@@ -1223,8 +1237,8 @@ Section ExtraLemmas.
   Lemma only_two_square_roots'_choice x y : x * x = y * y -> x = y \/ x = opp y.
   Proof.
     intro H.
-    destruct (eq_dec x y); [ left; assumption | right ].
-    destruct (eq_dec x (opp y)); [ assumption | exfalso ].
+    destruct (dec (eq x y)); [ left; assumption | right ].
+    destruct (dec (eq x (opp y))); [ assumption | exfalso ].
     eapply only_two_square_roots'; eassumption.
   Qed.