matita/contribs/library_auto/auto/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 set "baseuri" "cic:/matita/library_autobatch/nat/minus".
  17
  18 include "auto/nat/le_arith.ma".
  19 include "auto/nat/compare.ma".
  20
  21 let rec minus n m \def
  22  match n with
  23  [ O \Rightarrow O
  24  | (S p) \Rightarrow
  25         match m with
  26         [O \Rightarrow (S p)
  27         | (S q) \Rightarrow minus p q ]].
  28
  29 (*CSC: the URI must disappear: there is a bug now *)
  30 interpretation "natural minus" 'minus x y = (cic:/matita/library_autobatch/nat/minus/minus.con x y).
  31
  32 theorem minus_n_O: \forall n:nat.n=n-O.
  33 intros.
  34 elim n;
  35 autobatch. (* applico autobatch su entrambi i goal aperti*)
  36 (*simplify;reflexivity.*)
  37 qed.
  38
  39 theorem minus_n_n: \forall n:nat.O=n-n.
  40 intros.
  41 elim n;simplify
  42 [ reflexivity
  43 | apply H
  44 ]
  45 qed.
  46
  47 theorem minus_Sn_n: \forall n:nat. S O = (S n)-n.
  48 intro.
  49 elim n
  50 [ autobatch
  51   (*simplify.reflexivity.*)
  52 | elim H.
  53   reflexivity
  54 ]
  55 qed.
  56
  57
  58 theorem minus_Sn_m: \forall n,m:nat. m \leq n \to (S n)-m = S (n-m).
  59 intros 2.
  60 apply (nat_elim2
  61 (\lambda n,m.m \leq n \to (S n)-m = S (n-m)));intros
  62 [ apply (le_n_O_elim n1 H).
  63   autobatch
  64   (*simplify.
  65   reflexivity.*)
  66 | autobatch
  67   (*simplify.
  68   reflexivity.*)
  69 | rewrite < H
  70   [ reflexivity
  71   | autobatch
  72     (*apply le_S_S_to_le.
  73     assumption.*)
  74   ]
  75 ]
  76 qed.
  77
  78 theorem plus_minus:
  79 \forall n,m,p:nat. m \leq n \to (n-m)+p = (n+p)-m.
  80 intros 2.
  81 apply (nat_elim2
  82 (\lambda n,m.\forall p:nat.m \leq n \to (n-m)+p = (n+p)-m));intros
  83 [ apply (le_n_O_elim ? H).
  84   autobatch
  85   (*simplify.
  86   rewrite < minus_n_O.
  87   reflexivity.*)
  88 | autobatch
  89   (*simplify.
  90   reflexivity.*)
  91 | simplify.
  92   autobatch
  93   (*apply H.
  94   apply le_S_S_to_le.
  95   assumption.*)
  96 ]
  97 qed.
  98
  99 theorem minus_plus_m_m: \forall n,m:nat.n = (n+m)-m.
 100 intros 2.
 101 generalize in match n.
 102 elim m
 103 [ rewrite < minus_n_O.
 104   apply plus_n_O.
 105 | elim n2
 106   [ autobatch
 107     (*simplify.
 108     apply minus_n_n.*)
 109   | rewrite < plus_n_Sm.
 110     change with (S n3 = (S n3 + n1)-n1).
 111     apply H
 112   ]
 113 ]
 114 qed.
 115
 116 theorem plus_minus_m_m: \forall n,m:nat.
 117 m \leq n \to n = (n-m)+m.
 118 intros 2.
 119 apply (nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m));intros
 120 [ apply (le_n_O_elim n1 H).
 121   reflexivity
 122 | autobatch
 123   (*simplify.
 124   rewrite < plus_n_O.
 125   reflexivity.*)
 126 | simplify.
 127   rewrite < sym_plus.
 128   simplify.
 129   apply eq_f.
 130   rewrite < sym_plus.
 131   autobatch
 132   (*apply H.
 133   apply le_S_S_to_le.
 134   assumption.*)
 135 ]
 136 qed.
 137
 138 theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to
 139 n = m+p.
 140 intros.apply (trans_eq ? ? ((n-m)+m));autobatch.
 141 (*[ apply plus_minus_m_m.
 142   apply H.
 143 | elim H1.
 144   apply sym_plus.
 145 ]*)
 146 qed.
 147
 148 theorem plus_to_minus :\forall n,m,p:nat.
 149 n = m+p \to n-m = p.
 150 intros.
 151 apply (inj_plus_r m).
 152 rewrite < H.
 153 rewrite < sym_plus.
 154 symmetry.
 155 autobatch.
 156 (*apply plus_minus_m_m.
 157 rewrite > H.
 158 rewrite > sym_plus.
 159 apply le_plus_n.*)
 160 qed.
 161
 162 theorem minus_S_S : \forall n,m:nat.
 163 eq nat (minus (S n) (S m)) (minus n m).
 164 intros.
 165 reflexivity.
 166 qed.
 167
 168 theorem minus_pred_pred : \forall n,m:nat. lt O n \to lt O m \to
 169 eq nat (minus (pred n) (pred m)) (minus n m).
 170 intros.
 171 apply (lt_O_n_elim n H).
 172 intro.
 173 apply (lt_O_n_elim m H1).
 174 intro.
 175 autobatch.
 176 (*simplify.reflexivity.*)
 177 qed.
 178
 179 theorem eq_minus_n_m_O: \forall n,m:nat.
 180 n \leq m \to n-m = O.
 181 intros 2.
 182 apply (nat_elim2 (\lambda n,m.n \leq m \to n-m = O));intros
 183 [ autobatch
 184   (*simplify.
 185   reflexivity.*)
 186 | apply False_ind.
 187   autobatch
 188   (*apply not_le_Sn_O.
 189   goal 15.*) (*prima goal 13*)
 190 (* effettuando un'esecuzione passo-passo, quando si arriva a dover
 191    considerare questa tattica, la finestra di dimostrazione scompare
 192    e viene generato il seguente errore:
 193    Uncaught exception: File "matitaMathView.ml", line 677, characters
 194    6-12: Assertion failed.
 195
 196    tuttavia l'esecuzione continua, ed il teorema viene comunque
 197    dimostrato.
 198  *)
 199   (*apply H.*)
 200 | simplify.
 201   autobatch
 202   (*apply H.
 203   apply le_S_S_to_le.
 204   apply H1.*)
 205 ]
 206 qed.
 207
 208 theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
 209 intros.
 210 elim H
 211 [ elim (minus_Sn_n n).apply le_n
 212 | rewrite > minus_Sn_m;autobatch
 213   (*apply le_S.assumption.
 214   apply lt_to_le.assumption.*)
 215 ]
 216 qed.
 217
 218 theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)).
 219 intros.apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n))));intros
 220 [ elim n1;simplify
 221   [ apply le_n_Sn.
 222   | rewrite < minus_n_O.
 223     apply le_n.
 224   ]
 225 | autobatch
 226   (*simplify.apply le_n_Sn.*)
 227 | simplify.apply H.
 228 ]
 229 qed.
 230
 231 theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p.
 232 intros 3.
 233 autobatch.
 234 (*simplify.
 235 intro.
 236 apply (trans_le (m-n) (S (m-(S n))) p).
 237 apply minus_le_S_minus_S.
 238 assumption.*)
 239 qed.
 240
 241 theorem le_minus_m: \forall n,m:nat. n-m \leq n.
 242 intros.apply (nat_elim2 (\lambda m,n. n-m \leq n));intros
 243 [ autobatch
 244   (*rewrite < minus_n_O.
 245   apply le_n.*)
 246 | autobatch
 247   (*simplify.
 248   apply le_n.*)
 249 | simplify.
 250   autobatch
 251   (*apply le_S.
 252   assumption.*)
 253 ]
 254 qed.
 255
 256 theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
 257 intros.
 258 apply (lt_O_n_elim n H).
 259 intro.
 260 apply (lt_O_n_elim m H1).
 261 intro.
 262 simplify.
 263 autobatch.
 264 (*unfold lt.
 265 apply le_S_S.
 266 apply le_minus_m.*)
 267 qed.
 268
 269 theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
 270 intros 2.
 271 apply (nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m))
 272 [ intros.
 273   apply le_O_n
 274 | simplify.
 275   intros.
 276   assumption
 277 | simplify.
 278   intros.
 279   autobatch
 280   (*apply le_S_S.
 281   apply H.
 282   assumption.*)
 283 ]
 284 qed.
 285
 286 (* galois *)
 287 theorem monotonic_le_minus_r:
 288 \forall p,q,n:nat. q \leq p \to n-p \le n-q.
 289 (*simplify*).
 290 intros 2.
 291 apply (nat_elim2
 292 (\lambda p,q.\forall a.q \leq p \to a-p \leq a-q));intros
 293 [ apply (le_n_O_elim n H).
 294   apply le_n.
 295 | rewrite < minus_n_O.
 296   apply le_minus_m.
 297 | elim a
 298   [ autobatch
 299     (*simplify.
 300     apply le_n.*)
 301   | simplify.
 302     autobatch
 303     (*apply H.
 304     apply le_S_S_to_le.
 305     assumption.*)
 306   ]
 307 ]
 308 qed.
 309
 310 theorem le_minus_to_plus: \forall n,m,p. (le (n-m) p) \to (le n (p+m)).
 311 intros 2.
 312 apply (nat_elim2 (\lambda n,m.\forall p.(le (n-m) p) \to (le n (p+m))));intros
 313 [ apply le_O_n.
 314 | rewrite < plus_n_O.
 315   assumption.
 316 | rewrite < plus_n_Sm.
 317   apply le_S_S.
 318   apply H.
 319   exact H1.
 320 ]
 321 qed.
 322
 323 theorem le_plus_to_minus: \forall n,m,p. (le n (p+m)) \to (le (n-m) p).
 324 intros 2.
 325 apply (nat_elim2 (\lambda n,m.\forall p.(le n (p+m)) \to (le (n-m) p)))
 326 [ intros.
 327   autobatch
 328   (*simplify.
 329   apply le_O_n.*)
 330 | intros 2.
 331   rewrite < plus_n_O.
 332   autobatch
 333   (*intro.
 334   simplify.
 335   assumption.*)
 336 | intros.
 337   simplify.
 338   apply H.
 339   apply le_S_S_to_le.
 340   rewrite > plus_n_Sm.
 341   assumption
 342 ]
 343 qed.
 344
 345 (* the converse of le_plus_to_minus does not hold *)
 346 theorem le_plus_to_minus_r: \forall n,m,p. (le (n+m) p) \to (le n (p-m)).
 347 intros 3.
 348 apply (nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m))));intro
 349 [ rewrite < plus_n_O.
 350   rewrite < minus_n_O.
 351   autobatch
 352   (*intro.
 353   assumption.*)
 354 | intro.
 355   cut (n=O)
 356   [ autobatch
 357     (*rewrite > Hcut.
 358     apply le_O_n.*)
 359   | apply sym_eq.
 360     apply le_n_O_to_eq.
 361     autobatch
 362     (*apply (trans_le ? (n+(S n1)))
 363     [ rewrite < sym_plus.
 364       apply le_plus_n
 365     | assumption
 366     ]*)
 367   ]
 368 | intros.
 369   simplify.
 370   apply H.
 371   apply le_S_S_to_le.
 372   rewrite > plus_n_Sm.
 373   assumption
 374 ]
 375 qed.
 376
 377 (* minus and lt - to be completed *)
 378 theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p).
 379 intros 3.
 380 apply (nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p)))
 381 [ intro.
 382   rewrite < plus_n_O.
 383   rewrite < minus_n_O.
 384   autobatch
 385   (*intro.
 386   assumption.*)
 387 | simplify.
 388   intros.
 389   apply False_ind.
 390   apply (not_le_Sn_O n H)
 391 | (*simplify.*)
 392   intros.
 393   unfold lt.
 394   apply le_S_S.
 395   rewrite < plus_n_Sm.
 396   autobatch
 397   (*apply H.
 398   apply H1.*)
 399 ]
 400 qed.
 401
 402 theorem distributive_times_minus: distributive nat times minus.
 403 unfold distributive.
 404 intros.
 405 apply ((leb_elim z y));intro
 406 [ cut (x*(y-z)+x*z = (x*y-x*z)+x*z)
 407     [ autobatch
 408       (*apply (inj_plus_l (x*z)).
 409       assumption.*)
 410     | apply (trans_eq nat ? (x*y))
 411       [ rewrite < distr_times_plus.
 412         autobatch
 413         (*rewrite < (plus_minus_m_m ? ? H).
 414         reflexivity.*)
 415       | rewrite < plus_minus_m_m;autobatch
 416         (*[ reflexivity.
 417         | apply le_times_r.
 418           assumption.
 419         ]*)
 420       ]
 421     ]
 422 | rewrite > eq_minus_n_m_O
 423   [ rewrite > (eq_minus_n_m_O (x*y))
 424     [ autobatch
 425       (*rewrite < sym_times.
 426       simplify.
 427       reflexivity.*)
 428     | apply le_times_r.
 429       apply lt_to_le.
 430       autobatch
 431       (*apply not_le_to_lt.
 432       assumption.*)
 433     ]
 434   | autobatch
 435     (*apply lt_to_le.
 436     apply not_le_to_lt.
 437     assumption.*)
 438   ]
 439 ]
 440 qed.
 441
 442 theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
 443 \def distributive_times_minus.
 444
 445 theorem eq_minus_plus_plus_minus: \forall n,m,p:nat. p \le m \to (n+m)-p = n+(m-p).
 446 intros.
 447 apply plus_to_minus.
 448 rewrite > sym_plus in \vdash (? ? ? %).
 449 rewrite > assoc_plus.
 450 autobatch.
 451 (*rewrite < plus_minus_m_m.
 452 reflexivity.
 453 assumption.
 454 *)
 455 qed.
 456
 457 theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
 458 intros.
 459 cut (m+p \le n \or m+p \nleq n)
 460 [ elim Hcut
 461   [ symmetry.
 462     apply plus_to_minus.
 463     rewrite > assoc_plus.
 464     rewrite > (sym_plus p).
 465     rewrite < plus_minus_m_m
 466     [ rewrite > sym_plus.
 467       rewrite < plus_minus_m_m ; autobatch
 468       (*[ reflexivity.
 469       | apply (trans_le ? (m+p))
 470         [ rewrite < sym_plus.
 471           apply le_plus_n
 472         | assumption
 473         ]
 474       ]*)
 475     | apply le_plus_to_minus_r.
 476       rewrite > sym_plus.
 477       assumption.
 478     ]
 479   | rewrite > (eq_minus_n_m_O n (m+p))
 480     [ rewrite > (eq_minus_n_m_O (n-m) p)
 481       [ reflexivity
 482       | apply le_plus_to_minus.
 483         apply lt_to_le.
 484         rewrite < sym_plus.
 485         autobatch
 486         (*apply not_le_to_lt.
 487         assumption.*)
 488       ]
 489     | autobatch
 490       (*apply lt_to_le.
 491       apply not_le_to_lt.
 492       assumption.*)
 493     ]
 494   ]
 495 | apply (decidable_le (m+p) n)
 496 ]
 497 qed.
 498
 499 theorem eq_plus_minus_minus_minus: \forall n,m,p:nat. p \le m \to m \le n \to
 500 p+(n-m) = n-(m-p).
 501 intros.
 502 apply sym_eq.
 503 apply plus_to_minus.
 504 rewrite < assoc_plus.
 505 rewrite < plus_minus_m_m;
 506 [ rewrite < sym_plus.
 507   autobatch
 508   (*rewrite < plus_minus_m_m
 509   [ reflexivity
 510   | assumption
 511   ]*)
 512 | assumption
 513 ]
 514 qed.