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
|
Require Import Zpower Znumtheory ZArith.ZArith ZArith.Zdiv.
Require Import Omega NPeano Arith.
Require Import Crypto.Util.NatUtil.
Require Import Bedrock.Word.
Local Open Scope Z.
Lemma gt_lt_symmetry: forall n m, n > m <-> m < n.
Proof.
intros; split; omega.
Qed.
Lemma positive_is_nonzero : forall x, x > 0 -> x <> 0.
Proof.
intros; omega.
Qed.
Hint Resolve positive_is_nonzero.
Lemma div_positive_gt_0 : forall a b, a > 0 -> b > 0 -> a mod b = 0 ->
a / b > 0.
Proof.
intros; rewrite gt_lt_symmetry.
apply Z.div_str_pos.
split; intuition.
apply Z.divide_pos_le; try (apply Zmod_divide); omega.
Qed.
Lemma elim_mod : forall a b m, a = b -> a mod m = b mod m.
Proof.
intros; subst; auto.
Qed.
Hint Resolve elim_mod.
Lemma mod_mult_plus: forall a b c, (b <> 0) -> (a * b + c) mod b = c mod b.
Proof.
intros.
rewrite Zplus_mod.
rewrite Z.mod_mul; auto; simpl.
rewrite Zmod_mod; auto.
Qed.
Lemma pos_pow_nat_pos : forall x n,
Z.pos x ^ Z.of_nat n > 0.
do 2 (intros; induction n; subst; simpl in *; auto with zarith).
rewrite <- Pos.add_1_r, Zpower_pos_is_exp.
apply Zmult_gt_0_compat; auto; reflexivity.
Qed.
Lemma Z_div_mul' : forall a b : Z, b <> 0 -> (b * a) / b = a.
intros. rewrite Z.mul_comm. apply Z.div_mul; auto.
Qed.
Lemma Zgt0_neq0 : forall x, x > 0 -> x <> 0.
intuition.
Qed.
Lemma Zpow_pow2 : forall n, (pow2 n)%nat = Z.to_nat (2 ^ (Z.of_nat n)).
Proof.
induction n; intros; auto.
simpl pow2.
rewrite Nat2Z.inj_succ.
rewrite Z.pow_succ_r by apply Zle_0_nat.
rewrite untimes2.
rewrite Z2Nat.inj_mul by (try apply Z.pow_nonneg; omega).
rewrite <- IHn.
auto.
Qed.
Lemma mod_exp_0 : forall a x m, x > 0 -> m > 1 -> a mod m = 0 ->
a ^ x mod m = 0.
Proof.
intros.
replace x with (Z.of_nat (Z.to_nat x)) in * by (apply Z2Nat.id; omega).
induction (Z.to_nat x). {
simpl in *; omega.
} {
rewrite Nat2Z.inj_succ in *.
rewrite Z.pow_succ_r by omega.
rewrite Z.mul_mod by omega.
case_eq n; intros. {
subst. simpl.
rewrite Zmod_1_l by omega.
rewrite H1.
apply Zmod_0_l.
} {
subst.
rewrite IHn by (rewrite Nat2Z.inj_succ in *; omega).
rewrite H1.
auto.
}
}
Qed.
Lemma mod_pow : forall (a m b : Z), (0 <= b) -> (m <> 0) ->
a ^ b mod m = (a mod m) ^ b mod m.
Proof.
intros; rewrite <- (Z2Nat.id b) by auto.
induction (Z.to_nat b); auto.
rewrite Nat2Z.inj_succ.
do 2 rewrite Z.pow_succ_r by apply Nat2Z.is_nonneg.
rewrite Z.mul_mod by auto.
rewrite (Z.mul_mod (a mod m) ((a mod m) ^ Z.of_nat n) m) by auto.
rewrite <- IHn by auto.
rewrite Z.mod_mod by auto.
reflexivity.
Qed.
Ltac Zdivide_exists_mul := let k := fresh "k" in
match goal with
| [ H : (?a | ?b) |- _ ] => apply Z.mod_divide in H; try apply Zmod_divides in H; destruct H as [k H]
| [ |- (?a | ?b) ] => apply Z.mod_divide; try apply Zmod_divides
end; (omega || auto).
Lemma divide_mul_div: forall a b c (a_nonzero : a <> 0) (c_nonzero : c <> 0),
(a | b * (a / c)) -> (c | a) -> (c | b).
Proof.
intros ? ? ? ? ? divide_a divide_c_a; do 2 Zdivide_exists_mul.
rewrite divide_c_a in divide_a.
rewrite Z_div_mul' in divide_a by auto.
replace (b * k) with (k * b) in divide_a by ring.
replace (c * k * k0) with (k * (k0 * c)) in divide_a by ring.
rewrite Z.mul_cancel_l in divide_a by (intuition; rewrite H in divide_c_a; ring_simplify in divide_a; intuition).
eapply Zdivide_intro; eauto.
Qed.
Lemma divide2_even_iff : forall n, (2 | n) <-> Z.even n = true.
Proof.
intro; split. {
intro divide2_n.
Zdivide_exists_mul; [ | pose proof (Z.mod_pos_bound n 2); omega].
rewrite divide2_n.
apply Z.even_mul.
} {
intro n_even.
pose proof (Zmod_even n).
rewrite n_even in H.
apply Zmod_divide; omega || auto.
}
Qed.
Lemma prime_odd_or_2 : forall p (prime_p : prime p), p = 2 \/ Z.odd p = true.
Proof.
intros.
apply Decidable.imp_not_l; try apply Z.eq_decidable.
intros p_neq2.
pose proof (Zmod_odd p) as mod_odd.
destruct (Sumbool.sumbool_of_bool (Z.odd p)) as [? | p_not_odd]; auto.
rewrite p_not_odd in mod_odd.
apply Zmod_divides in mod_odd; try omega.
destruct mod_odd as [c c_id].
rewrite Z.mul_comm in c_id.
apply Zdivide_intro in c_id.
apply prime_divisors in c_id; auto.
destruct c_id; [omega | destruct H; [omega | destruct H; auto]].
pose proof (prime_ge_2 p prime_p); omega.
Qed.
Ltac prime_bound := match goal with
| [ H : prime ?p |- _ ] => pose proof (prime_ge_2 p H); try omega
end.
|
