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