Module mathcomp.boot.div
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
This file deals with divisibility for natural numbers.
It contains the definitions of:
edivn m d == the pair composed of the quotient and remainder
of the Euclidean division of m by d.
m %/ d == quotient of the Euclidean division of m by d.
m %% d == remainder of the Euclidean division of m by d.
m = n %[mod d] <-> m equals n modulo d.
m == n %[mod d] <=> m equals n modulo d (boolean version).
m <> n %[mod d] <-> m differs from n modulo d.
m != n %[mod d] <=> m differs from n modulo d (boolean version).
d %| m <=> d divides m.
gcdn m n == the GCD of m and n.
egcdn m n == the extended GCD (Bezout coefficient pair) of m and n.
If egcdn m n = (u, v), then gcdn m n = m * u - n * v.
lcmn m n == the LCM of m and n.
coprime m n <=> m and n are coprime (:= gcdn m n == 1).
chinese m n r s == witness of the chinese remainder theorem.
We adjoin an m to operator suffixes to indicate a nested %% (modn), as in
modnDml : m %% d + n = m + n %[mod d].
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Euclidean division
Definition edivn_rec d :=
fix loop m q := if m - d is m'.+1 then loop m' q.+1 else (q, m).
Definition edivn m d := if d > 0 then edivn_rec d.-1 m 0 else (0, m).
Variant edivn_spec m d : nat * nat -> Type :=
EdivnSpec q r of m = q * d + r & (d > 0) ==> (r < d) : edivn_spec m d (q, r).
Lemma edivnP m d : edivn_spec m d (edivn m d).
Proof.
Lemma edivn_eq d q r : r < d -> edivn (q * d + r) d = (q, r).
Proof.
move=> lt_rd; have d_gt0: 0 < d by apply: leq_trans lt_rd.
case: edivnP lt_rd => q' r'; rewrite d_gt0 /=.
wlog: q q' r r' / q <= q' by case/orP: (leq_total q q'); last symmetry; eauto.
have [||-> _ /addnI ->] //= := ltngtP q q'.
rewrite -(leq_pmul2r d_gt0) => /leq_add lt_qr _ eq_qr _ /lt_qr {lt_qr}.
by rewrite addnS ltnNge mulSn -addnA eq_qr addnCA addnA leq_addr.
Qed.
case: edivnP lt_rd => q' r'; rewrite d_gt0 /=.
wlog: q q' r r' / q <= q' by case/orP: (leq_total q q'); last symmetry; eauto.
have [||-> _ /addnI ->] //= := ltngtP q q'.
rewrite -(leq_pmul2r d_gt0) => /leq_add lt_qr _ eq_qr _ /lt_qr {lt_qr}.
by rewrite addnS ltnNge mulSn -addnA eq_qr addnCA addnA leq_addr.
Qed.
Definition divn m d := (edivn m d).1.
Notation "m %/ d" := (divn m d) : nat_scope.
Definition modn_rec d := fix loop m := if m - d is m'.+1 then loop m' else m.
Definition modn m d := if d > 0 then modn_rec d.-1 m else m.
Notation "m %% d" := (modn m d) : nat_scope.
Notation "m = n %[mod d ]" := (m %% d = n %% d) : nat_scope.
Notation "m == n %[mod d ]" := (m %% d == n %% d) : nat_scope.
Notation "m <> n %[mod d ]" := (m %% d <> n %% d) : nat_scope.
Notation "m != n %[mod d ]" := (m %% d != n %% d) : nat_scope.
Lemma modn_def m d : m %% d = (edivn m d).2.
Proof.
Lemma edivn_def m d : edivn m d = (m %/ d, m %% d).
Lemma divn_eq m d : m = m %/ d * d + m %% d.
Lemma div0n d : 0 %/ d = 0
Proof.
by case: d. Qed.
Proof.
by []. Qed.
Proof.
by case: d. Qed.
Proof.
by []. Qed.
Lemma divn_small m d : m < d -> m %/ d = 0.
Lemma divnMDl q m d : 0 < d -> (q * d + m) %/ d = q + m %/ d.
Proof.
Lemma mulnK m d : 0 < d -> m * d %/ d = m.
Lemma mulKn m d : 0 < d -> d * m %/ d = m.
Lemma expnB p m n : p > 0 -> m >= n -> p ^ (m - n) = p ^ m %/ p ^ n.
Lemma modn1 m : m %% 1 = 0.
Lemma divn1 m : m %/ 1 = m.
Lemma divnn d : d %/ d = (0 < d).
Lemma divnMl p m d : p > 0 -> p * m %/ (p * d) = m %/ d.
Proof.
Lemma divnMr p m d : p > 0 -> m * p %/ (d * p) = m %/ d.
Arguments divnMr [p m d].
Lemma ltn_mod m d : (m %% d < d) = (0 < d).
Lemma ltn_pmod m d : 0 < d -> m %% d < d.
Proof.
Lemma leq_divM m d : m %/ d * d <= m.
#[deprecated(since="mathcomp 2.4.0", use=leq_divM)]
Notation leq_trunc_div := leq_divM (only parsing).
Lemma leq_mod m d : m %% d <= m.
Lemma leq_div m d : m %/ d <= m.
Lemma ltn_ceil m d : 0 < d -> m < (m %/ d).+1 * d.
Lemma ltn_divLR m n d : d > 0 -> (m %/ d < n) = (m < n * d).
Proof.
move=> d_gt0; apply/idP/idP.
by rewrite -(leq_pmul2r d_gt0); apply: leq_trans (ltn_ceil _ _).
rewrite !ltnNge -(@leq_pmul2r d n) //; apply: contra => le_nd_floor.
exact: leq_trans le_nd_floor (leq_divM _ _).
Qed.
by rewrite -(leq_pmul2r d_gt0); apply: leq_trans (ltn_ceil _ _).
rewrite !ltnNge -(@leq_pmul2r d n) //; apply: contra => le_nd_floor.
exact: leq_trans le_nd_floor (leq_divM _ _).
Qed.
Lemma leq_divRL m n d : d > 0 -> (m <= n %/ d) = (m * d <= n).
Lemma ltn_Pdiv m d : 1 < d -> 0 < m -> m %/ d < m.
Lemma divn_gt0 d m : 0 < d -> (0 < m %/ d) = (d <= m).
Lemma leq_div2r d m n : m <= n -> m %/ d <= n %/ d.
Proof.
Lemma leq_div2l m d e : 0 < d -> d <= e -> m %/ e <= m %/ d.
Lemma edivnD m n d (offset := m %% d + n %% d >= d) : 0 < d ->
edivn (m + n) d = (m %/ d + n %/ d + offset, m %% d + n %% d - offset * d).
Proof.
rewrite {}/offset; case: d => // d _; rewrite /divn !modn_def.
case: (edivnP m d.+1) (edivnP n d.+1) => [/= q r -> r_lt] [/= p s -> s_lt].
rewrite addnACA -mulnDl; have [r_le s_le] := (ltnW r_lt, ltnW s_lt).
have [d_ge|d_lt] := leqP; first by rewrite addn0 mul0n subn0 edivn_eq.
rewrite addn1 mul1n -[in LHS](subnKC d_lt) addnA -mulSnr edivn_eq//.
by rewrite ltn_subLR// -addnS leq_add.
Qed.
case: (edivnP m d.+1) (edivnP n d.+1) => [/= q r -> r_lt] [/= p s -> s_lt].
rewrite addnACA -mulnDl; have [r_le s_le] := (ltnW r_lt, ltnW s_lt).
have [d_ge|d_lt] := leqP; first by rewrite addn0 mul0n subn0 edivn_eq.
rewrite addn1 mul1n -[in LHS](subnKC d_lt) addnA -mulSnr edivn_eq//.
by rewrite ltn_subLR// -addnS leq_add.
Qed.
Lemma divnD m n d : 0 < d ->
(m + n) %/ d = (m %/ d) + (n %/ d) + (m %% d + n %% d >= d).
Lemma modnD m n d : 0 < d ->
(m + n) %% d = m %% d + n %% d - (m %% d + n %% d >= d) * d.
Lemma leqDmod m n d : 0 < d ->
(d <= m %% d + n %% d) = ((m + n) %% d < n %% d).
Proof.
Lemma divnB n m d : 0 < d ->
(m - n) %/ d = (m %/ d) - (n %/ d) - (m %% d < n %% d).
Proof.
Lemma modnB m n d : 0 < d -> n <= m ->
(m - n) %% d = (m %% d < n %% d) * d + m %% d - n %% d.
Proof.
Lemma edivnB m n d (offset := m %% d < n %% d) : 0 < d -> n <= m ->
edivn (m - n) d = (m %/ d - n %/ d - offset, offset * d + m %% d - n %% d).
Lemma leq_divDl p m n : (m + n) %/ p <= m %/ p + n %/ p + 1.
Lemma geq_divBl k m p : k %/ p - m %/ p <= (k - m) %/ p + 1.
Proof.
Lemma divnMA m n p : m %/ (n * p) = m %/ n %/ p.
Proof.
Lemma divnAC m n p : m %/ n %/ p = m %/ p %/ n.
Lemma modn_small m d : m < d -> m %% d = m.
Proof.
Lemma modn_mod m d : m %% d = m %[mod d].
Proof.
Lemma modnMDl p m d : p * d + m = m %[mod d].
Proof.
Lemma muln_modr p m d : p * (m %% d) = (p * m) %% (p * d).
Proof.
Lemma muln_modl p m d : (m %% d) * p = (m * p) %% (d * p).
Lemma modn_divl m n d : (m %/ d) %% n = m %% (n * d) %/ d.
Proof.
Lemma modnDl m d : d + m = m %[mod d].
Lemma modnDr m d : m + d = m %[mod d]
Lemma modnn d : d %% d = 0
Lemma modnMl p d : p * d %% d = 0.
Lemma modnMr p d : d * p %% d = 0
Lemma modnDml m n d : m %% d + n = m + n %[mod d].
Lemma modnDmr m n d : m + n %% d = m + n %[mod d].
Lemma modnDm m n d : m %% d + n %% d = m + n %[mod d].
Lemma eqn_modDl p m n d : (p + m == p + n %[mod d]) = (m == n %[mod d]).
Proof.
Lemma eqn_modDr p m n d : (m + p == n + p %[mod d]) = (m == n %[mod d]).
Lemma modnMml m n d : m %% d * n = m * n %[mod d].
Lemma modnMmr m n d : m * (n %% d) = m * n %[mod d].
Lemma modnMm m n d : m %% d * (n %% d) = m * n %[mod d].
Lemma modn2 m : m %% 2 = odd m.
Lemma divn2 m : m %/ 2 = m./2.
Lemma odd_mod m d : odd d = false -> odd (m %% d) = odd m.
Lemma modnXm m n a : (a %% n) ^ m = a ^ m %[mod n].
Lemma modnMDXl p m n d : (p * d + m) ^ n = m ^ n %[mod d].
Lemma modnMBXl p m n d :
m <= p * d -> (p * d - m) ^ n = (p * d - m) ^ odd n * m ^ n./2.*2 %[mod d].
Proof.
move=> mpd; have [k]:= ubnP n; elim: k n => //= k IH; case => [|[|n nk]] //.
by rewrite muln1.
rewrite /= negbK doubleS -addn2 expnD -modnMmr.
suff -> : (p * d - m) ^ 2 = m ^ 2 %[mod d].
by rewrite modnMmr -modnMml IH 1? ltnW // modnMml -mulnA -expnD addn2.
rewrite -sqrnD_sub // -(modnMDXl p _ _ d).
suff pdm4 : 4 * (p * d * m) <= (p * d + m) ^ 2.
rewrite -[in RHS](subnK pdm4) -modnDmr -modnMmr [p * _ * _]mulnAC.
by rewrite modnMl muln0 mod0n addn0.
case: ltngtP mpd => [mpd|//|->] _; last by rewrite addnn -mul2n expnMn.
by apply: ltnW; rewrite -subn_gt0 sqrnD_sub ?expn_gt0 ?subn_gt0 ?mpd // ltnW.
Qed.
by rewrite muln1.
rewrite /= negbK doubleS -addn2 expnD -modnMmr.
suff -> : (p * d - m) ^ 2 = m ^ 2 %[mod d].
by rewrite modnMmr -modnMml IH 1? ltnW // modnMml -mulnA -expnD addn2.
rewrite -sqrnD_sub // -(modnMDXl p _ _ d).
suff pdm4 : 4 * (p * d * m) <= (p * d + m) ^ 2.
rewrite -[in RHS](subnK pdm4) -modnDmr -modnMmr [p * _ * _]mulnAC.
by rewrite modnMl muln0 mod0n addn0.
case: ltngtP mpd => [mpd|//|->] _; last by rewrite addnn -mul2n expnMn.
by apply: ltnW; rewrite -subn_gt0 sqrnD_sub ?expn_gt0 ?subn_gt0 ?mpd // ltnW.
Qed.
Lemma modn_sqrB m n : n <= m -> (m - n) ^ 2 = n ^ 2 %[mod m].
Divisibility *
Definition dvdn d m := m %% d == 0.
Notation "m %| d" := (dvdn m d) : nat_scope.
Lemma dvdnP d m : reflect (exists k, m = k * d) (d %| m).
Proof.
Lemma dvdn0 d : d %| 0.
Proof.
by case: d. Qed.
Lemma dvd0n n : (0 %| n) = (n == 0).
Proof.
by case: n. Qed.
Lemma dvdn1 d : (d %| 1) = (d == 1).
Proof.
Lemma dvd1n m : 1 %| m.
Lemma dvdn_gt0 d m : m > 0 -> d %| m -> d > 0.
Proof.
Lemma dvdnn m : m %| m.
Lemma dvdn_mull d m n : d %| n -> d %| m * n.
Lemma dvdn_mulr d m n : d %| m -> d %| m * n.
#[global] Hint Resolve dvdn0 dvd1n dvdnn dvdn_mull dvdn_mulr : core.
Lemma dvdn_mul d1 d2 m1 m2 : d1 %| m1 -> d2 %| m2 -> d1 * d2 %| m1 * m2.
Lemma dvdn_trans n d m : d %| n -> n %| m -> d %| m.
Lemma dvdn_eq d m : (d %| m) = (m %/ d * d == m).
Proof.
Lemma dvdn2 n : (2 %| n) = ~~ odd n.
Lemma dvdn_odd m n : m %| n -> odd n -> odd m.
Proof.
Lemma divnK d m : d %| m -> m %/ d * d = m.
Lemma leq_divLR d m n : d %| m -> (m %/ d <= n) = (m <= n * d).
Proof.
Lemma ltn_divRL d m n : d %| m -> (n < m %/ d) = (n * d < m).
Lemma eqn_div d m n : d > 0 -> d %| m -> (n == m %/ d) = (n * d == m).
Proof.
Lemma eqn_mul d m n : d > 0 -> d %| m -> (m == n * d) = (m %/ d == n).
Lemma divn_mulAC d m n : d %| m -> m %/ d * n = m * n %/ d.
Proof.
Lemma muln_divA d m n : d %| n -> m * (n %/ d) = m * n %/ d.
Proof.
Lemma muln_divCA d m n : d %| m -> d %| n -> m * (n %/ d) = n * (m %/ d).
Proof.
Lemma divnA m n p : p %| n -> m %/ (n %/ p) = m * p %/ n.
Lemma modn_dvdm m n d : d %| m -> n %% m = n %[mod d].
Lemma dvdn_leq d m : 0 < m -> d %| m -> d <= m.
Lemma gtnNdvd n d : 0 < n -> n < d -> (d %| n) = false.
Proof.
Lemma eqn_dvd m n : (m == n) = (m %| n) && (n %| m).
Proof.
Lemma dvdn_pmul2l p d m : 0 < p -> (p * d %| p * m) = (d %| m).
Arguments dvdn_pmul2l [p d m].
Lemma dvdn_pmul2r p d m : 0 < p -> (d * p %| m * p) = (d %| m).
Proof.
Lemma dvdn_divLR p d m : 0 < p -> p %| d -> (d %/ p %| m) = (d %| m * p).
Proof.
Lemma dvdn_divRL p d m : p %| m -> (d %| m %/ p) = (d * p %| m).
Proof.
Lemma dvdn_div d m : d %| m -> m %/ d %| m.
Lemma dvdn_exp2l p m n : m <= n -> p ^ m %| p ^ n.
Lemma dvdn_Pexp2l p m n : p > 1 -> (p ^ m %| p ^ n) = (m <= n).
Proof.
Lemma dvdn_exp2r m n k : m %| n -> m ^ k %| n ^ k.
Lemma divn_modl m n d : d %| n -> (m %% n) %/ d = (m %/ d) %% (n %/ d).
Lemma dvdn_addr m d n : d %| m -> (d %| m + n) = (d %| n).
Lemma dvdn_addl n d m : d %| n -> (d %| m + n) = (d %| m).
Lemma dvdn_add d m n : d %| m -> d %| n -> d %| m + n.
Proof.
Lemma dvdn_add_eq d m n : d %| m + n -> (d %| m) = (d %| n).
Lemma dvdn_subr d m n : n <= m -> d %| m -> (d %| m - n) = (d %| n).
Proof.
Lemma dvdn_subl d m n : n <= m -> d %| n -> (d %| m - n) = (d %| m).
Lemma dvdn_sub d m n : d %| m -> d %| n -> d %| m - n.
Lemma dvdn_exp k d m : 0 < k -> d %| m -> d %| (m ^ k).
Lemma dvdn_fact m n : 0 < m <= n -> m %| n`!.
Proof.
#[global] Hint Resolve dvdn_add dvdn_sub dvdn_exp : core.
Lemma eqn_mod_dvd d m n : n <= m -> (m == n %[mod d]) = (d %| m - n).
Lemma divnDMl q m d : 0 < d -> (m + q * d) %/ d = (m %/ d) + q.
Lemma divnMBl q m d : 0 < d -> (q * d - m) %/ d = q - (m %/ d) - (~~ (d %| m)).
Lemma divnBMl q m d : (m - q * d) %/ d = (m %/ d) - q.
Lemma divnDl m n d : d %| m -> (m + n) %/ d = m %/ d + n %/ d.
Lemma divnDr m n d : d %| n -> (m + n) %/ d = m %/ d + n %/ d.
Lemma divnBl m n d : d %| m -> (m - n) %/ d = m %/ d - (n %/ d) - (~~ (d %| n)).
Lemma divnBr m n d : d %| n -> (m - n) %/ d = m %/ d - n %/ d.
Lemma edivnS m d : 0 < d -> edivn m.+1 d =
if d %| m.+1 then ((m %/ d).+1, 0) else (m %/ d, (m %% d).+1).
Proof.
case: d => [|[|d]] //= _; first by rewrite edivn_def modn1 dvd1n !divn1.
rewrite -addn1 /dvdn modn_def edivnD//= (@modn_small 1)// (@divn_small 1)//.
rewrite addn1 addn0 ltnS; have [||<-] := ltngtP d.+1.
- by rewrite ltnNge -ltnS ltn_pmod.
- by rewrite addn0 mul0n subn0.
- by rewrite addn1 mul1n subnn.
Qed.
rewrite -addn1 /dvdn modn_def edivnD//= (@modn_small 1)// (@divn_small 1)//.
rewrite addn1 addn0 ltnS; have [||<-] := ltngtP d.+1.
- by rewrite ltnNge -ltnS ltn_pmod.
- by rewrite addn0 mul0n subn0.
- by rewrite addn1 mul1n subnn.
Qed.
Lemma modnS m d : m.+1 %% d = if d %| m.+1 then 0 else (m %% d).+1.
Lemma divnS m d : 0 < d -> m.+1 %/ d = (d %| m.+1) + m %/ d.
Lemma divn_pred m d : m.-1 %/ d = (m %/ d) - (d %| m).
Lemma modn_pred m d : d != 1 -> 0 < m ->
m.-1 %% d = if d %| m then d.-1 else (m %% d).-1.
Proof.
Lemma edivn_pred m d : d != 1 -> 0 < m ->
edivn m.-1 d = if d %| m then ((m %/ d).-1, d.-1) else (m %/ d, (m %% d).-1).
Proof.
A function that computes the gcd of 2 numbers
Fixpoint gcdn m n :=
let n' := n %% m in if n' is 0 then m else
if m - n'.-1 is m'.+1 then gcdn (m' %% n') n' else n'.
Arguments gcdn : simpl never.
Lemma gcdnE m n : gcdn m n = if m == 0 then n else gcdn (n %% m) m.
Proof.
Lemma gcdnn : idempotent_op gcdn.
Lemma gcdnC : commutative gcdn.
Proof.
Lemma gcd0n : left_id 0 gcdn
Proof.
by case. Qed.
Proof.
by case. Qed.
Lemma gcd1n : left_zero 1 gcdn.
Lemma gcdn1 : right_zero 1 gcdn.
Lemma dvdn_gcdr m n : gcdn m n %| n.
Proof.
elim/ltn_ind: m n => -[|m] IHm [|n] //=.
rewrite gcdnE; case def_p: (_ %% _) => [|p]; first by rewrite /dvdn def_p.
have lt_pm: p < m by rewrite -ltnS -def_p ltn_pmod.
rewrite /= (divn_eq n.+1 m.+1) def_p dvdn_addr ?dvdn_mull //; first exact: IHm.
by rewrite gcdnE /= IHm // (ltn_trans (ltn_pmod _ _)).
Qed.
rewrite gcdnE; case def_p: (_ %% _) => [|p]; first by rewrite /dvdn def_p.
have lt_pm: p < m by rewrite -ltnS -def_p ltn_pmod.
rewrite /= (divn_eq n.+1 m.+1) def_p dvdn_addr ?dvdn_mull //; first exact: IHm.
by rewrite gcdnE /= IHm // (ltn_trans (ltn_pmod _ _)).
Qed.
Lemma dvdn_gcdl m n : gcdn m n %| m.
Lemma gcdn_gt0 m n : (0 < gcdn m n) = (0 < m) || (0 < n).
Lemma gcdnMDl k m n : gcdn m (k * m + n) = gcdn m n.
Lemma gcdnDl m n : gcdn m (m + n) = gcdn m n.
Lemma gcdnDr m n : gcdn m (n + m) = gcdn m n.
Lemma gcdnMl n m : gcdn n (m * n) = n.
Lemma gcdnMr n m : gcdn n (n * m) = n.
Lemma gcdn_idPl {m n} : reflect (gcdn m n = m) (m %| n).
Lemma gcdn_idPr {m n} : reflect (gcdn m n = n) (n %| m).
Lemma expn_min e m n : e ^ minn m n = gcdn (e ^ m) (e ^ n).
Proof.
Lemma gcdn_modr m n : gcdn m (n %% m) = gcdn m n.
Lemma gcdn_modl m n : gcdn (m %% n) n = gcdn m n.
Fixpoint Bezout_rec km kn qs :=
if qs is q :: qs' then Bezout_rec kn (NatTrec.add_mul q kn km) qs'
else (km, kn).
Fixpoint egcdn_rec m n s qs :=
if s is s'.+1 then
let: (q, r) := edivn m n in
if r > 0 then egcdn_rec n r s' (q :: qs) else
if odd (size qs) then qs else q.-1 :: qs
else [::0].
Definition egcdn m n := Bezout_rec 0 1 (egcdn_rec m n n [::]).
Variant egcdn_spec m n : nat * nat -> Type :=
EgcdnSpec km kn of km * m = kn * n + gcdn m n & kn * gcdn m n < m :
egcdn_spec m n (km, kn).
Lemma egcd0n n : egcdn 0 n = (1, 0).
Proof.
by case: n. Qed.
Lemma egcdnP m n : m > 0 -> egcdn_spec m n (egcdn m n).
Proof.
have [-> /= | n_gt0 m_gt0] := posnP n; first by split; rewrite // mul1n gcdn0.
rewrite /egcdn; set s := (s in egcdn_rec _ _ s); pose bz := Bezout_rec n m [::].
have: n < s.+1 by []; move defSpec: (egcdn_spec bz.2 bz.1) s => Spec s.
elim: s => [[]|s IHs] //= in n m (qs := [::]) bz defSpec n_gt0 m_gt0 *.
case: edivnP => q r def_m; rewrite n_gt0 ltnS /= => lt_rn le_ns1.
case: posnP => [r0 {s le_ns1 IHs lt_rn}|r_gt0]; last first.
by apply: IHs => //=; [rewrite natTrecE -def_m | rewrite (leq_trans lt_rn)].
rewrite {r}r0 addn0 in def_m; set b := odd _; pose d := gcdn m n.
pose km := ~~ b : nat; pose kn := if b then 1 else q.-1.
rewrite [bz in Spec bz](_ : _ = Bezout_rec km kn qs).
by rewrite /kn /km; case: (b) => //=; rewrite natTrecE addn0 muln1.
have def_d: d = n by rewrite /d def_m gcdnC gcdnE modnMl gcd0n -[n]prednK.
have: km * m + 2 * b * d = kn * n + d.
rewrite {}/kn {}/km def_m def_d -mulSnr; case: b; rewrite //= addn0 mul1n.
by rewrite prednK //; apply: dvdn_gt0 m_gt0 _; rewrite def_m dvdn_mulr.
have{def_m}: kn * d <= m.
have q_gt0 : 0 < q by rewrite def_m muln_gt0 n_gt0 ?andbT in m_gt0.
by rewrite /kn; case b; rewrite def_d def_m leq_pmul2r // leq_pred.
have{def_d}: km * d <= n by rewrite -[n]mul1n def_d leq_pmul2r // leq_b1.
move: km {q}kn m_gt0 n_gt0 defSpec; rewrite {}/b {}/d {}/bz.
elim: qs m n => [|q qs IHq] n r kn kr n_gt0 r_gt0 /=.
set d := gcdn n r; rewrite mul0n addn0 => <- le_kn_r _ def_d; split=> //.
have d_gt0: 0 < d by rewrite gcdn_gt0 n_gt0.
have /ltn_pmul2l<-: 0 < kn by rewrite -(ltn_pmul2r n_gt0) def_d ltn_addl.
by rewrite def_d -addn1 leq_add // mulnCA leq_mul2l le_kn_r orbT.
rewrite !natTrecE; set m := _ + r; set km := _ + kn; pose d := gcdn m n.
have ->: gcdn n r = d by rewrite [d]gcdnC gcdnMDl.
have m_gt0: 0 < m by rewrite addn_gt0 r_gt0 orbT.
have d_gt0: 0 < d by rewrite gcdn_gt0 m_gt0.
move=> {}/IHq IHq le_kn_r le_kr_n def_d; apply: IHq => //; rewrite -/d.
by rewrite mulnDl leq_add // -mulnA leq_mul2l le_kr_n orbT.
apply: (@addIn d); rewrite mulnDr -addnA addnACA -def_d addnACA mulnA.
rewrite -!mulnDl -mulnDr -addnA [kr * _]mulnC; congr addn.
by rewrite addnC addn_negb muln1 mul2n addnn.
Qed.
rewrite /egcdn; set s := (s in egcdn_rec _ _ s); pose bz := Bezout_rec n m [::].
have: n < s.+1 by []; move defSpec: (egcdn_spec bz.2 bz.1) s => Spec s.
elim: s => [[]|s IHs] //= in n m (qs := [::]) bz defSpec n_gt0 m_gt0 *.
case: edivnP => q r def_m; rewrite n_gt0 ltnS /= => lt_rn le_ns1.
case: posnP => [r0 {s le_ns1 IHs lt_rn}|r_gt0]; last first.
by apply: IHs => //=; [rewrite natTrecE -def_m | rewrite (leq_trans lt_rn)].
rewrite {r}r0 addn0 in def_m; set b := odd _; pose d := gcdn m n.
pose km := ~~ b : nat; pose kn := if b then 1 else q.-1.
rewrite [bz in Spec bz](_ : _ = Bezout_rec km kn qs).
by rewrite /kn /km; case: (b) => //=; rewrite natTrecE addn0 muln1.
have def_d: d = n by rewrite /d def_m gcdnC gcdnE modnMl gcd0n -[n]prednK.
have: km * m + 2 * b * d = kn * n + d.
rewrite {}/kn {}/km def_m def_d -mulSnr; case: b; rewrite //= addn0 mul1n.
by rewrite prednK //; apply: dvdn_gt0 m_gt0 _; rewrite def_m dvdn_mulr.
have{def_m}: kn * d <= m.
have q_gt0 : 0 < q by rewrite def_m muln_gt0 n_gt0 ?andbT in m_gt0.
by rewrite /kn; case b; rewrite def_d def_m leq_pmul2r // leq_pred.
have{def_d}: km * d <= n by rewrite -[n]mul1n def_d leq_pmul2r // leq_b1.
move: km {q}kn m_gt0 n_gt0 defSpec; rewrite {}/b {}/d {}/bz.
elim: qs m n => [|q qs IHq] n r kn kr n_gt0 r_gt0 /=.
set d := gcdn n r; rewrite mul0n addn0 => <- le_kn_r _ def_d; split=> //.
have d_gt0: 0 < d by rewrite gcdn_gt0 n_gt0.
have /ltn_pmul2l<-: 0 < kn by rewrite -(ltn_pmul2r n_gt0) def_d ltn_addl.
by rewrite def_d -addn1 leq_add // mulnCA leq_mul2l le_kn_r orbT.
rewrite !natTrecE; set m := _ + r; set km := _ + kn; pose d := gcdn m n.
have ->: gcdn n r = d by rewrite [d]gcdnC gcdnMDl.
have m_gt0: 0 < m by rewrite addn_gt0 r_gt0 orbT.
have d_gt0: 0 < d by rewrite gcdn_gt0 m_gt0.
move=> {}/IHq IHq le_kn_r le_kr_n def_d; apply: IHq => //; rewrite -/d.
by rewrite mulnDl leq_add // -mulnA leq_mul2l le_kr_n orbT.
apply: (@addIn d); rewrite mulnDr -addnA addnACA -def_d addnACA mulnA.
rewrite -!mulnDl -mulnDr -addnA [kr * _]mulnC; congr addn.
by rewrite addnC addn_negb muln1 mul2n addnn.
Qed.
Lemma Bezoutl m n : m > 0 -> {a | a < m & m %| gcdn m n + a * n}.
Proof.
Lemma Bezoutr m n : n > 0 -> {a | a < n & n %| gcdn m n + a * m}.
Lemma dvdn_gcd p m n : (p %| gcdn m n) = (p %| m) && (p %| n).
Proof.
Lemma gcdnAC : right_commutative gcdn.
Proof.
Lemma gcdnA : associative gcdn.
Lemma gcdnCA : left_commutative gcdn.
Lemma gcdnACA : interchange gcdn gcdn.
Lemma muln_gcdr : right_distributive muln gcdn.
Proof.
Lemma muln_gcdl : left_distributive muln gcdn.
Lemma gcdn_def d m n :
d %| m -> d %| n -> (forall d', d' %| m -> d' %| n -> d' %| d) ->
gcdn m n = d.
Proof.
Lemma muln_divCA_gcd n m : n * (m %/ gcdn n m) = m * (n %/ gcdn n m).
Proof.
Definition lcmn m n := m * n %/ gcdn m n.
Lemma lcmnC : commutative lcmn.
Lemma lcm0n : left_zero 0 lcmn
Proof.
Lemma lcm1n : left_id 1 lcmn.
Lemma lcmn1 : right_id 1 lcmn.
Lemma muln_lcm_gcd m n : lcmn m n * gcdn m n = m * n.
Lemma lcmn_gt0 m n : (0 < lcmn m n) = (0 < m) && (0 < n).
Lemma muln_lcmr : right_distributive muln lcmn.
Proof.
Lemma muln_lcml : left_distributive muln lcmn.
Lemma lcmnA : associative lcmn.
Proof.
Lemma lcmnCA : left_commutative lcmn.
Lemma lcmnAC : right_commutative lcmn.
Lemma lcmnACA : interchange lcmn lcmn.
Lemma dvdn_lcml d1 d2 : d1 %| lcmn d1 d2.
Lemma dvdn_lcmr d1 d2 : d2 %| lcmn d1 d2.
Lemma dvdn_lcm d1 d2 m : (lcmn d1 d2 %| m) = (d1 %| m) && (d2 %| m).
Proof.
case: d1 d2 => [|d1] [|d2]; try by case: m => [|m]; rewrite ?lcmn0 ?andbF.
rewrite -(@dvdn_pmul2r (gcdn d1.+1 d2.+1)) ?gcdn_gt0 // muln_lcm_gcd.
by rewrite muln_gcdr dvdn_gcd {1}mulnC andbC !dvdn_pmul2r.
Qed.
rewrite -(@dvdn_pmul2r (gcdn d1.+1 d2.+1)) ?gcdn_gt0 // muln_lcm_gcd.
by rewrite muln_gcdr dvdn_gcd {1}mulnC andbC !dvdn_pmul2r.
Qed.
Lemma lcmnMl m n : lcmn m (m * n) = m * n.
Lemma lcmnMr m n : lcmn n (m * n) = m * n.
Lemma lcmn_idPr {m n} : reflect (lcmn m n = n) (m %| n).
Lemma lcmn_idPl {m n} : reflect (lcmn m n = m) (n %| m).
Lemma expn_max e m n : e ^ maxn m n = lcmn (e ^ m) (e ^ n).
Proof.
Definition coprime m n := gcdn m n == 1.
Lemma coprime1n n : coprime 1 n.
Lemma coprimen1 n : coprime n 1.
Lemma coprime_sym m n : coprime m n = coprime n m.
Lemma coprime_modl m n : coprime (m %% n) n = coprime m n.
Lemma coprime_modr m n : coprime m (n %% m) = coprime m n.
Lemma coprime2n n : coprime 2 n = odd n.
Proof.
Lemma coprimen2 n : coprime n 2 = odd n.
Proof.
Lemma coprimeSn n : coprime n.+1 n.
Proof.
Lemma coprimenS n : coprime n n.+1.
Proof.
Lemma coprimePn n : n > 0 -> coprime n.-1 n.
Proof.
Lemma coprimenP n : n > 0 -> coprime n n.-1.
Proof.
Lemma coprimeP n m :
n > 0 -> reflect (exists u, u.1 * n - u.2 * m = 1) (coprime n m).
Proof.
Lemma modn_coprime k n : 0 < k -> (exists u, (k * u) %% n = 1) -> coprime k n.
Proof.
Lemma Gauss_dvd m n p : coprime m n -> (m * n %| p) = (m %| p) && (n %| p).
Proof.
Lemma Gauss_dvdr m n p : coprime m n -> (m %| n * p) = (m %| p).
Proof.
Lemma Gauss_dvdl m n p : coprime m p -> (m %| n * p) = (m %| n).
Proof.
Lemma dvdn_double_leq m n : m %| n -> odd m -> ~~ odd n -> 0 < n -> m.*2 <= n.
Proof.
Lemma dvdn_double_ltn m n : m %| n.-1 -> odd m -> odd n -> 1 < n -> m.*2 < n.
Proof.
Lemma Gauss_gcdr p m n : coprime p m -> gcdn p (m * n) = gcdn p n.
Proof.
Lemma Gauss_gcdl p m n : coprime p n -> gcdn p (m * n) = gcdn p m.
Proof.
Lemma coprimeMr p m n : coprime p (m * n) = coprime p m && coprime p n.
Proof.
Lemma coprimeMl p m n : coprime (m * n) p = coprime m p && coprime n p.
Proof.
Lemma coprime_pexpl k m n : 0 < k -> coprime (m ^ k) n = coprime m n.
Proof.
Lemma coprime_pexpr k m n : 0 < k -> coprime m (n ^ k) = coprime m n.
Proof.
Lemma coprimeXl k m n : coprime m n -> coprime (m ^ k) n.
Proof.
Lemma coprimeXr k m n : coprime m n -> coprime m (n ^ k).
Proof.
Lemma coprime_dvdl m n p : m %| n -> coprime n p -> coprime m p.
Lemma coprime_dvdr m n p : m %| n -> coprime p n -> coprime p m.
Proof.
Lemma coprime_egcdn n m : n > 0 -> coprime (egcdn n m).1 (egcdn n m).2.
Proof.
move=> n_gt0; case: (egcdnP m n_gt0) => kn km /= /eqP.
have [/dvdnP[u defn] /dvdnP[v defm]] := (dvdn_gcdl n m, dvdn_gcdr n m).
rewrite -[gcdn n m]mul1n {1}defm {1}defn !mulnA -mulnDl addnC.
rewrite eqn_pmul2r ?gcdn_gt0 ?n_gt0 //; case: kn => // kn /eqP def_knu _.
by apply/coprimeP=> //; exists (u, v); rewrite mulnC def_knu mulnC addnK.
Qed.
have [/dvdnP[u defn] /dvdnP[v defm]] := (dvdn_gcdl n m, dvdn_gcdr n m).
rewrite -[gcdn n m]mul1n {1}defm {1}defn !mulnA -mulnDl addnC.
rewrite eqn_pmul2r ?gcdn_gt0 ?n_gt0 //; case: kn => // kn /eqP def_knu _.
by apply/coprimeP=> //; exists (u, v); rewrite mulnC def_knu mulnC addnK.
Qed.
Lemma dvdn_pexp2r m n k : k > 0 -> (m ^ k %| n ^ k) = (m %| n).
Proof.
move=> k_gt0; apply/idP/idP=> [dv_mn_k|]; last exact: dvdn_exp2r.
have [->|n_gt0] := posnP n; first by rewrite dvdn0.
have [n' def_n] := dvdnP (dvdn_gcdr m n); set d := gcdn m n in def_n.
have [m' def_m] := dvdnP (dvdn_gcdl m n); rewrite -/d in def_m.
have d_gt0: d > 0 by rewrite gcdn_gt0 n_gt0 orbT.
rewrite def_m def_n !expnMn dvdn_pmul2r ?expn_gt0 ?d_gt0 // in dv_mn_k.
have: coprime (m' ^ k) (n' ^ k).
rewrite coprime_pexpl // coprime_pexpr // /coprime -(eqn_pmul2r d_gt0) mul1n.
by rewrite muln_gcdl -def_m -def_n.
rewrite /coprime -gcdn_modr (eqnP dv_mn_k) gcdn0 -(exp1n k).
by rewrite (inj_eq (expIn k_gt0)) def_m; move/eqP->; rewrite mul1n dvdn_gcdr.
Qed.
have [->|n_gt0] := posnP n; first by rewrite dvdn0.
have [n' def_n] := dvdnP (dvdn_gcdr m n); set d := gcdn m n in def_n.
have [m' def_m] := dvdnP (dvdn_gcdl m n); rewrite -/d in def_m.
have d_gt0: d > 0 by rewrite gcdn_gt0 n_gt0 orbT.
rewrite def_m def_n !expnMn dvdn_pmul2r ?expn_gt0 ?d_gt0 // in dv_mn_k.
have: coprime (m' ^ k) (n' ^ k).
rewrite coprime_pexpl // coprime_pexpr // /coprime -(eqn_pmul2r d_gt0) mul1n.
by rewrite muln_gcdl -def_m -def_n.
rewrite /coprime -gcdn_modr (eqnP dv_mn_k) gcdn0 -(exp1n k).
by rewrite (inj_eq (expIn k_gt0)) def_m; move/eqP->; rewrite mul1n dvdn_gcdr.
Qed.
Section Chinese.
The chinese remainder theorem
Variables m1 m2 : nat.
Hypothesis co_m12 : coprime m1 m2.
Lemma chinese_remainder x y :
(x == y %[mod m1 * m2]) = (x == y %[mod m1]) && (x == y %[mod m2]).
Proof.
A function that solves the chinese remainder problem
Definition chinese r1 r2 :=
r1 * m2 * (egcdn m2 m1).1 + r2 * m1 * (egcdn m1 m2).1.
Lemma chinese_modl r1 r2 : chinese r1 r2 = r1 %[mod m1].
Proof.
Lemma chinese_modr r1 r2 : chinese r1 r2 = r2 %[mod m2].
Proof.
Lemma chinese_mod x : x = chinese (x %% m1) (x %% m2) %[mod m1 * m2].
Proof.
End Chinese.