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 auto paramod *)
22 (* this definition of log is based on pairs, with a remainder *)
24 let rec p_ord_aux p n m \def
28 [ O \Rightarrow pair nat nat O n
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].
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.
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 ].
42 apply (nat_case (n \mod m)).
43 simplify.apply plus_n_O.
45 simplify.apply plus_n_O.
47 apply (nat_case1 (n1 \mod m)).intro.
49 generalize in match (H (n1 / m) m).
50 elim (p_ord_aux n (n1 / m) m).
52 rewrite > assoc_times.
53 rewrite < H3.rewrite > (plus_n_O (m*(n1 / m))).
56 rewrite < div_mod.reflexivity.
57 assumption.assumption.
58 intros.simplify.apply plus_n_O.
61 theorem p_ord_aux_to_exp: \forall p,n,m,q,r. O < m \to
62 (pair nat nat q r) = p_ord_aux p n m \to n = m \sup q * r.
65 match (pair nat nat q r) with
66 [ (pair q r) \Rightarrow n = m \sup q * r ].
68 apply p_ord_aux_to_Prop.
72 (* questo va spostato in primes1.ma *)
73 theorem p_ord_exp: \forall n,m,i. O < m \to n \mod m \neq O \to
74 \forall p. i \le p \to p_ord_aux p (m \sup i * n) m = pair nat nat i n.
81 elim (n \mod m).simplify.reflexivity.simplify.reflexivity.
84 cut (O < n \mod m \lor O = n \mod m).
85 elim Hcut.apply (lt_O_n_elim (n \mod m) H3).
86 intros. simplify.reflexivity.
88 apply H1.apply sym_eq.assumption.
89 apply le_to_or_lt_eq.apply le_O_n.
90 generalize in match H3.
91 apply (nat_case p).intro.apply False_ind.apply (not_le_Sn_O n1 H4).
93 simplify. fold simplify (m \sup (S n1)).
94 cut (((m \sup (S n1)*n) \mod m) = O).
96 simplify.fold simplify (m \sup (S n1)).
97 cut ((m \sup (S n1) *n) / m = m \sup n1 *n).
99 rewrite > (H2 m1). simplify.reflexivity.
100 apply le_S_S_to_le.assumption.
103 rewrite > assoc_times.
104 apply (lt_O_n_elim m H).
105 intro.apply div_times.
107 apply divides_to_mod_O.
109 simplify.rewrite > assoc_times.
110 apply (witness ? ? (m \sup n1 *n)).reflexivity.
113 theorem p_ord_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
114 match p_ord_aux p n m with
115 [ (pair q r) \Rightarrow r \mod m \neq O].
116 intro.elim p.absurd (O < n).assumption.
117 apply le_to_not_lt.assumption.
119 apply (nat_case1 (n1 \mod m)).intro.
120 generalize in match (H (n1 / m) m).
121 elim (p_ord_aux n (n1 / m) m).
123 apply eq_mod_O_to_lt_O_div.
124 apply (trans_lt ? (S O)).unfold lt.apply le_n.
125 assumption.assumption.assumption.
127 apply (trans_le ? n1).change with (n1 / m < n1).
128 apply lt_div_n_m_n.assumption.assumption.assumption.
132 apply (not_eq_O_S m1).
133 rewrite > H5.reflexivity.
136 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
137 pair nat nat q r = p_ord_aux p n m \to r \mod m \neq O.
140 match (pair nat nat q r) with
141 [ (pair q r) \Rightarrow r \mod m \neq O].
143 apply p_ord_aux_to_Prop1.
144 assumption.assumption.assumption.
147 theorem p_ord_exp1: \forall p,n,q,r. O < p \to \lnot p \divides r \to
148 n = p \sup q * r \to p_ord n p = pair nat nat q r.
153 |unfold.intro.apply H1.
154 apply mod_O_to_divides[assumption|assumption]
155 |apply (trans_le ? (p \sup q)).
157 elim q.simplify.apply le_n_Sn.
159 generalize in match H3.
160 apply (nat_case n1).simplify.
161 rewrite < times_n_SO.intro.assumption.
163 apply (trans_le ? (p*(S m))).
164 apply (trans_le ? ((S (S O))*(S m))).
165 simplify.rewrite > plus_n_Sm.
170 apply le_times_r.assumption.
171 alias id "not_eq_to_le_to_lt" = "cic:/matita/algebra/finite_groups/not_eq_to_le_to_lt.con".
172 apply not_eq_to_le_to_lt.
173 unfold.intro.apply H1.
175 apply (witness ? r r ?).simplify.apply plus_n_O.
177 rewrite > times_n_SO in \vdash (? % ?).
179 change with (O \lt r).
180 apply not_eq_to_le_to_lt.
182 apply H1.rewrite < H3.
183 apply (witness ? ? O ?).rewrite < times_n_O.reflexivity.
188 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
189 \lnot p \divides r \land n = p \sup q * r.
193 apply (p_ord_aux_to_not_mod_O n n p q r).assumption.assumption.
194 apply le_n.symmetry.assumption.
195 apply divides_to_mod_O.apply (trans_lt ? (S O)).
196 unfold.apply le_n.assumption.assumption.
197 apply (p_ord_aux_to_exp n).apply (trans_lt ? (S O)).
198 unfold.apply le_n.assumption.symmetry.assumption.
201 theorem p_ord_times: \forall p,a,b,qa,ra,qb,rb. prime p
202 \to O \lt a \to O \lt b
203 \to p_ord a p = pair nat nat qa ra
204 \to p_ord b p = pair nat nat qb rb
205 \to p_ord (a*b) p = pair nat nat (qa + qb) (ra*rb).
208 elim (p_ord_to_exp1 ? ? ? ? Hcut H1 H3).
209 elim (p_ord_to_exp1 ? ? ? ? Hcut H2 H4).
211 apply (trans_lt ? (S O)).unfold.apply le_n.assumption.
213 elim (divides_times_to_divides ? ? ? H H9).
214 apply (absurd ? ? H10 H5).
215 apply (absurd ? ? H10 H7).
218 auto paramodulation library=yes.
219 unfold prime in H. elim H. assumption.
222 theorem fst_p_ord_times: \forall p,a,b. prime p
223 \to O \lt a \to O \lt b
224 \to fst ? ? (p_ord (a*b) p) = (fst ? ? (p_ord a p)) + (fst ? ? (p_ord b p)).
226 rewrite > (p_ord_times p a b (fst ? ? (p_ord a p)) (snd ? ? (p_ord a p))
227 (fst ? ? (p_ord b p)) (snd ? ? (p_ord b p)) H H1 H2).
228 simplify.reflexivity.
229 apply eq_pair_fst_snd.
230 apply eq_pair_fst_snd.
233 theorem p_ord_p : \forall p:nat. (S O) \lt p \to p_ord p p = pair ? ? (S O) (S O).
236 apply (trans_lt ? (S O)). unfold.apply le_n.assumption.
238 apply (absurd ? ? H).
240 apply divides_to_le.unfold.apply le_n.assumption.
241 rewrite < times_n_SO.