2 files changed, 90 insertions, 26 deletions

diff --git a/src/ModularArithmetic/ModularArithmeticTheorems.v b/src/ModularArithmetic/ModularArithmeticTheorems.v
index 7501bfa23..24bf49dc9 100644
--- a/src/ModularArithmetic/ModularArithmeticTheorems.v
+++ b/src/ModularArithmetic/ModularArithmeticTheorems.v
@@ -6,29 +6,34 @@ Require Import BinInt Zdiv Znumtheory NArith. (* import Zdiv before Znumtheory *
 Require Import Coq.Classes.Morphisms Setoid.
 Require Export Ring_theory Field_theory Field_tac.
 
-Theorem F_eq: forall {m} (x y : F m), x = y <-> FieldToZ x = FieldToZ y.
-Proof.
-  destruct x, y; intuition; simpl in *; try congruence.
-  subst_max.
-  f_equal.
-  eapply UIP_dec, Z.eq_dec.
-Qed.
-
-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.
+Section ModularArithmeticPreliminaries.
+  Context {m:Z}.
+  Local Coercion ZToFm := ZToField : BinNums.Z -> F m. Hint Unfold ZToFm.
 
-Lemma F_pow_spec : forall {m} (a:F m),
-    pow a 0%N = 1%F /\ forall x, pow a (1 + x)%N = mul a (pow a x).
-Proof.
-  intros m a.
-  pose (@pow_with_spec m) as H.
-  change (@pow m) with (proj1_sig H). 
-  destruct H; eauto.
-Qed.
+  Theorem F_eq: forall (x y : F m), x = y <-> FieldToZ x = FieldToZ y.
+  Proof.
+    destruct x, y; intuition; simpl in *; try congruence.
+    subst_max.
+    f_equal.
+    eapply UIP_dec, Z.eq_dec.
+  Qed.
+  
+  Lemma F_opp_spec : forall (a:F m), add a (opp a) = 0.
+    intros a.
+    pose (@opp_with_spec m) as H.
+    change (@opp m) with (proj1_sig H). 
+    destruct H; eauto.
+  Qed.
+  
+  Lemma F_pow_spec : forall (a:F m),
+      pow a 0%N = 1%F /\ forall x, pow a (1 + x)%N = mul a (pow a x).
+  Proof.
+    intros a.
+    pose (@pow_with_spec m) as H.
+    change (@pow m) with (proj1_sig H). 
+    destruct H; eauto.
+  Qed.
+End ModularArithmeticPreliminaries.
 
 (* Fails iff the input term does some arithmetic with mod'd values. *)
 Ltac notFancy E :=
@@ -77,7 +82,6 @@ end.
             
 Ltac Fdefn :=
   intros;
-  unfold unfoldFm;
   rewrite ?F_opp_spec;
   repeat match goal with [ x : F _ |- _ ] => destruct x end;
   try eq_remove_proofs;
@@ -239,6 +243,7 @@ End FandZ.
 
 Section RingModuloPre.
   Context {m:Z}.
+  Local Coercion ZToFm := ZToField : Z -> F m. Hint Unfold ZToFm.
   (* Substitution to prove all Compats *)
   Ltac compat := repeat intro; subst; trivial.
 
@@ -311,8 +316,8 @@ Section RingModuloPre.
   Qed.
 
   (***** Division Theory *****)
-  Definition Fquotrem(a b: F m): F m * F m :=
-    let '(q, r) := (Z.quotrem a b) in (ZToField q, ZToField r).
+  Definition Fquotrem(a b: F m): F m * F m := 
+    let '(q, r) := (Z.quotrem a b) in (q : F m, r : F m).
   Lemma Fdiv_theory : div_theory eq (@add m) (@mul m) (@id _) Fquotrem.
   Proof.
     constructor; intros; unfold Fquotrem, id.
@@ -346,7 +351,7 @@ Section RingModuloPre.
                  0%Z 1%Z Z.add    Z.mul    Z.sub    Z.opp  Z.eqb
                  (@ZToField m).
   Proof.
-    constructor; intros; try Fdefn; unfold id, unfoldFm;
+    constructor; intros; try Fdefn; unfold id;
       try (apply gf_eq; simpl; intuition).
 
     - apply sub_intersperse_modulus.
diff --git a/src/ModularArithmetic/Tutorial.v b/src/ModularArithmetic/Tutorial.v
index ae2b63bad..c80decdcf 100644
--- a/src/ModularArithmetic/Tutorial.v
+++ b/src/ModularArithmetic/Tutorial.v
@@ -1,6 +1,65 @@
 Require Import BinInt Zpower ZArith Znumtheory.
 Require Import Spec.ModularArithmetic ModularArithmetic.PrimeFieldTheorems.
 
+
+(* Example for modular arithmetic with a concrete modulus in a section *)
+Section Mod24.
+  (* Set notations + - * / refer to F operations *)
+  Local Open Scope F_scope.
+
+  (* Specify modulus *)
+  Let q := 24.
+  
+  (* Boilerplate for letting Z numbers be interpreted as field elements *)
+  Local Coercion ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq.
+
+  (* Boilerplate for [ring]. Similar boilerplate works for [field] if
+  the modulus is prime . *)
+  Add Ring Ffield_q : (@Fring_theory q)
+    (morphism (@Fring_morph q),
+     preprocess [unfold ZToFq; Fpreprocess],
+     postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
+     constants [Fconstant],
+     div (@Fmorph_div_theory q),
+     power_tac (@Fpower_theory q) [Fexp_tac]). 
+
+  Lemma sumOfSquares : forall a b: F q, (a+b)^2 = a^2 + ZToField 2*a*b + b^2.
+  Proof.
+    intros.
+    ring.
+  Qed.
+End Mod24.
+
+(* Example for modular arithmetic with an abstract modulus in a section *)
+Section Modq.
+  Context {q:Z} {prime_q:prime q}.
+  Existing Instance prime_q.
+
+  (* Set notations + - * / refer to F operations *)
+  Local Open Scope F_scope.
+  
+  (* Boilerplate for letting Z numbers be interpreted as field elements *)
+  Local Coercion ZToFq := ZToField : BinNums.Z -> F q. Hint Unfold ZToFq.
+
+  (* Boilerplate for [field]. Similar boilerplate works for [ring] if
+  the modulus is not prime . *)
+  Add Field Ffield_q' : (@Ffield_theory q _)
+    (morphism (@Fring_morph q),
+     preprocess [unfold ZToFq; Fpreprocess],
+     postprocess [Fpostprocess; try exact Fq_1_neq_0; try assumption],
+     constants [Fconstant],
+     div (@Fmorph_div_theory q),
+     power_tac (@Fpower_theory q) [Fexp_tac]). 
+
+  Lemma sumOfSquares' : forall a b: F q, (a+b)^2 = a^2 + ZToField 2*a*b + b^2.
+  Proof.
+    intros.
+    field.
+  Qed.
+End Modq.
+
+(*** The old way: Modules ***)
+
 Module Modulus31 <: PrimeModulus.
   Definition modulus := 2^5 - 1.
   Lemma prime_modulus : prime modulus.