]> matita.cs.unibo.it Git - helm.git/blob - matita/library/nat/exp.ma
More commands documented.
[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
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/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.elim p.
29 simplify.rewrite < plus_n_O.reflexivity.
30 simplify.rewrite > H.symmetry.
31 apply assoc_times.
32 qed.
33
34 theorem exp_n_O : \forall n:nat. S O = n \sup O.
35 intro.simplify.reflexivity.
36 qed.
37
38 theorem exp_n_SO : \forall n:nat. n = n \sup (S O).
39 intro.simplify.rewrite < times_n_SO.reflexivity.
40 qed.
41
42 theorem exp_exp_times : \forall n,p,q:nat. 
43 (n \sup p) \sup q = n \sup (p * q).
44 intros.
45 elim q.simplify.rewrite < times_n_O.simplify.reflexivity.
46 simplify.rewrite > H.rewrite < exp_plus_times.
47 rewrite < times_n_Sm.reflexivity.
48 qed.
49
50 theorem lt_O_exp: \forall n,m:nat. O < n \to O < n \sup m. 
51 intros.elim m.simplify.unfold lt.apply le_n.
52 simplify.unfold lt.rewrite > times_n_SO.
53 apply le_times.assumption.assumption.
54 qed.
55
56 theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < n \sup m.
57 intros.elim m.simplify.unfold lt.reflexivity.
58 simplify.unfold lt.
59 apply (trans_le ? ((S(S O))*(S n1))).
60 simplify.
61 rewrite < plus_n_Sm.apply le_S_S.apply le_S_S.
62 rewrite < sym_plus.
63 apply le_plus_n.
64 apply le_times.assumption.assumption.
65 qed.
66
67 theorem exp_to_eq_O: \forall n,m:nat. (S O) < n 
68 \to n \sup m = (S O) \to m = O.
69 intros.apply antisym_le.apply le_S_S_to_le.
70 rewrite < H1.change with (m < n \sup m).
71 apply lt_m_exp_nm.assumption.
72 apply le_O_n.
73 qed.
74
75 theorem injective_exp_r: \forall n:nat. (S O) < n \to 
76 injective nat nat (\lambda m:nat. n \sup m).
77 simplify.intros 4.
78 apply (nat_elim2 (\lambda x,y.n \sup x = n \sup y \to x = y)).
79 intros.apply sym_eq.apply (exp_to_eq_O n).assumption.
80 rewrite < H1.reflexivity.
81 intros.apply (exp_to_eq_O n).assumption.assumption.
82 intros.apply eq_f.
83 apply H1.
84 (* esprimere inj_times senza S *)
85 cut (\forall a,b:nat.O < n \to n*a=n*b \to a=b).
86 apply Hcut.simplify.unfold lt.apply le_S_S_to_le. apply le_S. assumption.
87 assumption.
88 intros 2.
89 apply (nat_case n).
90 intros.apply False_ind.apply (not_le_Sn_O O H3).
91 intros.
92 apply (inj_times_r m1).assumption.
93 qed.
94
95 variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat.
96 p \sup n = p \sup m \to n = m \def
97 injective_exp_r.