2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_____________________________________________________________*)
12 include "arithmetics/exp.ma".
13 include "basics/types.ma".
14 include "arithmetics/primes.ma".
15 include "arithmetics/gcd.ma".
17 let rec p_ord_aux p n m ≝
22 | S p ⇒ let 〈q,r〉 ≝ p_ord_aux p (n / m) m in 〈S q,r〉]
25 (* p_ord n m = <q,r> if m divides n q times, with remainder r *)
26 definition p_ord ≝ λn,m:nat.p_ord_aux n n m.
28 lemma p_ord_aux_0: ∀n,m.p_ord_aux 0 n m = 〈0,n〉.
29 #n #m whd in match (p_ord_aux 0??); cases (n\mod m) normalize //
32 lemma p_ord_aux_Strue: ∀n,m,p,q,r.
33 n\mod m = 0 → p_ord_aux p (n / m) m = 〈q,r〉 →
34 p_ord_aux (S p) n m = 〈S q,r〉.
35 #n #m #p #q #r whd in match (p_ord_aux (S p)??); #H >H
36 #Hord whd in ⊢(??%?); >Hord //
39 lemma p_ord_aux_false: ∀p,n,m,a.
40 n\mod m = (S a) → p_ord_aux p n m = 〈0,n〉.
41 #p #n #m #a cases p whd in match (p_ord_aux ???);
42 [#H whd in match (p_ord_aux ???); >H //
43 |#p1 #H whd in match (p_ord_aux ???); >H //
47 (* the definition of p_ord_aux only makes sense for m>1.
48 In case m=1 we always end up with the pair 〈p,n〉 *)
50 lemma p_ord_degenerate: ∀p,n. p_ord_aux p n 1 = 〈p,n〉.
51 #p elim p // #p1 #Hind #n
52 cut (mod n 1 = 0) [@divides_to_mod_O //] #Hmod
53 >(p_ord_aux_Strue … (Hind … ) ) // >(div_mod n 1) in ⊢ (???%); //
56 theorem p_ord_aux_to_exp: ∀p,n,m,q,r. O < m →
57 p_ord_aux p n m = 〈q,r〉 → n = m \sup q *r .
59 [#n #m @(nat_case (n \mod m))
60 [#Hmod #q #r #posm >p_ord_aux_0 #Hqr destruct (Hqr) //
61 |#a #H #q #r #posm >(p_ord_aux_false … H) #Hqr destruct (Hqr) //
63 |#p1 #Hind #n #m @(nat_case (n \mod m))
64 [#Hmod #q #r #posm lapply (refl …(p_ord_aux p1 (n/m) m));
65 cases (p_ord_aux p1 (n/m) m) in ⊢ (???%→?); #q1 #r1 #H1
66 >(p_ord_aux_Strue … Hmod H1) #H destruct (H) whd in match (exp ??);
67 >(div_mod n m) >Hmod <plus_n_O >(Hind … H1) //
68 |#a #H #q #r #posm >(p_ord_aux_false … H) #Hqr destruct (Hqr) //
73 (* questo va spostato in primes1.ma *)
74 theorem p_ord_exp: ∀n,m,i. O < m → n \mod m ≠ O →
75 ∀p. i ≤ p → p_ord_aux p (m \sup i * n) m = 〈i,n〉.
77 cut (∃a.n\mod m = S a)
78 [@(nat_case (n\mod m)) [#H @False_ind /2/|#a #Hmod1 %{a} //]] * #mod1 #Hmod1
80 [#p normalize #posp <plus_n_O @(p_ord_aux_false … Hmod1)
82 @(nat_case p) [#Hp >Hp #Habs @False_ind @(absurd … Habs) //]
84 cut (((m \sup (S i)*n) \mod m) = O)
85 [whd in match (exp ??); @divides_to_mod_O // %{(m^i*n)} //] #Hmod2
86 @(p_ord_aux_Strue … Hmod2) <(Hind p1) [2: @le_S_S_to_le //]
87 @eq_f2 // whd in match (exp ??); >associative_times >(commutative_times m)
88 <associative_times >div_times //
92 theorem p_ord_aux_to_not_mod_O: ∀p,n,m,q,r. 1<m → O<n → n≤p →
93 p_ord_aux p n m = 〈q,r〉 → r \mod m ≠ O.
95 [#n #m #q #r #_ #posn #nposn @False_ind @(absurd … posn) /2/
96 |#p1 #Hind #n #m @(nat_case (n \mod m))
97 [#Hmod #q #r #lt1m #posn #len lapply (refl …(p_ord_aux p1 (n/m) m));
98 cases (p_ord_aux p1 (n/m) m) in ⊢ (???%→?); #q1 #r1 #H1
99 >(p_ord_aux_Strue … Hmod H1) #H destruct (H) whd in match (exp ??);
101 [@(pos_div … posn Hmod) @lt_to_le //
102 |@le_S_S_to_le @(transitive_le … len) @lt_times_to_lt_div
103 >(times_n_1 n) in ⊢ (?%?); @monotonic_lt_times_r //
105 |#a #H #q #r #lt1m #posn #posm >(p_ord_aux_false … H) #Hqr destruct (Hqr)
111 theorem p_ord_exp1: ∀p,n,q,r. O < p → p ∤ r →
112 n = p \sup q * r → p_ord n p = 〈q,r〉.
113 #p #n #q #r #posp #ndivpr #Hn >Hn -Hn -n @(p_ord_exp … posp)
114 [@(not_to_not … ndivpr) /2/
115 |@(transitive_le ? (p \sup q))
117 [cases (le_to_or_lt_eq … posp) // #eqp1 @False_ind @(absurd ?? ndivpr)
119 #lt1p elim q // -q #q whd in match (exp ??);
120 cases q [#_ normalize <plus_n_O @lt_to_le //]
121 #q1 #Hind @(lt_to_le_to_lt ? ((S q1)*2))
122 [>(times_n_1 (S q1)) in ⊢ (?%?); @monotonic_lt_times_r //
125 |>(times_n_1 (p^q)) in ⊢ (?%?); @le_times //
126 lapply ndivpr -ndivpr cases r // #Habs @False_ind @(absurd ?? Habs) % //
131 theorem p_ord_to_exp1: ∀p,n,q,r. 1<p → O<n → p_ord n p = 〈q,r〉 →
132 p ∤ r ∧ n = p \sup q * r.
133 #p #n #q #r #lt1p #posn #Hord %
134 [@(not_to_not … (p_ord_aux_to_not_mod_O … lt1p posn (le_n n)… Hord))
135 @divides_to_mod_O @lt_to_le //
136 |@(p_ord_aux_to_exp n …Hord) @lt_to_le //
140 theorem eq_p_ord_q_O: ∀p,n,q. p_ord n p = 〈q,O〉 → n=O ∧ q=O.
141 #p #n whd in match (p_ord ??); cases n
142 [#q cases p normalize [|#q1] #H destruct (H) % //
144 [normalize #H destruct (H)
146 [>p_ord_degenerate #H destruct (H)
147 |#p2 lapply (refl …(p_ord_aux (S n1) (S n1) (S (S p2))));
148 cases (p_ord_aux (S n1) (S n1) (S (S p2))) in ⊢ (???%→?); #qa #ra #H
149 lapply (p_ord_to_exp1 (S (S p2)) (S n1) … H) //
150 * #_ #H1 >H #H2 @False_ind destruct (H2) <times_n_O in H1;
151 #Habs destruct (Habs)
157 theorem p_ord_times: ∀p,a,b,qa,ra,qb,rb. prime p → O < a → O < b
158 → p_ord a p = 〈qa,ra〉 → p_ord b p = 〈qb,rb〉
159 → p_ord (a*b) p = 〈qa + qb, ra*rb〉.
160 #p #a #b #qa #ra #qb #rb #Hprime #posa #posb #porda #pordb
161 cut (1<p) [@prime_to_lt_SO //] #Hp1
162 cases (p_ord_to_exp1 ???? Hp1 posa porda) -posa -porda #Hdiva #Ha
163 elim (p_ord_to_exp1 ???? Hp1 posb pordb) -posb -pordb #Hdivb #Hb
166 |% #Hdiv cases (divides_times_to_divides ? ? ? Hprime Hdiv)
172 theorem fst_p_ord_times: ∀p,a,b. prime p → O < a → O < b →
173 fst ?? (p_ord (a*b) p) = (fst ?? (p_ord a p)) + (fst ?? (p_ord b p)).
174 #p #a #b #primep #posa #posb
175 >(p_ord_times p a b (fst ?? (p_ord a p)) (snd ?? (p_ord a p))
176 (fst ?? (p_ord b p)) (snd ? ? (p_ord b p)) primep posa posb) //
179 theorem p_ord_p: ∀p:nat. 1 < p → p_ord p p = 〈1,1〉.
182 |% #divp1 @(absurd … ltp1) @le_to_not_lt @divides_to_le //
187 (* p_ord and divides *)
188 theorem divides_to_p_ord: ∀p,a,b,c,d,n,m:nat. O < n → O < m → prime p
189 → divides n m → p_ord n p = 〈a,b〉 →
190 p_ord m p = 〈c,d〉 → divides b d ∧ a ≤ c.
191 #p #a #b #c #d #n #m #posn #posm #primep #divnm #ordn #ordm
192 cut (1<p) [@prime_to_lt_SO //] #Hposp
193 cases (p_ord_to_exp1 ? ? ? ? Hposp posn ordn) #divn #eqn
194 cases (p_ord_to_exp1 ? ? ? ? Hposp posm ordm) #divm #eqm %
195 [@(gcd_1_to_divides_times_to_divides b (exp p c))
196 [cases (le_to_or_lt_eq ?? (le_O_n b)) //
199 |#c0 #Hind @eq_gcd_times_1
200 [@lt_O_exp @lt_to_le //
203 |>commutative_gcd @prime_to_gcd_1 //
206 |@(transitive_divides ? n) [%{(exp p a)} // |<eqm //]
208 |@(le_exp_to_le p) //
210 [@lt_O_exp @lt_to_le //
211 |@(gcd_1_to_divides_times_to_divides ? d)
212 [@lt_O_exp @lt_to_le //
215 |#a0 #Hind whd in match (exp ??);
216 >commutative_gcd @eq_gcd_times_1
217 [@lt_O_exp @lt_to_le //
220 |>commutative_gcd @prime_to_gcd_1 //
223 |@(transitive_divides ? n) // %{b} //
229 (* p_ord and primes *)
230 theorem not_divides_to_p_ord_O: ∀n,i.
231 (nth_prime i) ∤ n → p_ord n (nth_prime i) = 〈O,n〉.
232 #n #i #H @p_ord_exp1 //
235 theorem p_ord_O_to_not_divides: ∀n,i,r. O < n →
236 p_ord n (nth_prime i) = 〈O,r〉
239 lapply (p_ord_to_exp1 … Hord) // * #H
240 normalize <plus_n_O //
243 theorem p_ord_to_not_eq_O : ∀n,p,q,r. 1<n →
244 p_ord n (nth_prime p) = 〈q,r〉 → r≠O.
245 #n #p #q #r #lt1n #Hord
246 cut (O<n) [@lt_to_le //] #posn
247 lapply (p_ord_to_exp1 …posn … Hord)
249 |* #H1 #H2 @(not_to_not …(lt_to_not_eq … posn))
254 definition ord :nat → nat → nat ≝
255 λn,p. fst ?? (p_ord n p).
257 definition ord_rem :nat → nat → nat ≝
258 λn,p. snd ?? (p_ord n p).
260 lemma ord_eq: ∀n,p. ord n p = fst ?? (p_ord n p). //
263 lemma ord_rem_eq: ∀n,p. ord_rem n p = snd ?? (p_ord n p). //
266 theorem divides_to_ord: ∀p,n,m:nat.
267 O < n → O < m → prime p → divides n m
268 → divides (ord_rem n p) (ord_rem m p) ∧ (ord n p) ≤ (ord m p).
269 #p #n #m #H #H1 #H2 #H3
270 @(divides_to_p_ord p ? ? ? ? n m H H1 H2 H3)
271 [@eq_pair_fst_snd|@eq_pair_fst_snd]
274 theorem divides_to_divides_ord_rem: ∀p,n,m:nat.
275 O < n → O < m → prime p → divides n m →
276 divides (ord_rem n p) (ord_rem m p).
277 #p #n #m #H #H1 #H2 #H3 cases (divides_to_ord p n m H H1 H2 H3) //
280 theorem divides_to_le_ord: ∀p,n,m:nat.
281 O < n → O < m → prime p → divides n m →
283 #p #n #m #H #H1 #H2 #H3 cases (divides_to_ord p n m H H1 H2 H3) //
286 theorem exp_ord: \forall p,n. 1 < p → O < n →
287 n = p \sup (ord n p) * (ord_rem n p).
289 cases (p_ord_to_exp1 p n (ord n p) (ord_rem n p) H H1 ?)
290 [// |@eq_pair_fst_snd]
293 theorem divides_ord_rem: ∀p,n. 1 < p → O < n
294 → divides (ord_rem n p) n.
295 #p #n #H #H1 %{(p \sup (ord n p))} >commutative_times @exp_ord //
298 theorem lt_O_ord_rem: ∀p,n. 1 < p → O < n → O < ord_rem n p.
300 cases (le_to_or_lt_eq … (le_O_n (ord_rem n p))) //
301 #remO lapply(divides_ord_rem ?? H H1) <remO -remO #Hdiv0
302 @False_ind @(absurd (0=n)) [cases Hdiv0 // | @lt_to_not_eq //]
305 (* properties of ord e ord_rem *)
307 theorem ord_times: ∀p,m,n.O<m → O<n → prime p →
308 ord (m*n) p = ord m p+ord n p.
310 lapply (p_ord_times ??? (ord m p) (ord_rem m p) (ord n p) (ord_rem n p) H2 H H1
311 (eq_pair_fst_snd …) (eq_pair_fst_snd …)) #H3
312 @(eq_f … (fst …) … H3)
315 theorem ord_exp: ∀p,m. 1 < p → ord (exp p m) p = m.
316 #p #m #H >ord_eq >(p_ord_exp1 p (exp p m) m (S O)) //
317 [@(not_to_not … (lt_to_not_le … H)) @divides_to_le //
322 theorem not_divides_to_ord_O:
323 ∀p,m. prime p → p ∤ m → ord m p = O.
324 #p #m #H #H1 >ord_eq >(p_ord_exp1 p m O m) // @prime_to_lt_O //
327 theorem ord_O_to_not_divides: ∀p,m. O < m → prime p →
330 lapply (p_ord_to_exp1 p m (ord m p) (ord_rem m p) … H … (eq_pair_fst_snd …))
332 |* #H3 >H2 >commutative_times <times_n_1 //
336 theorem divides_to_not_ord_O:
337 ∀p,m. O < m → prime p → divides p m →
339 #p #m #H #H1 #H2 % #H3 @(absurd … H2) @(ord_O_to_not_divides ? ? H H1 H3)
342 theorem not_ord_O_to_divides:
343 ∀p,m. O < m → prime p → (ord m p ≠ O) → divides p m.
344 #p #m #H #H1 #H2 >(exp_ord p m) in ⊢ (??%);
345 [@(transitive_divides ? (exp p (ord m p)))
346 [lapply H2 cases (ord m p)
347 [* #H3 @False_ind @H3 //
348 |#a #_ normalize % //
357 theorem not_divides_ord_rem: ∀m,p.O< m → 1 < p →
360 lapply (p_ord_to_exp1 p m (ord m p) (ord_rem m p) ?? (eq_pair_fst_snd …)) // *
364 theorem ord_ord_rem: ∀p,q,m. O < m → prime p → prime q →q < p →
365 ord (ord_rem m p) q = ord m q.
366 #p #q #m #H #H1 #H2 #H3 >(exp_ord p m) in ⊢ (???(?%?));
368 [>not_divides_to_ord_O in ⊢ (???(?%?)); //
369 @(not_to_not … (lt_to_not_eq ? ? H3))
370 @(divides_exp_to_eq ? ? ? H2 H1)
371 |@lt_O_ord_rem // @prime_to_lt_SO //
372 |@lt_O_exp @prime_to_lt_O //
379 theorem lt_ord_rem: ∀n,m. prime n → O < m →
380 divides n m → ord_rem m n < m.
382 cases (le_to_or_lt_eq (ord_rem m n) m ?)
384 |#Hm @False_ind <Hm in H2; #Habs @(absurd ? Habs)
385 @not_divides_ord_rem // @prime_to_lt_SO //
387 @divides_ord_rem // @prime_to_lt_SO //
391 (* p_ord_inv may be used to encode the pair ord and rem into
392 a single natural number. *)
394 definition p_ord_inv ≝ λp,m,x.
395 let 〈q,r〉 ≝ p_ord x p in r*m+q.
397 theorem eq_p_ord_inv: ∀p,m,x.
398 p_ord_inv p m x = (ord_rem x p)*m+(ord x p).
399 #p #m #x normalize cases(p_ord_aux x x p) //
402 theorem div_p_ord_inv:
403 ∀p,m,x. ord x p < m → p_ord_inv p m x / m = ord_rem x p.
404 #p #m #x >eq_p_ord_inv @div_plus_times
407 theorem mod_p_ord_inv:
408 ∀p,m,x. ord x p < m → p_ord_inv p m x \mod m = ord x p.
409 #p #m #x >eq_p_ord_inv @mod_plus_times