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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(** 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. 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 strong_right_induction with (z:=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 strong_right_induction with (z:=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.
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. 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.
|
