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 notation "hvbox(n break ≅_{p} m)"
  19   non associative with precedence 45
  20 for @{ 'congruent $n $m $p }.
  21
  22 interpretation "congruent" 'congruent n m p = (congruent n m p).
  23
  24 theorem congruent_n_n: ∀n,p:nat.congruent n n p.
  25 // qed.
  26
  27 theorem transitive_congruent: ∀p. transitive ? (λn,m. congruent n m p).
  28 // qed.
  29
  30 theorem le_to_mod: ∀n,m:nat. n < m → n = n \mod m.
  31 #n #m #ltnm @(div_mod_spec_to_eq2 n m O n (n/m) (n \mod m))
  32 % // @lt_mod_m_m @(ltn_to_ltO … ltnm)
  33 qed.
  34
  35 theorem mod_mod : ∀n,p:nat. O<p → n \mod p = (n \mod p) \mod p.
  36 #n #p #posp >(div_mod (n \mod p) p) in ⊢ (??%?);
  37 >(eq_div_O ? p) // @lt_mod_m_m //
  38 qed.
  39
  40 theorem mod_times_mod : ∀n,m,p:nat. O<p → O<m →
  41   n \mod p = (n \mod (m*p)) \mod p.
  42 #n #m #p #posp #posm
  43 @(div_mod_spec_to_eq2 n p (n/p) (n \mod p) (n/(m*p)*m + (n \mod (m*p)/p)))
  44   [@div_mod_spec_div_mod //
  45   |% [@lt_mod_m_m //]
  46    >distributive_times_plus_r >associative_plus <div_mod //
  47   ]
  48 qed.
  49
  50 theorem congruent_n_mod_n: ∀n,p. 0 < p →
  51   congruent n (n \mod p) p.
  52 #n #p #posp @mod_mod //
  53 qed.
  54
  55 theorem congruent_n_mod_times: ∀n,m,p. 0 < p → 0 < m →
  56   congruent n (n \mod (m*p)) p.
  57 #n #p #posp @mod_times_mod
  58 qed.
  59
  60 theorem eq_times_plus_to_congruent: ∀n,m,p,r:nat. 0 < p →
  61   n = r*p+m → congruent n m p.
  62 #n #m #p #r #posp #Hn
  63 @(div_mod_spec_to_eq2 n p (div n p) (mod n p) (r +(div m p)) (mod m p))
  64   [@div_mod_spec_div_mod //
  65   |% [@lt_mod_m_m //]
  66    >commutative_times >distributive_times_plus >commutative_times
  67    >(commutative_times p) >associative_plus //
  68   ]
  69 qed.
  70
  71 theorem divides_to_congruent: ∀n,m,p:nat. 0 < p → m ≤ n →
  72   divides p (n - m) → congruent n m p.
  73 #n #m #p #posp #lemn * #q #Hdiv @(eq_times_plus_to_congruent n m p q) //
  74 >commutative_plus @minus_to_plus //
  75 qed.
  76
  77 theorem congruent_to_divides: ∀n,m,p:nat.
  78   0 < p → congruent n m p → divides p (n - m).
  79 #n #m #p #posp #Hcong %{((n / p)-(m / p))}
  80 >commutative_times >(div_mod n p) in ⊢ (??%?);
  81 >(div_mod m p) in ⊢ (??%?); //
  82 qed.
  83
  84 theorem mod_times: ∀n,m,p. 0 < p →
  85   mod (n*m) p = mod ((mod n p)*(mod m p)) p.
  86 #n #m #p #posp
  87 @(eq_times_plus_to_congruent ? ? p
  88   ((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p))) //
  89 @(trans_eq ? ? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p)))) //
  90 @(trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) +
  91   (n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p)))
  92   [cut (∀a,b,c,d.(a+b)*(c+d) = a*c +a*d + b*c + b*d)
  93     [#a #b #c #d >(distributive_times_plus_r (c+d) a b)
  94      >(distributive_times_plus a c d)
  95      >(distributive_times_plus b c d) //] #Hcut
  96    @Hcut
  97   |@eq_f2
  98     [<associative_times >(associative_times (n/p) p (m \mod p))
  99      >(commutative_times p (m \mod p)) <(associative_times (n/p) (m \mod p) p)
 100      >distributive_times_plus_r //
 101     |%
 102     ]
 103   ]
 104 qed.
 105
 106 theorem congruent_times: ∀n,m,n1,m1,p. O < p → congruent n n1 p →
 107   congruent m m1 p → congruent (n*m) (n1*m1) p.
 108 #n #m #n1 #m1 #p #posp #Hcongn #Hcongm whd
 109 >(mod_times n m p posp) >Hcongn >Hcongm @sym_eq @mod_times //
 110 qed.
 111