- -

Library mathcomp.algebra.intdiv

- -

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

- -

- This file provides various results on divisibility of integers. - It defines, for m, n, d : int, - (m %% d)%Z == the remainder of the Euclidean division of m by d; this is - the least non-negative element of the coset m + dZ when - d != 0, and m if d = 0. - (m %/ d)%Z == the quotient of the Euclidean division of m by d, such - that m = (m %/ d)%Z * d + (m %% d)%Z. Since for d != 0 the - remainder is non-negative, (m %/ d)%Z is non-zero for - (d %| m)%Z <=> m is divisible by d; dvdz d is the (collective) predicate - for integers divisible by d, and (d %| m)%Z is actually - (transposing) notation for m \in dvdz d. - (m = n % [mod d])%Z, (m == n % [mod d])%Z, (m != n % [mod d])%Z - m and n are (resp. compare, don't compare) equal mod d. - gcdz m n == the (non-negative) greatest common divisor of m and n, - with gcdz 0 0 = 0. - coprimez m n <=> m and n are coprime. - egcdz m n == the Bezout coefficients of the gcd of m and n: a pair - (u, v) of coprime integers such that u*m + v*n = gcdz m n. - Alternatively, a Bezoutz lemma states such u and v exist. - zchinese m1 m2 n1 n2 == for coprime m1 and m2, a solution to the Chinese - remainder problem for n1 and n2, i.e., and integer n such - that n = n1 % [mod m1] and n = n2 % [mod m2]. - zcontents p == the contents of p : {poly int}, that is, the gcd of the - coefficients of p, with the lead coefficient of p, - zprimitive p == the primitive part of p : {poly int}, i.e., p divided by - its contents. - inIntSpan X v <-> v is an integral linear combination of elements of - X : seq V, where V is a zmodType. We prove that this is a - decidable property for Q-vector spaces. - int_Smith_normal_form :: a theorem asserting the existence of the Smith - normal form for integer matrices. - Note that many of the concepts and results in this file could and perhaps - sould be generalized to the more general setting of integral, unique - factorization, principal ideal, or Euclidean domains. -

- -
-Set Implicit Arguments.
- -
-Import GRing.Theory Num.Theory.
-Local Open Scope ring_scope.
- -
-Definition divz (m d : int) :=
-  let: (K, n) := match m with Posz n ⇒ (Posz , n) | Negz n ⇒ (Negz , n) end in
-  sgz d × K (n %/ `|d |)%N.
- -
-Definition modz (m d : int) : int := m - divz m d × d.
- -
-Definition dvdz d m := (`|d | %| `|m |)%N.
- -
-Definition gcdz m n := (gcdn `|m | `|n |)%:Z.
- -
-Definition egcdz m n : int × int :=
-  if m == 0 then (0, (-1) ^+ (n < 0)%R) else
-  let: (u, v) := egcdn `|m | `|n | in (sgz m × u, - (-1) ^+ (n < 0)%R × v%:Z ).
- -
-Definition coprimez m n := (gcdz m n == 1).
- -
-Infix "%/" := divz : int_scope.
-Infix "%%" := modz : int_scope.
-Notation "d %| m" := (m \in dvdz d) : int_scope.
-Notation "m = n %[mod d ]" := (modz m d = modz n d) : int_scope.
-Notation "m == n %[mod d ]" := (modz m d == modz n d) : int_scope.
-Notation "m <> n %[mod d ]" := (modz m d ≠ modz n d) : int_scope.
-Notation "m != n %[mod d ]" := (modz m d != modz n d) : int_scope.
- -
-Lemma divz_nat (n d : nat) : (n %/ d)%Z = (n %/ d)%N.
- -
-Lemma divzN m d : (m %/ - d)%Z = - (m %/ d)%Z.
- -
-Lemma divz_abs m d : (m %/ `|d |)%Z = (-1) ^+ (d < 0)%R × (m %/ d)%Z.
- -
-Lemma div0z d : (0 %/ d)%Z = 0.
- -
-Lemma divNz_nat m d : (d > 0)%N → (Negz m %/ d)%Z = - (m %/ d ).+1 %:Z.
- -
-Lemma divz_eq m d : m = (m %/ d)%Z × d + (m %% d)%Z.
- -
-Lemma modzN m d : (m %% - d)%Z = (m %% d)%Z.
- -
-Lemma modz_abs m d : (m %% `|d |%N)%Z = (m %% d)%Z.
- -
-Lemma modz_nat (m d : nat) : (m %% d)%Z = (m %% d)%N.
- -
-Lemma modNz_nat m d : (d > 0)%N → (Negz m %% d)%Z = d %:Z - 1 - (m %% d )%:Z.
- -
-Lemma modz_ge0 m d : d != 0 → 0 ≤ (m %% d)%Z.
- -
-Lemma divz0 m : (m %/ 0)%Z = 0.
-Lemma mod0z d : (0 %% d)%Z = 0.
-Lemma modz0 m : (m %% 0)%Z = m.
- -
-Lemma divz_small m d : 0 ≤ m < `|d |%:Z → (m %/ d)%Z = 0.
- -
-Lemma divzMDl q m d : d != 0 → ((q × d + m ) %/ d)%Z = q + (m %/ d)%Z.
- -
-Lemma mulzK m d : d != 0 → (m × d %/ d)%Z = m.
- -
-Lemma mulKz m d : d != 0 → (d × m %/ d)%Z = m.
- -
-Lemma expzB p m n : p != 0 → (m ≥ n)%N → p ^+ (m - n ) = (p ^+ m %/ p ^+ n)%Z.
- -
-Lemma modz1 m : (m %% 1)%Z = 0.
- -
-Lemma divz1 m : (m %/ 1)%Z = m.
- -
-Lemma divzz d : (d %/ d)%Z = (d != 0).
- -
-Lemma ltz_pmod m d : d > 0 → (m %% d)%Z < d.
- -
-Lemma ltz_mod m d : d != 0 → (m %% d)%Z < `|d |.
- -
-Lemma divzMpl p m d : p > 0 → (p × m %/ (p × d ) = m %/ d)%Z.
- -
-Lemma divzMpr p m d : p > 0 → (m × p %/ (d × p ) = m %/ d)%Z.
- -
-Lemma lez_floor m d : d != 0 → (m %/ d)%Z × d ≤ m.
- -
-

- -

- leq_mod does not extend to negative m. -

-Lemma lez_div m d : (`|(m %/ d)%Z| ≤ `|m |)%N.
- -
-Lemma ltz_ceil m d : d > 0 → m < ((m %/ d)%Z + 1) × d.
- -
-Lemma ltz_divLR m n d : d > 0 → ((m %/ d)%Z < n ) = (m < n × d ).
- -
-Lemma lez_divRL m n d : d > 0 → (m ≤ (n %/ d)%Z) = (m × d ≤ n ).
- -
-Lemma divz_ge0 m d : d > 0 → ((m %/ d)%Z ≥ 0) = (m ≥ 0).
- -
-Lemma divzMA_ge0 m n p : n ≥ 0 → (m %/ (n × p ) = (m %/ n)%Z %/ p)%Z.
- -
-Lemma modz_small m d : 0 ≤ m < d → (m %% d)%Z = m.
- -
-Lemma modz_mod m d : ((m %% d)%Z = m %[mod d ])%Z.
- -
-Lemma modzMDl p m d : (p × d + m = m %[mod d ])%Z.
- -
-Lemma mulz_modr {p m d} : 0 < p → p × (m %% d)%Z = ((p × m ) %% (p × d ))%Z.
- -
-Lemma mulz_modl {p m d} : 0 < p → (m %% d)%Z × p = ((m × p ) %% (d × p ))%Z.
- -
-Lemma modzDl m d : (d + m = m %[mod d ])%Z.
- -
-Lemma modzDr m d : (m + d = m %[mod d ])%Z.
- -
-Lemma modzz d : (d %% d)%Z = 0.
- -
-Lemma modzMl p d : (p × d %% d)%Z = 0.
- -
-Lemma modzMr p d : (d × p %% d)%Z = 0.
- -
-Lemma modzDml m n d : ((m %% d)%Z + n = m + n %[mod d ])%Z.
- -
-Lemma modzDmr m n d : (m + (n %% d)%Z = m + n %[mod d ])%Z.
- -
-Lemma modzDm m n d : ((m %% d)%Z + (n %% d)%Z = m + n %[mod d ])%Z.
- -
-Lemma eqz_modDl p m n d : (p + m == p + n %[mod d ])%Z = (m == n %[mod d ])%Z.
- -
-Lemma eqz_modDr p m n d : (m + p == n + p %[mod d ])%Z = (m == n %[mod d ])%Z.
- -
-Lemma modzMml m n d : ((m %% d)%Z × n = m × n %[mod d ])%Z.
- -
-Lemma modzMmr m n d : (m × (n %% d)%Z = m × n %[mod d ])%Z.
- -
-Lemma modzMm m n d : ((m %% d)%Z × (n %% d)%Z = m × n %[mod d ])%Z.
- -
-Lemma modzXm k m d : ((m %% d)%Z ^+ k = m ^+ k %[mod d ])%Z.
- -
-Lemma modzNm m d : (- (m %% d)%Z = - m %[mod d ])%Z.
- -
-Lemma modz_absm m d : ((-1) ^+ (m < 0)%R × (m %% d)%Z = `|m |%:Z %[mod d ])%Z.
- -
-

- -

- Divisibility * -

- -
-Fact dvdz_key d : pred_key (dvdz d).
-Canonical dvdz_keyed d := KeyedPred (dvdz_key d).
- -
-Lemma dvdzE d m : (d %| m)%Z = (`|d | %| `|m |)%N.
-Lemma dvdz0 d : (d %| 0)%Z.
-Lemma dvd0z n : (0 %| n)%Z = (n == 0).
-Lemma dvdz1 d : (d %| 1)%Z = (`|d |%N == 1%N).
-Lemma dvd1z m : (1 %| m)%Z.
-Lemma dvdzz m : (m %| m)%Z.
- -
-Lemma dvdz_mull d m n : (d %| n)%Z → (d %| m × n)%Z.
- -
-Lemma dvdz_mulr d m n : (d %| m)%Z → (d %| m × n)%Z.
- Hint Resolve dvdz0 dvd1z dvdzz dvdz_mull dvdz_mulr : core.
- -
-Lemma dvdz_mul d1 d2 m1 m2 : (d1 %| m1 → d2 %| m2 → d1 × d2 %| m1 × m2)%Z.
- -
-Lemma dvdz_trans n d m : (d %| n → n %| m → d %| m)%Z.
- -
-Lemma dvdzP d m : reflect (∃ q, m = q × d) (d %| m)%Z.
- -
-Lemma dvdz_mod0P d m : reflect (m %% d = 0)%Z (d %| m)%Z.
- -
-Lemma dvdz_eq d m : (d %| m)%Z = ((m %/ d)%Z × d == m ).
- -
-Lemma divzK d m : (d %| m)%Z → (m %/ d)%Z × d = m.
- -
-Lemma lez_divLR d m n : 0 < d → (d %| m)%Z → ((m %/ d)%Z ≤ n ) = (m ≤ n × d ).
- -
-Lemma ltz_divRL d m n : 0 < d → (d %| m)%Z → (n < m %/ d)%Z = (n × d < m ).
- -
-Lemma eqz_div d m n : d != 0 → (d %| m)%Z → (n == m %/ d)%Z = (n × d == m ).
- -
-Lemma eqz_mul d m n : d != 0 → (d %| m)%Z → (m == n × d ) = (m %/ d == n)%Z.
- -
-Lemma divz_mulAC d m n : (d %| m)%Z → (m %/ d)%Z × n = (m × n %/ d)%Z.
- -
-Lemma mulz_divA d m n : (d %| n)%Z → m × (n %/ d)%Z = (m × n %/ d)%Z.
- -
-Lemma mulz_divCA d m n :
-  (d %| m)%Z → (d %| n)%Z → m × (n %/ d)%Z = n × (m %/ d)%Z.
- -
-Lemma divzA m n p : (p %| n → n %| m × p → m %/ (n %/ p)%Z = m × p %/ n)%Z.
- -
-Lemma divzMA m n p : (n × p %| m → m %/ (n × p ) = (m %/ n)%Z %/ p)%Z.
- -
-Lemma divzAC m n p : (n × p %| m → (m %/ n)%Z %/ p = (m %/ p)%Z %/ n)%Z.
- -
-Lemma divzMl p m d : p != 0 → (d %| m → p × m %/ (p × d ) = m %/ d)%Z.
- -
-Lemma divzMr p m d : p != 0 → (d %| m → m × p %/ (d × p ) = m %/ d)%Z.
- -
-Lemma dvdz_mul2l p d m : p != 0 → (p × d %| p × m)%Z = (d %| m)%Z.
- -
-Lemma dvdz_mul2r p d m : p != 0 → (d × p %| m × p)%Z = (d %| m)%Z.
- -
-Lemma dvdz_exp2l p m n : (m ≤ n)%N → (p ^+ m %| p ^+ n)%Z.
- -
-Lemma dvdz_Pexp2l p m n : `|p | > 1 → (p ^+ m %| p ^+ n)%Z = (m ≤ n)%N.
- -
-Lemma dvdz_exp2r m n k : (m %| n → m ^+ k %| n ^+ k)%Z.
- -
-Fact dvdz_zmod_closed d : zmod_closed (dvdz d).
-Canonical dvdz_addPred d := AddrPred (dvdz_zmod_closed d).
-Canonical dvdz_oppPred d := OpprPred (dvdz_zmod_closed d).
-Canonical dvdz_zmodPred d := ZmodPred (dvdz_zmod_closed d).
- -
-Lemma dvdz_exp k d m : (0 < k)%N → (d %| m → d %| m ^+ k)%Z.
- -
-Lemma eqz_mod_dvd d m n : (m == n %[mod d ])%Z = (d %| m - n)%Z.
- -
-Lemma divzDl m n d :
-  (d %| m)%Z → ((m + n ) %/ d)%Z = (m %/ d)%Z + (n %/ d)%Z.
- -
-Lemma divzDr m n d :
-  (d %| n)%Z → ((m + n ) %/ d)%Z = (m %/ d)%Z + (n %/ d)%Z.
- -
-Lemma Qint_dvdz (m d : int) : (d %| m)%Z → ((m %:~R / d %:~R : rat ) \is a Qint ).
- -
-Lemma Qnat_dvd (m d : nat) : (d %| m)%N → ((m %:R / d %:R : rat ) \is a Qnat ).
- -
-

- -

- Greatest common divisor -

- -
-Lemma gcdzz m : gcdz m m = `|m |%:Z.
-Lemma gcdzC : commutative gcdz.
-Lemma gcd0z m : gcdz 0 m = `|m |%:Z.
-Lemma gcdz0 m : gcdz m 0 = `|m |%:Z.
-Lemma gcd1z : left_zero 1 gcdz.
-Lemma gcdz1 : right_zero 1 gcdz.
-Lemma dvdz_gcdr m n : (gcdz m n %| n)%Z.
-Lemma dvdz_gcdl m n : (gcdz m n %| m)%Z.
-Lemma gcdz_eq0 m n : (gcdz m n == 0) = (m == 0) && (n == 0).
- Lemma gcdNz m n : gcdz (- m) n = gcdz m n.
-Lemma gcdzN m n : gcdz m (- n) = gcdz m n.
- -
-Lemma gcdz_modr m n : gcdz m (n %% m)%Z = gcdz m n.
- -
-Lemma gcdz_modl m n : gcdz (m %% n)%Z n = gcdz m n.
- -
-Lemma gcdzMDl q m n : gcdz m (q × m + n) = gcdz m n.
- -
-Lemma gcdzDl m n : gcdz m (m + n) = gcdz m n.
- -
-Lemma gcdzDr m n : gcdz m (n + m) = gcdz m n.
- -
-Lemma gcdzMl n m : gcdz n (m × n) = `|n |%:Z.
- -
-Lemma gcdzMr n m : gcdz n (n × m) = `|n |%:Z.
- -
-Lemma gcdz_idPl {m n} : reflect (gcdz m n = `|m |%:Z) (m %| n)%Z.
- -
-Lemma gcdz_idPr {m n} : reflect (gcdz m n = `|n |%:Z) (n %| m)%Z.
- -
-Lemma expz_min e m n : e ≥ 0 → e ^+ minn m n = gcdz (e ^+ m) (e ^+ n).
- -
-Lemma dvdz_gcd p m n : (p %| gcdz m n)%Z = (p %| m)%Z && (p %| n)%Z.
- -
-Lemma gcdzAC : right_commutative gcdz.
- -
-Lemma gcdzA : associative gcdz.
- -
-Lemma gcdzCA : left_commutative gcdz.
- -
-Lemma gcdzACA : interchange gcdz gcdz.
- -
-Lemma mulz_gcdr m n p : `|m |%:Z × gcdz n p = gcdz (m × n) (m × p).
- -
-Lemma mulz_gcdl m n p : gcdz m n × `|p |%:Z = gcdz (m × p) (n × p).
- -
-Lemma mulz_divCA_gcd n m : n × (m %/ gcdz n m)%Z = m × (n %/ gcdz n m)%Z.
- -
-

- -

- Not including lcm theory, for now. -

- - Coprime factors -

- -
-Lemma coprimezE m n : coprimez m n = coprime `|m | `|n |.
- -
-Lemma coprimez_sym : symmetric coprimez.
- -
-Lemma coprimeNz m n : coprimez (- m) n = coprimez m n.
- -
-Lemma coprimezN m n : coprimez m (- n) = coprimez m n.
- -
-Variant egcdz_spec m n : int × int → Type :=
-  EgcdzSpec u v of u × m + v × n = gcdz m n & coprimez u v
-     : egcdz_spec m n (u , v ).
- -
-Lemma egcdzP m n : egcdz_spec m n (egcdz m n).
- -
-Lemma Bezoutz m n : {u : int & {v : int | u × m + v × n = gcdz m n }}.
- -
-Lemma coprimezP m n :
-  reflect (∃ uv, uv .1 × m + uv .2 × n = 1) (coprimez m n).
- -
-Lemma Gauss_dvdz m n p :
-  coprimez m n → (m × n %| p)%Z = (m %| p)%Z && (n %| p)%Z.
- -
-Lemma Gauss_dvdzr m n p : coprimez m n → (m %| n × p)%Z = (m %| p)%Z.
- -
-Lemma Gauss_dvdzl m n p : coprimez m p → (m %| n × p)%Z = (m %| n)%Z.
- -
-Lemma Gauss_gcdzr p m n : coprimez p m → gcdz p (m × n) = gcdz p n.
- -
-Lemma Gauss_gcdzl p m n : coprimez p n → gcdz p (m × n) = gcdz p m.
- -
-Lemma coprimez_mulr p m n : coprimez p (m × n) = coprimez p m && coprimez p n.
- -
-Lemma coprimez_mull p m n : coprimez (m × n) p = coprimez m p && coprimez n p.
- -
-Lemma coprimez_pexpl k m n : (0 < k)%N → coprimez (m ^+ k) n = coprimez m n.
- -
-Lemma coprimez_pexpr k m n : (0 < k)%N → coprimez m (n ^+ k) = coprimez m n.
- -
-Lemma coprimez_expl k m n : coprimez m n → coprimez (m ^+ k) n.
- -
-Lemma coprimez_expr k m n : coprimez m n → coprimez m (n ^+ k).
- -
-Lemma coprimez_dvdl m n p : (m %| n)%N → coprimez n p → coprimez m p.
- -
-Lemma coprimez_dvdr m n p : (m %| n)%N → coprimez p n → coprimez p m.
- -
-Lemma dvdz_pexp2r m n k : (k > 0)%N → (m ^+ k %| n ^+ k)%Z = (m %| n)%Z.
- -
-Section Chinese.
- -
-

- -

- The chinese remainder theorem -

- -
-Variables m1 m2 : int.
-Hypothesis co_m12 : coprimez m1 m2.
- -
-Lemma zchinese_remainder x y :
- (x == y %[mod m1 × m2 ])%Z = (x == y %[mod m1 ])%Z && (x == y %[mod m2 ])%Z.
- -
-

- -

- A function that solves the chinese remainder problem -

- -
-Definition zchinese r1 r2 :=
-  r1 × m2 × (egcdz m1 m2 ).2 + r2 × m1 × (egcdz m1 m2 ).1.
- -
-Lemma zchinese_modl r1 r2 : (zchinese r1 r2 = r1 %[mod m1 ])%Z.
- -
-Lemma zchinese_modr r1 r2 : (zchinese r1 r2 = r2 %[mod m2 ])%Z.
- -
-Lemma zchinese_mod x : (x = zchinese (x %% m1)%Z (x %% m2)%Z %[mod m1 × m2 ])%Z.
- -
-End Chinese.
- -
-Section ZpolyScale.
- -
-Definition zcontents p :=
-  sgz (lead_coef p) × \big [gcdn /0%N]_(i < size p ) `|(p `_i)%R|%N.
- -
-Lemma sgz_contents p : sgz (zcontents p) = sgz (lead_coef p).
- -
-Lemma zcontents_eq0 p : (zcontents p == 0) = (p == 0).
- -
-Lemma zcontents0 : zcontents 0 = 0.
- -
-Lemma zcontentsZ a p : zcontents (a *: p) = a × zcontents p.
- -
-Lemma zcontents_monic p : p \is monic → zcontents p = 1.
- -
-Lemma dvdz_contents a p : (a %| zcontents p)%Z = (p \is a polyOver (dvdz a)).
- -
-Lemma map_poly_divzK {a} p :
-  p \is a polyOver (dvdz a) → a *: map_poly (divz ^~ a) p = p.
- -
-Lemma polyOver_dvdzP a p :
-  reflect (∃ q, p = a *: q) (p \is a polyOver (dvdz a)).
- -
-Definition zprimitive p := map_poly (divz ^~ (zcontents p )) p.
- -
-Lemma zpolyEprim p : p = zcontents p *: zprimitive p.
- -
-Lemma zprimitive0 : zprimitive 0 = 0.
- -
-Lemma zprimitive_eq0 p : (zprimitive p == 0) = (p == 0).
- -
-Lemma size_zprimitive p : size (zprimitive p) = size p.
- -
-Lemma sgz_lead_primitive p : sgz (lead_coef (zprimitive p)) = (p != 0).
- -
-Lemma zcontents_primitive p : zcontents (zprimitive p) = (p != 0).
- -
-Lemma zprimitive_id p : zprimitive (zprimitive p) = zprimitive p.
- -
-Lemma zprimitive_monic p : p \in monic → zprimitive p = p.
- -
-Lemma zprimitiveZ a p : a != 0 → zprimitive (a *: p) = zprimitive p.
- -
-Lemma zprimitive_min p a q :
-    p != 0 → p = a *: q →
-  {b | sgz b = sgz (lead_coef q) & q = b *: zprimitive p }.
- -
-Lemma zprimitive_irr p a q :
-  p != 0 → zprimitive p = a *: q → a = sgz (lead_coef q).
- -
-Lemma zcontentsM p q : zcontents (p × q) = zcontents p × zcontents q.
- -
-Lemma zprimitiveM p q : zprimitive (p × q) = zprimitive p × zprimitive q.
- -
-Lemma dvdpP_int p q : p %| q → {r | q = zprimitive p × r }.
- -
- -
-Lemma size_rat_int_poly p : size (pZtoQ p) = size p.
- -
-Lemma rat_poly_scale (p : {poly rat }) :
-  {q : {poly int } & {a | a != 0 & p = a %:~R ^-1 *: pZtoQ q }}.
- -
-Lemma dvdp_rat_int p q : (pZtoQ p %| pZtoQ q ) = (p %| q ).
- -
-Lemma dvdpP_rat_int p q :
-    p %| pZtoQ q →
-  {p1 : {poly int } & {a | a != 0 & p = a *: pZtoQ p1 } & {r | q = p1 × r }}.
- -
-End ZpolyScale.
- -
-

- -

- Integral spans. -

- -
-Lemma int_Smith_normal_form m n (M : 'M [int ]_(m , n )) :
-  {L : 'M [int ]_m & L \in unitmx &
-  {R : 'M [int ]_n & R \in unitmx &
-  {d : seq int | sorted dvdz d &
-   M = L ×m (\matrix_(i, j) (d `_i *+ (i == j :> nat ))) ×m R }}}.
- -
-Definition inIntSpan (V : zmodType) m (s : m .-tuple V) v :=
-  ∃ a : int ^ m , v = \sum_(i < m ) s `_i *~ a i.
- -
-Lemma dec_Qint_span (vT : vectType rat) m (s : m .-tuple vT) v :
-  decidable (inIntSpan s v).
- -
-