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