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