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/ord".
  16
  17 include "datatypes/constructors.ma".
  18 include "nat/exp.ma".
  19 include "nat/gcd.ma".
  20 include "nat/relevant_equations.ma". (* required by auto paramod *)
  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 n \mod 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 (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.simplify.
  42 apply (nat_case (n \mod m)).
  43 simplify.apply plus_n_O.
  44 intros.
  45 simplify.apply plus_n_O.
  46 simplify.
  47 apply (nat_case1 (n1 \mod m)).intro.
  48 simplify.
  49 generalize in match (H (n1 / m) m).
  50 elim (p_ord_aux n (n1 / m) m).
  51 simplify.
  52 rewrite > assoc_times.
  53 rewrite < H3.rewrite > (plus_n_O (m*(n1 / m))).
  54 rewrite < H2.
  55 rewrite > sym_times.
  56 rewrite < div_mod.reflexivity.
  57 assumption.assumption.
  58 intros.simplify.apply plus_n_O.
  59 qed.
  60
  61 theorem p_ord_aux_to_exp: \forall p,n,m,q,r. O < m \to
  62   (pair nat nat q r) = p_ord_aux p n m \to n = m \sup q * r.
  63 intros.
  64 change with
  65 match (pair nat nat q r) with
  66   [ (pair q r) \Rightarrow n = m \sup q * r ].
  67 rewrite > H1.
  68 apply p_ord_aux_to_Prop.
  69 assumption.
  70 qed.
  71
  72 (* questo va spostato in primes1.ma *)
  73 theorem p_ord_exp: \forall n,m,i. O < m \to n \mod m \neq O \to
  74 \forall p. i \le p \to p_ord_aux p (m \sup i * n) m = pair nat nat i n.
  75 intros 5.
  76 elim i.
  77 simplify.
  78 rewrite < plus_n_O.
  79 apply (nat_case p).
  80 simplify.
  81 elim (n \mod m).simplify.reflexivity.simplify.reflexivity.
  82 intro.
  83 simplify.
  84 cut (O < n \mod m \lor O = n \mod m).
  85 elim Hcut.apply (lt_O_n_elim (n \mod m) H3).
  86 intros. simplify.reflexivity.
  87 apply False_ind.
  88 apply H1.apply sym_eq.assumption.
  89 apply le_to_or_lt_eq.apply le_O_n.
  90 generalize in match H3.
  91 apply (nat_case p).intro.apply False_ind.apply (not_le_Sn_O n1 H4).
  92 intros.
  93 simplify. fold simplify (m \sup (S n1)).
  94 cut (((m \sup (S n1)*n) \mod m) = O).
  95 rewrite > Hcut.
  96 simplify.fold simplify (m \sup (S n1)).
  97 cut ((m \sup (S n1) *n) / m = m \sup n1 *n).
  98 rewrite > Hcut1.
  99 rewrite > (H2 m1). simplify.reflexivity.
 100 apply le_S_S_to_le.assumption.
 101 (* div_exp *)
 102 simplify.
 103 rewrite > assoc_times.
 104 apply (lt_O_n_elim m H).
 105 intro.apply div_times.
 106 (* mod_exp = O *)
 107 apply divides_to_mod_O.
 108 assumption.
 109 simplify.rewrite > assoc_times.
 110 apply (witness ? ? (m \sup n1 *n)).reflexivity.
 111 qed.
 112
 113 theorem p_ord_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
 114   match p_ord_aux p n m with
 115   [ (pair q r) \Rightarrow r \mod m \neq O].
 116 intro.elim p.absurd (O < n).assumption.
 117 apply le_to_not_lt.assumption.
 118 simplify.
 119 apply (nat_case1 (n1 \mod m)).intro.
 120 generalize in match (H (n1 / m) m).
 121 elim (p_ord_aux n (n1 / m) m).
 122 apply H5.assumption.
 123 apply eq_mod_O_to_lt_O_div.
 124 apply (trans_lt ? (S O)).unfold lt.apply le_n.
 125 assumption.assumption.assumption.
 126 apply le_S_S_to_le.
 127 apply (trans_le ? n1).change with (n1 / m < n1).
 128 apply lt_div_n_m_n.assumption.assumption.assumption.
 129 intros.simplify.
 130 rewrite > H4.
 131 unfold Not.intro.
 132 apply (not_eq_O_S m1).
 133 rewrite > H5.reflexivity.
 134 qed.
 135
 136 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
 137  pair nat nat q r = p_ord_aux p n m \to r \mod m \neq O.
 138 intros.
 139 change with
 140   match (pair nat nat q r) with
 141   [ (pair q r) \Rightarrow r \mod m \neq O].
 142 rewrite > H3.
 143 apply p_ord_aux_to_Prop1.
 144 assumption.assumption.assumption.
 145 qed.
 146
 147 theorem p_ord_exp1: \forall p,n,q,r. O < p \to \lnot p \divides r \to
 148 n = p \sup q * r \to p_ord n p = pair nat nat q r.
 149 intros.unfold p_ord.
 150 rewrite > H2.
 151 apply p_ord_exp
 152  [assumption
 153  |unfold.intro.apply H1.
 154   apply mod_O_to_divides[assumption|assumption]
 155  |apply (trans_le ? (p \sup q)).
 156   cut ((S O) \lt p).
 157   elim q.simplify.apply le_n_Sn.
 158   simplify.
 159   generalize in match H3.
 160   apply (nat_case n1).simplify.
 161   rewrite < times_n_SO.intro.assumption.
 162   intros.
 163   apply (trans_le ? (p*(S m))).
 164   apply (trans_le ? ((S (S O))*(S m))).
 165   simplify.rewrite > plus_n_Sm.
 166   rewrite < plus_n_O.
 167   apply le_plus_n.
 168   apply le_times_l.
 169   assumption.
 170   apply le_times_r.assumption.
 171 alias id "not_eq_to_le_to_lt" = "cic:/matita/algebra/finite_groups/not_eq_to_le_to_lt.con".
 172 apply not_eq_to_le_to_lt.
 173   unfold.intro.apply H1.
 174   rewrite < H3.
 175   apply (witness ? r r ?).simplify.apply plus_n_O.
 176   assumption.
 177   rewrite > times_n_SO in \vdash (? % ?).
 178   apply le_times_r.
 179   change with (O \lt r).
 180   apply not_eq_to_le_to_lt.
 181   unfold.intro.
 182   apply H1.rewrite < H3.
 183   apply (witness ? ? O ?).rewrite < times_n_O.reflexivity.
 184   apply le_O_n.
 185   ]
 186 qed.
 187
 188 theorem p_ord_to_exp1: \forall p,n,q,r. (S O) \lt p \to O \lt n \to p_ord n p = pair nat nat q r\to
 189 \lnot p \divides r \land n = p \sup q * r.
 190 intros.
 191 unfold p_ord in H2.
 192 split.unfold.intro.
 193 apply (p_ord_aux_to_not_mod_O n n p q r).assumption.assumption.
 194 apply le_n.symmetry.assumption.
 195 apply divides_to_mod_O.apply (trans_lt ? (S O)).
 196 unfold.apply le_n.assumption.assumption.
 197 apply (p_ord_aux_to_exp n).apply (trans_lt ? (S O)).
 198 unfold.apply le_n.assumption.symmetry.assumption.
 199 qed.
 200
 201 theorem p_ord_times: \forall p,a,b,qa,ra,qb,rb. prime p
 202 \to O \lt a \to O \lt b
 203 \to p_ord a p = pair nat nat qa ra
 204 \to p_ord b p = pair nat nat qb rb
 205 \to p_ord (a*b) p = pair nat nat (qa + qb) (ra*rb).
 206 intros.
 207 cut ((S O) \lt p).
 208 elim (p_ord_to_exp1 ? ? ? ? Hcut H1 H3).
 209 elim (p_ord_to_exp1 ? ? ? ? Hcut H2 H4).
 210 apply p_ord_exp1.
 211 apply (trans_lt ? (S O)).unfold.apply le_n.assumption.
 212 unfold.intro.
 213 elim (divides_times_to_divides ? ? ? H H9).
 214 apply (absurd ? ? H10 H5).
 215 apply (absurd ? ? H10 H7).
 216 (* rewrite > H6.
 217 rewrite > H8. *)
 218 auto paramodulation library=yes.
 219 unfold prime in H. elim H. assumption.
 220 qed.
 221
 222 theorem fst_p_ord_times: \forall p,a,b. prime p
 223 \to O \lt a \to O \lt b
 224 \to fst ? ? (p_ord (a*b) p) = (fst ? ? (p_ord a p)) + (fst ? ? (p_ord b p)).
 225 intros.
 226 rewrite > (p_ord_times p a b (fst ? ? (p_ord a p)) (snd ? ? (p_ord a p))
 227 (fst ? ? (p_ord b p)) (snd ? ? (p_ord b p)) H H1 H2).
 228 simplify.reflexivity.
 229 apply eq_pair_fst_snd.
 230 apply eq_pair_fst_snd.
 231 qed.
 232
 233 theorem p_ord_p : \forall p:nat. (S O) \lt p \to p_ord p p = pair ? ? (S O) (S O).
 234 intros.
 235 apply p_ord_exp1.
 236 apply (trans_lt ? (S O)). unfold.apply le_n.assumption.
 237 unfold.intro.
 238 apply (absurd ? ? H).
 239 apply le_to_not_lt.
 240 apply divides_to_le.unfold.apply le_n.assumption.
 241 rewrite < times_n_SO.
 242 apply exp_n_SO.
 243 qed.