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 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/exp".
17 include "nat/div_and_mod.ma".
18 include "nat/lt_arith.ma".
20 let rec exp n m on m\def
23 | (S p) \Rightarrow (times n (exp n p)) ].
25 interpretation "natural exponent" 'exp a b = (cic:/matita/nat/exp/exp.con a b).
27 theorem exp_plus_times : \forall n,p,q:nat.
28 n \sup (p + q) = (n \sup p) * (n \sup q).
30 simplify.rewrite < plus_n_O.reflexivity.
31 simplify.rewrite > H.symmetry.
35 theorem exp_n_O : \forall n:nat. S O = n \sup O.
36 intro.simplify.reflexivity.
39 theorem exp_n_SO : \forall n:nat. n = n \sup (S O).
40 intro.simplify.rewrite < times_n_SO.reflexivity.
43 theorem exp_SO_n : \forall n:nat. S O = (S O) \sup n.
46 |simplify.rewrite < plus_n_O.assumption
50 theorem exp_SSO: \forall n. exp n (S(S O)) = n*n.
56 theorem exp_exp_times : \forall n,p,q:nat.
57 (n \sup p) \sup q = n \sup (p * q).
59 elim q.simplify.rewrite < times_n_O.simplify.reflexivity.
60 simplify.rewrite > H.rewrite < exp_plus_times.
61 rewrite < times_n_Sm.reflexivity.
64 theorem lt_O_exp: \forall n,m:nat. O < n \to O < n \sup m.
65 intros.elim m.simplify.unfold lt.apply le_n.
66 simplify.unfold lt.rewrite > times_n_SO.
67 apply le_times.assumption.assumption.
70 theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < n \sup m.
71 intros.elim m.simplify.unfold lt.apply le_n.
73 apply (trans_le ? ((S(S O))*(S n1))).
75 rewrite < plus_n_Sm.apply le_S_S.apply le_S_S.
78 apply le_times.assumption.assumption.
81 theorem exp_to_eq_O: \forall n,m:nat. (S O) < n
82 \to n \sup m = (S O) \to m = O.
83 intros.apply antisym_le.apply le_S_S_to_le.
84 rewrite < H1.change with (m < n \sup m).
85 apply lt_m_exp_nm.assumption.
89 theorem injective_exp_r: \forall n:nat. (S O) < n \to
90 injective nat nat (\lambda m:nat. n \sup m).
92 apply (nat_elim2 (\lambda x,y.n \sup x = n \sup y \to x = y)).
93 intros.apply sym_eq.apply (exp_to_eq_O n).assumption.
94 rewrite < H1.reflexivity.
95 intros.apply (exp_to_eq_O n).assumption.assumption.
98 (* esprimere inj_times senza S *)
99 cut (\forall a,b:nat.O < n \to n*a=n*b \to a=b).
100 apply Hcut.simplify.unfold lt.apply le_S_S_to_le. apply le_S. assumption.
104 intros.apply False_ind.apply (not_le_Sn_O O H3).
106 apply (inj_times_r m1).assumption.
109 variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat.
110 p \sup n = p \sup m \to n = m \def
113 theorem le_exp: \forall n,m,p:nat. O < p \to n \le m \to exp p n \le exp p m.
116 apply lt_O_exp.assumption
119 apply (le_to_not_lt ? ? ? H1).
125 |apply H[assumption|apply le_S_S_to_le.assumption]
130 theorem lt_exp: \forall n,m,p:nat. S O < p \to n < m \to exp p n < exp p m.
133 apply (lt_O_n_elim ? H1).intro.
135 rewrite > times_n_SO.
139 apply (trans_lt ? (S O))[apply le_n|assumption]
143 apply (le_to_not_lt ? ? ? H1).
147 [apply (trans_lt ? (S O))[apply le_n|assumption]
150 |apply le_S_S_to_le.assumption
156 theorem lt_exp1: \forall n,m,p:nat. O < p \to n < m \to exp n p < exp m p.
159 [rewrite < exp_n_SO.rewrite < exp_n_SO.assumption
161 apply lt_times;assumption
165 theorem le_exp_to_le:
166 \forall a,n,m. S O < a \to exp a n \le exp a m \to n \le m.
168 apply nat_elim2;intros
171 apply (le_to_not_lt ? ? H1).
173 rewrite > times_n_SO.
174 apply lt_to_le_to_lt_times
176 |apply lt_O_exp.apply lt_to_le.assumption
177 |apply lt_O_exp.apply lt_to_le.assumption
183 |apply (le_times_to_le a)
184 [apply lt_to_le.assumption|assumption]
189 theorem le_exp_to_le1 : \forall n,m,p.O < p \to exp n p \leq exp m p \to n \leq m.
190 intros;apply not_lt_to_le;intro;apply (lt_to_not_le ? ? ? H1);
191 apply lt_exp1;assumption.
194 theorem lt_exp_to_lt:
195 \forall a,n,m. S O < a \to exp a n < exp a m \to n < m.
197 elim (le_to_or_lt_eq n m)
200 apply (lt_to_not_eq ? ? H1).
203 |apply (le_exp_to_le a)
212 \forall n,m,p. exp n p * exp m p = exp (n*m) p.
214 [simplify.reflexivity
216 rewrite > assoc_times.
217 rewrite < assoc_times in ⊢ (? ? (? ? %) ?).
218 rewrite < sym_times in ⊢ (? ? (? ? (? % ?)) ?).
219 rewrite > assoc_times in ⊢ (? ? (? ? %) ?).
220 rewrite < assoc_times.
226 theorem monotonic_exp1: \forall n.
227 monotonic nat le (\lambda x.(exp x n)).
228 unfold monotonic. intros.
232 apply le_times;assumption