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