blob: a554e826add808fbef0580f731a7db9a2ce69c4b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
|
Require Import BinInt BinNat ZArith Znumtheory.
Require Import BoolEq Field_theory.
Require Import Galois GaloisTheory.
Require Import Tactics.VerdiTactics.
Module ZGaloisField (M: Modulus).
Module G := Galois M.
Module T := GaloisTheory M.
Export M G T.
Lemma GFring_morph:
ring_morph GFzero GFone GFplus GFmult GFminus GFopp eq
0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
inject.
Proof.
constructor; intros; try galois;
try (apply gf_eq; simpl; intuition).
apply Zmod_small; destruct modulus; simpl;
apply prime_ge_2 in p; intuition.
replace (- (x mod modulus)) with (0 - (x mod modulus));
try rewrite Zminus_mod_idemp_r; trivial.
replace x with y; intuition.
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.
Lemma exist_neq: forall A (P: A -> Prop) x y Px Py, x <> y -> exist P x Px <> exist P y Py.
Proof.
intuition; solve_by_inversion.
Qed.
Ltac GFpreprocess :=
repeat rewrite injectZeroIsGFZero;
repeat rewrite injectOneIsGFOne.
Ltac GFpostprocess :=
repeat split;
repeat match goal with [ |- context[exist ?a ?b (inject_subproof ?x)] ] =>
replace (exist a b (inject_subproof x)) with (inject x%Z) by reflexivity
end;
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,
preprocess [GFpreprocess],
postprocess [GFpostprocess],
constants [GFconstant],
div GFmorph_div_theory,
power_tac GFpower_theory [GFexp_tac]).
End ZGaloisField.
|
