Library div

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 euclidian division of m by d                
          m %/ d  == quotient of m by d                                 
          m %% d  == remainder of m dy 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 of m and n                        
         lcmn m n == the LCM of m and n                                 
      coprime m n <=> m and n are coprime                               
  chinese m n r s == witness of the chinese remainder theorem           

Import Prenex Implicits.

Euclidian division 

Definition edivn_rec d := fix loop (m q : nat) {struct m} :=
  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).

CoInductive edivn_spec (m d : nat) : nat * nat -> Type :=
  EdivnSpec q r of m = q * d + r & (d > 0) ==> (r < d) : edivn_spec m d (q, r).

Lemma edivnP : forall m d, edivn_spec m d (edivn m d).

Lemma edivn_eq : forall 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) (at level 40, no associativity) : nat_scope.

We redefine modn so that it is structurally decreasing. 

Definition modn_rec d := fix loop (m : nat) :=
  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) (at level 40, no associativity) : nat_scope.
Notation "m = n %[mod d ]" := (m %% d = n %% d)
  (at level 70, n at next level,
   format "'[hv ' m '/' = n '/' %[mod d ] ']'") : nat_scope.
Notation "m == n %[mod d ]" := (m %% d == n %% d)
  (at level 70, n at next level,
   format "'[hv ' m '/' == n '/' %[mod d ] ']'") : nat_scope.
Notation "m <> n %[mod d ]" := (m %% d <> n %% d)
  (at level 70, n at next level,
   format "'[hv ' m '/' <> n '/' %[mod d ] ']'") : nat_scope.
Notation "m != n %[mod d ]" := (m %% d != n %% d)
  (at level 70, n at next level,
   format "'[hv ' m '/' != n '/' %[mod d ] ']'") : nat_scope.

Lemma modn_def : forall m d, m %% d = (edivn m d).2.

Lemma edivn_def : forall m d, edivn m d = (m %/ d, m %% d).

Lemma divn_eq : forall m d, m = m %/ d * d + m %% d.

Lemma div0n : forall d, 0 %/ d = 0.

Lemma divn0 : forall m, m %/ 0 = 0.

Lemma mod0n : forall d, 0 %% d = 0.

Lemma modn0 : forall m, m %% 0 = m.

Lemma divn_small : forall m d, m < d -> m %/ d = 0.

Lemma divn_addl_mul : forall q m d, 0 < d -> (q * d + m) %/ d = q + m %/ d.

Lemma mulnK : forall m d, 0 < d -> m * d %/ d = m.

Lemma mulKn : forall m d, 0 < d -> d * m %/ d = m.

Lemma modn1 : forall m, m %% 1 = 0.

Lemma divn1 : forall m, m %/ 1 = m.

Lemma divnn : forall d, d %/ d = (0 < d).

Lemma divn_pmul2l : forall p m d, p > 0 -> p * m %/ (p * d) = m %/ d.
Implicit Arguments divn_pmul2l [p m d].

Lemma divn_pmul2r : forall p m d, p > 0 -> m * p %/ (d * p) = m %/ d.
Implicit Arguments divn_pmul2r [p m d].

Lemma ltn_mod : forall m d, (m %% d < d) = (0 < d).

Lemma ltn_pmod : forall m d, 0 < d -> m %% d < d.

Lemma leq_floor : forall m d, m %/ d * d <= m.

Lemma leq_mod : forall m d, m %% d <= m.

Lemma leq_div : forall m d, m %/ d <= m.

Lemma ltn_ceil : forall m d, 0 < d -> m < (m %/ d).+1 * d.

Lemma ltn_divl : forall m n d, d > 0 -> (m %/ d < n) = (m < n * d).

Lemma leq_divr : forall m n d, d > 0 -> (m <= n %/ d) = (m * d <= n).

Lemma ltn_Pdiv : forall m d, 1 < d -> 0 < m -> m %/ d < m.

Lemma divn_gt0 : forall d m, 0 < d -> (0 < m %/ d) = (d <= m).

Lemma divn_divl : forall m n p, m %/ n %/ p = m %/ (n * p).

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

Lemma modn_small : forall m d, m < d -> m %% d = m.

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

Lemma modn_addl_mul : forall p m d, p * d + m = m %[mod d].

Lemma modn_pmul2l : forall p m d, 0 < p -> p * m %% (p * d) = p * (m %% d).
Implicit Arguments modn_pmul2l [p m d].

Lemma modn_addl : forall m d, d + m = m %[mod d].

Lemma modn_addr : forall m d, m + d = m %[mod d].

Lemma modnn : forall d, d %% d = 0.

Lemma modn_mull : forall p d, p * d %% d = 0.

Lemma modn_mulr : forall p d, d * p %% d = 0.

Lemma modn_addml : forall m n d, m %% d + n = m + n %[mod d].

Lemma modn_addmr : forall m n d, m + n %% d = m + n %[mod d].

Lemma modn_add2m : forall m n d, m %% d + n %% d = m + n %[mod d].

Lemma modn_add2l : forall p m n d,
  (p + m == p + n %[mod d]) = (m == n %[mod d]).

Lemma modn_add2r : forall p m n d,
  (m + p == n + p %[mod d]) = (m == n %[mod d]).

Lemma modn_mulml : forall m n d, m %% d * n = m * n %[mod d].

Lemma modn_mulmr : forall m n d, m * (n %% d) = m * n %[mod d].

Lemma modn_mul2m : forall m n d, m %% d * (n %% d) = m * n %[mod d].

Lemma modn2 : forall m, m %% 2 = odd m.

Lemma divn2 : forall m, m %/ 2 = m./2.

Lemma odd_mod : forall m d, odd d = false -> odd (m %% d) = odd m.

Lemma modn_exp : forall m n a, (a %% n) ^ m = a ^ m %[mod n].

Divisibility 

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

Notation "m %| d" := (dvdn m d) (at level 70, no associativity) : nat_scope.

Definition multn := [rel m d | d %| m].

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

Lemma dvdnP : forall d m, reflect (exists k, m = k * d) (d %| m).
Implicit Arguments dvdnP [d m].

Lemma dvdn0 : forall d, d %| 0.

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

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

Lemma dvd1n : forall m, 1 %| m.

Lemma dvdn_gt0 : forall d m, m > 0 -> d %| m -> d > 0.

Lemma dvdnn : forall m, m %| m.

Lemma dvdn_mull : forall d m n, d %| n -> d %| m * n.

Lemma dvdn_mulr : forall d m n, d %| m -> d %| m * n.

Hint Resolve dvdn0 dvd1n dvdnn dvdn_mull dvdn_mulr.

Lemma dvdn_mul : forall d1 d2 m1 m2, d1 %| m1 -> d2 %| m2 -> d1 * d2 %| m1 * m2.

Lemma dvdn_trans : forall n d m, d %| n -> n %| m -> d %| m.

Lemma dvdn_eq : forall d m, (d %| m) = (m %/ d * d == m).

Lemma divnK : forall d m, d %| m -> m %/ d * d = m.

Lemma leq_divl : forall d m n, d %| m -> (m %/ d <= n) = (m <= n * d).

Lemma ltn_divr : forall d m n, d %| m -> (n < m %/ d) = (n * d < m).

Lemma eqn_div : forall d m n, d > 0 -> d %| m -> (n == m %/ d) = (n * d == m).

Lemma eqn_mul : forall d m n, d > 0 -> d %| m -> (m == n * d) = (m %/ d == n).

Lemma divn_mulAC : forall d m n, d %| m -> m %/ d * n = m * n %/ d.

Lemma divn_mulA : forall d m n, d %| n -> m * (n %/ d) = m * n %/ d.

Lemma divn_mulCA : forall d m n,
  d %| m -> d %| n -> m * (n %/ d) = n * (m %/ d).

Lemma divn_divr : forall m n p, p %| n -> m %/ (n %/ p) = m * p %/ n.

Lemma modn_dvdm : forall m n d, d %| m -> n %% m = n %[mod d].

Lemma dvdn_leq : forall d m, 0 < m -> d %| m -> d <= m.

Lemma gtnNdvd : forall n d, 0 < n -> n < d -> (d %| n) = false.

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

Lemma dvdn_pmul2l : forall p d m, 0 < p -> (p * d %| p * m) = (d %| m).
Implicit Arguments dvdn_pmul2l [p m d].

Lemma dvdn_pmul2r : forall p d m, 0 < p -> (d * p %| m * p) = (d %| m).
Implicit Arguments dvdn_pmul2r [p m d].

Lemma dvdn_exp2l : forall p m n, m <= n -> p ^ m %| p ^ n.

Lemma dvdn_Pexp2l : forall p m n, p > 1 -> (p ^ m %| p ^ n) = (m <= n).

Lemma dvdn_exp2r : forall m n k, m %| n -> m ^ k %| n ^ k.

Lemma dvdn_addr : forall m d n, d %| m -> (d %| m + n) = (d %| n).

Lemma dvdn_addl : forall n d m, d %| n -> (d %| m + n) = (d %| m).

Lemma dvdn_add : forall d m n, d %| m -> d %| n -> d %| m + n.

Lemma dvdn_add_eq : forall d m n, d %| m + n -> (d %| m) = (d %| n).

Lemma dvdn_subr : forall d m n, n <= m -> d %| m -> (d %| m - n) = (d %| n).

Lemma dvdn_subl : forall d m n, n <= m -> d %| n -> (d %| m - n) = (d %| m).

Lemma dvdn_sub : forall d m n, d %|m -> d %| n -> d %| m - n.

Lemma dvdn_exp : forall k d m, 0 < k -> d %| m -> d %| (m ^ k).

Hint Resolve dvdn_add dvdn_sub dvdn_exp.

Lemma eqn_mod_dvd : forall d m n, n <= m -> (m == n %[mod d]) = (d %| m - n).

Lemma divn_addl : forall m n d, d %| m -> (m + n) %/ d = m %/ d + n %/ d.

Lemma divn_addr : forall m n d, d %| n -> (m + n) %/ d = m %/ d + n %/ d.

  A function that computes the gcd of 2 numbers                     

Fixpoint gcdn_rec (m n : nat) {struct m} :=
  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 : forall 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 : forall m n, gcdn m n %| n.

Lemma dvdn_gcdl : forall m n, gcdn m n %| m.

Lemma gcdn_gt0 : forall m n, (0 < gcdn m n) = (0 < m) || (0 < n).

Lemma gcdn_addl_mul : forall k m n, gcdn m (k * m + n) = gcdn m n.

Lemma gcdn_addl : forall m n, gcdn m (m + n) = gcdn m n.

Lemma gcdn_addr : forall m n, gcdn m (n + m) = gcdn m n.

Lemma gcdn_mull : forall n m, gcdn n (m * n) = n.

Lemma gcdn_mulr : forall n m, gcdn n (n * m) = n.

Extended gcd, which computes Bezout coefficients. 

Fixpoint bezout_rec (km kn : nat) (qs : seq nat) {struct 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 : nat) (qs : seq nat) {struct s} :=
  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 [::]).

CoInductive egcdn_spec (m n : nat) : 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 : forall n, egcdn 0 n = (1, 0).

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

Lemma bezoutl : forall m n, m > 0 -> {a | a < m & m %| gcdn m n + a * n}.

Lemma bezoutr : forall m n, n > 0 -> {a | a < n & n %| gcdn m n + a * m}.

Back to the gcd. 

Lemma dvdn_gcd : forall p m n, p %| gcdn m n = (p %| m) && (p %| n).

Lemma gcdn_mul2l : forall p m n, gcdn (p * m) (p * n) = p * gcdn m n.

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

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

Lemma gcdnAC : right_commutative gcdn.

Lemma gcdnA : associative gcdn.

Lemma gcdnCA : left_commutative gcdn.

Lemma muln_gcdl : left_distributive muln gcdn.

Lemma muln_gcdr : right_distributive muln gcdn.

Lemma gcdn_def : forall d m n,
    d %| m -> d %| n -> (forall d', d' %| m -> d' %| n -> d' %| d)
  -> gcdn m n = d.

Lemma gcdn_divnC : forall n m, n * (m %/ gcdn n m) = m * (n %/ gcdn n m).

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 : forall m n, lcmn m n * gcdn m n = m * n.

Lemma lcmn_gt0 : forall 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 dvdn_lcml : forall d1 d2, d1 %| lcmn d1 d2.

Lemma dvdn_lcmr : forall d1 d2, d2 %| lcmn d1 d2.

Lemma dvdn_lcm : forall d1 d2 m, lcmn d1 d2 %| m = (d1 %| m) && (d2 %| m).

Coprime factors 

Definition coprime m n := gcdn m n == 1.

Lemma coprime1n : forall n, coprime 1 n.

Lemma coprimen1 : forall n, coprime n 1.

Lemma coprime_sym : forall m n, coprime m n = coprime n m.

Lemma coprime_modl : forall m n, coprime (m %% n) n = coprime m n.

Lemma coprime_modr : forall m n, coprime m (n %% m) = coprime m n.

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

Lemma modn_coprime : forall k n, O < k ->
  (exists u, (k * u) %% n = 1%N) -> coprime k n.

Lemma gauss_inv : forall m n p,
  coprime m n -> (m * n %| p) = (m %| p) && (n %| p).

Lemma gauss : forall m n p, coprime m n -> (m %| n * p) = (m %| p).

Lemma gauss_gcdr : forall p m n, coprime p m -> gcdn p (m * n) = gcdn p n.

Lemma gauss_gcdl : forall p m n, coprime p n -> gcdn p (m * n) = gcdn p m.

Lemma coprime_mulr : forall p m n,
  coprime p (m * n) = coprime p m && coprime p n.

Lemma coprime_mull : forall p m n,
  coprime (m * n) p = coprime m p && coprime n p.

Lemma coprime_pexpl : forall k m n, 0 < k -> coprime (m ^ k) n = coprime m n.

Lemma coprime_pexpr : forall k m n, 0 < k -> coprime m (n ^ k) = coprime m n.

Lemma coprime_expl : forall k m n, coprime m n -> coprime (m ^ k) n.

Lemma coprime_expr : forall k m n, coprime m n -> coprime m (n ^ k).

Lemma coprime_dvdl : forall m n p, m %| n -> coprime n p -> coprime m p.

Lemma coprime_dvdr : forall m n p, m %| n -> coprime p n -> coprime p m.

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

Lemma dvdn_pexp2r : forall 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 : forall x y,
  (x == y %[mod m1 * m2]) = (x == y %[mod m1]) && (x == y %[mod m2]).

  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 : forall r1 r2, chinese r1 r2 = r1 %[mod m1].

Lemma chinese_modr : forall r1 r2, chinese r1 r2 = r2 %[mod m2].

Lemma chinese_modlr : forall x, x = chinese (x %% m1) (x %% m2) %[mod m1 * m2].

End Chinese.