]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/library/nat/exp.ma
fixed, it seems the new handling of hints in some rare cases made inference stupid
[helm.git] / helm / software / matita / library / nat / exp.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 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "nat/div_and_mod.ma".
16 include "nat/lt_arith.ma".
17
18 let rec exp n m on m\def 
19  match m with 
20  [ O \Rightarrow (S O)
21  | (S p) \Rightarrow (times n (exp n p)) ].
22
23 interpretation "natural exponent" 'exp a b = (cic:/matita/nat/exp/exp.con a b).
24
25 theorem exp_plus_times : \forall n,p,q:nat. 
26 n \sup (p + q) = (n \sup p) * (n \sup q).
27 intros.elim p.
28 simplify.rewrite < plus_n_O.reflexivity.
29 simplify.rewrite > H.symmetry.
30 apply assoc_times.
31 qed.
32
33 theorem exp_n_O : \forall n:nat. S O = n \sup O.
34 intro.simplify.reflexivity.
35 qed.
36
37 theorem exp_n_SO : \forall n:nat. n = n \sup (S O).
38 intro.simplify.rewrite < times_n_SO.reflexivity.
39 qed.
40
41 theorem exp_SO_n : \forall n:nat. S O = (S O) \sup n.
42 intro.elim n
43   [reflexivity
44   |simplify.rewrite < plus_n_O.assumption
45   ]
46 qed.
47
48 theorem exp_SSO: \forall n. exp n (S(S O)) = n*n.
49 intro.simplify.
50 rewrite < times_n_SO.
51 reflexivity.
52 qed.
53
54 theorem exp_exp_times : \forall n,p,q:nat. 
55 (n \sup p) \sup q = n \sup (p * q).
56 intros.
57 elim q.simplify.rewrite < times_n_O.simplify.reflexivity.
58 simplify.rewrite > H.rewrite < exp_plus_times.
59 rewrite < times_n_Sm.reflexivity.
60 qed.
61
62 theorem lt_O_exp: \forall n,m:nat. O < n \to O < n \sup m. 
63 intros.elim m.simplify.unfold lt.apply le_n.
64 simplify.unfold lt.rewrite > times_n_SO.
65 apply le_times.assumption.assumption.
66 qed.
67
68 theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < n \sup m.
69 intros.elim m.simplify.unfold lt.apply le_n.
70 simplify.unfold lt.
71 apply (trans_le ? ((S(S O))*(S n1))).
72 simplify.
73 rewrite < plus_n_Sm.apply le_S_S.apply le_S_S.
74 rewrite < sym_plus.
75 apply le_plus_n.
76 apply le_times.assumption.assumption.
77 qed.
78
79 theorem exp_to_eq_O: \forall n,m:nat. (S O) < n 
80 \to n \sup m = (S O) \to m = O.
81 intros.apply antisym_le.apply le_S_S_to_le.
82 rewrite < H1.change with (m < n \sup m).
83 apply lt_m_exp_nm.assumption.
84 apply le_O_n.
85 qed.
86
87 theorem injective_exp_r: \forall n:nat. (S O) < n \to 
88 injective nat nat (\lambda m:nat. n \sup m).
89 simplify.intros 4.
90 apply (nat_elim2 (\lambda x,y.n \sup x = n \sup y \to x = y)).
91 intros.apply sym_eq.apply (exp_to_eq_O n).assumption.
92 rewrite < H1.reflexivity.
93 intros.apply (exp_to_eq_O n).assumption.assumption.
94 intros.apply eq_f.
95 apply H1.
96 (* esprimere inj_times senza S *)
97 cut (\forall a,b:nat.O < n \to n*a=n*b \to a=b).
98 apply Hcut.simplify.unfold lt.apply le_S_S_to_le. apply le_S. assumption.
99 assumption.
100 intros 2.
101 apply (nat_case n).
102 intros.apply False_ind.apply (not_le_Sn_O O H3).
103 intros.
104 apply (inj_times_r m1).assumption.
105 qed.
106
107 variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat.
108 p \sup n = p \sup m \to n = m \def
109 injective_exp_r.
110
111 theorem le_exp: \forall n,m,p:nat. O < p \to n \le m \to exp p n \le exp p m.
112 apply nat_elim2
113   [intros.
114    apply lt_O_exp.assumption
115   |intros.
116    apply False_ind.
117    apply (le_to_not_lt ? ? ? H1).
118    apply le_O_n
119   |intros.
120    simplify.
121    apply le_times
122     [apply le_n
123     |apply H[assumption|apply le_S_S_to_le.assumption]
124     ]
125   ]
126 qed.
127
128 theorem lt_exp: \forall n,m,p:nat. S O < p \to n < m \to exp p n < exp p m.
129 apply nat_elim2
130   [intros.
131    apply (lt_O_n_elim ? H1).intro.
132    simplify.unfold lt.
133    rewrite > times_n_SO.
134    apply le_times
135     [assumption
136     |apply lt_O_exp.
137      apply (trans_lt ? (S O))[apply le_n|assumption]
138     ]
139   |intros.
140    apply False_ind.
141    apply (le_to_not_lt ? ? ? H1).
142    apply le_O_n
143   |intros.simplify.
144    apply lt_times_r1
145     [apply (trans_lt ? (S O))[apply le_n|assumption]
146     |apply H
147       [apply H1
148       |apply le_S_S_to_le.assumption
149       ]
150     ]
151   ]
152 qed.
153
154 theorem lt_exp1: \forall n,m,p:nat. O < p \to n < m \to exp n p < exp m p.
155 intros.
156 elim H
157   [rewrite < exp_n_SO.rewrite < exp_n_SO.assumption
158   |simplify.
159    apply lt_times;assumption
160   ]
161 qed.
162
163 theorem le_exp_to_le: 
164 \forall a,n,m. S O < a \to exp a n \le exp a m \to n \le m.
165 intro.
166 apply nat_elim2;intros
167   [apply le_O_n
168   |apply False_ind.
169    apply (le_to_not_lt ? ? H1).
170    simplify.
171    rewrite > times_n_SO.
172    apply lt_to_le_to_lt_times
173     [assumption
174     |apply lt_O_exp.apply lt_to_le.assumption
175     |apply lt_O_exp.apply lt_to_le.assumption
176     ]
177   |simplify in H2.
178    apply le_S_S.
179    apply H
180     [assumption
181     |apply (le_times_to_le a)
182       [apply lt_to_le.assumption|assumption]
183     ]
184   ]
185 qed.
186
187 theorem le_exp_to_le1 : \forall n,m,p.O < p \to exp n p \leq exp m p \to n \leq m.
188 intros;apply not_lt_to_le;intro;apply (lt_to_not_le ? ? ? H1);
189 apply lt_exp1;assumption.
190 qed.
191      
192 theorem lt_exp_to_lt: 
193 \forall a,n,m. S O < a \to exp a n < exp a m \to n < m.
194 intros.
195 elim (le_to_or_lt_eq n m)
196   [assumption
197   |apply False_ind.
198    apply (lt_to_not_eq ? ? H1).
199    rewrite < H2.
200    reflexivity
201   |apply (le_exp_to_le a)
202     [assumption
203     |apply lt_to_le.
204      assumption
205     ]
206   ]
207 qed.
208
209 theorem lt_exp_to_lt1: 
210 \forall a,n,m. O < a \to exp n a < exp m a \to n < m.
211 intros.
212 elim (le_to_or_lt_eq n m)
213   [assumption
214   |apply False_ind.
215    apply (lt_to_not_eq ? ? H1).
216    rewrite < H2.
217    reflexivity
218   |apply (le_exp_to_le1 ? ? a)
219     [assumption
220     |apply lt_to_le.
221      assumption
222     ]
223   ]
224 qed.
225      
226 theorem times_exp: 
227 \forall n,m,p. exp n p * exp m p = exp (n*m) p.
228 intros.elim p
229   [simplify.reflexivity
230   |simplify.
231    rewrite > assoc_times.
232    rewrite < assoc_times in ⊢ (? ? (? ? %) ?).
233    rewrite < sym_times in ⊢ (? ? (? ? (? % ?)) ?).
234    rewrite > assoc_times in ⊢ (? ? (? ? %) ?).
235    rewrite < assoc_times.
236    rewrite < H.
237    reflexivity
238   ]
239 qed.
240
241 theorem monotonic_exp1: \forall n.
242 monotonic nat le (\lambda x.(exp x n)).
243 unfold monotonic. intros.
244 simplify.elim n
245   [apply le_n
246   |simplify.
247    apply le_times;assumption
248   ]
249 qed.
250   
251    
252