matita/contribs/library_auto/auto/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/library_autobatch/nat/lt_arith".
  16
  17 include "auto/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
  24 [ assumption
  25 | autobatch.
  26   (*unfold lt.
  27   apply le_S_S.
  28   assumption.*)
  29 ]
  30 qed.
  31
  32 variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def
  33 monotonic_lt_plus_r.
  34
  35 theorem monotonic_lt_plus_l:
  36 \forall n:nat.monotonic nat lt (\lambda m.m+n).
  37 simplify.
  38 intros.
  39 (*rewrite < sym_plus.
  40  rewrite < (sym_plus n).*)
  41 applyS lt_plus_r.assumption.
  42 qed.
  43 (* IN ALTERNATIVA: mantengo le 2 rewrite, e concludo con autobatch. *)
  44
  45 variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def
  46 monotonic_lt_plus_l.
  47
  48 theorem lt_plus: \forall n,m,p,q:nat. n < m \to p < q \to n + p < m + q.
  49 intros.
  50 autobatch.
  51 (*apply (trans_lt ? (n + q)).
  52 apply lt_plus_r.assumption.
  53 apply lt_plus_l.assumption.*)
  54 qed.
  55
  56 theorem lt_plus_to_lt_l :\forall n,p,q:nat. p+n < q+n \to p<q.
  57 intro.elim n
  58 [ rewrite > plus_n_O.
  59   rewrite > (plus_n_O q).
  60   assumption.
  61 | apply H.
  62   unfold lt.
  63   apply le_S_S_to_le.
  64   rewrite > plus_n_Sm.
  65   rewrite > (plus_n_Sm q).
  66   exact H1.
  67 ]
  68 qed.
  69
  70 theorem lt_plus_to_lt_r :\forall n,p,q:nat. n+p < n+q \to p<q.
  71 intros.
  72 apply (lt_plus_to_lt_l n).
  73 rewrite > sym_plus.
  74 rewrite > (sym_plus q).
  75 assumption.
  76 qed.
  77
  78 (* times and zero *)
  79 theorem lt_O_times_S_S: \forall n,m:nat.O < (S n)*(S m).
  80 intros.
  81 autobatch.
  82 (*simplify.
  83 unfold lt.
  84 apply le_S_S.
  85 apply le_O_n.*)
  86 qed.
  87
  88 (* times *)
  89 theorem monotonic_lt_times_r:
  90 \forall n:nat.monotonic nat lt (\lambda m.(S n)*m).
  91 simplify.
  92 intros.elim n
  93 [ autobatch
  94   (*simplify.
  95   rewrite < plus_n_O.
  96   rewrite < plus_n_O.
  97   assumption.*)
  98 | apply lt_plus;assumption (* chiudo con assumption entrambi i sottogoal attivi*)
  99 ]
 100 qed.
 101
 102 theorem lt_times_r: \forall n,p,q:nat. p < q \to (S n) * p < (S n) * q
 103 \def monotonic_lt_times_r.
 104
 105 theorem monotonic_lt_times_l:
 106 \forall m:nat.monotonic nat lt (\lambda n.n * (S m)).
 107 simplify.
 108 intros.
 109 (*rewrite < sym_times.
 110  rewrite < (sym_times (S m)).*)
 111 applyS lt_times_r.assumption.
 112 qed.
 113
 114 (* IN ALTERNATIVA: mantengo le 2 rewrite, e concludo con autobatch. *)
 115
 116
 117 variant lt_times_l: \forall n,p,q:nat. p<q \to p*(S n) < q*(S n)
 118 \def monotonic_lt_times_l.
 119
 120 theorem lt_times:\forall n,m,p,q:nat. n<m \to p<q \to n*p < m*q.
 121 intro.
 122 elim n
 123 [ apply (lt_O_n_elim m H).
 124   intro.
 125   cut (lt O q)
 126   [ apply (lt_O_n_elim q Hcut).
 127     intro.
 128     autobatch
 129     (*change with (O < (S m1)*(S m2)).
 130     apply lt_O_times_S_S.*)
 131   | apply (ltn_to_ltO p q H1). (*funziona anche autobatch*)
 132   ]
 133 | apply (trans_lt ? ((S n1)*q))
 134   [ autobatch
 135     (*apply lt_times_r.
 136     assumption.*)
 137   | cut (lt O q)
 138     [ apply (lt_O_n_elim q Hcut).
 139       intro.
 140       autobatch
 141       (*apply lt_times_l.
 142       assumption.*)
 143     |apply (ltn_to_ltO p q H2). (*funziona anche autobatch*)
 144     ]
 145   ]
 146 ]
 147 qed.
 148
 149 theorem lt_times_to_lt_l:
 150 \forall n,p,q:nat. p*(S n) < q*(S n) \to p < q.
 151 intros.
 152 cut (p < q \lor p \nlt q)
 153 [ elim Hcut
 154   [ assumption
 155   | absurd (p * (S n) < q * (S n))
 156     [ assumption
 157     | apply le_to_not_lt.
 158       autobatch
 159       (*apply le_times_l.
 160       apply not_lt_to_le.
 161       assumption.*)
 162     ]
 163   ]
 164 |exact (decidable_lt p q).
 165 ]
 166 qed.
 167
 168 theorem lt_times_to_lt_r:
 169 \forall n,p,q:nat. (S n)*p < (S n)*q \to lt p q.
 170 intros.
 171 apply (lt_times_to_lt_l n).
 172 rewrite < sym_times.
 173 rewrite < (sym_times (S n)).
 174 assumption.
 175 qed.
 176
 177 theorem nat_compare_times_l : \forall n,p,q:nat.
 178 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
 179 intros.
 180 apply nat_compare_elim
 181 [ intro.
 182   apply nat_compare_elim
 183   [ intro.
 184     reflexivity
 185   | intro.
 186     absurd (p=q)
 187     [ autobatch.
 188       (*apply (inj_times_r n).
 189       assumption*)
 190     | autobatch
 191       (*apply lt_to_not_eq.
 192       assumption*)
 193     ]
 194   | intro.
 195     absurd (q<p)
 196     [ autobatch.
 197       (*apply (lt_times_to_lt_r n).
 198       assumption.*)
 199     | autobatch
 200       (*apply le_to_not_lt.
 201       apply lt_to_le.
 202       assumption*)
 203     ]
 204   ].
 205 | intro.
 206   autobatch
 207   (*rewrite < H.
 208   rewrite > nat_compare_n_n.
 209   reflexivity*)
 210 | intro.
 211   apply nat_compare_elim
 212   [ intro.
 213     absurd (p<q)
 214     [ autobatch
 215       (*apply (lt_times_to_lt_r n).
 216       assumption.*)
 217     | autobatch
 218       (*apply le_to_not_lt.
 219       apply lt_to_le.
 220       assumption.*)
 221     ]
 222   | intro.
 223     absurd (q=p)
 224     [ autobatch.
 225       (*symmetry.
 226       apply (inj_times_r n).
 227       assumption*)
 228     | autobatch
 229       (*apply lt_to_not_eq.
 230       assumption*)
 231     ]
 232   | intro.
 233     reflexivity
 234   ]
 235 ].
 236 qed.
 237
 238 (* div *)
 239
 240 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.
 241 intros 4.
 242 apply (lt_O_n_elim m H).
 243 intros.
 244 apply (lt_times_to_lt_r m1).
 245 rewrite < times_n_O.
 246 rewrite > (plus_n_O ((S m1)*(n / (S m1)))).
 247 rewrite < H2.
 248 rewrite < sym_times.
 249 rewrite < div_mod
 250 [ rewrite > H2.
 251   assumption.
 252 | autobatch
 253   (*unfold lt.
 254   apply le_S_S.
 255   apply le_O_n.*)
 256 ]
 257 qed.
 258
 259 theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to n / m \lt n.
 260 intros.
 261 apply (nat_case1 (n / m))
 262 [ intro.
 263   assumption
 264 | intros.
 265   rewrite < H2.
 266   rewrite > (div_mod n m) in \vdash (? ? %)
 267   [ apply (lt_to_le_to_lt ? ((n / m)*m))
 268     [ apply (lt_to_le_to_lt ? ((n / m)*(S (S O))))
 269       [ rewrite < sym_times.
 270         rewrite > H2.
 271         simplify.
 272         unfold lt.
 273         autobatch.
 274         (*rewrite < plus_n_O.
 275         rewrite < plus_n_Sm.
 276         apply le_S_S.
 277         apply le_S_S.
 278         apply le_plus_n*)
 279       | autobatch
 280         (*apply le_times_r.
 281         assumption*)
 282       ]
 283     | autobatch
 284       (*rewrite < sym_plus.
 285       apply le_plus_n*)
 286     ]
 287   | autobatch
 288     (*apply (trans_lt ? (S O)).
 289     unfold lt.
 290     apply le_n.
 291     assumption*)
 292   ]
 293 ]
 294 qed.
 295
 296 (* general properties of functions *)
 297 theorem monotonic_to_injective: \forall f:nat\to nat.
 298 monotonic nat lt f \to injective nat nat f.
 299 unfold injective.intros.
 300 apply (nat_compare_elim x y)
 301 [ intro.
 302   apply False_ind.
 303   apply (not_le_Sn_n (f x)).
 304   rewrite > H1 in \vdash (? ? %).
 305   change with (f x < f y).
 306   autobatch
 307   (*apply H.
 308   apply H2*)
 309 | intros.
 310   assumption
 311 | intro.
 312   apply False_ind.
 313   apply (not_le_Sn_n (f y)).
 314   rewrite < H1 in \vdash (? ? %).
 315   change with (f y < f x).
 316   autobatch
 317   (*apply H.
 318   apply H2*)
 319 ]
 320 qed.
 321
 322 theorem increasing_to_injective: \forall f:nat\to nat.
 323 increasing f \to injective nat nat f.
 324 intros.
 325 autobatch.
 326 (*apply monotonic_to_injective.
 327 apply increasing_to_monotonic.
 328 assumption.*)
 329 qed.