matita/library/nat/minus.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
  16 include "nat/le_arith.ma".
  17 include "nat/compare.ma".
  18
  19 let rec minus n m \def
  20  match n with
  21  [ O \Rightarrow O
  22  | (S p) \Rightarrow
  23         match m with
  24         [O \Rightarrow (S p)
  25         | (S q) \Rightarrow minus p q ]].
  26
  27 (*CSC: the URI must disappear: there is a bug now *)
  28 interpretation "natural minus" 'minus x y = (cic:/matita/nat/minus/minus.con x y).
  29
  30 theorem minus_n_O: \forall n:nat.n=n-O.
  31 intros.elim n.simplify.reflexivity.
  32 simplify.reflexivity.
  33 qed.
  34
  35 theorem minus_n_n: \forall n:nat.O=n-n.
  36 intros.elim n.simplify.
  37 reflexivity.
  38 simplify.apply H.
  39 qed.
  40
  41 theorem minus_Sn_n: \forall n:nat. S O = (S n)-n.
  42 intro.elim n.
  43 simplify.reflexivity.
  44 elim H.reflexivity.
  45 qed.
  46
  47 theorem minus_Sn_m: \forall n,m:nat. m \leq n \to (S n)-m = S (n-m).
  48 intros 2.
  49 apply (nat_elim2
  50 (\lambda n,m.m \leq n \to (S n)-m = S (n-m))).
  51 intros.apply (le_n_O_elim n1 H).
  52 simplify.reflexivity.
  53 intros.simplify.reflexivity.
  54 intros.rewrite < H.reflexivity.
  55 apply le_S_S_to_le. assumption.
  56 qed.
  57
  58 theorem eq_minus_S_pred: \forall n,m. n - (S m) = pred(n -m).
  59 apply nat_elim2
  60   [intro.reflexivity
  61   |intro.simplify.autobatch
  62   |intros.simplify.assumption
  63   ]
  64 qed.
  65
  66 theorem plus_minus:
  67 \forall n,m,p:nat. m \leq n \to (n-m)+p = (n+p)-m.
  68 intros 2.
  69 apply (nat_elim2
  70 (\lambda n,m.\forall p:nat.m \leq n \to (n-m)+p = (n+p)-m)).
  71 intros.apply (le_n_O_elim ? H).
  72 simplify.rewrite < minus_n_O.reflexivity.
  73 intros.simplify.reflexivity.
  74 intros.simplify.apply H.apply le_S_S_to_le.assumption.
  75 qed.
  76
  77 theorem minus_plus_m_m: \forall n,m:nat.n = (n+m)-m.
  78 intros 2.
  79 generalize in match n.
  80 elim m.
  81 rewrite < minus_n_O.apply plus_n_O.
  82 elim n2.simplify.
  83 apply minus_n_n.
  84 rewrite < plus_n_Sm.
  85 change with (S n3 = (S n3 + n1)-n1).
  86 apply H.
  87 qed.
  88
  89 theorem plus_minus_m_m: \forall n,m:nat.
  90 m \leq n \to n = (n-m)+m.
  91 intros 2.
  92 apply (nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m)).
  93 intros.apply (le_n_O_elim n1 H).
  94 reflexivity.
  95 intros.simplify.rewrite < plus_n_O.reflexivity.
  96 intros.simplify.rewrite < sym_plus.simplify.
  97 apply eq_f.rewrite < sym_plus.apply H.
  98 apply le_S_S_to_le.assumption.
  99 qed.
 100
 101 theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to
 102 n = m+p.
 103 intros.apply (trans_eq ? ? ((n-m)+m)).
 104 apply plus_minus_m_m.
 105 apply H.elim H1.
 106 apply sym_plus.
 107 qed.
 108
 109 theorem plus_to_minus :\forall n,m,p:nat.
 110 n = m+p \to n-m = p.
 111 intros.
 112 apply (inj_plus_r m).
 113 rewrite < H.
 114 rewrite < sym_plus.
 115 symmetry.
 116 apply plus_minus_m_m.rewrite > H.
 117 rewrite > sym_plus.
 118 apply le_plus_n.
 119 qed.
 120
 121 theorem minus_S_S : \forall n,m:nat.
 122 eq nat (minus (S n) (S m)) (minus n m).
 123 intros.
 124 reflexivity.
 125 qed.
 126
 127 theorem minus_pred_pred : \forall n,m:nat. lt O n \to lt O m \to
 128 eq nat (minus (pred n) (pred m)) (minus n m).
 129 intros.
 130 apply (lt_O_n_elim n H).intro.
 131 apply (lt_O_n_elim m H1).intro.
 132 simplify.reflexivity.
 133 qed.
 134
 135 theorem eq_minus_n_m_O: \forall n,m:nat.
 136 n \leq m \to n-m = O.
 137 intros 2.
 138 apply (nat_elim2 (\lambda n,m.n \leq m \to n-m = O)).
 139 intros.simplify.reflexivity.
 140 intros.apply False_ind.
 141 apply not_le_Sn_O;
 142 [2: apply H | skip].
 143 intros.
 144 simplify.apply H.apply le_S_S_to_le. apply H1.
 145 qed.
 146
 147 theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
 148 intros.elim H.elim (minus_Sn_n n).apply le_n.
 149 rewrite > minus_Sn_m.
 150 apply le_S.assumption.
 151 apply lt_to_le.assumption.
 152 qed.
 153
 154 theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)).
 155 intros.apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n)))).
 156 intro.elim n1.simplify.apply le_n_Sn.
 157 simplify.rewrite < minus_n_O.apply le_n.
 158 intros.simplify.apply le_n_Sn.
 159 intros.simplify.apply H.
 160 qed.
 161
 162 theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p.
 163 intros 3.simplify.intro.
 164 apply (trans_le (m-n) (S (m-(S n))) p).
 165 apply minus_le_S_minus_S.
 166 assumption.
 167 qed.
 168
 169 theorem le_minus_m: \forall n,m:nat. n-m \leq n.
 170 intros.apply (nat_elim2 (\lambda m,n. n-m \leq n)).
 171 intros.rewrite < minus_n_O.apply le_n.
 172 intros.simplify.apply le_n.
 173 intros.simplify.apply le_S.assumption.
 174 qed.
 175
 176 theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
 177 intros.apply (lt_O_n_elim n H).intro.
 178 apply (lt_O_n_elim m H1).intro.
 179 simplify.unfold lt.apply le_S_S.apply le_minus_m.
 180 qed.
 181
 182 theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
 183 intros 2.
 184 apply (nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m)).
 185 intros.apply le_O_n.
 186 simplify.intros. assumption.
 187 simplify.intros.apply le_S_S.apply H.assumption.
 188 qed.
 189
 190 (* galois *)
 191 theorem monotonic_le_minus_r:
 192 \forall p,q,n:nat. q \leq p \to n-p \le n-q.
 193 simplify.intros 2.apply (nat_elim2
 194 (\lambda p,q.\forall a.q \leq p \to a-p \leq a-q)).
 195 intros.apply (le_n_O_elim n H).apply le_n.
 196 intros.rewrite < minus_n_O.
 197 apply le_minus_m.
 198 intros.elim a.simplify.apply le_n.
 199 simplify.apply H.apply le_S_S_to_le.assumption.
 200 qed.
 201
 202 theorem le_minus_to_plus: \forall n,m,p. (le (n-m) p) \to (le n (p+m)).
 203 intros 2.apply (nat_elim2 (\lambda n,m.\forall p.(le (n-m) p) \to (le n (p+m)))).
 204 intros.apply le_O_n.
 205 simplify.intros.rewrite < plus_n_O.assumption.
 206 intros.
 207 rewrite < plus_n_Sm.
 208 apply le_S_S.apply H.
 209 exact H1.
 210 qed.
 211
 212 theorem le_plus_to_minus: \forall n,m,p. (le n (p+m)) \to (le (n-m) p).
 213 intros 2.apply (nat_elim2 (\lambda n,m.\forall p.(le n (p+m)) \to (le (n-m) p))).
 214 intros.simplify.apply le_O_n.
 215 intros 2.rewrite < plus_n_O.intro.simplify.assumption.
 216 intros.simplify.apply H.
 217 apply le_S_S_to_le.rewrite > plus_n_Sm.assumption.
 218 qed.
 219
 220 (* the converse of le_plus_to_minus does not hold *)
 221 theorem le_plus_to_minus_r: \forall n,m,p. (le (n+m) p) \to (le n (p-m)).
 222 intros 3.apply (nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m)))).
 223 intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
 224 intro.intro.cut (n=O).rewrite > Hcut.apply le_O_n.
 225 apply sym_eq. apply le_n_O_to_eq.
 226 apply (trans_le ? (n+(S n1))).
 227 rewrite < sym_plus.
 228 apply le_plus_n.assumption.
 229 intros.simplify.
 230 apply H.apply le_S_S_to_le.
 231 rewrite > plus_n_Sm.assumption.
 232 qed.
 233
 234 (* minus and lt - to be completed *)
 235 theorem lt_minus_l: \forall m,l,n:nat.
 236   l < m \to m \le n \to n - m < n - l.
 237 apply nat_elim2
 238   [intros.apply False_ind.apply (not_le_Sn_O ? H)
 239   |intros.rewrite < minus_n_O.
 240    autobatch
 241   |intros.
 242    generalize in match H2.
 243    apply (nat_case n1)
 244     [intros.apply False_ind.apply (not_le_Sn_O ? H3)
 245     |intros.simplify.
 246      apply H
 247       [
 248        apply lt_S_S_to_lt.
 249        assumption
 250       |apply le_S_S_to_le.assumption
 251       ]
 252     ]
 253   ]
 254 qed.
 255
 256 theorem lt_minus_r: \forall n,m,l:nat.
 257   n \le l \to l < m \to l -n < m -n.
 258 intro.elim n
 259   [applyS H1
 260   |rewrite > eq_minus_S_pred.
 261    rewrite > eq_minus_S_pred.
 262    apply lt_pred
 263     [unfold lt.apply le_plus_to_minus_r.applyS H1
 264     |apply H[autobatch|assumption]
 265     ]
 266   ]
 267 qed.
 268
 269 lemma lt_to_lt_O_minus : \forall m,n.
 270   n < m \to O < m - n.
 271 intros.
 272 unfold. apply le_plus_to_minus_r. unfold in H. rewrite > sym_plus.
 273 rewrite < plus_n_Sm.
 274 rewrite < plus_n_O.
 275 assumption.
 276 qed.
 277
 278 theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p).
 279 intros 3.apply (nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p))).
 280 intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
 281 simplify.intros.apply False_ind.apply (not_le_Sn_O n H).
 282 simplify.intros.unfold lt.
 283 apply le_S_S.
 284 rewrite < plus_n_Sm.
 285 apply H.apply H1.
 286 qed.
 287
 288 theorem lt_O_minus_to_lt: \forall a,b:nat.
 289 O \lt b-a \to a \lt b.
 290 intros.
 291 rewrite > (plus_n_O a).
 292 rewrite > (sym_plus a O).
 293 apply (lt_minus_to_plus O  a b).
 294 assumption.
 295 qed.
 296
 297 theorem lt_minus_to_lt_plus:
 298 \forall n,m,p. n - m < p \to n < m + p.
 299 intros 2.
 300 apply (nat_elim2 ? ? ? ? n m)
 301   [simplify.intros.autobatch.
 302   |intros 2.rewrite < minus_n_O.
 303    intro.assumption
 304   |intros.
 305    simplify.
 306    cut (n1 < m1+p)
 307     [autobatch
 308     |apply H.
 309      apply H1
 310     ]
 311   ]
 312 qed.
 313
 314 theorem lt_plus_to_lt_minus:
 315 \forall n,m,p. m \le n \to n < m + p \to n - m < p.
 316 intros 2.
 317 apply (nat_elim2 ? ? ? ? n m)
 318   [simplify.intros 3.
 319    apply (le_n_O_elim ? H).
 320    simplify.intros.assumption
 321   |simplify.intros.assumption.
 322   |intros.
 323    simplify.
 324    apply H
 325     [apply le_S_S_to_le.assumption
 326     |apply le_S_S_to_le.apply H2
 327     ]
 328   ]
 329 qed.
 330
 331 theorem minus_m_minus_mn: \forall n,m. n\le m \to n=m-(m-n).
 332 intros.
 333 apply sym_eq.
 334 apply plus_to_minus.
 335 autobatch.
 336 qed.
 337
 338 theorem distributive_times_minus: distributive nat times minus.
 339 unfold distributive.
 340 intros.
 341 apply ((leb_elim z y)).
 342   intro.cut (x*(y-z)+x*z = (x*y-x*z)+x*z).
 343     apply (inj_plus_l (x*z)).assumption.
 344     apply (trans_eq nat ? (x*y)).
 345       rewrite < distr_times_plus.rewrite < (plus_minus_m_m ? ? H).reflexivity.
 346       rewrite < plus_minus_m_m.
 347         reflexivity.
 348         apply le_times_r.assumption.
 349   intro.rewrite > eq_minus_n_m_O.
 350     rewrite > (eq_minus_n_m_O (x*y)).
 351       rewrite < sym_times.simplify.reflexivity.
 352         apply le_times_r.apply lt_to_le.apply not_le_to_lt.assumption.
 353         apply lt_to_le.apply not_le_to_lt.assumption.
 354 qed.
 355
 356 theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
 357 \def distributive_times_minus.
 358
 359 theorem eq_minus_plus_plus_minus: \forall n,m,p:nat. p \le m \to (n+m)-p = n+(m-p).
 360 intros.
 361 apply plus_to_minus.
 362 rewrite > sym_plus in \vdash (? ? ? %).
 363 rewrite > assoc_plus.
 364 rewrite < plus_minus_m_m.
 365 reflexivity.assumption.
 366 qed.
 367
 368 theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
 369 intros.
 370 cut (m+p \le n \or m+p \nleq n).
 371   elim Hcut.
 372     symmetry.apply plus_to_minus.
 373     rewrite > assoc_plus.rewrite > (sym_plus p).rewrite < plus_minus_m_m.
 374       rewrite > sym_plus.rewrite < plus_minus_m_m.
 375         reflexivity.
 376         apply (trans_le ? (m+p)).
 377           rewrite < sym_plus.apply le_plus_n.
 378           assumption.
 379       apply le_plus_to_minus_r.rewrite > sym_plus.assumption.
 380     rewrite > (eq_minus_n_m_O n (m+p)).
 381       rewrite > (eq_minus_n_m_O (n-m) p).
 382         reflexivity.
 383       apply le_plus_to_minus.apply lt_to_le. rewrite < sym_plus.
 384        apply not_le_to_lt. assumption.
 385     apply lt_to_le.apply not_le_to_lt.assumption.
 386   apply (decidable_le (m+p) n).
 387 qed.
 388
 389 theorem eq_plus_minus_minus_minus: \forall n,m,p:nat. p \le m \to m \le n \to
 390 p+(n-m) = n-(m-p).
 391 intros.
 392 apply sym_eq.
 393 apply plus_to_minus.
 394 rewrite < assoc_plus.
 395 rewrite < plus_minus_m_m.
 396 rewrite < sym_plus.
 397 rewrite < plus_minus_m_m.reflexivity.
 398 assumption.assumption.
 399 qed.