blob: 527acd547503bb1ceca38b51325fc3fcf00fe337 (
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
|
Require Import Zpower ZArith Znumtheory.
Require Import Crypto.Galois.GaloisField Crypto.Galois.GaloisFieldTheory.
Definition two_5_1 := (two_p 5) - 1.
Lemma two_5_1_prime : prime two_5_1.
Admitted.
Definition two_127_1 := (two_p 127) - 1.
Lemma two_127_1_prime : prime two_127_1.
Admitted.
Module Modulus31 <: Modulus.
Definition modulus := exist _ two_5_1 two_5_1_prime.
End Modulus31.
Module Modulus127_1 <: Modulus.
Definition modulus := exist _ two_127_1 two_127_1_prime.
End Modulus127_1.
Module Example31.
Module Theory := GaloisFieldTheory Modulus31.
Import Modulus31 Theory Theory.Field.
Local Open Scope GF_scope.
Lemma example1: forall x y z: GF, z <> 0 -> x * (y / z) / z = x * y / (z ^ 2).
Proof.
intros; simpl.
field; trivial.
Qed.
Lemma example2: forall x: GF, x * (ZToGF 2) = x + x.
Proof.
intros; simpl.
field.
Qed.
Lemma example3: forall x: GF, x ^ 2 + (ZToGF 2) * x + (ZToGF 1) = (x + (ZToGF 1)) ^ 2.
Proof.
intros; simpl.
field; trivial.
Qed.
End Example31.
Module TimesZeroTransparentTestModule.
Module Theory := GaloisFieldTheory Modulus127_1.
Import Modulus127_1 Theory Theory.Field.
Local Open Scope GF_scope.
Lemma timesZero : forall a, a*0 = 0.
intros.
field.
Qed.
End TimesZeroTransparentTestModule.
Module TimesZeroParametricTestModule (M: Modulus).
Module Theory := GaloisFieldTheory M.
Import M Theory Theory.Field.
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.
|
