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