]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/chinese_reminder.ma
- oCic2NCic and nCic2OCic moved to ng_library
[helm.git] / helm / software / matita / library / nat / chinese_reminder.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 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "nat/exp.ma".
16 include "nat/gcd.ma".
17 include "nat/permutation.ma".
18 include "nat/congruence.ma".
19
20 theorem and_congruent_congruent: \forall m,n,a,b:nat. O < n \to O < m \to 
21 gcd n m = (S O) \to ex nat (\lambda x. congruent x a m \land congruent x b n).
22 intros.
23 cut (\exists c,d.c*n - d*m = (S O) \lor d*m - c*n = (S O)).
24 elim Hcut.elim H3.elim H4.
25 apply (ex_intro nat ? ((a+b*m)*a1*n-b*a2*m)).
26 split.
27 (* congruent to a *)
28 cut (a1*n = a2*m + (S O)).
29 rewrite > assoc_times.
30 rewrite > Hcut1.
31 rewrite < (sym_plus ? (a2*m)).
32 rewrite > distr_times_plus.
33 rewrite < times_n_SO.
34 rewrite > assoc_plus.
35 rewrite < assoc_times.
36 rewrite < times_plus_l.
37 rewrite > eq_minus_plus_plus_minus.
38 rewrite < times_minus_l.
39 rewrite > sym_plus.
40 apply (eq_times_plus_to_congruent ? ? ? ((b+(a+b*m)*a2)-b*a2)).
41 assumption.reflexivity.
42 apply le_times_l.
43 apply (trans_le ? ((a+b*m)*a2)).
44 apply le_times_l.
45 apply (trans_le ? (b*m)).
46 rewrite > times_n_SO in \vdash (? % ?).
47 apply le_times_r.assumption.
48 apply le_plus_n.
49 apply le_plus_n.
50 apply minus_to_plus.
51 apply lt_to_le.
52 change with (O + a2*m < a1*n).
53 apply lt_minus_to_plus.
54 rewrite > H5.unfold lt.apply le_n.
55 assumption.
56 (* congruent to b *)
57 cut (a2*m = a1*n - (S O)).
58 rewrite > (assoc_times b a2).
59 rewrite > Hcut1.
60 rewrite > distr_times_minus.
61 rewrite < assoc_times.
62 rewrite < eq_plus_minus_minus_minus.
63 rewrite < times_n_SO.
64 rewrite < times_minus_l.
65 rewrite < sym_plus.
66 apply (eq_times_plus_to_congruent ? ? ? ((a+b*m)*a1-b*a1)).
67 assumption.reflexivity.
68 rewrite > assoc_times.
69 apply le_times_r.
70 apply (trans_le ? (a1*n - a2*m)).
71 rewrite > H5.apply le_n.
72 apply (le_minus_m ? (a2*m)).
73 apply le_times_l.
74 apply le_times_l.
75 apply (trans_le ? (b*m)).
76 rewrite > times_n_SO in \vdash (? % ?).
77 apply le_times_r.assumption.
78 apply le_plus_n.
79 apply sym_eq. apply plus_to_minus.
80 rewrite > sym_plus.
81 apply minus_to_plus.
82 apply lt_to_le.
83 change with (O + a2*m < a1*n).
84 apply lt_minus_to_plus.
85 rewrite > H5.unfold lt.apply le_n.
86 assumption.
87 (* and now the symmetric case; the price to pay for working
88    in nat instead than Z *)
89 apply (ex_intro nat ? ((b+a*n)*a2*m-a*a1*n)).
90 split.
91 (* congruent to a *)
92 cut (a1*n = a2*m - (S O)).
93 rewrite > (assoc_times a a1).
94 rewrite > Hcut1.
95 rewrite > distr_times_minus.
96 rewrite < assoc_times.
97 rewrite < eq_plus_minus_minus_minus.
98 rewrite < times_n_SO.
99 rewrite < times_minus_l.
100 rewrite < sym_plus.
101 apply (eq_times_plus_to_congruent ? ? ? ((b+a*n)*a2-a*a2)).
102 assumption.reflexivity.
103 rewrite > assoc_times.
104 apply le_times_r.
105 apply (trans_le ? (a2*m - a1*n)).
106 rewrite > H5.apply le_n.
107 apply (le_minus_m ? (a1*n)).
108 rewrite > assoc_times.rewrite > assoc_times.
109 apply le_times_l.
110 apply (trans_le ? (a*n)).
111 rewrite > times_n_SO in \vdash (? % ?).
112 apply le_times_r.assumption.
113 apply le_plus_n.
114 apply sym_eq.apply plus_to_minus.
115 rewrite > sym_plus.
116 apply minus_to_plus.
117 apply lt_to_le.
118 change with (O + a1*n < a2*m).
119 apply lt_minus_to_plus.
120 rewrite > H5.unfold lt.apply le_n.
121 assumption.
122 (* congruent to a *)
123 cut (a2*m = a1*n + (S O)).
124 rewrite > assoc_times.
125 rewrite > Hcut1.
126 rewrite > (sym_plus (a1*n)).
127 rewrite > distr_times_plus.
128 rewrite < times_n_SO.
129 rewrite < assoc_times.
130 rewrite > assoc_plus.
131 rewrite < times_plus_l.
132 rewrite > eq_minus_plus_plus_minus.
133 rewrite < times_minus_l.
134 rewrite > sym_plus.
135 apply (eq_times_plus_to_congruent ? ? ? ((a+(b+a*n)*a1)-a*a1)).
136 assumption.reflexivity.
137 apply le_times_l.
138 apply (trans_le ? ((b+a*n)*a1)).
139 apply le_times_l.
140 apply (trans_le ? (a*n)).
141 rewrite > times_n_SO in \vdash (? % ?).
142 apply le_times_r.
143 assumption.
144 apply le_plus_n.
145 apply le_plus_n.
146 apply minus_to_plus.
147 apply lt_to_le.
148 change with (O + a1*n < a2*m).
149 apply lt_minus_to_plus.
150 rewrite > H5.unfold lt.apply le_n.
151 assumption.
152 (* proof of the cut *)
153 rewrite < H2.
154 apply eq_minus_gcd.
155 qed.
156
157 theorem and_congruent_congruent_lt: \forall m,n,a,b:nat. O < n \to O < m \to 
158 gcd n m = (S O) \to 
159 ex nat (\lambda x. (congruent x a m \land congruent x b n) \land
160  (x < m*n)).
161 intros.elim (and_congruent_congruent m n a b).
162 elim H3.
163 apply (ex_intro ? ? (a1 \mod (m*n))).
164 split.split.
165 apply (transitive_congruent m ? a1).
166 unfold congruent.
167 apply sym_eq.
168 change with (congruent a1 (a1 \mod (m*n)) m).
169 rewrite < sym_times.
170 apply congruent_n_mod_times.
171 assumption.assumption.assumption.
172 apply (transitive_congruent n ? a1).
173 unfold congruent.
174 apply sym_eq.
175 change with (congruent a1 (a1 \mod (m*n)) n).
176 apply congruent_n_mod_times.
177 assumption.assumption.assumption.
178 apply lt_mod_m_m.
179 rewrite > (times_n_O O).
180 apply lt_times.assumption.assumption.
181 assumption.assumption.assumption.
182 qed.
183
184 definition cr_pair : nat \to nat \to nat \to nat \to nat \def
185 \lambda n,m,a,b. 
186 min (pred (n*m)) (\lambda x. andb (eqb (x \mod n) a) (eqb (x \mod m) b)).
187
188 theorem cr_pair1: cr_pair (S (S O)) (S (S (S O))) O O = O.
189 reflexivity.
190 qed.
191
192 theorem cr_pair2: cr_pair (S(S O)) (S(S(S O))) (S O) O = (S(S(S O))).
193 simplify.
194 reflexivity.
195 qed.
196
197 theorem cr_pair3: cr_pair (S(S O)) (S(S(S O))) (S O) (S(S O)) = (S(S(S(S(S O))))).
198 reflexivity.
199 qed.
200
201 theorem cr_pair4: cr_pair (S(S(S(S(S O))))) (S(S(S(S(S(S(S O))))))) (S(S(S O))) (S(S O)) = 
202 (S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S O))))))))))))))))))))))).
203 reflexivity.
204 qed.
205
206 theorem mod_cr_pair : \forall m,n,a,b. a \lt m \to b \lt n \to 
207 gcd n m = (S O) \to 
208 (cr_pair m n a b) \mod m = a \land (cr_pair m n a b) \mod n = b.
209 intros.
210 cut (andb (eqb ((cr_pair m n a b) \mod m) a) 
211          (eqb ((cr_pair m n a b) \mod n) b) = true).
212 generalize in match Hcut.
213 apply andb_elim.
214 apply eqb_elim.intro.
215 rewrite > H3.
216 simplify.
217 intro.split.reflexivity.
218 apply eqb_true_to_eq.assumption.
219 intro.
220 simplify.
221 intro.apply False_ind.
222 apply not_eq_true_false.apply sym_eq.assumption.
223 apply (f_min_aux_true 
224 (\lambda x. andb (eqb (x \mod m) a) (eqb (x \mod n) b)) (pred (m*n)) O).
225 elim (and_congruent_congruent_lt m n a b).
226 apply (ex_intro ? ? a1).split.split.
227 apply le_O_n.
228 elim H3.apply le_S_S_to_le.apply (trans_le ? (m*n)).
229 assumption.apply (nat_case (m*n)).apply le_O_n.
230 intro.
231 rewrite < pred_Sn.
232 rewrite < plus_n_O.apply le_n.
233 elim H3.elim H4.
234 apply andb_elim.
235 cut (a1 \mod m = a).
236 cut (a1 \mod n = b).
237 rewrite > (eq_to_eqb_true ? ? Hcut).
238 rewrite > (eq_to_eqb_true ? ? Hcut1).
239 simplify.reflexivity.
240 rewrite < (lt_to_eq_mod b n).assumption.
241 assumption.
242 rewrite < (lt_to_eq_mod a m).assumption.
243 assumption.
244 apply (le_to_lt_to_lt ? b).apply le_O_n.assumption.
245 apply (le_to_lt_to_lt ? a).apply le_O_n.assumption.
246 assumption.
247 qed.