]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library_auto/auto/nat/ord.ma
added library_auto/ to tests.
[helm.git] / helm / software / matita / library_auto / auto / nat / ord.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 (*       \ /        Matita is distributed under the terms of the          *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/library_auto/nat/ord".
16
17 include "datatypes/constructors.ma".
18 include "auto/nat/exp.ma".
19 include "auto/nat/gcd.ma".
20 include "auto/nat/relevant_equations.ma". (* required by auto paramod *)
21
22 (* this definition of log is based on pairs, with a remainder *)
23
24 let rec p_ord_aux p n m \def
25   match n \mod m with
26   [ O \Rightarrow 
27     match p with
28       [ O \Rightarrow pair nat nat O n
29       | (S p) \Rightarrow 
30        match (p_ord_aux p (n / m) m) with
31        [ (pair q r) \Rightarrow pair nat nat (S q) r] ]
32   | (S a) \Rightarrow pair nat nat O n].
33   
34 (* p_ord n m = <q,r> if m divides n q times, with remainder r *)
35 definition p_ord \def \lambda n,m:nat.p_ord_aux n n m.
36
37 theorem p_ord_aux_to_Prop: \forall p,n,m. O < m \to
38   match p_ord_aux p n m with
39   [ (pair q r) \Rightarrow n = m \sup q *r ].
40 intro.
41 elim p
42 [ simplify.
43   apply (nat_case (n \mod m))
44   [ simplify.
45     apply plus_n_O
46   | intros.
47     simplify.
48     apply plus_n_O
49   ]
50 | simplify. 
51   apply (nat_case1 (n1 \mod m))
52   [ intro.
53     simplify.
54     generalize in match (H (n1 / m) m).
55     elim (p_ord_aux n (n1 / m) m).
56     simplify.
57     rewrite > assoc_times.
58     rewrite < H3
59     [ rewrite > (plus_n_O (m*(n1 / m))).
60       rewrite < H2.
61       rewrite > sym_times.
62       auto
63       (*rewrite < div_mod
64       [ reflexivity
65       | assumption
66       ]*)
67     | assumption
68     ]
69   | intros.
70     simplify.
71     apply plus_n_O
72   ]
73 ]
74 qed.
75
76 theorem p_ord_aux_to_exp: \forall p,n,m,q,r. O < m \to
77   (pair nat nat q r) = p_ord_aux p n m \to n = m \sup q * r.
78 intros.
79 change with 
80 match (pair nat nat q r) with
81   [ (pair q r) \Rightarrow n = m \sup q * r ].
82 rewrite > H1.
83 apply p_ord_aux_to_Prop.
84 assumption.
85 qed.
86
87 (* questo va spostato in primes1.ma *)
88 theorem p_ord_exp: \forall n,m,i. O < m \to n \mod m \neq O \to
89 \forall p. i \le p \to p_ord_aux p (m \sup i * n) m = pair nat nat i n.
90 intros 5.
91 elim i
92 [ simplify.
93   rewrite < plus_n_O.
94   apply (nat_case p)
95   [ simplify.
96     elim (n \mod m);auto
97     (*[ simplify.
98       reflexivity
99     | simplify.
100       reflexivity
101     ]*)
102   | intro.
103     simplify.
104     cut (O < n \mod m \lor O = n \mod m)
105     [ elim Hcut
106       [ apply (lt_O_n_elim (n \mod m) H3).
107         intros.auto
108         (*simplify.
109         reflexivity*)
110       | apply False_ind.auto
111         (*apply H1.
112         apply sym_eq.
113         assumption*)
114       ]
115     | auto
116       (*apply le_to_or_lt_eq.
117       apply le_O_n*)
118     ]  
119   ]
120 | generalize in match H3.
121   apply (nat_case p)
122   [ intro.
123     apply False_ind.
124     apply (not_le_Sn_O n1 H4)
125   | intros.
126     simplify.
127     fold simplify (m \sup (S n1)).
128     cut (((m \sup (S n1)*n) \mod m) = O)
129     [ rewrite > Hcut.
130       simplify.
131       fold simplify (m \sup (S n1)). 
132       cut ((m \sup (S n1) *n) / m = m \sup n1 *n)
133       [ rewrite > Hcut1.
134         rewrite > (H2 m1);auto
135         (*[ simplify.
136           reflexivity
137         | apply le_S_S_to_le.
138           assumption
139         ]*)
140       | (* div_exp *)
141         simplify.
142         rewrite > assoc_times.
143         apply (lt_O_n_elim m H).
144         intro.
145         apply div_times
146       ]
147     | (* mod_exp = O *)
148       apply divides_to_mod_O
149       [ assumption
150       | simplify.auto
151         (*rewrite > assoc_times.
152         apply (witness ? ? (m \sup n1 *n)).
153         reflexivity*)
154       ]
155     ]
156   ]
157 ]
158 qed.
159
160 theorem p_ord_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
161   match p_ord_aux p n m with
162   [ (pair q r) \Rightarrow r \mod m \neq O].
163 intro.
164 elim p
165 [ absurd (O < n);auto
166   (*[ assumption
167   | apply le_to_not_lt.
168     assumption
169   ]*)
170 | simplify.
171   apply (nat_case1 (n1 \mod m))
172   [ intro.
173     generalize in match (H (n1 / m) m).
174     elim (p_ord_aux n (n1 / m) m).
175     apply H5
176     [ assumption
177     | auto
178       (*apply eq_mod_O_to_lt_O_div
179       [ apply (trans_lt ? (S O))
180         [ unfold lt.
181           apply le_n
182         | assumption
183         ]
184       | assumption
185       | assumption
186       ]*)
187     | apply le_S_S_to_le.auto
188       (*apply (trans_le ? n1)
189       [ change with (n1 / m < n1).
190         apply lt_div_n_m_n;assumption        
191       | assumption
192       ]*)
193     ]
194   | intros.
195     simplify.auto
196     (*rewrite > H4.    
197     unfold Not.
198     intro.
199     apply (not_eq_O_S m1).
200     rewrite > H5.
201     reflexivity.*)
202   ]
203 ]
204 qed.
205
206 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
207  pair nat nat q r = p_ord_aux p n m \to r \mod m \neq O.
208 intros.
209 change with 
210   match (pair nat nat q r) with
211   [ (pair q r) \Rightarrow r \mod m \neq O].
212 rewrite > H3. 
213 apply p_ord_aux_to_Prop1;
214   assumption.
215 qed.
216
217 theorem p_ord_exp1: \forall p,n,q,r. O < p \to \lnot p \divides r \to
218 n = p \sup q * r \to p_ord n p = pair nat nat q r.
219 intros.
220 unfold p_ord.
221 rewrite > H2.
222 apply p_ord_exp
223 [ assumption
224 | unfold.
225   intro.
226   auto
227   (*apply H1.
228   apply mod_O_to_divides
229   [ assumption
230   | assumption
231   ]*)
232 | apply (trans_le ? (p \sup q))
233   [ cut ((S O) \lt p)
234     [ auto
235       (*elim q
236       [ simplify.
237         apply le_n_Sn
238       | simplify.
239         generalize in match H3.
240         apply (nat_case n1)
241         [ simplify.
242           rewrite < times_n_SO.
243           intro.
244           assumption
245         | intros.
246           apply (trans_le ? (p*(S m)))
247           [ apply (trans_le ? ((S (S O))*(S m)))
248             [ simplify.
249               rewrite > plus_n_Sm.
250               rewrite < plus_n_O.
251               apply le_plus_n
252             | apply le_times_l.
253               assumption
254             ]
255           | apply le_times_r.
256             assumption
257           ]
258         ]
259       ]*)
260     | alias id "not_eq_to_le_to_lt" = "cic:/matita/algebra/finite_groups/not_eq_to_le_to_lt.con".
261       apply not_eq_to_le_to_lt
262       [ unfold.
263         intro.
264         auto
265         (*apply H1.
266         rewrite < H3.
267         apply (witness ? r r ?).
268         simplify.
269         apply plus_n_O*)
270       | assumption
271       ]
272     ]
273   | rewrite > times_n_SO in \vdash (? % ?).
274     apply le_times_r.
275     change with (O \lt r).
276     apply not_eq_to_le_to_lt
277     [ unfold.
278       intro.auto
279       (*apply H1.rewrite < H3.
280       apply (witness ? ? O ?).rewrite < times_n_O.
281       reflexivity*)
282     | apply le_O_n
283     ]
284   ]
285 ]
286 qed.
287
288 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 
289 \lnot p \divides r \land n = p \sup q * r.
290 intros.
291 unfold p_ord in H2.
292 split
293 [ unfold.intro.
294   apply (p_ord_aux_to_not_mod_O n n p q r);auto
295   (*[ assumption
296   | assumption
297   | apply le_n
298   | symmetry.
299     assumption
300   | apply divides_to_mod_O
301     [ apply (trans_lt ? (S O))
302       [ unfold.
303         apply le_n
304       | assumption         
305       ]
306     | assumption
307     ]
308   ]*)
309 | apply (p_ord_aux_to_exp n);auto
310   (*[ apply (trans_lt ? (S O))
311     [ unfold.
312       apply le_n
313     | assumption
314     ]
315   | symmetry.
316     assumption
317   ]*)
318 ]
319 qed.
320
321 theorem p_ord_times: \forall p,a,b,qa,ra,qb,rb. prime p 
322 \to O \lt a \to O \lt b 
323 \to p_ord a p = pair nat nat qa ra  
324 \to p_ord b p = pair nat nat qb rb
325 \to p_ord (a*b) p = pair nat nat (qa + qb) (ra*rb).
326 intros.
327 cut ((S O) \lt p)
328 [ elim (p_ord_to_exp1 ? ? ? ? Hcut H1 H3).
329   elim (p_ord_to_exp1 ? ? ? ? Hcut H2 H4).
330   apply p_ord_exp1
331   [ auto
332     (*apply (trans_lt ? (S O))
333     [ unfold.
334       apply le_n
335     | assumption
336     ]*)
337   | unfold.
338     intro.
339     elim (divides_times_to_divides ? ? ? H H9);auto
340     (*[ apply (absurd ? ? H10 H5)
341     | apply (absurd ? ? H10 H7)
342     ]*)
343   | (* rewrite > H6.
344     rewrite > H8. *)
345     auto paramodulation
346   ]
347 | unfold prime in H. 
348   elim H. 
349   assumption
350 ]
351 qed.
352
353 theorem fst_p_ord_times: \forall p,a,b. prime p 
354 \to O \lt a \to O \lt b 
355 \to fst ? ? (p_ord (a*b) p) = (fst ? ? (p_ord a p)) + (fst ? ? (p_ord b p)).
356 intros.
357 rewrite > (p_ord_times p a b (fst ? ? (p_ord a p)) (snd ? ? (p_ord a p))
358 (fst ? ? (p_ord b p)) (snd ? ? (p_ord b p)) H H1 H2);auto.
359 (*[ simplify.
360   reflexivity
361 | apply eq_pair_fst_snd
362 | apply eq_pair_fst_snd
363 ]*)
364 qed.
365
366 theorem p_ord_p : \forall p:nat. (S O) \lt p \to p_ord p p = pair ? ? (S O) (S O).
367 intros.
368 apply p_ord_exp1
369 [ auto
370   (*apply (trans_lt ? (S O))
371   [ unfold.
372     apply le_n
373   | assumption
374   ]*)
375 | unfold.
376   intro.
377   apply (absurd ? ? H).auto
378   (*apply le_to_not_lt.
379   apply divides_to_le
380   [ unfold.
381     apply le_n
382   | assumption
383   ]*)
384 | auto
385   (*rewrite < times_n_SO.
386   apply exp_n_SO*)
387 ]
388 qed.