Define F m, a replacement for GF with several benefits.

- F has a human readable complete specification
- F is a parametric type, not a parametric module
        - Different F instances can be disambiguated by type inference,
          which is more conventient that notation scopes.
- F has significant support for non-prime moduli
- It should be relatively easy to port existing GF code to F.

Since the repository currently contains code referencing both F and GF,
it makes sense to keep the names different for now. Later, F may or may
not be renamed to GF.

1 files changed, 51 insertions, 0 deletions

diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v
new file mode 100644
index 000000000..4cdd1192e
--- /dev/null
+++ b/src/ModularArithmetic/PrimeFieldTheorems.v
@@ -0,0 +1,51 @@
+Require Export Spec.ModularArithmetic ModularArithmetic.ModularArithmeticTheorems.
+Require Export Ring_theory Field_theory Field_tac.
+
+Require Import Tactics.VerdiTactics.
+Require Import Coq.Classes.Morphisms Setoid.
+Require Import BinInt BinNat ZArith Znumtheory NArith. (* import Zdiv before Znumtheory *)
+Require Import Eqdep_dec.
+
+Existing Class prime.
+
+Section FieldModuloPre.
+  Context {q:Z} {prime_q:prime q}.
+  Local Open Scope F_scope.
+
+  Lemma Fq_1_neq_0 : (1:F q) <> (0:F q).
+  Proof.
+    pose proof prime_ge_2 q _.
+    rewrite F_eq, !FieldToZ_ZToField, !Zmod_small by omega; congruence.
+  Qed.
+
+  Lemma F_mul_inv_l : forall x : F q, inv x * x = 1.
+  Proof.
+    intros.
+    rewrite <-(proj1 (F_inv_spec _ x)).
+    Fdefn.
+  Qed.
+
+  (* Add an abstract field (without modifiers) *)
+  Definition Ffield_theory : field_theory 0%F 1%F (@add q) (@mul q) (@sub q) (@opp q) (@div q) (@inv q) eq.
+  Proof.
+    constructor; auto using Fring_theory, Fq_1_neq_0, F_mul_inv_l.
+  Qed.
+End FieldModuloPre.
+
+Module Type PrimeModulus.
+  Parameter modulus : Z.
+  Parameter prime_modulus : prime modulus.
+End PrimeModulus.
+
+Module FieldModulo (Import M : PrimeModulus).
+  (* Add our field with all the fixin's *)
+  Module Import RingM := RingModulo M.
+  Definition field_theory_modulo := @Ffield_theory modulus prime_modulus.
+  Add Field Ffield_Z : field_theory_modulo
+    (morphism ring_morph_modulo,
+     preprocess [Fpreprocess],
+     postprocess [Fpostprocess],
+     constants [Fconstant],
+     div morph_div_theory_modulo,
+     power_tac power_theory_modulo [Fexp_tac]). 
+End FieldModulo.
\ No newline at end of file