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