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/nat/ord".
17 include "datatypes/constructors.ma".
19 include "nat/nth_prime.ma".
20 include "nat/relevant_equations.ma". (* required by autobatch paramod *)
22 let rec p_ord_aux p n m \def
26 [ O \Rightarrow pair nat nat O n
28 match (p_ord_aux p (n / m) m) with
29 [ (pair q r) \Rightarrow pair nat nat (S q) r] ]
30 | (S a) \Rightarrow pair nat nat O n].
32 (* p_ord n m = <q,r> if m divides n q times, with remainder r *)
33 definition p_ord \def \lambda n,m:nat.p_ord_aux n n m.
35 theorem p_ord_aux_to_Prop: \forall p,n,m. O < m \to
36 match p_ord_aux p n m with
37 [ (pair q r) \Rightarrow n = m \sup q *r ].
40 apply (nat_case (n \mod m)).
41 simplify.apply plus_n_O.
43 simplify.apply plus_n_O.
45 apply (nat_case1 (n1 \mod m)).intro.
47 generalize in match (H (n1 / m) m).
48 elim (p_ord_aux n (n1 / m) m).
50 rewrite > assoc_times.
51 rewrite < H3.rewrite > (plus_n_O (m*(n1 / m))).
54 rewrite < div_mod.reflexivity.
55 assumption.assumption.
56 intros.simplify.apply plus_n_O.
59 theorem p_ord_aux_to_exp: \forall p,n,m,q,r. O < m \to
60 (pair nat nat q r) = p_ord_aux p n m \to n = m \sup q * r.
63 match (pair nat nat q r) with
64 [ (pair q r) \Rightarrow n = m \sup q * r ].
66 apply p_ord_aux_to_Prop.
70 (* questo va spostato in primes1.ma *)
71 theorem p_ord_exp: \forall n,m,i. O < m \to n \mod m \neq O \to
72 \forall p. i \le p \to p_ord_aux p (m \sup i * n) m = pair nat nat i n.
79 elim (n \mod m).simplify.reflexivity.simplify.reflexivity.
82 cut (O < n \mod m \lor O = n \mod m).
83 elim Hcut.apply (lt_O_n_elim (n \mod m) H3).
84 intros. simplify.reflexivity.
86 apply H1.apply sym_eq.assumption.
87 apply le_to_or_lt_eq.apply le_O_n.
88 generalize in match H3.
89 apply (nat_case p).intro.apply False_ind.apply (not_le_Sn_O n1 H4).
91 simplify. fold simplify (m \sup (S n1)).
92 cut (((m \sup (S n1)*n) \mod m) = O).
94 simplify.fold simplify (m \sup (S n1)).
95 cut ((m \sup (S n1) *n) / m = m \sup n1 *n).
97 rewrite > (H2 m1). simplify.reflexivity.
98 apply le_S_S_to_le.assumption.
101 rewrite > assoc_times.
102 apply (lt_O_n_elim m H).
103 intro.apply div_times.
105 apply divides_to_mod_O.
107 simplify.rewrite > assoc_times.
108 apply (witness ? ? (m \sup n1 *n)).reflexivity.
111 theorem p_ord_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
112 match p_ord_aux p n m with
113 [ (pair q r) \Rightarrow r \mod m \neq O].
114 intro.elim p.absurd (O < n).assumption.
115 apply le_to_not_lt.assumption.
117 apply (nat_case1 (n1 \mod m)).intro.
118 generalize in match (H (n1 / m) m).
119 elim (p_ord_aux n (n1 / m) m).
121 apply eq_mod_O_to_lt_O_div.
122 apply (trans_lt ? (S O)).unfold lt.apply le_n.
123 assumption.assumption.assumption.
125 apply (trans_le ? n1).change with (n1 / m < n1).
126 apply lt_div_n_m_n.assumption.assumption.assumption.
130 apply (not_eq_O_S m1).
131 rewrite > H5.reflexivity.
134 theorem p_ord_aux_to_not_mod_O: \forall p,n,m,q,r. (S O) < m \to O < n \to n \le p \to
135 pair nat nat q r = p_ord_aux p n m \to r \mod m \neq O.
138 match (pair nat nat q r) with
139 [ (pair q r) \Rightarrow r \mod m \neq O].
141 apply p_ord_aux_to_Prop1.
142 assumption.assumption.assumption.
145 theorem p_ord_exp1: \forall p,n,q,r. O < p \to \lnot p \divides r \to
146 n = p \sup q * r \to p_ord n p = pair nat nat q r.
151 |unfold.intro.apply H1.
152 apply mod_O_to_divides[assumption|assumption]
153 |apply (trans_le ? (p \sup q)).
155 elim q.simplify.apply le_n_Sn.
157 generalize in match H3.
158 apply (nat_case n1).simplify.
159 rewrite < times_n_SO.intro.assumption.
161 apply (trans_le ? (p*(S m))).
162 apply (trans_le ? ((S (S O))*(S m))).
163 simplify.rewrite > plus_n_Sm.
168 apply le_times_r.assumption.
169 alias id "not_eq_to_le_to_lt" = "cic:/matita/algebra/finite_groups/not_eq_to_le_to_lt.con".
170 apply not_eq_to_le_to_lt.
171 unfold.intro.apply H1.
173 apply (witness ? r r ?).simplify.apply plus_n_O.
175 rewrite > times_n_SO in \vdash (? % ?).
177 change with (O \lt r).
178 apply not_eq_to_le_to_lt.
180 apply H1.rewrite < H3.
181 apply (witness ? ? O ?).rewrite < times_n_O.reflexivity.
186 theorem p_ord_to_exp1: \forall p,n,q,r. (S O) \lt p \to O \lt n \to p_ord n p = pair nat nat q r\to
187 \lnot p \divides r \land n = p \sup q * r.
191 apply (p_ord_aux_to_not_mod_O n n p q r).assumption.assumption.
192 apply le_n.symmetry.assumption.
193 apply divides_to_mod_O.apply (trans_lt ? (S O)).
194 unfold.apply le_n.assumption.assumption.
195 apply (p_ord_aux_to_exp n).apply (trans_lt ? (S O)).
196 unfold.apply le_n.assumption.symmetry.assumption.
199 theorem p_ord_times: \forall p,a,b,qa,ra,qb,rb. prime p
200 \to O \lt a \to O \lt b
201 \to p_ord a p = pair nat nat qa ra
202 \to p_ord b p = pair nat nat qb rb
203 \to p_ord (a*b) p = pair nat nat (qa + qb) (ra*rb).
206 elim (p_ord_to_exp1 ? ? ? ? Hcut H1 H3).
207 elim (p_ord_to_exp1 ? ? ? ? Hcut H2 H4).
209 apply (trans_lt ? (S O)).unfold.apply le_n.assumption.
211 elim (divides_times_to_divides ? ? ? H H9).
212 apply (absurd ? ? H10 H5).
213 apply (absurd ? ? H10 H7).
216 autobatch paramodulation.
217 unfold prime in H. elim H. assumption.
220 theorem fst_p_ord_times: \forall p,a,b. prime p
221 \to O \lt a \to O \lt b
222 \to fst ? ? (p_ord (a*b) p) = (fst ? ? (p_ord a p)) + (fst ? ? (p_ord b p)).
224 rewrite > (p_ord_times p a b (fst ? ? (p_ord a p)) (snd ? ? (p_ord a p))
225 (fst ? ? (p_ord b p)) (snd ? ? (p_ord b p)) H H1 H2).
226 simplify.reflexivity.
227 apply eq_pair_fst_snd.
228 apply eq_pair_fst_snd.
231 theorem p_ord_p : \forall p:nat. (S O) \lt p \to p_ord p p = pair ? ? (S O) (S O).
234 apply (trans_lt ? (S O)). unfold.apply le_n.assumption.
236 apply (absurd ? ? H).
238 apply divides_to_le.unfold.apply le_n.assumption.
239 rewrite < times_n_SO.
243 (* p_ord and divides *)
244 theorem divides_to_p_ord: \forall p,a,b,c,d,n,m:nat.
245 O < n \to O < m \to prime p
246 \to divides n m \to p_ord n p = pair ? ? a b \to
247 p_ord m p = pair ? ? c d \to divides b d \land a \le c.
250 [lapply (p_ord_to_exp1 ? ? ? ? Hcut H H4).
251 lapply (p_ord_to_exp1 ? ? ? ? Hcut H1 H5).
252 elim Hletin. clear Hletin.
253 elim Hletin1. clear Hletin1.
256 [apply (gcd_SO_to_divides_times_to_divides (exp p c))
257 [elim (le_to_or_lt_eq ? ? (le_O_n b))
260 apply (lt_to_not_eq O ? H).
269 apply eq_gcd_times_SO
270 [apply lt_to_le.assumption
271 |apply lt_O_exp.apply lt_to_le.assumption
273 (* hint non trova prime_to_gcd_SO e
274 autobatch non chiude il goal *)
275 apply prime_to_gcd_SO
276 [assumption|assumption]
280 |apply (trans_divides ? n)
281 [apply (witness ? ? (exp p a)).
287 |apply (le_exp_to_le p)
290 [apply lt_O_exp.apply lt_to_le.assumption
291 |apply (gcd_SO_to_divides_times_to_divides d)
292 [apply lt_O_exp.apply lt_to_le.assumption
295 |simplify.rewrite < sym_gcd.
296 apply eq_gcd_times_SO
297 [apply lt_to_le.assumption
298 |apply lt_O_exp.apply lt_to_le.assumption
300 (* hint non trova prime_to_gcd_SO e
301 autobatch non chiude il goal *)
302 apply prime_to_gcd_SO
303 [assumption|assumption]
304 |rewrite > sym_gcd. assumption
307 |apply (trans_divides ? n)
308 [apply (witness ? ? b).assumption
309 |rewrite > sym_times.assumption
319 (* p_ord and primes *)
320 theorem not_divides_to_p_ord_O: \forall n,i.
321 Not (divides (nth_prime i) n) \to p_ord n (nth_prime i) =
325 [apply lt_O_nth_prime_n
331 theorem p_ord_O_to_not_divides: \forall n,i,r.
333 p_ord n (nth_prime i) = pair nat nat O r
334 \to Not (divides (nth_prime i) n).
336 lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
337 [apply lt_SO_nth_prime_n
347 theorem p_ord_to_not_eq_O : \forall n,p,q,r.
349 p_ord n (nth_prime p) = pair nat nat q r \to
354 [lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
355 [apply lt_SO_nth_prime_n.
358 apply (lt_to_not_eq ? ? Hcut).
363 |apply (trans_lt ? (S O))[apply lt_O_S|assumption]
367 definition ord :nat \to nat \to nat \def
368 \lambda n,p. fst ? ? (p_ord n p).
370 definition ord_rem :nat \to nat \to nat \def
371 \lambda n,p. snd ? ? (p_ord n p).
373 theorem divides_to_ord: \forall p,n,m:nat.
374 O < n \to O < m \to prime p
376 \to divides (ord_rem n p) (ord_rem m p) \land (ord n p) \le (ord m p).
378 apply (divides_to_p_ord p ? ? ? ? n m H H1 H2 H3)
379 [unfold ord.unfold ord_rem.apply eq_pair_fst_snd
380 |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
384 theorem divides_to_divides_ord_rem: \forall p,n,m:nat.
385 O < n \to O < m \to prime p \to divides n m \to
386 divides (ord_rem n p) (ord_rem m p).
388 elim (divides_to_ord p n m H H1 H2 H3).assumption.
391 theorem divides_to_le_ord: \forall p,n,m:nat.
392 O < n \to O < m \to prime p \to divides n m \to
393 (ord n p) \le (ord m p).
395 elim (divides_to_ord p n m H H1 H2 H3).assumption.
398 theorem exp_ord: \forall p,n. (S O) \lt p
399 \to O \lt n \to n = p \sup (ord n p) * (ord_rem n p).
401 elim (p_ord_to_exp1 p n (ord n p) (ord_rem n p))
405 |unfold ord.unfold ord_rem.
406 apply eq_pair_fst_snd
410 theorem divides_ord_rem: \forall p,n. (S O) < p \to O < n
411 \to divides (ord_rem n p) n.
413 apply (witness ? ? (p \sup (ord n p))).
415 apply exp_ord[assumption|assumption]
418 theorem lt_O_ord_rem: \forall p,n. (S O) < p \to O < n \to O < ord_rem n p.
420 elim (le_to_or_lt_eq O (ord_rem n p))
423 apply (lt_to_not_eq ? ? H1).
424 lapply (divides_ord_rem ? ? H H1).
425 rewrite < H2 in Hletin.
433 (* p_ord_inv is the inverse of ord *)
434 definition p_ord_inv \def
437 [pair q r \Rightarrow r*m+q].
439 theorem eq_p_ord_inv: \forall p,m,x.
440 p_ord_inv p m x = (ord_rem x p)*m+(ord x p).
441 intros.unfold p_ord_inv. unfold ord_rem.
447 theorem div_p_ord_inv:
448 \forall p,m,x. ord x p < m \to p_ord_inv p m x / m = ord_rem x p.
449 intros.rewrite > eq_p_ord_inv.
450 apply div_plus_times.
454 theorem mod_p_ord_inv:
455 \forall p,m,x. ord x p < m \to p_ord_inv p m x \mod m = ord x p.
456 intros.rewrite > eq_p_ord_inv.
457 apply mod_plus_times.