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
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(** Properties of the greatest common divisor *)
Require Import NAxioms NSub NZGcd.
Module Type NGcdProp
(Import A : NAxiomsSig')
(Import B : NSubProp A).
Include NZGcdProp A A B.
(** Results concerning divisibility*)
Definition divide_1_r n : (n | 1) -> n == 1
:= divide_1_r_nonneg n (le_0_l n).
Definition divide_antisym n m : (n | m) -> (m | n) -> n == m
:= divide_antisym_nonneg n m (le_0_l n) (le_0_l m).
Lemma divide_add_cancel_r : forall n m p, (n | m) -> (n | m + p) -> (n | p).
Proof.
intros n m p (q,Hq) (r,Hr).
exists (r-q). rewrite mul_sub_distr_r, <- Hq, <- Hr.
now rewrite add_comm, add_sub.
Qed.
Lemma divide_sub_r : forall n m p, (n | m) -> (n | p) -> (n | m - p).
Proof.
intros n m p H H'.
destruct (le_ge_cases m p) as [LE|LE].
apply sub_0_le in LE. rewrite LE. apply divide_0_r.
apply divide_add_cancel_r with p; trivial.
now rewrite add_comm, sub_add.
Qed.
(** Properties of gcd *)
Definition gcd_0_l n : gcd 0 n == n := gcd_0_l_nonneg n (le_0_l n).
Definition gcd_0_r n : gcd n 0 == n := gcd_0_r_nonneg n (le_0_l n).
Definition gcd_diag n : gcd n n == n := gcd_diag_nonneg n (le_0_l n).
Definition gcd_unique' n m p := gcd_unique n m p (le_0_l p).
Definition gcd_unique_alt' n m p := gcd_unique_alt n m p (le_0_l p).
Definition divide_gcd_iff' n m := divide_gcd_iff n m (le_0_l n).
Lemma gcd_add_mult_diag_r : forall n m p, gcd n (m+p*n) == gcd n m.
Proof.
intros n m p. apply gcd_unique_alt'.
intros. rewrite gcd_divide_iff. split; intros (U,V); split; trivial.
apply divide_add_r; trivial. now apply divide_mul_r.
apply divide_add_cancel_r with (p*n); trivial.
now apply divide_mul_r. now rewrite add_comm.
Qed.
Lemma gcd_add_diag_r : forall n m, gcd n (m+n) == gcd n m.
Proof.
intros n m. rewrite <- (mul_1_l n) at 2. apply gcd_add_mult_diag_r.
Qed.
Lemma gcd_sub_diag_r : forall n m, n<=m -> gcd n (m-n) == gcd n m.
Proof.
intros n m H. symmetry.
rewrite <- (sub_add n m H) at 1. apply gcd_add_diag_r.
Qed.
(** On natural numbers, we should use a particular form
for the Bezout identity, since we don't have full subtraction. *)
Definition Bezout n m p := exists a b, a*n == p + b*m.
Instance Bezout_wd : Proper (eq==>eq==>eq==>iff) Bezout.
Proof.
unfold Bezout. intros x x' Hx y y' Hy z z' Hz.
setoid_rewrite Hx. setoid_rewrite Hy. now setoid_rewrite Hz.
Qed.
Lemma bezout_1_gcd : forall n m, Bezout n m 1 -> gcd n m == 1.
Proof.
intros n m (q & r & H).
apply gcd_unique; trivial using divide_1_l, le_0_1.
intros p Hn Hm.
apply divide_add_cancel_r with (r*m).
now apply divide_mul_r.
rewrite add_comm, <- H. now apply divide_mul_r.
Qed.
(** For strictly positive numbers, we have Bezout in the two directions. *)
Lemma gcd_bezout_pos_pos : forall n, 0<n -> forall m, 0<m ->
Bezout n m (gcd n m) /\ Bezout m n (gcd n m).
Proof.
intros n Hn. rewrite <- le_succ_l, <- one_succ in Hn.
pattern n. apply (fun H => strong_right_induction _ H 1); trivial.
unfold Bezout. solve_proper.
clear n Hn. intros n Hn IHn.
intros m Hm. rewrite <- le_succ_l, <- one_succ in Hm.
pattern m. apply (fun H => strong_right_induction _ H 1); trivial.
unfold Bezout. solve_proper.
clear m Hm. intros m Hm IHm.
destruct (lt_trichotomy n m) as [LT|[EQ|LT]].
(* n < m *)
destruct (IHm (m-n)) as ((a & b & EQ), (a' & b' & EQ')).
rewrite one_succ, le_succ_l.
apply lt_add_lt_sub_l; now nzsimpl.
apply sub_lt; order'.
split.
exists (a+b). exists b.
rewrite mul_add_distr_r, EQ, mul_sub_distr_l, <- add_assoc.
rewrite gcd_sub_diag_r by order.
rewrite sub_add. reflexivity. apply mul_le_mono_l; order.
exists a'. exists (a'+b').
rewrite gcd_sub_diag_r in EQ' by order.
rewrite (add_comm a'), mul_add_distr_r, add_assoc, <- EQ'.
rewrite mul_sub_distr_l, sub_add. reflexivity. apply mul_le_mono_l; order.
(* n = m *)
rewrite EQ. rewrite gcd_diag.
split.
exists 1. exists 0. now nzsimpl.
exists 1. exists 0. now nzsimpl.
(* m < n *)
rewrite gcd_comm, and_comm.
apply IHn; trivial.
now rewrite <- le_succ_l, <- one_succ.
Qed.
Lemma gcd_bezout_pos : forall n m, 0<n -> Bezout n m (gcd n m).
Proof.
intros n m Hn.
destruct (eq_0_gt_0_cases m) as [EQ|LT].
rewrite EQ, gcd_0_r. exists 1. exists 0. now nzsimpl.
now apply gcd_bezout_pos_pos.
Qed.
(** For arbitrary natural numbers, we could only say that at least
one of the Bezout identities holds. *)
Lemma gcd_bezout : forall n m,
Bezout n m (gcd n m) \/ Bezout m n (gcd n m).
Proof.
intros n m.
destruct (eq_0_gt_0_cases n) as [EQ|LT].
right. rewrite EQ, gcd_0_l. exists 1. exists 0. now nzsimpl.
left. now apply gcd_bezout_pos.
Qed.
(** Bezout on natural numbers commutes *)
Theorem bezout_comm : forall a b g,
b ~= 0 -> Bezout a b g -> Bezout b a g.
Proof.
intros a b g Hbz (u & v & Huv).
destruct (eq_0_gt_0_cases a) as [Haz| Haz].
-rewrite Haz in Huv |-*.
rewrite mul_0_r in Huv; symmetry in Huv.
apply eq_add_0 in Huv.
rewrite (proj1 Huv).
now exists 0, 0; nzsimpl.
-apply neq_0_lt_0 in Haz.
destruct (lt_trichotomy (u / b) (v / a)) as [Hm| Hm].
+apply lt_le_incl in Hm.
remember (v / a + 1) as k eqn:Hk.
exists (k * a - v), (k * b - u).
do 2 rewrite mul_sub_distr_r.
rewrite Huv.
rewrite (add_comm _ (v * b)).
rewrite sub_add_distr.
rewrite add_sub_assoc.
*rewrite add_comm, add_sub.
now rewrite mul_shuffle0.
*apply (add_le_mono_r _ _ (v * b)).
rewrite <- Huv.
rewrite sub_add.
--apply mul_le_mono_r.
rewrite Hk.
specialize (div_mod u b Hbz) as H1.
rewrite mul_add_distr_r, mul_1_l, mul_comm.
rewrite H1 at 1.
apply add_le_mono.
++now apply mul_le_mono_l.
++apply lt_le_incl.
apply mod_bound_pos.
**apply le_0_l.
**now apply neq_0_lt_0.
--rewrite mul_shuffle0.
apply mul_le_mono_r.
rewrite Hk.
specialize (div_mod v a Haz) as H1.
rewrite mul_add_distr_r, mul_1_l, mul_comm.
rewrite H1 at 1.
apply add_le_mono_l.
apply lt_le_incl.
apply mod_bound_pos.
++apply le_0_l.
++now apply neq_0_lt_0.
+remember (u / b + 1) as k eqn:Hk.
exists (k * a - v), (k * b - u).
do 2 rewrite mul_sub_distr_r.
rewrite Huv.
rewrite (add_comm _ (v * b)).
rewrite sub_add_distr.
rewrite add_sub_assoc.
*rewrite add_comm, add_sub.
now rewrite mul_shuffle0.
*apply (add_le_mono_r _ _ (v * b)).
rewrite sub_add.
--rewrite <- Huv.
apply mul_le_mono_r.
rewrite Hk.
specialize (div_mod u b Hbz) as H1.
rewrite mul_add_distr_r, mul_1_l, mul_comm.
rewrite H1 at 1.
apply add_le_mono_l.
apply lt_le_incl.
apply mod_bound_pos.
++apply le_0_l.
++now apply neq_0_lt_0.
--rewrite mul_shuffle0.
apply mul_le_mono_r.
rewrite Hk.
specialize (div_mod v a Haz) as H1.
rewrite mul_add_distr_r, mul_1_l, mul_comm.
rewrite H1 at 1.
apply add_le_mono.
++apply mul_le_mono_l.
destruct Hm as [Hm| Hm].
**now rewrite Hm.
**now apply lt_le_incl.
++apply lt_le_incl.
apply mod_bound_pos.
**apply le_0_l.
**now apply neq_0_lt_0.
Qed.
Lemma gcd_mul_mono_l :
forall n m p, gcd (p * n) (p * m) == p * gcd n m.
Proof.
intros n m p.
apply gcd_unique'.
apply mul_divide_mono_l, gcd_divide_l.
apply mul_divide_mono_l, gcd_divide_r.
intros q H H'.
destruct (eq_0_gt_0_cases n) as [EQ|LT].
rewrite EQ in *. now rewrite gcd_0_l.
destruct (gcd_bezout_pos n m) as (a & b & EQ); trivial.
apply divide_add_cancel_r with (p*m*b).
now apply divide_mul_l.
rewrite <- mul_assoc, <- mul_add_distr_l, add_comm, (mul_comm m), <- EQ.
rewrite (mul_comm a), mul_assoc.
now apply divide_mul_l.
Qed.
Lemma gcd_mul_mono_r :
forall n m p, gcd (n*p) (m*p) == gcd n m * p.
Proof.
intros n m p. rewrite !(mul_comm _ p). apply gcd_mul_mono_l.
Qed.
Lemma gauss : forall n m p, (n | m * p) -> gcd n m == 1 -> (n | p).
Proof.
intros n m p H G.
destruct (eq_0_gt_0_cases n) as [EQ|LT].
rewrite EQ in *. rewrite gcd_0_l in G. now rewrite <- (mul_1_l p), <- G.
destruct (gcd_bezout_pos n m) as (a & b & EQ); trivial.
rewrite G in EQ.
apply divide_add_cancel_r with (m*p*b).
now apply divide_mul_l.
rewrite (mul_comm _ b), mul_assoc. rewrite <- (mul_1_l p) at 2.
rewrite <- mul_add_distr_r, add_comm, <- EQ.
now apply divide_mul_l, divide_factor_r.
Qed.
Lemma divide_mul_split : forall n m p, n ~= 0 -> (n | m * p) ->
exists q r, n == q*r /\ (q | m) /\ (r | p).
Proof.
intros n m p Hn H.
assert (G := gcd_nonneg n m). le_elim G.
destruct (gcd_divide_l n m) as (q,Hq).
exists (gcd n m). exists q.
split. now rewrite mul_comm.
split. apply gcd_divide_r.
destruct (gcd_divide_r n m) as (r,Hr).
rewrite Hr in H. rewrite Hq in H at 1.
rewrite mul_shuffle0 in H. apply mul_divide_cancel_r in H; [|order].
apply gauss with r; trivial.
apply mul_cancel_r with (gcd n m); [order|].
rewrite mul_1_l.
rewrite <- gcd_mul_mono_r, <- Hq, <- Hr; order.
symmetry in G. apply gcd_eq_0 in G. destruct G as (Hn',_); order.
Qed.
(** TODO : relation between gcd and division and modulo *)
(** TODO : more about rel_prime (i.e. gcd == 1), about prime ... *)
End NGcdProp.
|
