blob: 35faf3f033c386416bc76827b66b9dc2d8cebb23 (
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
|
Require Import Zpower ZArith Znumtheory.
Require Import Crypto.Galois.Galois Crypto.Galois.GaloisTheory.
Require Import Crypto.Galois.ComputationalGaloisField.
Require Import Crypto.Galois.AbstractGaloisField.
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 Field := Galois Modulus31.
Module Theory := ComputationalGaloisField Modulus31.
Import Modulus31 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 := ComputationalGaloisField 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 := AbstractGaloisField 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.
|