matita/library/nat/lt_arith.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/lt_arith".
  16
  17 include "nat/div_and_mod.ma".
  18
  19 (* plus *)
  20 theorem monotonic_lt_plus_r:
  21 \forall n:nat.monotonic nat lt (\lambda m.n+m).
  22 simplify.intros.
  23 elim n.simplify.assumption.
  24 simplify.unfold lt.
  25 apply le_S_S.assumption.
  26 qed.
  27
  28 variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def
  29 monotonic_lt_plus_r.
  30
  31 theorem monotonic_lt_plus_l:
  32 \forall n:nat.monotonic nat lt (\lambda m.m+n).
  33 simplify.
  34 intros.
  35 rewrite < sym_plus. rewrite < (sym_plus n).
  36 apply lt_plus_r.assumption.
  37 qed.
  38
  39 variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def
  40 monotonic_lt_plus_l.
  41
  42 theorem lt_plus: \forall n,m,p,q:nat. n < m \to p < q \to n + p < m + q.
  43 intros.
  44 apply (trans_lt ? (n + q)).
  45 apply lt_plus_r.assumption.
  46 apply lt_plus_l.assumption.
  47 qed.
  48
  49 theorem lt_plus_to_lt_l :\forall n,p,q:nat. p+n < q+n \to p<q.
  50 intro.elim n.
  51 rewrite > plus_n_O.
  52 rewrite > (plus_n_O q).assumption.
  53 apply H.
  54 unfold lt.apply le_S_S_to_le.
  55 rewrite > plus_n_Sm.
  56 rewrite > (plus_n_Sm q).
  57 exact H1.
  58 qed.
  59
  60 theorem lt_plus_to_lt_r :\forall n,p,q:nat. n+p < n+q \to p<q.
  61 intros.apply (lt_plus_to_lt_l n).
  62 rewrite > sym_plus.
  63 rewrite > (sym_plus q).assumption.
  64 qed.
  65
  66 (* times and zero *)
  67 theorem lt_O_times_S_S: \forall n,m:nat.O < (S n)*(S m).
  68 intros.simplify.unfold lt.apply le_S_S.apply le_O_n.
  69 qed.
  70
  71 (* times *)
  72 theorem monotonic_lt_times_r:
  73 \forall n:nat.monotonic nat lt (\lambda m.(S n)*m).
  74 simplify.
  75 intros.elim n.
  76 simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
  77 apply lt_plus.assumption.assumption.
  78 qed.
  79
  80 theorem lt_times_r: \forall n,p,q:nat. p < q \to (S n) * p < (S n) * q
  81 \def monotonic_lt_times_r.
  82
  83 theorem monotonic_lt_times_l:
  84 \forall m:nat.monotonic nat lt (\lambda n.n * (S m)).
  85 simplify.
  86 intros.
  87 rewrite < sym_times.rewrite < (sym_times (S m)).
  88 apply lt_times_r.assumption.
  89 qed.
  90
  91 variant lt_times_l: \forall n,p,q:nat. p<q \to p*(S n) < q*(S n)
  92 \def monotonic_lt_times_l.
  93
  94 theorem lt_times:\forall n,m,p,q:nat. n<m \to p<q \to n*p < m*q.
  95 intro.
  96 elim n.
  97 apply (lt_O_n_elim m H).
  98 intro.
  99 cut (lt O q).
 100 apply (lt_O_n_elim q Hcut).
 101 intro.change with (O < (S m1)*(S m2)).
 102 apply lt_O_times_S_S.
 103 apply (ltn_to_ltO p q H1).
 104 apply (trans_lt ? ((S n1)*q)).
 105 apply lt_times_r.assumption.
 106 cut (lt O q).
 107 apply (lt_O_n_elim q Hcut).
 108 intro.
 109 apply lt_times_l.
 110 assumption.
 111 apply (ltn_to_ltO p q H2).
 112 qed.
 113
 114 theorem lt_times_r1:
 115 \forall n,m,p. O < n \to m < p \to n*m < n*p.
 116 intros.
 117 elim H;apply lt_times_r;assumption.
 118 qed.
 119
 120 theorem lt_times_l1:
 121 \forall n,m,p. O < n \to m < p \to m*n < p*n.
 122 intros.
 123 elim H;apply lt_times_l;assumption.
 124 qed.
 125
 126 theorem lt_to_le_to_lt_times :
 127 \forall n,n1,m,m1. n < n1 \to m \le m1 \to O < m1 \to n*m < n1*m1.
 128 intros.
 129 apply (le_to_lt_to_lt ? (n*m1))
 130   [apply le_times_r.assumption
 131   |apply lt_times_l1
 132     [assumption|assumption]
 133   ]
 134 qed.
 135
 136 theorem lt_times_to_lt_l:
 137 \forall n,p,q:nat. p*(S n) < q*(S n) \to p < q.
 138 intros.
 139 cut (p < q \lor p \nlt q).
 140 elim Hcut.
 141 assumption.
 142 absurd (p * (S n) < q * (S n)).
 143 assumption.
 144 apply le_to_not_lt.
 145 apply le_times_l.
 146 apply not_lt_to_le.
 147 assumption.
 148 exact (decidable_lt p q).
 149 qed.
 150
 151 theorem lt_times_n_to_lt:
 152 \forall n,p,q:nat. O < n \to p*n < q*n \to p < q.
 153 intro.
 154 apply (nat_case n)
 155   [intros.apply False_ind.apply (not_le_Sn_n ? H)
 156   |intros 4.apply lt_times_to_lt_l
 157   ]
 158 qed.
 159
 160 theorem lt_times_to_lt_r:
 161 \forall n,p,q:nat. (S n)*p < (S n)*q \to lt p q.
 162 intros.
 163 apply (lt_times_to_lt_l n).
 164 rewrite < sym_times.
 165 rewrite < (sym_times (S n)).
 166 assumption.
 167 qed.
 168
 169 theorem lt_times_n_to_lt_r:
 170 \forall n,p,q:nat. O < n \to n*p < n*q \to lt p q.
 171 intro.
 172 apply (nat_case n)
 173   [intros.apply False_ind.apply (not_le_Sn_n ? H)
 174   |intros 4.apply lt_times_to_lt_r
 175   ]
 176 qed.
 177
 178 theorem nat_compare_times_l : \forall n,p,q:nat.
 179 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
 180 intros.apply nat_compare_elim.intro.
 181 apply nat_compare_elim.
 182 intro.reflexivity.
 183 intro.absurd (p=q).
 184 apply (inj_times_r n).assumption.
 185 apply lt_to_not_eq. assumption.
 186 intro.absurd (q<p).
 187 apply (lt_times_to_lt_r n).assumption.
 188 apply le_to_not_lt.apply lt_to_le.assumption.
 189 intro.rewrite < H.rewrite > nat_compare_n_n.reflexivity.
 190 intro.apply nat_compare_elim.intro.
 191 absurd (p<q).
 192 apply (lt_times_to_lt_r n).assumption.
 193 apply le_to_not_lt.apply lt_to_le.assumption.
 194 intro.absurd (q=p).
 195 symmetry.
 196 apply (inj_times_r n).assumption.
 197 apply lt_to_not_eq.assumption.
 198 intro.reflexivity.
 199 qed.
 200
 201 (* div *)
 202
 203 theorem eq_mod_O_to_lt_O_div: \forall n,m:nat. O < m \to O < n\to n \mod m = O \to O < n / m.
 204 intros 4.apply (lt_O_n_elim m H).intros.
 205 apply (lt_times_to_lt_r m1).
 206 rewrite < times_n_O.
 207 rewrite > (plus_n_O ((S m1)*(n / (S m1)))).
 208 rewrite < H2.
 209 rewrite < sym_times.
 210 rewrite < div_mod.
 211 rewrite > H2.
 212 assumption.
 213 unfold lt.apply le_S_S.apply le_O_n.
 214 qed.
 215
 216 theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to n / m \lt n.
 217 intros.
 218 apply (nat_case1 (n / m)).intro.
 219 assumption.intros.rewrite < H2.
 220 rewrite > (div_mod n m) in \vdash (? ? %).
 221 apply (lt_to_le_to_lt ? ((n / m)*m)).
 222 apply (lt_to_le_to_lt ? ((n / m)*(S (S O)))).
 223 rewrite < sym_times.
 224 rewrite > H2.
 225 simplify.unfold lt.
 226 rewrite < plus_n_O.
 227 rewrite < plus_n_Sm.
 228 apply le_S_S.
 229 apply le_S_S.
 230 apply le_plus_n.
 231 apply le_times_r.
 232 assumption.
 233 rewrite < sym_plus.
 234 apply le_plus_n.
 235 apply (trans_lt ? (S O)).
 236 unfold lt. apply le_n.assumption.
 237 qed.
 238
 239 (* general properties of functions *)
 240 theorem monotonic_to_injective: \forall f:nat\to nat.
 241 monotonic nat lt f \to injective nat nat f.
 242 unfold injective.intros.
 243 apply (nat_compare_elim x y).
 244 intro.apply False_ind.apply (not_le_Sn_n (f x)).
 245 rewrite > H1 in \vdash (? ? %).
 246 change with (f x < f y).
 247 apply H.apply H2.
 248 intros.assumption.
 249 intro.apply False_ind.apply (not_le_Sn_n (f y)).
 250 rewrite < H1 in \vdash (? ? %).
 251 change with (f y < f x).
 252 apply H.apply H2.
 253 qed.
 254
 255 theorem increasing_to_injective: \forall f:nat\to nat.
 256 increasing f \to injective nat nat f.
 257 intros.apply monotonic_to_injective.
 258 apply increasing_to_monotonic.assumption.
 259 qed.