blob: e83e22feab4d0d55ee38d6ad2a30207f5546d5ea (
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
|
Require Import BinInt BinNat ZArith Znumtheory.
Require Import Eqdep_dec.
Require Import Tactics.VerdiTactics.
Require Import Galois GaloisTheory.
Module ComputationalGaloisField (M: Modulus).
Module G := Galois M.
Module T := GaloisTheory M.
Export M G T.
Ltac isModulusConstant :=
let hnfModulus := eval hnf in (proj1_sig modulus)
in match (isZcst hnfModulus) with
| NotConstant => NotConstant
| _ => match hnfModulus with
| Z.pos _ => true
| _ => false
end
end.
Ltac isGFconstant t :=
match t with
| GFzero => true
| GFone => true
| ZToGF _ => isModulusConstant
| exist _ ?z _ => match (isZcst z) with
| NotConstant => NotConstant
| _ => isModulusConstant
end
| _ => NotConstant
end.
Ltac GFconstants t :=
match isGFconstant t with
| NotConstant => NotConstant
| _ => t
end.
Add Ring GFring_computational : GFring_theory
(decidable GFdecidable,
constants [GFconstants],
div GFdiv_theory,
power_tac GFpower_theory [GFexp_tac]).
Add Field GFfield_computational : GFfield_theory
(decidable GFdecidable,
completeness GFcomplete,
constants [GFconstants],
div GFdiv_theory,
power_tac GFpower_theory [GFexp_tac]).
End ComputationalGaloisField.
|
