]> matita.cs.unibo.it Git - helm.git/blob - matita/library/nat/exp.ma
fixed propagation under Fix/Lambda/Case of coercions, better names are
[helm.git] / 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 set "baseuri" "cic:/matita/nat/exp".
16
17 include "nat/div_and_mod.ma".
18 include "nat/lt_arith.ma".
19
20 let rec exp n m on m\def 
21  match m with 
22  [ O \Rightarrow (S O)
23  | (S p) \Rightarrow (times n (exp n p)) ].
24
25 interpretation "natural exponent" 'exp a b = (cic:/matita/nat/exp/exp.con a b).
26
27 theorem exp_plus_times : \forall n,p,q:nat. 
28 n \sup (p + q) = (n \sup p) * (n \sup q).
29 intros.elim p.
30 simplify.rewrite < plus_n_O.reflexivity.
31 simplify.rewrite > H.symmetry.
32 apply assoc_times.
33 qed.
34
35 theorem exp_n_O : \forall n:nat. S O = n \sup O.
36 intro.simplify.reflexivity.
37 qed.
38
39 theorem exp_n_SO : \forall n:nat. n = n \sup (S O).
40 intro.simplify.rewrite < times_n_SO.reflexivity.
41 qed.
42
43 theorem exp_exp_times : \forall n,p,q:nat. 
44 (n \sup p) \sup q = n \sup (p * q).
45 intros.
46 elim q.simplify.rewrite < times_n_O.simplify.reflexivity.
47 simplify.rewrite > H.rewrite < exp_plus_times.
48 rewrite < times_n_Sm.reflexivity.
49 qed.
50
51 theorem lt_O_exp: \forall n,m:nat. O < n \to O < n \sup m. 
52 intros.elim m.simplify.unfold lt.apply le_n.
53 simplify.unfold lt.rewrite > times_n_SO.
54 apply le_times.assumption.assumption.
55 qed.
56
57 theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < n \sup m.
58 intros.elim m.simplify.unfold lt.apply le_n.
59 simplify.unfold lt.
60 apply (trans_le ? ((S(S O))*(S n1))).
61 simplify.
62 rewrite < plus_n_Sm.apply le_S_S.apply le_S_S.
63 rewrite < sym_plus.
64 apply le_plus_n.
65 apply le_times.assumption.assumption.
66 qed.
67
68 theorem exp_to_eq_O: \forall n,m:nat. (S O) < n 
69 \to n \sup m = (S O) \to m = O.
70 intros.apply antisym_le.apply le_S_S_to_le.
71 rewrite < H1.change with (m < n \sup m).
72 apply lt_m_exp_nm.assumption.
73 apply le_O_n.
74 qed.
75
76 theorem injective_exp_r: \forall n:nat. (S O) < n \to 
77 injective nat nat (\lambda m:nat. n \sup m).
78 simplify.intros 4.
79 apply (nat_elim2 (\lambda x,y.n \sup x = n \sup y \to x = y)).
80 intros.apply sym_eq.apply (exp_to_eq_O n).assumption.
81 rewrite < H1.reflexivity.
82 intros.apply (exp_to_eq_O n).assumption.assumption.
83 intros.apply eq_f.
84 apply H1.
85 (* esprimere inj_times senza S *)
86 cut (\forall a,b:nat.O < n \to n*a=n*b \to a=b).
87 apply Hcut.simplify.unfold lt.apply le_S_S_to_le. apply le_S. assumption.
88 assumption.
89 intros 2.
90 apply (nat_case n).
91 intros.apply False_ind.apply (not_le_Sn_O O H3).
92 intros.
93 apply (inj_times_r m1).assumption.
94 qed.
95
96 variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat.
97 p \sup n = p \sup m \to n = m \def
98 injective_exp_r.
99
100 theorem le_exp: \forall n,m,p:nat. O < p \to n \le m \to exp p n \le exp p m.
101 apply nat_elim2
102   [intros.
103    apply lt_O_exp.assumption
104   |intros.
105    apply False_ind.
106    apply (le_to_not_lt ? ? ? H1).
107    apply le_O_n
108   |intros.
109    simplify.
110    apply le_times
111     [apply le_n
112     |apply H[assumption|apply le_S_S_to_le.assumption]
113     ]
114   ]
115 qed.
116
117 theorem lt_exp: \forall n,m,p:nat. S O < p \to n < m \to exp p n < exp p m.
118 apply nat_elim2
119   [intros.
120    apply (lt_O_n_elim ? H1).intro.
121    simplify.unfold lt.
122    rewrite > times_n_SO.
123    apply le_times
124     [assumption
125     |apply lt_O_exp.
126      apply (trans_lt ? (S O))[apply le_n|assumption]
127     ]
128   |intros.
129    apply False_ind.
130    apply (le_to_not_lt ? ? ? H1).
131    apply le_O_n
132   |intros.simplify.
133    apply lt_times_r1
134     [apply (trans_lt ? (S O))[apply le_n|assumption]
135     |apply H
136       [apply H1
137       |apply le_S_S_to_le.assumption
138       ]
139     ]
140   ]
141 qed.
142
143 theorem le_exp_to_le: 
144 \forall a,n,m. S O < a \to exp a n \le exp a m \to n \le m.
145 intro.
146 apply nat_elim2;intros
147   [apply le_O_n
148   |apply False_ind.
149    apply (le_to_not_lt ? ? H1).
150    simplify.
151    rewrite > times_n_SO.
152    apply lt_to_le_to_lt_times
153     [assumption
154     |apply lt_O_exp.apply lt_to_le.assumption
155     |apply lt_O_exp.apply lt_to_le.assumption
156     ]
157   |simplify in H2.
158    apply le_S_S.
159    apply H
160     [assumption
161     |apply (le_times_to_le a)
162       [apply lt_to_le.assumption|assumption]
163     ]
164   ]
165 qed.
166
167
168      
169    
170    
171