diff options
Diffstat (limited to 'src/Galois')
-rw-r--r-- | src/Galois/GaloisExamples.v | 21 | ||||
-rw-r--r-- | src/Galois/GaloisTheory.v | 9 | ||||
-rw-r--r-- | src/Galois/ZGaloisField.v | 50 |
3 files changed, 58 insertions, 22 deletions
diff --git a/src/Galois/GaloisExamples.v b/src/Galois/GaloisExamples.v index 35faf3f03..f649701b7 100644 --- a/src/Galois/GaloisExamples.v +++ b/src/Galois/GaloisExamples.v @@ -1,8 +1,7 @@ Require Import Zpower ZArith Znumtheory. Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory. -Require Import Crypto.Galois.ComputationalGaloisField. -Require Import Crypto.Galois.AbstractGaloisField. +Require Import Crypto.Galois.ZGaloisField. Definition two_5_1 := (two_p 5) - 1. Lemma two_5_1_prime : prime two_5_1. @@ -21,9 +20,8 @@ Module Modulus127_1 <: Modulus. End Modulus127_1. Module Example31. - Module Field := Galois Modulus31. - Module Theory := ComputationalGaloisField Modulus31. - Import Modulus31 Theory Field. + Module Theory := ZGaloisField Modulus31. + Import Theory. Local Open Scope GF_scope. Lemma example1: forall x y z: GF, z <> 0 -> x * (y / z) / z = x * y / (z ^ 2). @@ -32,13 +30,13 @@ Module Example31. field; trivial. Qed. - Lemma example2: forall x: GF, x * (ZToGF 2) = x + x. + Lemma example2: forall x: GF, x * (inject 2) = x + x. Proof. intros; simpl. field. Qed. - Lemma example3: forall x: GF, x ^ 2 + (ZToGF 2) * x + (ZToGF 1) = (x + (ZToGF 1)) ^ 2. + Lemma example3: forall x: GF, x ^ 2 + (inject 2) * x + (inject 1) = (x + (inject 1)) ^ 2. Proof. intros; simpl. field; trivial. @@ -47,8 +45,8 @@ Module Example31. End Example31. Module TimesZeroTransparentTestModule. - Module Theory := ComputationalGaloisField Modulus127_1. - Import Modulus127_1 Theory Theory.Field. + Module Theory := ZGaloisField Modulus127_1. + Import Theory. Local Open Scope GF_scope. Lemma timesZero : forall a, a*0 = 0. @@ -58,13 +56,12 @@ Module TimesZeroTransparentTestModule. End TimesZeroTransparentTestModule. Module TimesZeroParametricTestModule (M: Modulus). - Module Theory := AbstractGaloisField M. - Import M Theory Theory.Field. + Module Theory := ZGaloisField M. + Import Theory. Local Open Scope GF_scope. Lemma timesZero : forall a, a*0 = 0. intros. field. - ring. (* field doesn't work but ring does :) *) Qed. End TimesZeroParametricTestModule. diff --git a/src/Galois/GaloisTheory.v b/src/Galois/GaloisTheory.v index e95eed864..8fa1b4113 100644 --- a/src/Galois/GaloisTheory.v +++ b/src/Galois/GaloisTheory.v @@ -158,14 +158,7 @@ Module GaloisTheory (M: Modulus). (* Ring properties *) - Ltac GFexp_tac t := - match t with - | Z0 => N0 - | Zpos ?n => Ncst (Npos n) - | Z_of_N ?n => Ncst n - | NtoZ ?n => Ncst n - | _ => NotConstant - end. + Ltac GFexp_tac t := Ncst t. Lemma GFdecidable : forall (x y: GF), Zeq_bool x y = true -> x = y. Proof. 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. |