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