Library mathcomp.ssreflect.div

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B.                                  *)

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.

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).

Lemma edivn_eq d q r : r < d edivn (q × d + r) d = (q, r).

Definition divn m d := (edivn m d).1.

Notation "m %/ d" := (divn m d) : nat_scope.

We redefine modn so that it is structurally decreasing.

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.

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.
Lemma divn0 m : m %/ 0 = 0.
Lemma mod0n d : 0 %% d = 0.
Lemma modn0 m : m %% 0 = m.

Lemma divn_small m d : m < d m %/ d = 0.

Lemma divnMDl q m d : 0 < d (q × d + m) %/ d = q + m %/ d.

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.
Arguments divnMl [p m d].

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.

Lemma leq_trunc_div m d : m %/ d × d m.

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).

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.

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).

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).

Lemma divnB n m d : 0 < d
(m - n) %/ d = (m %/ d) - (n %/ d) - (m %% d < n %% d).

Lemma modnB m n d : 0 < d n m
(m - n) %% d = (m %% d < n %% d) × d + m %% d - n %% d.

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.

Lemma divnMA m n p : m %/ (n × p) = m %/ n %/ p.

Lemma divnAC m n p : m %/ n %/ p = m %/ p %/ n.

Lemma modn_small m d : m < d m %% d = m.

Lemma modn_mod m d : m %% d = m %[mod d].

Lemma modnMDl p m d : p × d + m = m %[mod d].

Lemma muln_modr p m d : p × (m %% d) = (p × m) %% (p × d).

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.

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]).

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].

Divisibility *

Definition dvdn d m := m %% d == 0.

Notation "m %| d" := (dvdn m d) : nat_scope.

Lemma dvdnP d m : reflect ( k, m = k × d) (d %| m).
Arguments dvdnP {d m}.

Lemma dvdn0 d : d %| 0.

Lemma dvd0n n : (0 %| n) = (n == 0).

Lemma dvdn1 d : (d %| 1) = (d == 1).

Lemma dvd1n m : 1 %| m.

Lemma dvdn_gt0 d m : m > 0 d %| m d > 0.

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).

Lemma dvdn2 n : (2 %| n) = ~~ odd n.

Lemma dvdn_odd m n : m %| n odd n odd m.

Lemma divnK d m : d %| m m %/ d × d = m.

Lemma leq_divLR d m n : d %| m (m %/ d n) = (m n × d).

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).

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.

Lemma muln_divA d m n : d %| n m × (n %/ d) = m × n %/ d.

Lemma muln_divCA d m n : d %| m d %| n m × (n %/ d) = n × (m %/ d).

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.

Lemma eqn_dvd m n : (m == n) = (m %| n) && (n %| m).

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).
Arguments dvdn_pmul2r [p d m].

Lemma dvdn_divLR p d m : 0 < p p %| d (d %/ p %| m) = (d %| m × p).

Lemma dvdn_divRL p d m : p %| m (d %| m %/ p) = (d × p %| m).

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).

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.

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).

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`!.

#[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).

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.

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).

A function that computes the gcd of 2 numbers

Fixpoint gcdn_rec m n :=
let n' := n %% m in if n' is 0 then m else
if m - n'.-1 is m'.+1 then gcdn_rec (m' %% n') n' else n'.

Definition gcdn := nosimpl gcdn_rec.

Lemma gcdnE m n : gcdn m n = if m == 0 then n else gcdn (n %% m) m.

Lemma gcdnn : idempotent gcdn.

Lemma gcdnC : commutative gcdn.

Lemma gcd0n : left_id 0 gcdn.
Lemma gcdn0 : right_id 0 gcdn.

Lemma gcd1n : left_zero 1 gcdn.

Lemma gcdn1 : right_zero 1 gcdn.

Lemma dvdn_gcdr m n : gcdn m n %| n.

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).

Lemma gcdn_modr m n : gcdn m (n %% m) = gcdn m n.

Lemma gcdn_modl m n : gcdn (m %% n) n = gcdn m n.

Extended gcd, which computes Bezout coefficients.

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).

Lemma egcdnP m n : m > 0 egcdn_spec m n (egcdn m n).

Lemma Bezoutl m n : m > 0 {a | a < m & m %| gcdn m n + a × n}.

Lemma Bezoutr m n : n > 0 {a | a < n & n %| gcdn m n + a × m}.

Back to the gcd.
We derive the lcm directly.

Definition lcmn m n := m × n %/ gcdn m n.

Lemma lcmnC : commutative lcmn.

Lemma lcm0n : left_zero 0 lcmn.
Lemma lcmn0 : right_zero 0 lcmn.

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.

Lemma muln_lcml : left_distributive muln lcmn.

Lemma lcmnA : associative lcmn.

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).

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).

Coprime factors

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.

Lemma coprimen2 n : coprime n 2 = odd n.

Lemma coprimeSn n : coprime n.+1 n.

Lemma coprimenS n : coprime n n.+1.

Lemma coprimePn n : n > 0 coprime n.-1 n.

Lemma coprimenP n : n > 0 coprime n n.-1.

Lemma coprimeP n m :
n > 0 reflect ( u, u.1 × n - u.2 × m = 1) (coprime n m).

Lemma modn_coprime k n : 0 < k ( u, (k × u) %% n = 1) coprime k n.

Lemma Gauss_dvd m n p : coprime m n (m × n %| p) = (m %| p) && (n %| p).

Lemma Gauss_dvdr m n p : coprime m n (m %| n × p) = (m %| p).

Lemma Gauss_dvdl m n p : coprime m p (m %| n × p) = (m %| n).

Lemma dvdn_double_leq m n : m %| n odd m ~~ odd n 0 < n m.*2 n.

Lemma dvdn_double_ltn m n : m %| n.-1 odd m odd n 1 < n m.*2 < n.

Lemma Gauss_gcdr p m n : coprime p m gcdn p (m × n) = gcdn p n.

Lemma Gauss_gcdl p m n : coprime p n gcdn p (m × n) = gcdn p m.

Lemma coprimeMr p m n : coprime p (m × n) = coprime p m && coprime p n.

Lemma coprimeMl p m n : coprime (m × n) p = coprime m p && coprime n p.

Lemma coprime_pexpl k m n : 0 < k coprime (m ^ k) n = coprime m n.

Lemma coprime_pexpr k m n : 0 < k coprime m (n ^ k) = coprime m n.

Lemma coprimeXl k m n : coprime m n coprime (m ^ k) n.

Lemma coprimeXr k m n : coprime m n coprime m (n ^ k).

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.

Lemma coprime_egcdn n m : n > 0 coprime (egcdn n m).1 (egcdn n m).2.

Lemma dvdn_pexp2r m n k : k > 0 (m ^ k %| n ^ k) = (m %| n).

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]).

A function that solves the chinese remainder problem