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
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
|
Require Import NPeano.
Require Import List.
Require Import Sorting.Permutation.
Require Import BinInt.
Require Import Util.ListUtil.
Require Znumtheory.
Lemma all_neq_NoDup : forall {T} (xs:list T),
(forall i j x y,
nth_error xs i = Some x ->
nth_error xs j = Some y ->
i <> j -> x <> y) <-> NoDup xs.
Admitted.
Definition F (q:nat) := { n : nat | n = n mod q}.
Section Fq.
Context {q : nat}.
Axiom q_prime : Znumtheory.prime (Z.of_nat q).
Let Fq := F q.
Lemma q_is_succ : q = S (q-1). Admitted.
Definition natToField (n:nat) : Fq. exists (n mod q). abstract admit. Defined.
Definition fieldToNat (n:Fq) : nat := proj1_sig n.
Coercion fieldToNat : Fq >-> nat.
Definition zero : Fq. exists 0. abstract admit. Defined.
Definition one : Fq. exists 1. abstract admit. Defined.
Definition add (a b: Fq) : Fq. exists (a+b mod q); abstract admit. Defined.
Infix "+" := add.
Definition mul (a b: Fq) : Fq. exists (a*b mod q); abstract admit. Defined.
Infix "*" := mul.
Definition pow (a:Fq) (n:nat) : Fq. exists (pow a n mod q). abstract admit. Defined.
Infix "^" := pow.
Axiom opp : Fq -> Fq.
Axiom opp_spec : forall a, opp a + a = zero.
Definition sub a b := add a (opp b).
Infix "-" := sub.
Axiom inv : Fq -> Fq.
Axiom inv_spec : forall a, inv a * a = one.
Definition div a b := mul a (inv b).
Infix "/" := div.
Fixpoint replicate {T} n (x:T) : list T := match n with O => nil | S n' => x::replicate n' x end.
Definition prod := fold_right mul one.
Lemma mul_one_l : forall a, one * a = a. Admitted.
Lemma mul_one_r : forall a, a * one = a. Admitted.
Lemma mul_cancel_l : forall a, a <> zero -> forall b c, a * b = a * c -> b = c. Admitted.
Lemma mul_cancel_r : forall a, a <> zero -> forall b c, b * a = c * c -> b = c. Admitted.
Lemma mul_cancel_l_1 : forall a, a <> zero -> forall b, a * b = a -> b = one. Admitted.
Lemma mul_cancel_r_1 : forall a, a <> zero -> forall b, b * a = a -> b = one. Admitted.
Lemma mul_0_why : forall a b, a * b = zero -> a = zero \/ b = zero. Admitted.
Lemma mul_assoc : forall a b c, a * (b * c) = a * b * c. Admitted.
Lemma mul_assoc_pairs' : forall a b c d, (a * b) * (c * d) = a * (c * (b * d)). Admitted.
Lemma div_cancel : forall a, a <> zero -> forall b c, b / a = c / a -> b = c. Admitted.
Lemma div_cancel_neq : forall a, a <> zero -> forall b c, b / a <> c / a -> b <> c. Admitted.
Lemma div_mul : forall a, a <> zero -> forall b, (a * b) / a = b. Admitted.
Hint Resolve mul_assoc.
Hint Rewrite div_mul.
Lemma pow_zero : forall (n:nat), zero^n = zero. Admitted.
Lemma pow_S : forall a n, a ^ S n = a * a ^ n. Admitted.
Lemma prod_replicate : forall a n, a ^ n = prod (replicate n a). Admitted.
Lemma prod_perm : forall xs ys, Permutation xs ys -> prod xs = prod ys. Admitted.
Hint Resolve pow_zero mul_one_l mul_one_r prod_replicate.
Definition F_eq_dec : forall (a b:Fq), {a = b} + {a <> b}. Admitted.
Definition elements : list Fq := map natToField (seq 0 q).
Lemma elements_all : forall (a:Fq), In a elements. Admitted.
Lemma elements_unique : forall (a:Fq), NoDup elements. Admitted.
Lemma length_elements : length elements = q. Admitted.
Definition invertibles : list Fq := map natToField (seq 1 (q-1)%nat).
Lemma invertibles_all : forall (a:Fq), a <> zero -> In a invertibles. Admitted.
Lemma invertibles_unique : NoDup invertibles. Admitted.
Lemma prod_invertibles_nonzero : prod invertibles <> zero. Admitted.
Lemma length_invertibles : length invertibles = (q-1)%nat. Admitted.
Hint Resolve invertibles_unique.
Section FermatsLittleTheorem.
Variable a : Fq.
Axiom a_nonzero : a <> zero.
Hint Resolve a_nonzero.
Definition bag := map (mul a) invertibles.
Lemma bag_unique : NoDup bag.
Proof.
unfold bag; intros.
eapply all_neq_NoDup; intros.
eapply div_cancel_neq; eauto.
eapply all_neq_NoDup; eauto;
match goal with
| [H: nth_error (map _ _) ?i = Some _ |- _ ] =>
destruct (nth_error_map _ _ _ _ _ _ H) as [t [HtIn HtEq]]; rewrite <- HtEq; autorewrite with core; auto
end.
Qed.
Lemma bag_invertibles : forall b, b <> zero -> In b bag.
Proof.
unfold bag; intros.
assert (b/a <> zero) as Hdnz by admit.
replace b with (a * (b/a)) by admit.
destruct (In_nth_error_value _ _ (invertibles_all _ Hdnz)).
eauto using nth_error_value_In, map_nth_error.
Qed.
Lemma In_bag_equiv_In_invertibles : forall b, In b bag <-> In b invertibles.
Proof.
unfold bag; intros.
case (F_eq_dec b zero); intuition; subst;
eauto using invertibles_all, bag_invertibles;
repeat progress match goal with
| [ H : In _ (map _ _) |- _ ] => rewrite in_map_iff in H; destruct H;
pose proof a_nonzero; intuition
| [ H : ?a * ?b = zero |- _ ] => destruct (mul_0_why a b H); clear H;
intuition; try solve [subst; auto]
end.
assert (In zero invertibles -> In zero (map (mul a) invertibles)) by admit; auto.
Qed.
Lemma bag_perm_elements : Permutation bag invertibles.
Proof.
eauto using NoDup_Permutation, bag_unique, invertibles_unique, In_bag_equiv_In_invertibles.
Qed.
Hint Resolve prod_perm bag_perm_elements.
Lemma prod_bag_ref : prod bag = prod invertibles.
Proof.
auto.
Qed.
Lemma prod_bag_interspersed : prod (flat_map (fun b => a::b::nil) invertibles) = prod invertibles.
Proof.
intros.
rewrite <- prod_bag_ref.
unfold bag.
induction invertibles; auto; simpl.
rewrite IHl.
auto.
Qed.
Lemma prod_bag_sorted : prod (replicate (q-1)%nat a) * prod invertibles = prod invertibles.
rewrite <- length_invertibles.
rewrite <- prod_bag_interspersed at 2.
induction invertibles; auto; simpl.
rewrite mul_assoc_pairs'; repeat f_equal; auto.
Qed.
Theorem fermat' : a <> zero -> a^(q-1) = one.
Proof.
rewrite prod_replicate; eauto using mul_cancel_r_1, prod_bag_sorted, prod_invertibles_nonzero.
Qed.
End FermatsLittleTheorem.
Theorem fermat (a:Fq) : a^q = a.
Proof.
case (F_eq_dec a zero); intros; subst; auto.
rewrite q_is_succ, pow_S, fermat'; auto.
Qed.
End Fq.
Arguments fermat' : default implicits.
Arguments fermat : default implicits.
Arguments elements : default implicits.
Arguments invertibles : default implicits.
Print Assumptions fermat.
Check fermat.
|
