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/gcd.ma". (* for some properties of divides *)
21 include "nat/relevant_equations.ma". (* required by autobatch paramod *)
23 let rec p_ord_aux p n m \def
27 [ O \Rightarrow pair nat nat O n
29 match (p_ord_aux p (n / m) m) with
30 [ (pair q r) \Rightarrow pair nat nat (S q) r] ]
31 | (S a) \Rightarrow pair nat nat O n].
33 (* p_ord n m = <q,r> if m divides n q times, with remainder r *)
34 definition p_ord \def \lambda n,m:nat.p_ord_aux n n m.
36 theorem p_ord_aux_to_Prop: \forall p,n,m. O < m \to
37 match p_ord_aux p n m with
38 [ (pair q r) \Rightarrow n = m \sup q *r ].
41 apply (nat_case (n \mod m)).
42 simplify.apply plus_n_O.
44 simplify.apply plus_n_O.
46 apply (nat_case1 (n1 \mod m)).intro.
48 generalize in match (H (n1 / m) m).
49 elim (p_ord_aux n (n1 / m) m).
51 rewrite > assoc_times.
52 rewrite < H3.rewrite > (plus_n_O (m*(n1 / m))).
55 rewrite < div_mod.reflexivity.
56 assumption.assumption.
57 intros.simplify.apply plus_n_O.
60 theorem p_ord_aux_to_exp: \forall p,n,m,q,r. O < m \to
61 (pair nat nat q r) = p_ord_aux p n m \to n = m \sup q * r.
64 match (pair nat nat q r) with
65 [ (pair q r) \Rightarrow n = m \sup q * r ].
67 apply p_ord_aux_to_Prop.
71 (* questo va spostato in primes1.ma *)
72 theorem p_ord_exp: \forall n,m,i. O < m \to n \mod m \neq O \to
73 \forall p. i \le p \to p_ord_aux p (m \sup i * n) m = pair nat nat i n.
80 elim (n \mod m).simplify.reflexivity.simplify.reflexivity.
83 cut (O < n \mod m \lor O = n \mod m).
84 elim Hcut.apply (lt_O_n_elim (n \mod m) H3).
85 intros. simplify.reflexivity.
87 apply H1.apply sym_eq.assumption.
88 apply le_to_or_lt_eq.apply le_O_n.
89 generalize in match H3.
90 apply (nat_case p).intro.apply False_ind.apply (not_le_Sn_O n1 H4).
92 simplify. fold simplify (m \sup (S n1)).
93 cut (((m \sup (S n1)*n) \mod m) = O).
95 simplify.fold simplify (m \sup (S n1)).
96 cut ((m \sup (S n1) *n) / m = m \sup n1 *n).
98 rewrite > (H2 m1). simplify.reflexivity.
99 apply le_S_S_to_le.assumption.
102 rewrite > assoc_times.
103 apply (lt_O_n_elim m H).
104 intro.apply div_times.
106 apply divides_to_mod_O.
108 simplify.rewrite > assoc_times.
109 apply (witness ? ? (m \sup n1 *n)).reflexivity.
112 theorem p_ord_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
113 match p_ord_aux p n m with
114 [ (pair q r) \Rightarrow r \mod m \neq O].
115 intro.elim p.absurd (O < n).assumption.
116 apply le_to_not_lt.assumption.
118 apply (nat_case1 (n1 \mod m)).intro.
119 generalize in match (H (n1 / m) m).
120 elim (p_ord_aux n (n1 / m) m).
122 apply eq_mod_O_to_lt_O_div.
123 apply (trans_lt ? (S O)).unfold lt.apply le_n.
124 assumption.assumption.assumption.
126 apply (trans_le ? n1).change with (n1 / m < n1).
127 apply lt_div_n_m_n.assumption.assumption.assumption.
131 apply (not_eq_O_S m1).
132 rewrite > H5.reflexivity.
135 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
136 pair nat nat q r = p_ord_aux p n m \to r \mod m \neq O.
139 match (pair nat nat q r) with
140 [ (pair q r) \Rightarrow r \mod m \neq O].
142 apply p_ord_aux_to_Prop1.
143 assumption.assumption.assumption.
146 theorem p_ord_exp1: \forall p,n,q,r. O < p \to \lnot p \divides r \to
147 n = p \sup q * r \to p_ord n p = pair nat nat q r.
152 |unfold.intro.apply H1.
153 apply mod_O_to_divides[assumption|assumption]
154 |apply (trans_le ? (p \sup q)).
156 elim q.simplify.apply le_n_Sn.
158 generalize in match H3.
159 apply (nat_case n1).simplify.
160 rewrite < times_n_SO.intro.assumption.
162 apply (trans_le ? (p*(S m))).
163 apply (trans_le ? ((S (S O))*(S m))).
164 simplify.rewrite > plus_n_Sm.
169 apply le_times_r.assumption.
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 (* properties of ord e ord_rem *)
435 theorem ord_times: \forall p,m,n.O<m \to O<n \to prime p \to
436 ord (m*n) p = ord m p+ord n p.
438 rewrite > (p_ord_times ? ? ? (ord m p) (ord_rem m p) (ord n p) (ord_rem n p))
443 |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
444 |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
448 theorem ord_exp: \forall p,m.S O < p \to
452 rewrite > (p_ord_exp1 p (exp p m) m (S O))
454 |apply lt_to_le.assumption
455 |intro.apply (lt_to_not_le ? ? H).
464 theorem not_divides_to_ord_O:
465 \forall p,m. prime p \to \lnot (divides p m) \to
468 rewrite > (p_ord_exp1 p m O m)
470 |apply prime_to_lt_O.assumption
472 |simplify.apply plus_n_O
476 theorem ord_O_to_not_divides:
477 \forall p,m. O < m \to prime p \to ord m p = O \to
480 lapply (p_ord_to_exp1 p m (ord m p) (ord_rem m p))
485 rewrite < times_n_SO.
487 |apply prime_to_lt_SO.assumption
489 |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
493 theorem divides_to_not_ord_O:
494 \forall p,m. O < m \to prime p \to divides p m \to
497 apply (ord_O_to_not_divides ? ? H H1 H3).
501 theorem not_ord_O_to_divides:
502 \forall p,m. O < m \to prime p \to \lnot (ord m p = O) \to
505 rewrite > (exp_ord p) in ⊢ (? ? %)
506 [apply (trans_divides ? (exp p (ord m p)))
507 [generalize in match H2.
508 cases (ord m p);intro
509 [apply False_ind.apply H3.reflexivity
514 |apply prime_to_lt_SO.
520 theorem not_divides_ord_rem: \forall m,p.O< m \to S O < p \to
521 \lnot (divides p (ord_rem m p)).
523 elim (p_ord_to_exp1 p m (ord m p) (ord_rem m p))
527 |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
531 theorem ord_ord_rem: \forall p,q,m. O < m \to
532 prime p \to prime q \to
533 q < p \to ord (ord_rem m p) q = ord m q.
535 rewrite > (exp_ord p) in ⊢ (? ? ? (? % ?))
537 [rewrite > not_divides_to_ord_O in ⊢ (? ? ? (? % ?))
541 apply (lt_to_not_eq ? ? H3).
542 apply (divides_exp_to_eq ? ? ? H2 H1 H4)
545 apply (ltn_to_ltO ? ? H3)
558 theorem lt_ord_rem: \forall n,m. prime n \to O < m \to
559 divides n m \to ord_rem m n < m.
561 elim (le_to_or_lt_eq (ord_rem m n) m)
564 apply (ord_O_to_not_divides ? ? H1 H ? H2).
566 [apply prime_to_lt_SO.assumption
567 |apply (inj_times_l1 m)
569 |rewrite > sym_times in ⊢ (? ? ? %).
570 rewrite < times_n_SO.
571 rewrite < H3 in ⊢ (? ? (? ? %) ?).
574 [apply prime_to_lt_SO.assumption
581 |apply divides_ord_rem
582 [apply prime_to_lt_SO.assumption
589 (* p_ord_inv is used to encode the pair ord and rem into
590 a single natural number. *)
592 definition p_ord_inv \def
595 [pair q r \Rightarrow r*m+q].
597 theorem eq_p_ord_inv: \forall p,m,x.
598 p_ord_inv p m x = (ord_rem x p)*m+(ord x p).
599 intros.unfold p_ord_inv. unfold ord_rem.
605 theorem div_p_ord_inv:
606 \forall p,m,x. ord x p < m \to p_ord_inv p m x / m = ord_rem x p.
607 intros.rewrite > eq_p_ord_inv.
608 apply div_plus_times.
612 theorem mod_p_ord_inv:
613 \forall p,m,x. ord x p < m \to p_ord_inv p m x \mod m = ord x p.
614 intros.rewrite > eq_p_ord_inv.
615 apply mod_plus_times.