matita/library_auto/auto/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/library_auto/nat/exp".
  16
  17 include "auto/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/library_auto/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.
  29 elim p;simplify;auto.
  30 (*[ rewrite < plus_n_O.
  31   reflexivity
  32 | rewrite > H.
  33   symmetry.
  34   apply assoc_times
  35 ]*)
  36 qed.
  37
  38 theorem exp_n_O : \forall n:nat. S O = n \sup O.
  39 intro.
  40 auto.
  41 (*simplify.
  42 reflexivity.*)
  43 qed.
  44
  45 theorem exp_n_SO : \forall n:nat. n = n \sup (S O).
  46 intro.
  47 auto.
  48 (*simplify.
  49 rewrite < times_n_SO.
  50 reflexivity.*)
  51 qed.
  52
  53 theorem exp_exp_times : \forall n,p,q:nat.
  54 (n \sup p) \sup q = n \sup (p * q).
  55 intros.
  56 elim q;simplify
  57 [ auto.
  58   (*rewrite < times_n_O.
  59   simplify.
  60   reflexivity*)
  61 | rewrite > H.
  62   rewrite < exp_plus_times.
  63   auto
  64   (*rewrite < times_n_Sm.
  65   reflexivity*)
  66 ]
  67 qed.
  68
  69 theorem lt_O_exp: \forall n,m:nat. O < n \to O < n \sup m.
  70 intros.
  71 elim m;simplify;auto.
  72                 (*unfold lt
  73 [ apply le_n
  74 | rewrite > times_n_SO.
  75   apply le_times;assumption
  76 ]*)
  77 qed.
  78
  79 theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < n \sup m.
  80 intros.
  81 elim m;simplify;unfold lt;
  82 [ apply le_n.
  83 | apply (trans_le ? ((S(S O))*(S n1)))
  84   [ simplify.
  85     rewrite < plus_n_Sm.
  86     apply le_S_S.
  87     auto
  88     (*apply le_S_S.
  89     rewrite < sym_plus.
  90     apply le_plus_n*)
  91   | auto
  92     (*apply le_times;assumption*)
  93   ]
  94 ]
  95 qed.
  96
  97 theorem exp_to_eq_O: \forall n,m:nat. (S O) < n
  98 \to n \sup m = (S O) \to m = O.
  99 intros.
 100 apply antisym_le
 101 [ apply le_S_S_to_le.
 102   rewrite < H1.
 103   auto
 104   (*change with (m < n \sup m).
 105   apply lt_m_exp_nm.
 106   assumption*)
 107 | apply le_O_n
 108 ]
 109 qed.
 110
 111 theorem injective_exp_r: \forall n:nat. (S O) < n \to
 112 injective nat nat (\lambda m:nat. n \sup m).
 113 simplify.
 114 intros 4.
 115 apply (nat_elim2 (\lambda x,y.n \sup x = n \sup y \to x = y))
 116 [ intros.
 117   auto
 118   (*apply sym_eq.
 119   apply (exp_to_eq_O n)
 120   [ assumption
 121   | rewrite < H1.
 122     reflexivity
 123   ]*)
 124 | intros.
 125   apply (exp_to_eq_O n);assumption
 126 | intros.
 127   apply eq_f.
 128   apply H1.
 129   (* esprimere inj_times senza S *)
 130   cut (\forall a,b:nat.O < n \to n*a=n*b \to a=b)
 131   [ apply Hcut
 132     [ auto
 133       (*simplify.
 134       unfold lt.
 135       apply le_S_S_to_le.
 136       apply le_S.
 137       assumption*)
 138     | (*NB qui auto non chiude il goal, chiuso invece chiamando solo la tattica assumption*)
 139       assumption
 140     ]
 141   | intros 2.
 142     apply (nat_case n);intros;auto
 143     (*[ apply False_ind.
 144       apply (not_le_Sn_O O H3)
 145     | apply (inj_times_r m1).
 146       assumption
 147     ]*)
 148   ]
 149 ]
 150 qed.
 151
 152 variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat.
 153 p \sup n = p \sup m \to n = m \def
 154 injective_exp_r.