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
  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_SO_n : \forall n:nat. S O = (S O) \sup n.
  44 intro.elim n
  45   [reflexivity
  46   |simplify.rewrite < plus_n_O.assumption
  47   ]
  48 qed.
  49
  50 theorem exp_SSO: \forall n. exp n (S(S O)) = n*n.
  51 intro.simplify.
  52 rewrite < times_n_SO.
  53 reflexivity.
  54 qed.
  55
  56 theorem exp_exp_times : \forall n,p,q:nat.
  57 (n \sup p) \sup q = n \sup (p * q).
  58 intros.
  59 elim q.simplify.rewrite < times_n_O.simplify.reflexivity.
  60 simplify.rewrite > H.rewrite < exp_plus_times.
  61 rewrite < times_n_Sm.reflexivity.
  62 qed.
  63
  64 theorem lt_O_exp: \forall n,m:nat. O < n \to O < n \sup m.
  65 intros.elim m.simplify.unfold lt.apply le_n.
  66 simplify.unfold lt.rewrite > times_n_SO.
  67 apply le_times.assumption.assumption.
  68 qed.
  69
  70 theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < n \sup m.
  71 intros.elim m.simplify.unfold lt.apply le_n.
  72 simplify.unfold lt.
  73 apply (trans_le ? ((S(S O))*(S n1))).
  74 simplify.
  75 rewrite < plus_n_Sm.apply le_S_S.apply le_S_S.
  76 rewrite < sym_plus.
  77 apply le_plus_n.
  78 apply le_times.assumption.assumption.
  79 qed.
  80
  81 theorem exp_to_eq_O: \forall n,m:nat. (S O) < n
  82 \to n \sup m = (S O) \to m = O.
  83 intros.apply antisym_le.apply le_S_S_to_le.
  84 rewrite < H1.change with (m < n \sup m).
  85 apply lt_m_exp_nm.assumption.
  86 apply le_O_n.
  87 qed.
  88
  89 theorem injective_exp_r: \forall n:nat. (S O) < n \to
  90 injective nat nat (\lambda m:nat. n \sup m).
  91 simplify.intros 4.
  92 apply (nat_elim2 (\lambda x,y.n \sup x = n \sup y \to x = y)).
  93 intros.apply sym_eq.apply (exp_to_eq_O n).assumption.
  94 rewrite < H1.reflexivity.
  95 intros.apply (exp_to_eq_O n).assumption.assumption.
  96 intros.apply eq_f.
  97 apply H1.
  98 (* esprimere inj_times senza S *)
  99 cut (\forall a,b:nat.O < n \to n*a=n*b \to a=b).
 100 apply Hcut.simplify.unfold lt.apply le_S_S_to_le. apply le_S. assumption.
 101 assumption.
 102 intros 2.
 103 apply (nat_case n).
 104 intros.apply False_ind.apply (not_le_Sn_O O H3).
 105 intros.
 106 apply (inj_times_r m1).assumption.
 107 qed.
 108
 109 variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat.
 110 p \sup n = p \sup m \to n = m \def
 111 injective_exp_r.
 112
 113 theorem le_exp: \forall n,m,p:nat. O < p \to n \le m \to exp p n \le exp p m.
 114 apply nat_elim2
 115   [intros.
 116    apply lt_O_exp.assumption
 117   |intros.
 118    apply False_ind.
 119    apply (le_to_not_lt ? ? ? H1).
 120    apply le_O_n
 121   |intros.
 122    simplify.
 123    apply le_times
 124     [apply le_n
 125     |apply H[assumption|apply le_S_S_to_le.assumption]
 126     ]
 127   ]
 128 qed.
 129
 130 theorem lt_exp: \forall n,m,p:nat. S O < p \to n < m \to exp p n < exp p m.
 131 apply nat_elim2
 132   [intros.
 133    apply (lt_O_n_elim ? H1).intro.
 134    simplify.unfold lt.
 135    rewrite > times_n_SO.
 136    apply le_times
 137     [assumption
 138     |apply lt_O_exp.
 139      apply (trans_lt ? (S O))[apply le_n|assumption]
 140     ]
 141   |intros.
 142    apply False_ind.
 143    apply (le_to_not_lt ? ? ? H1).
 144    apply le_O_n
 145   |intros.simplify.
 146    apply lt_times_r1
 147     [apply (trans_lt ? (S O))[apply le_n|assumption]
 148     |apply H
 149       [apply H1
 150       |apply le_S_S_to_le.assumption
 151       ]
 152     ]
 153   ]
 154 qed.
 155
 156 theorem lt_exp1: \forall n,m,p:nat. O < p \to n < m \to exp n p < exp m p.
 157 intros.
 158 elim H
 159   [rewrite < exp_n_SO.rewrite < exp_n_SO.assumption
 160   |simplify.
 161    apply lt_times;assumption
 162   ]
 163 qed.
 164
 165 theorem le_exp_to_le:
 166 \forall a,n,m. S O < a \to exp a n \le exp a m \to n \le m.
 167 intro.
 168 apply nat_elim2;intros
 169   [apply le_O_n
 170   |apply False_ind.
 171    apply (le_to_not_lt ? ? H1).
 172    simplify.
 173    rewrite > times_n_SO.
 174    apply lt_to_le_to_lt_times
 175     [assumption
 176     |apply lt_O_exp.apply lt_to_le.assumption
 177     |apply lt_O_exp.apply lt_to_le.assumption
 178     ]
 179   |simplify in H2.
 180    apply le_S_S.
 181    apply H
 182     [assumption
 183     |apply (le_times_to_le a)
 184       [apply lt_to_le.assumption|assumption]
 185     ]
 186   ]
 187 qed.
 188
 189 theorem le_exp_to_le1 : \forall n,m,p.O < p \to exp n p \leq exp m p \to n \leq m.
 190 intros;apply not_lt_to_le;intro;apply (lt_to_not_le ? ? ? H1);
 191 apply lt_exp1;assumption.
 192 qed.
 193
 194 theorem lt_exp_to_lt:
 195 \forall a,n,m. S O < a \to exp a n < exp a m \to n < m.
 196 intros.
 197 elim (le_to_or_lt_eq n m)
 198   [assumption
 199   |apply False_ind.
 200    apply (lt_to_not_eq ? ? H1).
 201    rewrite < H2.
 202    reflexivity
 203   |apply (le_exp_to_le a)
 204     [assumption
 205     |apply lt_to_le.
 206      assumption
 207     ]
 208   ]
 209 qed.
 210
 211 theorem times_exp:
 212 \forall n,m,p. exp n p * exp m p = exp (n*m) p.
 213 intros.elim p
 214   [simplify.reflexivity
 215   |simplify.
 216    rewrite > assoc_times.
 217    rewrite < assoc_times in ⊢ (? ? (? ? %) ?).
 218    rewrite < sym_times in ⊢ (? ? (? ? (? % ?)) ?).
 219    rewrite > assoc_times in ⊢ (? ? (? ? %) ?).
 220    rewrite < assoc_times.
 221    rewrite < H.
 222    reflexivity
 223   ]
 224 qed.
 225
 226 theorem monotonic_exp1: \forall n.
 227 monotonic nat le (\lambda x.(exp x n)).
 228 unfold monotonic. intros.
 229 simplify.elim n
 230   [apply le_n
 231   |simplify.
 232    apply le_times;assumption
 233   ]
 234 qed.
 235
 236
 237