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