Library mathcomp.algebra.intdiv

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)
Require Import mathcomp.ssreflect.ssreflect.

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 divn1 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.
Implicit Arguments divzMpl [p m d].

Lemma divzMpr p m d : p > 0 → (m × p %/ (d × p) = m %/ d)%Z.
Implicit 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 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.

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.
Implicit Arguments dvdzP [d m].

Lemma dvdz_mod0P d m : reflect (m %% d = 0)%Z (d %| m)%Z.
Implicit 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.
Implicit Arguments dvdz_mul2l [p m d].

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

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.

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