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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Require Import NAxioms NSub NDiv NGcd.
(** * Least Common Multiple *)
(** Unlike other functions around, we will define lcm below instead of
axiomatizing it. Indeed, there is no "prior art" about lcm in the
standard library to be compliant with, and the generic definition
of lcm via gcd is quite reasonable.
By the way, we also state here some combined properties of div/mod
and gcd.
*)
Module Type NLcmProp
(Import A : NAxiomsSig')
(Import B : NSubProp A)
(Import C : NDivProp A B)
(Import D : NGcdProp A B).
(** Divibility and modulo *)
Lemma mod_divide : forall a b, b~=0 -> (a mod b == 0 <-> (b|a)).
Proof.
intros a b Hb. split.
intros Hab. exists (a/b). rewrite mul_comm.
rewrite (div_mod a b Hb) at 1. rewrite Hab; now nzsimpl.
intros (c,Hc). rewrite Hc. now apply mod_mul.
Qed.
Lemma divide_div_mul_exact : forall a b c, b~=0 -> (b|a) ->
(c*a)/b == c*(a/b).
Proof.
intros a b c Hb H.
apply mul_cancel_l with b; trivial.
rewrite mul_assoc, mul_shuffle0.
assert (H':=H). apply mod_divide, div_exact in H'; trivial.
rewrite <- H', (mul_comm a c).
symmetry. apply div_exact; trivial.
apply mod_divide; trivial.
now apply divide_mul_r.
Qed.
(** Gcd of divided elements, for exact divisions *)
Lemma gcd_div_factor : forall a b c, c~=0 -> (c|a) -> (c|b) ->
gcd (a/c) (b/c) == (gcd a b)/c.
Proof.
intros a b c Hc Ha Hb.
apply mul_cancel_l with c; try order.
assert (H:=gcd_greatest _ _ _ Ha Hb).
apply mod_divide, div_exact in H; try order.
rewrite <- H.
rewrite <- gcd_mul_mono_l; try order.
f_equiv; symmetry; apply div_exact; try order;
apply mod_divide; trivial; try order.
Qed.
Lemma gcd_div_gcd : forall a b g, g~=0 -> g == gcd a b ->
gcd (a/g) (b/g) == 1.
Proof.
intros a b g NZ EQ. rewrite gcd_div_factor.
now rewrite <- EQ, div_same.
generalize (gcd_nonneg a b); order.
rewrite EQ; apply gcd_divide_l.
rewrite EQ; apply gcd_divide_r.
Qed.
(** The following equality is crucial for Euclid algorithm *)
Lemma gcd_mod : forall a b, b~=0 -> gcd (a mod b) b == gcd b a.
Proof.
intros a b Hb. rewrite (gcd_comm _ b).
rewrite <- (gcd_add_mult_diag_r b (a mod b) (a/b)).
now rewrite add_comm, mul_comm, <- div_mod.
Qed.
(** We now define lcm thanks to gcd:
lcm a b = a * (b / gcd a b)
= (a / gcd a b) * b
= (a*b) / gcd a b
Nota: [lcm 0 0] should be 0, which isn't garantee with the third
equation above.
*)
Definition lcm a b := a*(b/gcd a b).
Instance lcm_wd : Proper (eq==>eq==>eq) lcm.
Proof. unfold lcm. solve_proper. Qed.
Lemma lcm_equiv1 : forall a b, gcd a b ~= 0 ->
a * (b / gcd a b) == (a*b)/gcd a b.
Proof.
intros a b H. rewrite divide_div_mul_exact; try easy. apply gcd_divide_r.
Qed.
Lemma lcm_equiv2 : forall a b, gcd a b ~= 0 ->
(a / gcd a b) * b == (a*b)/gcd a b.
Proof.
intros a b H. rewrite 2 (mul_comm _ b).
rewrite divide_div_mul_exact; try easy. apply gcd_divide_l.
Qed.
Lemma gcd_div_swap : forall a b,
(a / gcd a b) * b == a * (b / gcd a b).
Proof.
intros a b. destruct (eq_decidable (gcd a b) 0) as [EQ|NEQ].
apply gcd_eq_0 in EQ. destruct EQ as (EQ,EQ'). rewrite EQ, EQ'. now nzsimpl.
now rewrite lcm_equiv1, <-lcm_equiv2.
Qed.
Lemma divide_lcm_l : forall a b, (a | lcm a b).
Proof.
unfold lcm. intros a b. apply divide_factor_l.
Qed.
Lemma divide_lcm_r : forall a b, (b | lcm a b).
Proof.
unfold lcm. intros a b. rewrite <- gcd_div_swap.
apply divide_factor_r.
Qed.
Lemma divide_div : forall a b c, a~=0 -> (a|b) -> (b|c) -> (b/a|c/a).
Proof.
intros a b c Ha Hb (c',Hc). exists c'.
now rewrite <- divide_div_mul_exact, Hc.
Qed.
Lemma lcm_least : forall a b c,
(a | c) -> (b | c) -> (lcm a b | c).
Proof.
intros a b c Ha Hb. unfold lcm.
destruct (eq_decidable (gcd a b) 0) as [EQ|NEQ].
apply gcd_eq_0 in EQ. destruct EQ as (EQ,EQ'). rewrite EQ in *. now nzsimpl.
assert (Ga := gcd_divide_l a b).
assert (Gb := gcd_divide_r a b).
set (g:=gcd a b) in *.
assert (Ha' := divide_div g a c NEQ Ga Ha).
assert (Hb' := divide_div g b c NEQ Gb Hb).
destruct Ha' as (a',Ha'). rewrite Ha', mul_comm in Hb'.
apply gauss in Hb'; [|apply gcd_div_gcd; unfold g; trivial using gcd_comm].
destruct Hb' as (b',Hb').
exists b'.
rewrite mul_shuffle3, <- Hb'.
rewrite (proj2 (div_exact c g NEQ)).
rewrite Ha', mul_shuffle3, (mul_comm a a'). f_equiv.
symmetry. apply div_exact; trivial.
apply mod_divide; trivial.
apply mod_divide; trivial. transitivity a; trivial.
Qed.
Lemma lcm_comm : forall a b, lcm a b == lcm b a.
Proof.
intros a b. unfold lcm. rewrite (gcd_comm b), (mul_comm b).
now rewrite <- gcd_div_swap.
Qed.
Lemma lcm_divide_iff : forall n m p,
(lcm n m | p) <-> (n | p) /\ (m | p).
Proof.
intros. split. split.
transitivity (lcm n m); trivial using divide_lcm_l.
transitivity (lcm n m); trivial using divide_lcm_r.
intros (H,H'). now apply lcm_least.
Qed.
Lemma lcm_unique : forall n m p,
0<=p -> (n|p) -> (m|p) ->
(forall q, (n|q) -> (m|q) -> (p|q)) ->
lcm n m == p.
Proof.
intros n m p Hp Hn Hm H.
apply divide_antisym; trivial.
now apply lcm_least.
apply H. apply divide_lcm_l. apply divide_lcm_r.
Qed.
Lemma lcm_unique_alt : forall n m p, 0<=p ->
(forall q, (p|q) <-> (n|q) /\ (m|q)) ->
lcm n m == p.
Proof.
intros n m p Hp H.
apply lcm_unique; trivial.
apply H, divide_refl.
apply H, divide_refl.
intros. apply H. now split.
Qed.
Lemma lcm_assoc : forall n m p, lcm n (lcm m p) == lcm (lcm n m) p.
Proof.
intros. apply lcm_unique_alt. apply le_0_l.
intros. now rewrite !lcm_divide_iff, and_assoc.
Qed.
Lemma lcm_0_l : forall n, lcm 0 n == 0.
Proof.
intros. apply lcm_unique; trivial. order.
apply divide_refl.
apply divide_0_r.
Qed.
Lemma lcm_0_r : forall n, lcm n 0 == 0.
Proof.
intros. now rewrite lcm_comm, lcm_0_l.
Qed.
Lemma lcm_1_l : forall n, lcm 1 n == n.
Proof.
intros. apply lcm_unique; trivial using divide_1_l, le_0_l, divide_refl.
Qed.
Lemma lcm_1_r : forall n, lcm n 1 == n.
Proof.
intros. now rewrite lcm_comm, lcm_1_l.
Qed.
Lemma lcm_diag : forall n, lcm n n == n.
Proof.
intros. apply lcm_unique; trivial using divide_refl, le_0_l.
Qed.
Lemma lcm_eq_0 : forall n m, lcm n m == 0 <-> n == 0 \/ m == 0.
Proof.
intros. split.
intros EQ.
apply eq_mul_0.
apply divide_0_l. rewrite <- EQ. apply lcm_least.
apply divide_factor_l. apply divide_factor_r.
destruct 1 as [EQ|EQ]; rewrite EQ. apply lcm_0_l. apply lcm_0_r.
Qed.
Lemma divide_lcm_eq_r : forall n m, (n|m) -> lcm n m == m.
Proof.
intros n m H. apply lcm_unique_alt; trivial using le_0_l.
intros q. split. split; trivial. now transitivity m.
now destruct 1.
Qed.
Lemma divide_lcm_iff : forall n m, (n|m) <-> lcm n m == m.
Proof.
intros n m. split. now apply divide_lcm_eq_r.
intros EQ. rewrite <- EQ. apply divide_lcm_l.
Qed.
Lemma lcm_mul_mono_l :
forall n m p, lcm (p * n) (p * m) == p * lcm n m.
Proof.
intros n m p.
destruct (eq_decidable p 0) as [Hp|Hp].
rewrite Hp. nzsimpl. rewrite lcm_0_l. now nzsimpl.
destruct (eq_decidable (gcd n m) 0) as [Hg|Hg].
apply gcd_eq_0 in Hg. destruct Hg as (Hn,Hm); rewrite Hn, Hm.
nzsimpl. rewrite lcm_0_l. now nzsimpl.
unfold lcm.
rewrite gcd_mul_mono_l.
rewrite mul_assoc. f_equiv.
now rewrite div_mul_cancel_l.
Qed.
Lemma lcm_mul_mono_r :
forall n m p, lcm (n * p) (m * p) == lcm n m * p.
Proof.
intros n m p. now rewrite !(mul_comm _ p), lcm_mul_mono_l, mul_comm.
Qed.
Lemma gcd_1_lcm_mul : forall n m, n~=0 -> m~=0 ->
(gcd n m == 1 <-> lcm n m == n*m).
Proof.
intros n m Hn Hm. split; intros H.
unfold lcm. rewrite H. now rewrite div_1_r.
unfold lcm in *.
apply mul_cancel_l in H; trivial.
assert (Hg : gcd n m ~= 0) by (red; rewrite gcd_eq_0; destruct 1; order).
assert (H' := gcd_divide_r n m).
apply mod_divide in H'; trivial. apply div_exact in H'; trivial.
rewrite H in H'.
rewrite <- (mul_1_l m) in H' at 1.
now apply mul_cancel_r in H'.
Qed.
End NLcmProp.
|
