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".
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 theorem divides_to_p_ord: \forall p,a,b,c,d,n,m:nat.
244 O < n \to O < m \to prime p
245 \to divides n m \to p_ord n p = pair ? ? a b \to
246 p_ord m p = pair ? ? c d \to divides b d \land a \le c.
249 [lapply (p_ord_to_exp1 ? ? ? ? Hcut H H4).
250 lapply (p_ord_to_exp1 ? ? ? ? Hcut H1 H5).
251 elim Hletin. clear Hletin.
252 elim Hletin1. clear Hletin1.
255 [apply (gcd_SO_to_divides_times_to_divides (exp p c))
256 [elim (le_to_or_lt_eq ? ? (le_O_n b))
259 apply (lt_to_not_eq O ? H).
268 apply eq_gcd_times_SO
269 [apply lt_to_le.assumption
270 |apply lt_O_exp.apply lt_to_le.assumption
272 (* hint non trova prime_to_gcd_SO e
273 autobatch non chiude il goal *)
274 apply prime_to_gcd_SO
275 [assumption|assumption]
279 |apply (trans_divides ? n)
280 [apply (witness ? ? (exp p a)).
286 |apply (le_exp_to_le p)
289 [apply lt_O_exp.apply lt_to_le.assumption
290 |apply (gcd_SO_to_divides_times_to_divides d)
291 [apply lt_O_exp.apply lt_to_le.assumption
294 |simplify.rewrite < sym_gcd.
295 apply eq_gcd_times_SO
296 [apply lt_to_le.assumption
297 |apply lt_O_exp.apply lt_to_le.assumption
299 (* hint non trova prime_to_gcd_SO e
300 autobatch non chiude il goal *)
301 apply prime_to_gcd_SO
302 [assumption|assumption]
303 |rewrite > sym_gcd. assumption
306 |apply (trans_divides ? n)
307 [apply (witness ? ? b).assumption
308 |rewrite > sym_times.assumption
318 definition ord :nat \to nat \to nat \def
319 \lambda n,p. fst ? ? (p_ord n p).
321 definition ord_rem :nat \to nat \to nat \def
322 \lambda n,p. snd ? ? (p_ord n p).
324 theorem divides_to_ord: \forall p,n,m:nat.
325 O < n \to O < m \to prime p
327 \to divides (ord_rem n p) (ord_rem m p) \land (ord n p) \le (ord m p).
329 apply (divides_to_p_ord p ? ? ? ? n m H H1 H2 H3)
330 [unfold ord.unfold ord_rem.apply eq_pair_fst_snd
331 |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
335 theorem divides_to_divides_ord_rem: \forall p,n,m:nat.
336 O < n \to O < m \to prime p \to divides n m \to
337 divides (ord_rem n p) (ord_rem m p).
339 elim (divides_to_ord p n m H H1 H2 H3).assumption.
342 theorem divides_to_le_ord: \forall p,n,m:nat.
343 O < n \to O < m \to prime p \to divides n m \to
344 (ord n p) \le (ord m p).
346 elim (divides_to_ord p n m H H1 H2 H3).assumption.
349 theorem exp_ord: \forall p,n. (S O) \lt p
350 \to O \lt n \to n = p \sup (ord n p) * (ord_rem n p).
352 elim (p_ord_to_exp1 p n (ord n p) (ord_rem n p))
356 |unfold ord.unfold ord_rem.
357 apply eq_pair_fst_snd
361 theorem divides_ord_rem: \forall p,n. (S O) < p \to O < n
362 \to divides (ord_rem n p) n.
364 apply (witness ? ? (p \sup (ord n p))).
366 apply exp_ord[assumption|assumption]
369 theorem lt_O_ord_rem: \forall p,n. (S O) < p \to O < n \to O < ord_rem n p.
371 elim (le_to_or_lt_eq O (ord_rem n p))
374 apply (lt_to_not_eq ? ? H1).
375 lapply (divides_ord_rem ? ? H H1).
376 rewrite < H2 in Hletin.
384 (* p_ord_inv is the inverse of ord *)
385 definition p_ord_inv \def
388 [pair q r \Rightarrow r*m+q].
390 theorem eq_p_ord_inv: \forall p,m,x.
391 p_ord_inv p m x = (ord_rem x p)*m+(ord x p).
392 intros.unfold p_ord_inv. unfold ord_rem.
398 theorem div_p_ord_inv:
399 \forall p,m,x. ord x p < m \to p_ord_inv p m x / m = ord_rem x p.
400 intros.rewrite > eq_p_ord_inv.
401 apply div_plus_times.
405 theorem mod_p_ord_inv:
406 \forall p,m,x. ord x p < m \to p_ord_inv p m x \mod m = ord x p.
407 intros.rewrite > eq_p_ord_inv.
408 apply mod_plus_times.