]> matita.cs.unibo.it Git - helm.git/blob - matita/library/nat/ord.ma
removed a pointless call to auto
[helm.git] / matita / library / 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/nat/ord".
16
17 include "datatypes/constructors.ma".
18 include "nat/exp.ma".
19 include "nat/gcd.ma".
20
21 (* this definition of log is based on pairs, with a remainder *)
22
23 let rec p_ord_aux p n m \def
24   match n \mod m with
25   [ O \Rightarrow 
26     match p with
27       [ O \Rightarrow pair nat nat O n
28       | (S p) \Rightarrow 
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].
32   
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.
35
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 ].
39 intro.
40 elim p.simplify.
41 apply (nat_case (n \mod m)).
42 simplify.apply plus_n_O.
43 intros.
44 simplify.apply plus_n_O.
45 simplify. 
46 apply (nat_case1 (n1 \mod m)).intro.
47 simplify.
48 generalize in match (H (n1 / m) m).
49 elim (p_ord_aux n (n1 / m) m).
50 simplify.
51 rewrite > assoc_times.
52 rewrite < H3.rewrite > (plus_n_O (m*(n1 / m))).
53 rewrite < H2.
54 rewrite > sym_times.
55 rewrite < div_mod.reflexivity.
56 assumption.assumption.
57 intros.simplify.apply plus_n_O. 
58 qed.
59
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.
62 intros.
63 change with 
64 match (pair nat nat q r) with
65   [ (pair q r) \Rightarrow n = m \sup q * r ].
66 rewrite > H1.
67 apply p_ord_aux_to_Prop.
68 assumption.
69 qed.
70
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.
74 intros 5.
75 elim i.
76 simplify.
77 rewrite < plus_n_O.
78 apply (nat_case p).
79 simplify.
80 elim (n \mod m).simplify.reflexivity.simplify.reflexivity.
81 intro.
82 simplify.
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.
86 apply False_ind.
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).
91 intros.
92 simplify. fold simplify (m \sup (S n1)).
93 cut (((m \sup (S n1)*n) \mod m) = O).
94 rewrite > Hcut.
95 simplify.fold simplify (m \sup (S n1)).
96 cut ((m \sup (S n1) *n) / m = m \sup n1 *n).
97 rewrite > Hcut1.
98 rewrite > (H2 m1). simplify.reflexivity.
99 apply le_S_S_to_le.assumption.
100 (* div_exp *)
101 simplify.
102 rewrite > assoc_times.
103 apply (lt_O_n_elim m H).
104 intro.apply div_times.
105 (* mod_exp = O *)
106 apply divides_to_mod_O.
107 assumption.
108 simplify.rewrite > assoc_times.
109 apply (witness ? ? (m \sup n1 *n)).reflexivity.
110 qed.
111
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.
117 simplify.
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).
121 apply H5.assumption.
122 apply eq_mod_O_to_lt_O_div.
123 apply (trans_lt ? (S O)).unfold lt.apply le_n.
124 assumption.assumption.assumption.
125 apply le_S_S_to_le.
126 apply (trans_le ? n1).change with (n1 / m < n1).
127 apply lt_div_n_m_n.assumption.assumption.assumption.
128 intros.simplify.
129 rewrite > H4.
130 unfold Not.intro.
131 apply (not_eq_O_S m1).
132 rewrite > H5.reflexivity.
133 qed.
134
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.
137 intros.
138 change with 
139   match (pair nat nat q r) with
140   [ (pair q r) \Rightarrow r \mod m \neq O].
141 rewrite > H3. 
142 apply p_ord_aux_to_Prop1.
143 assumption.assumption.assumption.
144 qed.
145
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.
148 intros.unfold p_ord.
149 rewrite > H2.
150 apply p_ord_exp
151  [assumption
152  |unfold.intro.apply H1.
153   apply mod_O_to_divides[assumption|assumption]
154  |apply (trans_le ? (p \sup q)).
155   cut ((S O) \lt p).
156   elim q.simplify.apply le_n_Sn.
157   simplify.
158   generalize in match H3.
159   apply (nat_case n1).simplify.
160   rewrite < times_n_SO.intro.assumption.
161   intros.
162   apply (trans_le ? (p*(S m))).
163   apply (trans_le ? ((S (S O))*(S m))).
164   simplify.rewrite > plus_n_Sm.
165   rewrite < plus_n_O.
166   apply le_plus_n.
167   apply le_times_l.
168   assumption.
169   apply le_times_r.assumption.
170   alias id "not_eq_to_le_to_lt" = "cic:/matita/algebra/finite_groups/not_eq_to_le_to_lt.con".
171 apply not_eq_to_le_to_lt.
172   unfold.intro.apply H1.
173   rewrite < H3.
174   apply (witness ? r r ?).simplify.apply plus_n_O.
175   assumption.
176   rewrite > times_n_SO in \vdash (? % ?).
177   apply le_times_r.
178   change with (O \lt r).
179   apply not_eq_to_le_to_lt.
180   unfold.intro.
181   apply H1.rewrite < H3.
182   apply (witness ? ? O ?).rewrite < times_n_O.reflexivity.
183   apply le_O_n.
184   ]
185 qed.
186
187 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 
188 \lnot p \divides r \land n = p \sup q * r.
189 intros.
190 unfold p_ord in H2.
191 split.unfold.intro.
192 apply (p_ord_aux_to_not_mod_O n n p q r).assumption.assumption.
193 apply le_n.symmetry.assumption.
194 apply divides_to_mod_O.apply (trans_lt ? (S O)).
195 unfold.apply le_n.assumption.assumption.
196 apply (p_ord_aux_to_exp n).apply (trans_lt ? (S O)).
197 unfold.apply le_n.assumption.symmetry.assumption.
198 qed.
199
200 theorem p_ord_times: \forall p,a,b,qa,ra,qb,rb. prime p 
201 \to O \lt a \to O \lt b 
202 \to p_ord a p = pair nat nat qa ra  
203 \to p_ord b p = pair nat nat qb rb
204 \to p_ord (a*b) p = pair nat nat (qa + qb) (ra*rb).
205 intros.
206 cut ((S O) \lt p).
207 elim (p_ord_to_exp1 ? ? ? ? Hcut H1 H3).
208 elim (p_ord_to_exp1 ? ? ? ? Hcut H2 H4).
209 apply p_ord_exp1.
210 apply (trans_lt ? (S O)).unfold.apply le_n.assumption.
211 unfold.intro.
212 elim (divides_times_to_divides ? ? ? H H9).
213 apply (absurd ? ? H10 H5).
214 apply (absurd ? ? H10 H7).
215 rewrite > H6.
216 rewrite > H8.
217 auto paramodulation.
218 unfold prime in H. elim H. assumption.
219 qed.
220
221 theorem fst_p_ord_times: \forall p,a,b. prime p 
222 \to O \lt a \to O \lt b 
223 \to fst ? ? (p_ord (a*b) p) = (fst ? ? (p_ord a p)) + (fst ? ? (p_ord b p)).
224 intros.
225 rewrite > (p_ord_times p a b (fst ? ? (p_ord a p)) (snd ? ? (p_ord a p))
226 (fst ? ? (p_ord b p)) (snd ? ? (p_ord b p)) H H1 H2).
227 simplify.reflexivity.
228 apply eq_pair_fst_snd.
229 apply eq_pair_fst_snd.
230 qed.
231
232 theorem p_ord_p : \forall p:nat. (S O) \lt p \to p_ord p p = pair ? ? (S O) (S O).
233 intros.
234 apply p_ord_exp1.
235 apply (trans_lt ? (S O)). unfold.apply le_n.assumption.
236 unfold.intro.
237 apply (absurd ? ? H).
238 apply le_to_not_lt.
239 apply divides_to_le.unfold.apply le_n.assumption.
240 rewrite < times_n_SO.
241 apply exp_n_SO.
242 qed.