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 (* successor mod n *)
  15 definition S_mod: nat → nat → nat ≝
  16 λn,m:nat. (S m) \mod n.
  17
  18 definition congruent: nat → nat → nat → Prop ≝
  19 λn,m,p:nat. mod n p = mod m p.
  20
  21 interpretation "congruent" 'congruent n m p = (congruent n m p).
  22
  23 notation "hvbox(n break ≅_{p} m)"
  24   non associative with precedence 45
  25   for @{ 'congruent $n $m $p }.
  26
  27 theorem congruent_n_n: ∀n,p:nat.n ≅_{p} n .
  28 // qed.
  29
  30 theorem transitive_congruent:
  31   ∀p.transitive nat (λn,m.congruent n m p).
  32 /2/ qed.
  33
  34 theorem le_to_mod: ∀n,m:nat. n < m → n = n \mod m.
  35 #n #m #ltnm @(div_mod_spec_to_eq2 n m O n (n/m) (n \mod m))
  36 % // @lt_mod_m_m @(ltn_to_ltO … ltnm)
  37 qed.
  38
  39 theorem mod_mod : ∀n,p:nat. O<p → n \mod p = (n \mod p) \mod p.
  40 #n #p #posp >(div_mod (n \mod p) p) in ⊢ (? ? % ?);
  41 >(eq_div_O ? p) // @lt_mod_m_m //
  42 qed.
  43
  44 theorem mod_times_mod : ∀n,m,p:nat. O<p → O<m →
  45   n \mod p = (n \mod (m*p)) \mod p.
  46 #n #m #p #posp #posm
  47 @(div_mod_spec_to_eq2 n p (n/p) (n \mod p)
  48 (n/(m*p)*m + (n \mod (m*p)/p)))
  49   [@div_mod_spec_div_mod //
  50   |% [@lt_mod_m_m //] >distributive_times_plus_r
  51    >associative_plus <div_mod >associative_times <div_mod //
  52   ]
  53 qed.
  54
  55 theorem congruent_n_mod_n : ∀n,p:nat. O < p →
  56  n ≅_{p} (n \mod p).
  57 /2/ qed.
  58
  59 theorem congruent_n_mod_times : ∀n,m,p:nat. O < p → O < m →
  60   n ≅_{p} (n \mod (m*p)).
  61 /2/ qed.
  62
  63 theorem eq_times_plus_to_congruent: ∀n,m,p,r:nat. O< p →
  64   n = r*p+m → n ≅_{p} m .
  65 #n #m #p #r #posp #eqn
  66 @(div_mod_spec_to_eq2 n p (div n p) (mod n p) (r +(div m p)) (mod m p))
  67   [@div_mod_spec_div_mod //
  68   |% [@lt_mod_m_m //] >distributive_times_plus_r
  69    >associative_plus <div_mod //
  70   ]
  71 qed.
  72
  73 theorem divides_to_congruent: ∀n,m,p:nat. O < p → m ≤ n →
  74   p ∣(n - m) → n ≅_{p} m .
  75 #n #m #p #posp #lemn * #l #eqpl
  76 @(eq_times_plus_to_congruent … l posp) /2/
  77 qed.
  78
  79 theorem congruent_to_divides: ∀n,m,p:nat.O < p →
  80   n ≅_{p} m → p ∣ (n - m).
  81 #n #m #p #posp #congnm @(quotient ? ? ((n / p)-(m / p)))
  82 >commutative_times >(div_mod n p) in ⊢ (??%?);
  83 >(div_mod m p) in ⊢ (??%?); <(commutative_plus (m \mod p))
  84 <congnm <(minus_plus ? (n \mod p)) <minus_plus_m_m //
  85 qed.
  86
  87 theorem mod_times: ∀n,m,p:nat. O < p →
  88   n*m ≅_{p} (n \mod p)*(m \mod p).
  89 #n #m #p #posp @(eq_times_plus_to_congruent ?? p
  90   ((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p))) //
  91 @(trans_eq ?? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p))))
  92   [@eq_f2 //
  93   |@(trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) +
  94     (n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p))) //
  95    >distributive_times_plus >distributive_times_plus_r
  96    >distributive_times_plus_r <associative_plus @eq_f2 //
  97   ]
  98 qed.
  99
 100 theorem congruent_times: ∀n,m,n1,m1,p. O < p →
 101   n ≅_{p} n1 → m ≅_{p} m1 → n*m ≅_{p} n1*m1 .
 102 #n #m #n1 #m1 #p #posp #congn #congm
 103 @(transitive_congruent … (mod_times n m p posp))
 104 >congn >congm @sym_eq @mod_times //
 105 qed.
 106
 107 (*
 108 theorem congruent_pi: \forall f:nat \to nat. \forall n,m,p:nat.O < p \to
 109 congruent (pi n f m) (pi n (\lambda m. mod (f m) p) m) p.
 110 intros.
 111 elim n. simplify.
 112 apply congruent_n_mod_n.assumption.
 113 simplify.
 114 apply congruent_times.
 115 assumption.
 116 apply congruent_n_mod_n.assumption.
 117 assumption.
 118 qed. *)