helm/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.