1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / Matita is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/library_autobatch/nat/congruence".
17 include "auto/nat/relevant_equations.ma".
18 include "auto/nat/primes.ma".
20 definition S_mod: nat \to nat \to nat \def
21 \lambda n,m:nat. (S m) \mod n.
23 definition congruent: nat \to nat \to nat \to Prop \def
24 \lambda n,m,p:nat. mod n p = mod m p.
26 interpretation "congruent" 'congruent n m p =
27 (cic:/matita/library_autobatch/nat/congruence/congruent.con n m p).
29 notation < "hvbox(n break \cong\sub p m)"
30 (*non associative*) with precedence 45
31 for @{ 'congruent $n $m $p }.
33 theorem congruent_n_n: \forall n,p:nat.congruent n n p.
39 theorem transitive_congruent: \forall p:nat. transitive nat
40 (\lambda n,m. congruent n m p).
41 intros.unfold transitive.
45 apply (trans_eq ? ? (y \mod p))
46 [ (*qui autobatch non chiude il goal*)
48 | (*qui autobatch non chiude il goal*)
53 theorem le_to_mod: \forall n,m:nat. n \lt m \to n = n \mod m.
56 (*apply (div_mod_spec_to_eq2 n m O n (n/m) (n \mod m))
62 | apply div_mod_spec_div_mod.
63 apply (le_to_lt_to_lt O n m)
70 theorem mod_mod : \forall n,p:nat. O<p \to n \mod p = (n \mod p) \mod p.
73 (*rewrite > (div_mod (n \mod p) p) in \vdash (? ? % ?)
74 [ rewrite > (eq_div_O ? p)
83 theorem mod_times_mod : \forall n,m,p:nat. O<p \to O<m \to n \mod p = (n \mod (m*p)) \mod p.
85 apply (div_mod_spec_to_eq2 n p (n/p) (n \mod p)
86 (n/(m*p)*m + (n \mod (m*p)/p)))
88 (*apply div_mod_spec_div_mod.
94 | rewrite > times_plus_l.
97 [ rewrite > assoc_times.
98 rewrite < div_mod;autobatch
100 | rewrite > (times_n_O O).
101 apply lt_times;assumption
109 theorem congruent_n_mod_n :
110 \forall n,p:nat. O < p \to congruent n (n \mod p) p.
118 theorem congruent_n_mod_times :
119 \forall n,m,p:nat. O < p \to O < m \to congruent n (n \mod (m*p)) p.
120 intros.unfold congruent.
121 apply mod_times_mod;assumption.
124 theorem eq_times_plus_to_congruent: \forall n,m,p,r:nat. O< p \to
125 n = r*p+m \to congruent n m p.
128 apply (div_mod_spec_to_eq2 n p (div n p) (mod n p) (r +(div m p)) (mod m p))
130 (*apply div_mod_spec_div_mod.
137 (*cut (n = r * p + (m / p * p + m \mod p)).*)
138 (*lapply (div_mod m p H).
140 rewrite > distr_times_plus.
141 (*rewrite > (sym_times p (m/p)).*)
142 (*rewrite > sym_times.*)
143 rewrite > assoc_plus.
144 autobatch paramodulation.
150 rewrite > distr_times_plus.
152 rewrite > (sym_times p).
153 rewrite > assoc_plus.
154 rewrite < div_mod;assumption.
159 theorem divides_to_congruent: \forall n,m,p:nat. O < p \to m \le n \to
160 divides p (n - m) \to congruent n m p.
163 apply (eq_times_plus_to_congruent n m p n2)
165 | rewrite < sym_plus.
166 apply minus_to_plus;autobatch
168 | rewrite > sym_times. assumption
173 theorem congruent_to_divides: \forall n,m,p:nat.
174 O < p \to congruent n m p \to divides p (n - m).
176 unfold congruent in H1.
177 apply (witness ? ? ((n / p)-(m / p))).
179 rewrite > (div_mod n p) in \vdash (? ? % ?)
180 [ rewrite > (div_mod m p) in \vdash (? ? % ?)
181 [ rewrite < (sym_plus (m \mod p)).
184 rewrite < (eq_minus_minus_minus_plus ? (n \mod p)).
185 rewrite < minus_plus_m_m.
187 apply times_minus_l*)
194 theorem mod_times: \forall n,m,p:nat.
195 O < p \to mod (n*m) p = mod ((mod n p)*(mod m p)) p.
197 change with (congruent (n*m) ((mod n p)*(mod m p)) p).
198 apply (eq_times_plus_to_congruent ? ? p
199 ((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p)))
201 | apply (trans_eq ? ? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p))))
202 [ apply eq_f2;autobatch(*;apply div_mod.assumption.*)
203 | apply (trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) +
204 (n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p)))
205 [ apply times_plus_plus
207 [ rewrite < assoc_times.
209 (*rewrite > (assoc_times (n/p) p (m \mod p)).
210 rewrite > (sym_times p (m \mod p)).
211 rewrite < (assoc_times (n/p) (m \mod p) p).
212 rewrite < times_plus_l.
213 rewrite < (assoc_times (n \mod p)).
214 rewrite < times_plus_l.
229 theorem congruent_times: \forall n,m,n1,m1,p. O < p \to congruent n n1 p \to
230 congruent m m1 p \to congruent (n*m) (n1*m1) p.
233 rewrite > (mod_times n m p H).
243 theorem congruent_pi: \forall f:nat \to nat. \forall n,m,p:nat.O < p \to
244 congruent (pi n f m) (pi n (\lambda m. mod (f m) p) m) p.
248 (*apply congruent_n_mod_n.
250 | apply congruent_times
253 (*apply congruent_n_mod_n.
255 | (*NB: QUI AUTO NON RIESCE A CHIUDERE IL GOAL*)