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/log".
17 include "datatypes/constructors.ma".
19 include "nat/lt_arith.ma".
20 include "nat/primes.ma".
22 (* this definition of log is based on pairs, with a remainder *)
24 let rec plog_aux p n m \def
28 [ O \Rightarrow pair nat nat O n
30 match (plog_aux p (div 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 (* plog n m = <q,r> if m divides n q times, with remainder r *)
35 definition plog \def \lambda n,m:nat.plog_aux n n m.
37 theorem plog_aux_to_Prop: \forall p,n,m. O < m \to
38 match plog_aux p n m with
39 [ (pair q r) \Rightarrow n = (exp m q)*r ].
45 [ O \Rightarrow pair nat nat O n
46 | (S a) \Rightarrow pair nat nat O n] )
48 [ (pair q r) \Rightarrow n = (exp m q)*r ].
49 apply nat_case (mod n m).
50 simplify.apply plus_n_O.
52 simplify.apply plus_n_O.
57 match (plog_aux n (div n1 m) m) with
58 [ (pair q r) \Rightarrow pair nat nat (S q) r]
59 | (S a) \Rightarrow pair nat nat O n1] )
61 [ (pair q r) \Rightarrow n1 = (exp m q)*r].
62 apply nat_case1 (mod n1 m).intro.
65 match (plog_aux n (div n1 m) m) with
66 [ (pair q r) \Rightarrow pair nat nat (S q) r])
68 [ (pair q r) \Rightarrow n1 = (exp m q)*r].
69 generalize in match (H (div n1 m) m).
70 elim plog_aux n (div n1 m) m.
72 rewrite > assoc_times.
73 rewrite < H3.rewrite > plus_n_O (m*(div n1 m)).
76 rewrite < div_mod.reflexivity.
77 assumption.assumption.
78 intros.simplify.apply plus_n_O.
81 theorem plog_aux_to_exp: \forall p,n,m,q,r. O < m \to
82 (pair nat nat q r) = plog_aux p n m \to n = (exp m q)*r.
85 match (pair nat nat q r) with
86 [ (pair q r) \Rightarrow n = (exp m q)*r ].
88 apply plog_aux_to_Prop.
91 (* questo va spostato in primes1.ma *)
92 theorem plog_exp: \forall n,m,i. O < m \to \not (mod n m = O) \to
93 \forall p. i \le p \to plog_aux p ((exp m i)*n) m = pair nat nat i n.
101 [ O \Rightarrow pair nat nat O n
102 | (S a) \Rightarrow pair nat nat O n]
104 elim (mod n m).simplify.reflexivity.simplify.reflexivity.
109 match (plog_aux m1 (div n m) m) with
110 [ (pair q r) \Rightarrow pair nat nat (S q) r]
111 | (S a) \Rightarrow pair nat nat O n]
113 cut O < mod n m \lor O = mod n m.
114 elim Hcut.apply lt_O_n_elim (mod n m) H3.
115 intros. simplify.reflexivity.
117 apply H1.apply sym_eq.assumption.
118 apply le_to_or_lt_eq.apply le_O_n.
119 generalize in match H3.
120 apply nat_case p.intro.apply False_ind.apply not_le_Sn_O n1 H4.
123 match (mod ((exp m (S n1))*n) m) with
125 match (plog_aux m1 (div ((exp m (S n1))*n) m) m) with
126 [ (pair q r) \Rightarrow pair nat nat (S q) r]
127 | (S a) \Rightarrow pair nat nat O ((exp m (S n1))*n)]
128 = pair nat nat (S n1) n.
129 cut (mod ((exp m (S n1))*n) m) = O.
132 match (plog_aux m1 (div ((exp m (S n1))*n) m) m) with
133 [ (pair q r) \Rightarrow pair nat nat (S q) r]
134 = pair nat nat (S n1) n.
135 cut div ((exp m (S n1))*n) m = (exp m n1)*n.
137 rewrite > H2 m1. simplify.reflexivity.
138 apply le_S_S_to_le.assumption.
140 change with div (m*(exp m n1)*n) m = (exp m n1)*n.
141 rewrite > assoc_times.
142 apply lt_O_n_elim m H.
143 intro.apply div_times.
145 apply divides_to_mod_O.
147 simplify.rewrite > assoc_times.
148 apply witness ? ? ((exp m n1)*n).reflexivity.
151 theorem plog_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
152 match plog_aux p n m with
153 [ (pair q r) \Rightarrow \lnot (mod r m = O)].
154 intro.elim p.absurd O < n.assumption.
155 apply le_to_not_lt.assumption.
158 (match (mod n1 m) with
160 match (plog_aux n(div n1 m) m) with
161 [ (pair q r) \Rightarrow pair nat nat (S q) r]
162 | (S a) \Rightarrow pair nat nat O n1])
164 [ (pair q r) \Rightarrow \lnot(mod r m = O)].
165 apply nat_case1 (mod n1 m).intro.
166 generalize in match (H (div n1 m) m).
167 elim (plog_aux n (div n1 m) m).
169 apply eq_mod_O_to_lt_O_div.
170 apply trans_lt ? (S O).simplify.apply le_n.
171 assumption.assumption.assumption.
173 apply trans_le ? n1.change with div n1 m < n1.
174 apply lt_div_n_m_n.assumption.assumption.assumption.
176 change with (\lnot (mod n1 m = O)).
178 (* Andrea: META NOT FOUND !!!
182 rewrite > H5.reflexivity.
185 theorem plog_aux_to_not_mod_O: \forall p,n,m,q,r. (S O) < m \to O < n \to n \le p \to
186 pair nat nat q r = plog_aux p n m \to \lnot (mod r m = O).
189 match (pair nat nat q r) with
190 [ (pair q r) \Rightarrow \lnot (mod r m = O)].
192 apply plog_aux_to_Prop1.
193 assumption.assumption.assumption.