diff options
Diffstat (limited to 'src/Galois/ZGaloisField.v')
-rw-r--r-- | src/Galois/ZGaloisField.v | 50 |
1 files changed, 48 insertions, 2 deletions
diff --git a/src/Galois/ZGaloisField.v b/src/Galois/ZGaloisField.v index 23b1c8dd8..bf9efa964 100644 --- a/src/Galois/ZGaloisField.v +++ b/src/Galois/ZGaloisField.v @@ -1,6 +1,6 @@ Require Import BinInt BinNat ZArith Znumtheory. -Require Import BoolEq. +Require Import BoolEq Field_theory. Require Import Galois GaloisTheory. Module ZGaloisField (M: Modulus). @@ -26,13 +26,59 @@ Module ZGaloisField (M: Modulus). symmetry; apply Zeq_bool_eq; trivial. Qed. + Lemma GFmorph_div_theory: + div_theory eq Zplus Zmult inject Z.quotrem. + Proof. + constructor; intros; intuition. + replace (Z.quotrem a b) with (Z.quot a b, Z.rem a b); + try (unfold Z.quot, Z.rem; rewrite <- surjective_pairing; trivial). + + eq_remove_proofs; demod; + rewrite <- (Z.quot_rem' a b); + destruct a; simpl; trivial. + Qed. + + Lemma injectZeroIsGFZero : + GFzero = inject 0. + Proof. + apply gf_eq; simpl; trivial. + Qed. + + Lemma injectOneIsGFOne : + GFone = inject 1. + Proof. + apply gf_eq; simpl; intuition. + symmetry; apply Zmod_small; destruct modulus; simpl; + apply prime_ge_2 in p; intuition. + Qed. + + Ltac GFpreprocess := + repeat rewrite injectZeroIsGFZero; + repeat rewrite injectOneIsGFOne. + + Ltac GFpostprocess := + repeat rewrite <- injectZeroIsGFZero; + repeat rewrite <- injectOneIsGFOne. + + Ltac GFconstant t := + match t with + | inject ?x => x + | _ => NotConstant + end. + Add Ring GFring_Z : GFring_theory (morphism GFring_morph, + constants [GFconstant], + div GFmorph_div_theory, power_tac GFpower_theory [GFexp_tac]). Add Field GFfield_Z : GFfield_theory (morphism GFring_morph, - power_tac GFpower_theory [GFexp_tac]). + preprocess [GFpreprocess], + postprocess [GFpostprocess], + constants [GFconstant], + div GFmorph_div_theory, + power_tac GFpower_theory [GFexp_tac]). End ZGaloisField. |