[F] has its own module now

[ZToField] -> [F.of_Z]
[FieldToZ] -> [F.to_Z]
[Zmod.lem] -> [F.lem]

1 files changed, 44 insertions, 44 deletions

diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
index f30472911..a64bf4fc8 100644
--- a/src/ModularArithmetic/PrimeFieldTheorems.v
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -13,33 +13,32 @@ Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Decidable.
 Require Export Crypto.Util.FixCoqMistakes.
 Require Crypto.Algebra.
-Import Crypto.ModularArithmetic.ModularArithmeticTheorems.Zmod.
 
 Existing Class prime.
 
-Module Zmod.
+Module F.
   Section Field.
     Context (q:Z) {prime_q:prime q}.
-    Lemma inv_spec : inv 0%F = (0%F : F q) 
-                     /\ (prime q -> forall x : F q, x <> 0%F -> (inv x * x)%F = 1%F).
-    Proof. change (@inv q) with (proj1_sig (@inv_with_spec q)); destruct (@inv_with_spec q); eauto. Qed.
+    Lemma inv_spec : F.inv 0%F = (0%F : F q) 
+                     /\ (prime q -> forall x : F q, x <> 0%F -> (F.inv x * x)%F = 1%F).
+    Proof. change (@F.inv q) with (proj1_sig (@F.inv_with_spec q)); destruct (@F.inv_with_spec q); eauto. Qed.
 
-    Lemma inv_0 : inv 0 = ZToField q 0. Proof. destruct inv_spec; auto. Qed.
-    Lemma inv_nonzero (x:F q) : (x <> 0 -> inv x * x%F = 1)%F. Proof. destruct inv_spec; auto. Qed.
+    Lemma inv_0 : F.inv 0%F = F.of_Z q 0. Proof. destruct inv_spec; auto. Qed.
+    Lemma inv_nonzero (x:F q) : (x <> 0 -> F.inv x * x%F = 1)%F. Proof. destruct inv_spec; auto. Qed.
 
-    Global Instance field_modulo : @Algebra.field (F q) Logic.eq 0%F 1%F opp add sub mul inv div.
+    Global Instance field_modulo : @Algebra.field (F q) Logic.eq 0%F 1%F F.opp F.add F.sub F.mul F.inv F.div.
     Proof.
       repeat match goal with
              | _ => solve [ solve_proper
-                          | apply commutative_ring_modulo
+                          | apply F.commutative_ring_modulo
                           | apply inv_nonzero
                           | cbv [not]; pose proof prime_ge_2 q prime_q;
-                            rewrite Zmod.eq_FieldToZ_iff, !Zmod.FieldToZ_ZToField, !Zmod_small; omega ]
+                            rewrite F.eq_to_Z_iff, !F.to_Z_of_Z, !Zmod_small; omega ]
              | _ => split
              end.
     Qed.
 
-    Definition field_theory : field_theory 0%F 1%F add mul sub opp div inv eq
+    Definition field_theory : field_theory 0%F 1%F F.add F.mul F.sub F.opp F.div F.inv eq
       := Algebra.Field.field_theory_for_stdlib_tactic.
   End Field.
 
@@ -49,43 +48,44 @@ Module Zmod.
     Parameter prime_modulus : prime modulus.
   End PrimeModulus.
   Module FieldModulo (Export M : PrimeModulus).
-    Module Import RingM := RingModulo M.
-    Add Field _field : (field_theory modulus)
-                         (morphism (ring_morph modulus),
-                          constants [is_constant],
-                          div (morph_div_theory modulus),
-                          power_tac (power_theory modulus) [is_pow_constant]).
+    Module Import RingM := F.RingModulo M.
+    Add Field _field : (F.field_theory modulus)
+                         (morphism (F.ring_morph modulus),
+                          constants [F.is_constant],
+                          div (F.morph_div_theory modulus),
+                          power_tac (F.power_theory modulus) [F.is_pow_constant]).
   End FieldModulo.
 
   Section NumberThoery.
     Context {q:Z} {prime_q:prime q} {two_lt_q: 2 < q}.
     Local Open Scope F_scope.
     Add Field _field : (field_theory q)
-                         (morphism (ring_morph q),
-                          constants [is_constant],
-                          div (morph_div_theory q),
-                          power_tac (power_theory q) [is_pow_constant]).
+                         (morphism (F.ring_morph q),
+                          constants [F.is_constant],
+                          div (F.morph_div_theory q),
+                          power_tac (F.power_theory q) [F.is_pow_constant]).
 
-    Lemma FieldToZ_1 : @FieldToZ q 1 = 1%Z.
+    (* TODO: move to PrimeFieldTheorems *)
+    Lemma to_Z_1 : @F.to_Z q 1 = 1%Z.
     Proof. simpl. rewrite Zmod_small; omega. Qed.
 
-    Lemma Fq_inv_fermat (x:F q) : inv x = x ^ Z.to_N (q - 2)%Z.
+    Lemma Fq_inv_fermat (x:F q) : F.inv x = x ^ Z.to_N (q - 2)%Z.
     Proof.
       destruct (dec (x = 0%F)) as [?|Hnz].
-      { subst x; rewrite inv_0, pow_0_l; trivial.
+      { subst x; rewrite inv_0, F.pow_0_l; trivial.
         change (0%N) with (Z.to_N 0%Z); rewrite Z2N.inj_iff; omega. }
       erewrite <-Algebra.Field.inv_unique; try reflexivity.
-      rewrite eq_FieldToZ_iff, FieldToZ_mul, FieldToZ_pow, Z2N.id, FieldToZ_1 by omega.
-      apply (fermat_inv q _ (FieldToZ x)); rewrite mod_FieldToZ; eapply FieldToZ_nonzero; trivial.
+      rewrite F.eq_to_Z_iff, F.to_Z_mul, F.to_Z_pow, Z2N.id, to_Z_1 by omega.
+      apply (fermat_inv q _ (F.to_Z x)); rewrite F.mod_to_Z; eapply F.to_Z_nonzero; trivial.
     Qed.
     
     Lemma euler_criterion (a : F q) (a_nonzero : a <> 0) :
       (a ^ (Z.to_N (q / 2)) = 1) <-> (exists b, b*b = a).
     Proof.
-      pose proof FieldToZ_nonzero_range a; pose proof (odd_as_div q).
+      pose proof F.to_Z_nonzero_range a; pose proof (odd_as_div q).
       specialize_by ltac:(destruct (Z.prime_odd_or_2 _ prime_q); try omega; trivial).
-      rewrite eq_FieldToZ_iff, !FieldToZ_pow, !FieldToZ_1, !Z2N.id by omega.
-      rewrite square_iff, <-(euler_criterion (q/2)) by (trivial || omega); reflexivity.
+      rewrite F.eq_to_Z_iff, !F.to_Z_pow, !to_Z_1, !Z2N.id by omega.
+      rewrite F.square_iff, <-(euler_criterion (q/2)) by (trivial || omega); reflexivity.
     Qed.
 
     Global Instance Decidable_square (x:F q) : Decidable (exists y, y*y = x).
@@ -100,15 +100,15 @@ Module Zmod.
     Context {q:Z} {prime_q: prime q} {q_5mod8 : q mod 8 = 5}.
 
     (* This is always true, but easier to check by computation than to prove *)
-    Context (sqrt_minus1_valid : ((ZToField q 2 ^ Z.to_N (q / 4)) ^ 2 = opp 1)%F).
+    Context (sqrt_minus1_valid : ((F.of_Z q 2 ^ Z.to_N (q / 4)) ^ 2 = F.opp 1)%F).
     Local Open Scope F_scope.
     Add Field _field2 : (field_theory q)
-                          (morphism (ring_morph q),
-                           constants [is_constant],
-                           div (morph_div_theory q),
-                           power_tac (power_theory q) [is_pow_constant]).
+                          (morphism (F.ring_morph q),
+                           constants [F.is_constant],
+                           div (F.morph_div_theory q),
+                           power_tac (F.power_theory q) [F.is_pow_constant]).
 
-    Let sqrt_minus1 : F q :=  ZToField _ 2 ^ Z.to_N (q / 4).
+    Let sqrt_minus1 :=  F.of_Z q 2 ^ Z.to_N (q / 4).
 
     Lemma two_lt_q_5mod8 : 2 < q.
     Proof.
@@ -132,8 +132,8 @@ Module Zmod.
       assert (0 <= q/8)%Z by (apply Z.div_le_lower_bound; rewrite ?Z.mul_0_r; omega).
       assert (Z.to_N (q / 8 + 1) <> 0%N) by
           (intro Hbad; change (0%N) with (Z.to_N 0%Z) in Hbad; rewrite Z2N.inj_iff in Hbad; omega).
-      destruct (dec (x = 0)); [subst; rewrite !pow_0_l by (trivial || lazy_decide); reflexivity|].
-      rewrite !pow_pow_l.
+      destruct (dec (x = 0)); [subst; rewrite !F.pow_0_l by (trivial || lazy_decide); reflexivity|].
+      rewrite !F.pow_pow_l.
 
       replace (Z.to_N (q / 8 + 1) * (2*2))%N with (Z.to_N (q / 2 + 2))%N.
       Focus 2. { (* this is a boring but gnarly proof :/ *)
@@ -151,8 +151,8 @@ Module Zmod.
         ring.
       } Unfocus.
 
-      rewrite Z2N.inj_add, pow_add_r by zero_bounds.
-      replace (x ^ Z.to_N (q / 2)) with (@ZToField q 1) by
+      rewrite Z2N.inj_add, F.pow_add_r by zero_bounds.
+      replace (x ^ Z.to_N (q / 2)) with (F.of_Z q 1) by
           (symmetry; apply @euler_criterion; eauto).
       change (Z.to_N 2) with 2%N; ring.
     Qed.
@@ -161,14 +161,14 @@ Module Zmod.
                                        (sqrt_5mod8 x)*(sqrt_5mod8 x) = x.
     Proof.
       intros x x_square.
-      pose proof (eq_b4_a2 x x_square) as Hyy; rewrite !pow_2_r in Hyy.
+      pose proof (eq_b4_a2 x x_square) as Hyy; rewrite !F.pow_2_r in Hyy.
       destruct (Algebra.only_two_square_roots_choice _ x (x*x) Hyy eq_refl) as [Hb|Hb]; clear Hyy;
-        unfold sqrt_5mod8; break_if; rewrite !@pow_2_r in *; intuition.
+        unfold sqrt_5mod8; break_if; rewrite !@F.pow_2_r in *; intuition.
       ring_simplify.
-      unfold sqrt_minus1; rewrite @pow_2_r.
-      rewrite sqrt_minus1_valid; rewrite @pow_2_r.
+      unfold sqrt_minus1; rewrite @F.pow_2_r.
+      rewrite sqrt_minus1_valid; rewrite @F.pow_2_r.
       rewrite Hb.
       ring.
     Qed.
   End SquareRootsPrime5Mod8.
-End Zmod.
\ No newline at end of file
+End F.
\ No newline at end of file