matita/library/nat/congruence.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        Matita is distributed under the terms of the          *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/nat/congruence".
  16
  17 include "nat/relevant_equations.ma".
  18 include "nat/primes.ma".
  19
  20 definition S_mod: nat \to nat \to nat \def
  21 \lambda n,m:nat. (S m) \mod n.
  22
  23 definition congruent: nat \to nat \to nat \to Prop \def
  24 \lambda n,m,p:nat. mod n p = mod m p.
  25
  26 interpretation "congruent" 'congruent n m p =
  27   (cic:/matita/nat/congruence/congruent.con n m p).
  28
  29 notation < "hvbox(n break \cong\sub p m)"
  30   (*non associative*) with precedence 45
  31 for @{ 'congruent $n $m $p }.
  32
  33 theorem congruent_n_n: \forall n,p:nat.congruent n n p.
  34 intros.unfold congruent.reflexivity.
  35 qed.
  36
  37 theorem transitive_congruent: \forall p:nat. transitive nat
  38 (\lambda n,m. congruent n m p).
  39 intros.unfold transitive.unfold congruent.intros.
  40 whd.apply (trans_eq ? ? (y \mod p)).
  41 apply H.apply H1.
  42 qed.
  43
  44 theorem le_to_mod: \forall n,m:nat. n \lt m \to n = n \mod m.
  45 intros.
  46 apply (div_mod_spec_to_eq2 n m O n (n/m) (n \mod m)).
  47 constructor 1.assumption.simplify.reflexivity.
  48 apply div_mod_spec_div_mod.
  49 apply (le_to_lt_to_lt O n m).apply le_O_n.assumption.
  50 qed.
  51
  52 theorem mod_mod : \forall n,p:nat. O<p \to n \mod p = (n \mod p) \mod p.
  53 intros.
  54 rewrite > (div_mod (n \mod p) p) in \vdash (? ? % ?).
  55 rewrite > (eq_div_O ? p).reflexivity.
  56 (* uffa: hint non lo trova lt vs. le*)
  57 apply lt_mod_m_m.
  58 assumption.
  59 assumption.
  60 qed.
  61
  62 theorem mod_times_mod : \forall n,m,p:nat. O<p \to O<m \to n \mod p = (n \mod (m*p)) \mod p.
  63 intros.
  64 apply (div_mod_spec_to_eq2 n p (n/p) (n \mod p)
  65 (n/(m*p)*m + (n \mod (m*p)/p))).
  66 apply div_mod_spec_div_mod.assumption.
  67 constructor 1.
  68 apply lt_mod_m_m.assumption.
  69 rewrite > times_plus_l.
  70 rewrite > assoc_plus.
  71 rewrite < div_mod.
  72 rewrite > assoc_times.
  73 rewrite < div_mod.
  74 reflexivity.
  75 rewrite > (times_n_O O).
  76 apply lt_times.
  77 assumption.assumption.assumption.
  78 qed.
  79
  80 theorem congruent_n_mod_n :
  81 \forall n,p:nat. O < p \to congruent n (n \mod p) p.
  82 intros.unfold congruent.
  83 apply mod_mod.assumption.
  84 qed.
  85
  86 theorem congruent_n_mod_times :
  87 \forall n,m,p:nat. O < p \to O < m \to congruent n (n \mod (m*p)) p.
  88 intros.unfold congruent.
  89 apply mod_times_mod.assumption.assumption.
  90 qed.
  91
  92 theorem eq_times_plus_to_congruent: \forall n,m,p,r:nat. O< p \to
  93 n = r*p+m \to congruent n m p.
  94 intros.unfold congruent.
  95 apply (div_mod_spec_to_eq2 n p (div n p) (mod n p) (r +(div m p)) (mod m p)).
  96 apply div_mod_spec_div_mod.assumption.
  97 constructor 1.
  98 apply lt_mod_m_m.assumption.
  99 (*cut (n = r * p + (m / p * p + m \mod p)).*)
 100 (*lapply (div_mod m p H).
 101 rewrite > sym_times.
 102 rewrite > distr_times_plus.
 103 (*rewrite > (sym_times p (m/p)).*)
 104 (*rewrite > sym_times.*)
 105 rewrite > assoc_plus.
 106 auto paramodulation.
 107 rewrite < div_mod.
 108 assumption.
 109 assumption.
 110 *)
 111 rewrite > sym_times.
 112 rewrite > distr_times_plus.
 113 rewrite > sym_times.
 114 rewrite > (sym_times p).
 115 rewrite > assoc_plus.
 116 rewrite < div_mod.
 117 assumption.assumption.
 118 qed.
 119
 120 theorem divides_to_congruent: \forall n,m,p:nat. O < p \to m \le n \to
 121 divides p (n - m) \to congruent n m p.
 122 intros.elim H2.
 123 apply (eq_times_plus_to_congruent n m p n2).
 124 assumption.
 125 rewrite < sym_plus.
 126 apply minus_to_plus.assumption.
 127 rewrite > sym_times. assumption.
 128 qed.
 129
 130 theorem congruent_to_divides: \forall n,m,p:nat.
 131 O < p \to congruent n m p \to divides p (n - m).
 132 intros.unfold congruent in H1.
 133 apply (witness ? ? ((n / p)-(m / p))).
 134 rewrite > sym_times.
 135 rewrite > (div_mod n p) in \vdash (? ? % ?).
 136 rewrite > (div_mod m p) in \vdash (? ? % ?).
 137 rewrite < (sym_plus (m \mod p)).
 138 rewrite < H1.
 139 rewrite < (eq_minus_minus_minus_plus ? (n \mod p)).
 140 rewrite < minus_plus_m_m.
 141 apply sym_eq.
 142 apply times_minus_l.
 143 assumption.assumption.
 144 qed.
 145
 146 theorem mod_times: \forall n,m,p:nat.
 147 O < p \to mod (n*m) p = mod ((mod n p)*(mod m p)) p.
 148 intros.
 149 change with (congruent (n*m) ((mod n p)*(mod m p)) p).
 150 apply (eq_times_plus_to_congruent ? ? p
 151 ((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p))).
 152 assumption.
 153 apply (trans_eq ? ? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p)))).
 154 apply eq_f2.
 155 apply div_mod.assumption.
 156 apply div_mod.assumption.
 157 apply (trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) +
 158 (n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p))).
 159 apply times_plus_plus.
 160 apply eq_f2.
 161 rewrite < assoc_times.
 162 rewrite > (assoc_times (n/p) p (m \mod p)).
 163 rewrite > (sym_times p (m \mod p)).
 164 rewrite < (assoc_times (n/p) (m \mod p) p).
 165 rewrite < times_plus_l.
 166 rewrite < (assoc_times (n \mod p)).
 167 rewrite < times_plus_l.
 168 apply eq_f2.
 169 apply eq_f2.reflexivity.
 170 reflexivity.reflexivity.
 171 reflexivity.
 172 qed.
 173
 174 theorem congruent_times: \forall n,m,n1,m1,p. O < p \to congruent n n1 p \to
 175 congruent m m1 p \to congruent (n*m) (n1*m1) p.
 176 unfold congruent.
 177 intros.
 178 rewrite > (mod_times n m p H).
 179 rewrite > H1.
 180 rewrite > H2.
 181 apply sym_eq.
 182 apply mod_times.assumption.
 183 qed.
 184
 185 theorem congruent_pi: \forall f:nat \to nat. \forall n,m,p:nat.O < p \to
 186 congruent (pi n f m) (pi n (\lambda m. mod (f m) p) m) p.
 187 intros.
 188 elim n. simplify.
 189 apply congruent_n_mod_n.assumption.
 190 simplify.
 191 apply congruent_times.
 192 assumption.
 193 apply congruent_n_mod_n.assumption.
 194 assumption.
 195 qed.