matita/matita/lib/arithmetics/exp.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/div_and_mod.ma".
  13 include "basics/core_notation/exp_2.ma".
  14
  15 let rec exp n m on m ≝
  16  match m with
  17  [ O ⇒ 1
  18  | S p ⇒ (exp n p) * n].
  19
  20 interpretation "natural exponent" 'exp a b = (exp a b).
  21
  22 theorem exp_plus_times : ∀n,p,q:nat.
  23   n^(p + q) = n^p * n^q.
  24 #n #p #q elim p normalize //
  25 qed.
  26
  27 theorem exp_n_O : ∀n:nat. 1 = n^O.
  28 //
  29 qed.
  30
  31 theorem exp_n_1 : ∀n:nat. n = n^1.
  32 #n normalize //
  33 qed.
  34
  35 theorem exp_1_n : ∀n:nat. 1 = 1^n.
  36 #n (elim n) normalize //
  37 qed.
  38
  39 theorem exp_2: ∀n. n^2 = n*n.
  40 #n normalize //
  41 qed.
  42
  43 theorem exp_exp_times : ∀n,p,q:nat.
  44   (n^p)^q = n^(p * q).
  45 #n #p #q (elim q) normalize
  46 (* [applyS exp_n_O funziona ma non lo trova *)
  47 // <times_n_O //
  48 qed.
  49
  50 theorem lt_O_exp: ∀n,m:nat. O < n → O < n^m.
  51 #n #m (elim m) normalize // #a #Hind #posn
  52 @(le_times 1 ? 1) /2/ qed.
  53
  54 (* [applyS monotonic_le_minus_r /2/
  55
  56 > (minus_Sn_n ?)
  57 [cut (∃x.∃y.∃z.(x - y ≤ x - z) = (1 ≤ n ^a))
  58   [@ex_intro
  59     [|@ex_intro
  60       [|@ex_intro
  61         [|
  62 @(rewrite_r \Nopf  (S  n \sup a - n \sup a )
  63  (\lambda x:\Nopf
  64   .(S  n \sup a - n \sup a \le S  n \sup a -(S ?-?))=(x\le  n \sup a ))
  65  (rewrite_r \Nopf  ?
  66   (\lambda x:\Nopf
  67    .(S  n \sup a - n \sup a \le x)=(S  n \sup a - n \sup a \le  n \sup a ))
  68   ( refl … Type[0]  (S  n \sup a - n \sup a \le  n \sup a ) ) (S ?-(S ?-?))
  69   (rewrite_r \Nopf  (?-O) (\lambda x:\Nopf .S ?-(S ?-?)=x)
  70    (rewrite_l \Nopf  1 (\lambda x:\Nopf .S ?-x=n ^a -O) (minus_S_S ? O) (S ?-?)
  71     (minus_Sn_n ?)) ?
  72    (minus_n_O ?))) 1
  73  (minus_Sn_n  n \sup a ))
  74
  75 @(rewrite_r \Nopf  (S ?-?)
  76  (\lambda x:\Nopf
  77   .(S  n \sup a - n \sup a \le S  n \sup a -(S ?-?))=(x\le  n \sup a ))
  78  (rewrite_r \Nopf  ?
  79   (\lambda x:\Nopf
  80    .(S  n \sup a - n \sup a \le x)=(S  n \sup a - n \sup a \le  n \sup a ))
  81   ( refl ??) (S ?-(S ?-?))
  82   ?) 1
  83  (minus_Sn_n ?))
  84   [||
  85 @(rewrite_r \Nopf  (?-O) (\lambda x:\Nopf .S ?-(S ?-?)=x)
  86   ???)
  87 [|<(minus_Sn_n ?)
  88 @(rewrite_r \Nopf  (?-O) (\lambda x:\Nopf .S ?-(S ?-?)=x)
  89  (rewrite_l \Nopf  1 (\lambda x:\Nopf .S ?-x=?-O)
  90     ? (S ?-?)
  91     (minus_Sn_n ?)) ??)
  92
  93 @(rewrite_r \Nopf  (?-O) (\lambda x:\Nopf .S ?-(S ?-?)=x)
  94    (rewrite_l \Nopf  1 (\lambda x:\Nopf .S ?-x=?-O) (minus_S_S ? O) (S ?-?)
  95     (minus_Sn_n ?)) ?
  96    (minus_n_O ?)))
  97
  98 applyS monotonic_le_minus_r /2/
  99 qed. *)
 100
 101 theorem lt_m_exp_nm: ∀n,m:nat. 1 < n → m < n^m.
 102 #n #m #lt1n (elim m) normalize //
 103 #n #Hind @(transitive_le ? ((S n)*2)) // @le_times //
 104 qed.
 105
 106 theorem exp_to_eq_O: ∀n,m:nat. 1 < n →
 107   n^m = 1 → m = O.
 108 #n #m #ltin #eq1 @le_to_le_to_eq //
 109 @le_S_S_to_le <eq1 @lt_m_exp_nm //
 110 qed.
 111
 112 theorem injective_exp_r: ∀b:nat. 1 < b →
 113   injective nat nat (λi:nat. b^i).
 114 #b #lt1b @nat_elim2 normalize
 115   [#n #H @sym_eq @(exp_to_eq_O b n lt1b) //
 116   |#n #H @False_ind @(absurd (1 < 1) ? (not_le_Sn_n 1))
 117    <H in ⊢ (??%); @(lt_to_le_to_lt ? (1*b)) //
 118    @le_times // @lt_O_exp /2/
 119   |#n #m #Hind #H @eq_f @Hind @(injective_times_l … H) /2/
 120   ]
 121 qed.
 122
 123 theorem le_exp: ∀n,m,p:nat. O < p →
 124   n ≤m → p^n ≤ p^m.
 125 @nat_elim2 #n #m
 126   [#ltm #len @lt_O_exp //
 127   |#_ #len @False_ind /2/
 128   |#Hind #p #posp #lenm normalize @le_times // @Hind /2/
 129   ]
 130 qed.
 131
 132 theorem le_exp1: ∀n,m,a:nat. O < a →
 133   n ≤m → n^a ≤ m^a.
 134 #n #m #a #posa #lenm (elim posa) //
 135 #a #posa #Hind @le_times //
 136 qed.
 137
 138 theorem lt_exp: ∀n,m,p:nat. 1 < p →
 139   n < m → p^n < p^m.
 140 #n #m #p #lt1p #ltnm
 141 cut (p \sup n ≤ p \sup m) [@le_exp /2/] #H
 142 cases(le_to_or_lt_eq … H) // #eqexp
 143 @False_ind @(absurd (n=m)) /2/
 144 qed.
 145
 146 theorem lt_exp1: ∀n,m,p:nat. 0 < p →
 147   n < m → n^p < m^p.
 148 #n #m #p #posp #ltnm (elim posp) //
 149 #p #posp #Hind @lt_times //
 150 qed.
 151
 152 theorem le_exp_to_le:
 153 ∀b,n,m. 1 < b → b^n ≤ b^m → n ≤ m.
 154 #b #n #m #lt1b #leexp cases(decidable_le n m) //
 155 #notle @False_ind @(absurd … leexp) @lt_to_not_le
 156 @lt_exp /2/
 157 qed.
 158
 159 theorem le_exp_to_le1 : ∀n,m,p.O < p →
 160   n^p ≤ m^p → n ≤ m.
 161 #n #m #p #posp #leexp @not_lt_to_le
 162 @(not_to_not … (lt_exp1 ??? posp)) @le_to_not_lt //
 163 qed.
 164
 165 theorem lt_exp_to_lt:
 166 ∀a,n,m. 0 < a → a^n < a^m → n < m.
 167 #a #n #m #lt1a #ltexp cases(decidable_le (S n) m) //
 168 #H @False_ind @(absurd … ltexp) @le_to_not_lt
 169 @le_exp // @not_lt_to_le @H
 170 qed.
 171
 172 theorem lt_exp_to_lt1:
 173 ∀a,n,m. O < a → n^a < m^a → n < m.
 174 #a #n #m #posa #ltexp cases(decidable_le (S n) m) //
 175 #H @False_ind @(absurd … ltexp) @le_to_not_lt
 176 @le_exp1 // @not_lt_to_le @H
 177 qed.
 178
 179 theorem times_exp: ∀n,m,p.
 180   n^p * m^p = (n*m)^p.
 181 #n #m #p (elim p) // #p #Hind normalize //
 182 qed.
 183
 184
 185
 186