diff options
Diffstat (limited to 'src/Galois/Galois.v')
| -rw-r--r-- | src/Galois/Galois.v | 54 |
1 files changed, 51 insertions, 3 deletions
diff --git a/src/Galois/Galois.v b/src/Galois/Galois.v index 4fd151d36..86ce7f05e 100644 --- a/src/Galois/Galois.v +++ b/src/Galois/Galois.v @@ -3,24 +3,59 @@ Require Import BinInt BinNat ZArith Znumtheory. Require Import Eqdep_dec. Require Import Tactics.VerdiTactics. +(* This file is for the high-level type definitions of + * GF, Primes, Moduli, etc. and their notations and essential + * operations. + * + * The lemmas required for the ring and field theories are + * in GaloisTheory.v and the actual tactic implementations + * for the field are in GaloisField.v. An introduction to the + * use of our implementation of the Galois field is in + * GaloisTutorial.v + *) + Section GaloisPreliminaries. + (* The core prime modulus type, relying on Znumtheory's prime *) Definition Prime := {x: Z | prime x}. + (* Automagically coerce primes to Z *) Definition primeToZ(x: Prime) := proj1_sig x. Coercion primeToZ: Prime >-> Z. End GaloisPreliminaries. +(* A module to hold the field's modulus, which will be an argument to + * all of our Galois modules. + *) Module Type Modulus. Parameter modulus: Prime. End Modulus. +(* The core Galois Field model *) Module Galois (M: Modulus). Import M. + (* The sigma definition of an element of the field: we have + * an element corresponding to the values in Z which can be + * produced by a 'mod' operation. + *) Definition GF := {x: Z | x = x mod modulus}. + + Delimit Scope GF_scope with GF. + Local Open Scope GF_scope. + + (* Automagically convert GF to Z when needed *) Definition GFToZ(x: GF) := proj1_sig x. Coercion GFToZ: GF >-> Z. + (* Automagically convert Z to GF when needed *) + Definition inject(x: Z): GF. + exists (x mod modulus). + abstract (rewrite Zmod_mod; trivial). + Defined. + + Coercion inject : Z >-> GF. + + (* Convert Z to GF without a mod operation, for when the modulus is opaque *) Definition ZToGF (x: Z) : if ((0 <=? x) && (x <? modulus))%bool then GF else True. break_if; [|trivial]. exists x. @@ -31,6 +66,7 @@ Module Galois (M: Modulus). - rewrite <- Z.ltb_lt; auto. Defined. + (* Core lemma: equality in GF implies equality in Z *) Theorem gf_eq: forall (x y: GF), x = y <-> GFToZ x = GFToZ y. Proof. destruct x, y; intuition; simpl in *; try congruence. @@ -40,7 +76,7 @@ Module Galois (M: Modulus). apply Z.eq_dec. Qed. - (* Elementary operations *) + (* Core values: One and Zero *) Definition GFzero: GF. exists 0. abstract trivial. @@ -60,6 +96,7 @@ Module Galois (M: Modulus). Qed. Hint Resolve GFone_nonzero. + (* Elementary operations: +, -, * *) Definition GFplus(x y: GF): GF. exists ((x + y) mod modulus); abstract (rewrite Zmod_mod; trivial). @@ -77,7 +114,7 @@ Module Galois (M: Modulus). Definition GFopp(x: GF): GF := GFminus GFzero x. - (* Totient Preliminaries *) + (* Modular exponentiation *) Fixpoint GFexp' (x: GF) (power: positive) := match power with | xH => x @@ -91,12 +128,13 @@ Module Galois (M: Modulus). | Npos power' => GFexp' x power' end. - (* Inverses + division derived from the existence of a totient *) + (* Preliminaries to inversion in a prime field *) Definition isTotient(e: N) := N.gt e 0 /\ forall g: GF, g <> GFzero -> GFexp g e = GFone. Definition Totient := {e: N | isTotient e}. + (* Get a totient via Fermat's little theorem *) Theorem fermat_little_theorem: isTotient (N.pred (Z.to_N modulus)). Admitted. @@ -108,8 +146,18 @@ Module Galois (M: Modulus). Definition totientToN(x: Totient) := proj1_sig x. Coercion totientToN: Totient >-> N. + (* Define inversion and division *) Definition GFinv(x: GF): GF := GFexp x (N.pred totient). Definition GFdiv(x y: GF): GF := GFmult x (GFinv y). + (* Notations for all of the operations we just made *) + Notation "1" := GFone : GF_scope. + Notation "0" := GFzero : GF_scope. + Infix "+" := GFplus : GF_scope. + Infix "-" := GFminus : GF_scope. + Infix "*" := GFmult : GF_scope. + Infix "/" := GFdiv : GF_scope. + Infix "^" := GFexp : GF_scope. + End Galois. |