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