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/times.ma".
  18 include "nat/orders.ma".
  19 include "higher_order_defs/functions.ma".
  20
  21 let rec exp n m on m\def
  22  match m with
  23  [ O \Rightarrow (S O)
  24  | (S p) \Rightarrow (times n (exp n p)) ].
  25
  26 theorem exp_plus_times : \forall n,p,q:nat.
  27 eq nat (exp n (plus p q)) (times (exp n p) (exp n 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. eq nat (S O) (exp n O).
  35 intro.simplify.reflexivity.
  36 qed.
  37
  38 theorem exp_n_SO : \forall n:nat. eq nat n (exp n (S O)).
  39 intro.simplify.rewrite < times_n_SO.reflexivity.
  40 qed.
  41
  42 theorem exp_exp_times : \forall n,p,q:nat.
  43 eq nat (exp (exp n p) q) (exp n (times 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 < exp n m.
  51 intros.elim m.simplify.apply le_n.
  52 simplify.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 < exp n m.
  57 intros.elim m.simplify.reflexivity.
  58 simplify.
  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 exp n m = (S O) \to m = O.
  69 intros.apply antisym_le.apply le_S_S_to_le.
  70 rewrite < H1.change with m < exp n 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. exp n m).
  77 simplify.intros 4.
  78 apply nat_elim2 (\lambda x,y.exp n x = exp n 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. 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.apply inj_times_r m1.assumption.
  92 qed.
  93
  94 variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat.
  95 (exp p n) = (exp p m) \to n = m \def
  96 injective_exp_r.
  97
  98