Library mathcomp.algebra.intdiv

(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
From mathcomp Require Import div choice fintype tuple finfun bigop prime order.
From mathcomp Require Import ssralg poly ssrnum ssrint rat matrix.
From mathcomp Require Import polydiv perm zmodp mxalgebra vector.

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 negative m. (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. lcmz m n == the (non-negative) least common multiple of m and n. 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 same sign as 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 should be generalized to the more general setting of integral, unique factorization, principal ideal, or Euclidean domains.

Set Implicit Arguments.

Import Order.TTheory 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 lcmz m n := (lcmn `|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 : int) : (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.
Arguments divzMpl [p m d].

Lemma divzMpr p m d : p > 0 → (m × p %/ (d × p) = m %/ d)%Z.
Arguments divzMpr [p m d].

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 lez_pdiv2r d : 0 ≤ d → {homo divz^~ d : m n / m ≤ 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.
Arguments dvdzP {d m}.

Lemma dvdz_mod0P d m : reflect (m %% d = 0)%Z (d %| m)%Z.
Arguments dvdz_mod0P {d m}.

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

Lemma dvdz_mul2r p d m : p != 0 → (d × p %| m × p)%Z = (d %| m)%Z.
Arguments dvdz_mul2r [p d m].

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.

Least common multiple

Lemma dvdz_lcmr m n : (n %| lcmz m n)%Z.

Lemma dvdz_lcml m n : (m %| lcmz m n)%Z.

Lemma dvdz_lcm d1 d2 m : ((lcmn d1 d2 %| m) = (d1 %| m) && (d2 %| m))%Z.

Lemma lcmzC : commutative lcmz.

Lemma lcm0z : left_zero 0 lcmz.

Lemma lcmz0 : right_zero 0 lcmz.

Lemma lcmz_ge0 m n : 0 ≤ lcmz m n.

Lemma lcmz_neq0 m n : (lcmz m n != 0) = (m != 0) && (n != 0).

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 coprimezMr p m n : coprimez p (m × n) = coprimez p m && coprimez p n.

Lemma coprimezMl 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 coprimezXl k m n : coprimez m n → coprimez (m ^+ k) n.

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

#[deprecated(since="mathcomp 1.12.0", note="Use coprimezMl instead.")]
Notation coprimez_mull := coprimezMl (only parsing).
#[deprecated(since="mathcomp 1.12.0", note="Use coprimezMr instead.")]
Notation coprimez_mulr := coprimezMr (only parsing).
#[deprecated(since="mathcomp 1.12.0", note="Use coprimezXl instead.")]
Notation coprimez_expl := coprimezXl (only parsing).
#[deprecated(since="mathcomp 1.12.0", note="Use coprimezXr instead.")]
Notation coprimez_expr := coprimezXr (only parsing).