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