matita/matita/lib/arithmetics/congruence.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/primes.ma".
  13
  14 definition S_mod ≝ λn,m:nat. S m \mod n.
  15
  16 definition congruent ≝ λn,m,p:nat. mod n p = mod m p.
  17
  18 interpretation "congruent" 'congruent n m p = (congruent n m p).
  19
  20 theorem congruent_n_n: ∀n,p:nat.congruent n n p.
  21 // qed.
  22
  23 theorem transitive_congruent: ∀p. transitive ? (λn,m. congruent n m p).
  24 // qed.
  25
  26 theorem le_to_mod: ∀n,m:nat. n < m → n = n \mod m.
  27 #n #m #ltnm @(div_mod_spec_to_eq2 n m O n (n/m) (n \mod m))
  28 % // @lt_mod_m_m @(ltn_to_ltO … ltnm)
  29 qed.
  30
  31 theorem mod_mod : ∀n,p:nat. O<p → n \mod p = (n \mod p) \mod p.
  32 #n #p #posp >(div_mod (n \mod p) p) in ⊢ (??%?);
  33 >(eq_div_O ? p) // @lt_mod_m_m //
  34 qed.
  35
  36 theorem mod_times_mod : ∀n,m,p:nat. O<p → O<m →
  37   n \mod p = (n \mod (m*p)) \mod p.
  38 #n #m #p #posp #posm
  39 @(div_mod_spec_to_eq2 n p (n/p) (n \mod p) (n/(m*p)*m + (n \mod (m*p)/p)))
  40   [@div_mod_spec_div_mod //
  41   |% [@lt_mod_m_m //]
  42    >distributive_times_plus_r >associative_plus <div_mod //
  43   ]
  44 qed.
  45
  46 theorem congruent_n_mod_n: ∀n,p. 0 < p →
  47   congruent n (n \mod p) p.
  48 #n #p #posp @mod_mod //
  49 qed.
  50
  51 theorem congruent_n_mod_times: ∀n,m,p. 0 < p → 0 < m →
  52   congruent n (n \mod (m*p)) p.
  53 #n #p #posp @mod_times_mod
  54 qed.
  55
  56 theorem eq_times_plus_to_congruent: ∀n,m,p,r:nat. 0 < p →
  57   n = r*p+m → congruent n m p.
  58 #n #m #p #r #posp #Hn
  59 @(div_mod_spec_to_eq2 n p (div n p) (mod n p) (r +(div m p)) (mod m p))
  60   [@div_mod_spec_div_mod //
  61   |% [@lt_mod_m_m //]
  62    >commutative_times >distributive_times_plus >commutative_times
  63    >(commutative_times p) >associative_plus //
  64   ]
  65 qed.
  66
  67 theorem divides_to_congruent: ∀n,m,p:nat. 0 < p → m ≤ n →
  68   divides p (n - m) → congruent n m p.
  69 #n #m #p #posp #lemn * #q #Hdiv @(eq_times_plus_to_congruent n m p q) //
  70 >commutative_plus @minus_to_plus //
  71 qed.
  72
  73 theorem congruent_to_divides: ∀n,m,p:nat.
  74   0 < p → congruent n m p → divides p (n - m).
  75 #n #m #p #posp #Hcong %{((n / p)-(m / p))}
  76 >commutative_times >(div_mod n p) in ⊢ (??%?);
  77 >(div_mod m p) in ⊢ (??%?); //
  78 qed.
  79
  80 theorem mod_times: ∀n,m,p. 0 < p →
  81   mod (n*m) p = mod ((mod n p)*(mod m p)) p.
  82 #n #m #p #posp
  83 @(eq_times_plus_to_congruent ? ? p
  84   ((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p))) //
  85 @(trans_eq ? ? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p)))) //
  86 @(trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) +
  87   (n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p)))
  88   [cut (∀a,b,c,d.(a+b)*(c+d) = a*c +a*d + b*c + b*d)
  89     [#a #b #c #d >(distributive_times_plus_r (c+d) a b)
  90      >(distributive_times_plus a c d)
  91      >(distributive_times_plus b c d) //] #Hcut
  92    @Hcut
  93   |@eq_f2
  94     [<associative_times >(associative_times (n/p) p (m \mod p))
  95      >(commutative_times p (m \mod p)) <(associative_times (n/p) (m \mod p) p)
  96      >distributive_times_plus_r //
  97     |%
  98     ]
  99   ]
 100 qed.
 101
 102 theorem congruent_times: ∀n,m,n1,m1,p. O < p → congruent n n1 p →
 103   congruent m m1 p → congruent (n*m) (n1*m1) p.
 104 #n #m #n1 #m1 #p #posp #Hcongn #Hcongm whd
 105 >(mod_times n m p posp) >Hcongn >Hcongm @sym_eq @mod_times //
 106 qed.
 107