helm/matita/library/nat/log.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 (*       \ /        Matita 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/log".
  16
  17 include "datatypes/constructors.ma".
  18 include "nat/primes.ma".
  19 include "nat/exp.ma".
  20
  21 (* this definition of log is based on pairs, with a remainder *)
  22
  23 let rec plog_aux p n m \def
  24   match (mod n m) with
  25   [ O \Rightarrow
  26     match p with
  27       [ O \Rightarrow pair nat nat O n
  28       | (S p) \Rightarrow
  29        match (plog_aux p (div n m) m) with
  30        [ (pair q r) \Rightarrow pair nat nat (S q) r]]
  31   | (S a) \Rightarrow pair nat nat O n].
  32
  33 (* plog n m = <q,r> if m divides n q times, with remainder r *)
  34 definition plog \def \lambda n,m:nat.plog_aux n n m.
  35
  36 theorem plog_aux_to_Prop: \forall p,n,m. O < m \to
  37   match plog_aux p n m with
  38   [ (pair q r) \Rightarrow n = (exp m q)*r ].
  39 intro.
  40 elim p.
  41 change with
  42 match (
  43 match (mod n m) with
  44   [ O \Rightarrow pair nat nat O n
  45   | (S a) \Rightarrow pair nat nat O n] )
  46 with
  47   [ (pair q r) \Rightarrow n = (exp m q)*r ].
  48 apply nat_case (mod n m).
  49 simplify.apply plus_n_O.
  50 intros.
  51 simplify.apply plus_n_O.
  52 change with
  53 match (
  54 match (mod n1 m) with
  55   [ O \Rightarrow
  56      match (plog_aux n (div n1 m) m) with
  57        [ (pair q r) \Rightarrow pair nat nat (S q) r]
  58   | (S a) \Rightarrow pair nat nat O n1] )
  59 with
  60   [ (pair q r) \Rightarrow n1 = (exp m q)*r].
  61 apply nat_case1 (mod n1 m).intro.
  62 change with
  63 match (
  64  match (plog_aux n (div n1 m) m) with
  65    [ (pair q r) \Rightarrow pair nat nat (S q) r])
  66 with
  67   [ (pair q r) \Rightarrow n1 = (exp m q)*r].
  68 generalize in match (H (div n1 m) m).
  69 elim plog_aux n (div n1 m) m.
  70 simplify.
  71 rewrite > assoc_times.
  72 rewrite < H3.rewrite > plus_n_O (m*(div n1 m)).
  73 rewrite < H2.
  74 rewrite > sym_times.
  75 rewrite < div_mod.reflexivity.
  76 intros.simplify.apply plus_n_O.
  77 assumption.assumption.
  78 qed.
  79
  80 theorem plog_aux_to_exp: \forall p,n,m,q,r. O < m \to
  81   (pair nat nat q r) = plog_aux p n m \to n = (exp m q)*r.
  82 intros.
  83 change with
  84 match (pair nat nat q r) with
  85   [ (pair q r) \Rightarrow n = (exp m q)*r ].
  86 rewrite > H1.
  87 apply plog_aux_to_Prop.
  88 assumption.
  89 qed.
  90 (* questo va spostato in primes1.ma *)
  91 theorem plog_exp: \forall n,m,i. O < m \to \not (mod n m = O) \to
  92 \forall p. i \le p \to plog_aux p ((exp m i)*n) m = pair nat nat i n.
  93 intros 5.
  94 elim i.
  95 simplify.
  96 rewrite < plus_n_O.
  97 apply nat_case p.
  98 change with
  99  match (mod n m) with
 100   [ O \Rightarrow pair nat nat O n
 101   | (S a) \Rightarrow pair nat nat O n]
 102   = pair nat nat O n.
 103 elim (mod n m).simplify.reflexivity.simplify.reflexivity.
 104 intro.
 105 change with
 106  match (mod n m) with
 107   [ O \Rightarrow
 108        match (plog_aux m1 (div n m) m) with
 109        [ (pair q r) \Rightarrow pair nat nat (S q) r]
 110   | (S a) \Rightarrow pair nat nat O n]
 111   = pair nat nat O n.
 112 cut O < mod n m \lor O = mod n m.
 113 elim Hcut.apply lt_O_n_elim (mod n m) H3.
 114 intros. simplify.reflexivity.
 115 apply False_ind.
 116 apply H1.apply sym_eq.assumption.
 117 apply le_to_or_lt_eq.apply le_O_n.
 118 generalize in match H3.
 119 apply nat_case p.intro.apply False_ind.apply not_le_Sn_O n1 H4.
 120 intros.
 121 change with
 122  match (mod ((exp m (S n1))*n) m) with
 123   [ O \Rightarrow
 124        match (plog_aux m1 (div ((exp m (S n1))*n) m) m) with
 125        [ (pair q r) \Rightarrow pair nat nat (S q) r]
 126   | (S a) \Rightarrow pair nat nat O ((exp m (S n1))*n)]
 127   = pair nat nat (S n1) n.
 128 cut (mod ((exp m (S n1))*n) m) = O.
 129 rewrite > Hcut.
 130 change with
 131 match (plog_aux m1 (div ((exp m (S n1))*n) m) m) with
 132        [ (pair q r) \Rightarrow pair nat nat (S q) r]
 133   = pair nat nat (S n1) n.
 134 cut div ((exp m (S n1))*n) m = (exp m n1)*n.
 135 rewrite > Hcut1.
 136 rewrite > H2 m1. simplify.reflexivity.
 137 (* div_exp *)
 138 change with div (m*(exp m n1)*n) m = (exp m n1)*n.
 139 rewrite > assoc_times.
 140 apply lt_O_n_elim m H.
 141 intro.apply div_times.
 142 (* mod_exp = O *)
 143 apply divides_to_mod_O.
 144 assumption.
 145 simplify.rewrite > assoc_times.
 146 apply witness ? ? ((exp m n1)*n).reflexivity.
 147 apply le_S_S_to_le.assumption.
 148 qed.
 149
 150 theorem plog_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
 151   match plog_aux p n m with
 152   [ (pair q r) \Rightarrow \lnot (mod r m = O)].
 153 intro.elim p.absurd O < n.assumption.
 154 apply le_to_not_lt.assumption.
 155 change with
 156 match
 157   (match (mod n1 m) with
 158     [ O \Rightarrow
 159         match (plog_aux n(div n1 m) m) with
 160         [ (pair q r) \Rightarrow pair nat nat (S q) r]
 161     | (S a) \Rightarrow pair nat nat O n1])
 162 with
 163   [ (pair q r) \Rightarrow \lnot(mod r m = O)].
 164 apply nat_case1 (mod n1 m).intro.
 165 generalize in match (H (div n1 m) m).
 166 elim (plog_aux n (div n1 m) m).
 167 apply H5.assumption.
 168 apply eq_mod_O_to_lt_O_div.
 169 apply trans_lt ? (S O).simplify.apply le_n.
 170 assumption.assumption.assumption.
 171 apply le_S_S_to_le.
 172 apply trans_le ? n1.change with div n1 m < n1.
 173 apply lt_div_n_m_n.assumption.assumption.assumption.
 174 intros.
 175 change with (\lnot (mod n1 m = O)).
 176 rewrite > H4.
 177 (* META NOT FOUND !!!
 178 rewrite > sym_eq. *)
 179 simplify.intro.
 180 apply not_eq_O_S m1 ?.
 181 rewrite > H5.reflexivity.
 182 qed.
 183
 184 theorem plog_aux_to_not_mod_O: \forall p,n,m,q,r. (S O) < m \to O < n \to n \le p \to
 185  pair nat nat q r = plog_aux p n m \to \lnot (mod r m = O).
 186 intros.
 187 change with
 188   match (pair nat nat q r) with
 189   [ (pair q r) \Rightarrow \lnot (mod r m = O)].
 190 rewrite > H3.
 191 apply plog_aux_to_Prop1.
 192 assumption.assumption.assumption.
 193 qed.
 194