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