helm/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 plus_minus:
  61 \forall n,m,p:nat. m \leq n \to (n-m)+p = (n+p)-m.
  62 intros 2.
  63 apply (nat_elim2
  64 (\lambda n,m.\forall p:nat.m \leq n \to (n-m)+p = (n+p)-m)).
  65 intros.apply (le_n_O_elim ? H).
  66 simplify.rewrite < minus_n_O.reflexivity.
  67 intros.simplify.reflexivity.
  68 intros.simplify.apply H.apply le_S_S_to_le.assumption.
  69 qed.
  70
  71 theorem minus_plus_m_m: \forall n,m:nat.n = (n+m)-m.
  72 intros 2.
  73 generalize in match n.
  74 elim m.
  75 rewrite < minus_n_O.apply plus_n_O.
  76 elim n2.simplify.
  77 apply minus_n_n.
  78 rewrite < plus_n_Sm.
  79 change with (S n3 = (S n3 + n1)-n1).
  80 apply H.
  81 qed.
  82
  83 theorem plus_minus_m_m: \forall n,m:nat.
  84 m \leq n \to n = (n-m)+m.
  85 intros 2.
  86 apply (nat_elim2 (\lambda n,m.m \leq n \to n = (n-m)+m)).
  87 intros.apply (le_n_O_elim n1 H).
  88 reflexivity.
  89 intros.simplify.rewrite < plus_n_O.reflexivity.
  90 intros.simplify.rewrite < sym_plus.simplify.
  91 apply eq_f.rewrite < sym_plus.apply H.
  92 apply le_S_S_to_le.assumption.
  93 qed.
  94
  95 theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to
  96 n = m+p.
  97 intros.apply (trans_eq ? ? ((n-m)+m)).
  98 apply plus_minus_m_m.
  99 apply H.elim H1.
 100 apply sym_plus.
 101 qed.
 102
 103 theorem plus_to_minus :\forall n,m,p:nat.
 104 n = m+p \to n-m = p.
 105 intros.
 106 apply (inj_plus_r m).
 107 rewrite < H.
 108 rewrite < sym_plus.
 109 symmetry.
 110 apply plus_minus_m_m.rewrite > H.
 111 rewrite > sym_plus.
 112 apply le_plus_n.
 113 qed.
 114
 115 theorem minus_S_S : \forall n,m:nat.
 116 eq nat (minus (S n) (S m)) (minus n m).
 117 intros.
 118 reflexivity.
 119 qed.
 120
 121 theorem minus_pred_pred : \forall n,m:nat. lt O n \to lt O m \to
 122 eq nat (minus (pred n) (pred m)) (minus n m).
 123 intros.
 124 apply (lt_O_n_elim n H).intro.
 125 apply (lt_O_n_elim m H1).intro.
 126 simplify.reflexivity.
 127 qed.
 128
 129 theorem eq_minus_n_m_O: \forall n,m:nat.
 130 n \leq m \to n-m = O.
 131 intros 2.
 132 apply (nat_elim2 (\lambda n,m.n \leq m \to n-m = O)).
 133 intros.simplify.reflexivity.
 134 intros.apply False_ind.
 135 apply not_le_Sn_O.
 136 goal 13.apply H.
 137 intros.
 138 simplify.apply H.apply le_S_S_to_le. apply H1.
 139 qed.
 140
 141 theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
 142 intros.elim H.elim (minus_Sn_n n).apply le_n.
 143 rewrite > minus_Sn_m.
 144 apply le_S.assumption.
 145 apply lt_to_le.assumption.
 146 qed.
 147
 148 theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)).
 149 intros.apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n)))).
 150 intro.elim n1.simplify.apply le_n_Sn.
 151 simplify.rewrite < minus_n_O.apply le_n.
 152 intros.simplify.apply le_n_Sn.
 153 intros.simplify.apply H.
 154 qed.
 155
 156 theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p.
 157 intros 3.simplify.intro.
 158 apply (trans_le (m-n) (S (m-(S n))) p).
 159 apply minus_le_S_minus_S.
 160 assumption.
 161 qed.
 162
 163 theorem le_minus_m: \forall n,m:nat. n-m \leq n.
 164 intros.apply (nat_elim2 (\lambda m,n. n-m \leq n)).
 165 intros.rewrite < minus_n_O.apply le_n.
 166 intros.simplify.apply le_n.
 167 intros.simplify.apply le_S.assumption.
 168 qed.
 169
 170 theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
 171 intros.apply (lt_O_n_elim n H).intro.
 172 apply (lt_O_n_elim m H1).intro.
 173 simplify.apply le_S_S.apply le_minus_m.
 174 qed.
 175
 176 theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
 177 intros 2.
 178 apply (nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m)).
 179 intros.apply le_O_n.
 180 simplify.intros. assumption.
 181 simplify.intros.apply le_S_S.apply H.assumption.
 182 qed.
 183
 184 (* galois *)
 185 theorem monotonic_le_minus_r:
 186 \forall p,q,n:nat. q \leq p \to n-p \le n-q.
 187 simplify.intros 2.apply (nat_elim2
 188 (\lambda p,q.\forall a.q \leq p \to a-p \leq a-q)).
 189 intros.apply (le_n_O_elim n H).apply le_n.
 190 intros.rewrite < minus_n_O.
 191 apply le_minus_m.
 192 intros.elim a.simplify.apply le_n.
 193 simplify.apply H.apply le_S_S_to_le.assumption.
 194 qed.
 195
 196 theorem le_minus_to_plus: \forall n,m,p. (le (n-m) p) \to (le n (p+m)).
 197 intros 2.apply (nat_elim2 (\lambda n,m.\forall p.(le (n-m) p) \to (le n (p+m)))).
 198 intros.apply le_O_n.
 199 simplify.intros.rewrite < plus_n_O.assumption.
 200 intros.
 201 rewrite < plus_n_Sm.
 202 apply le_S_S.apply H.
 203 exact H1.
 204 qed.
 205
 206 theorem le_plus_to_minus: \forall n,m,p. (le n (p+m)) \to (le (n-m) p).
 207 intros 2.apply (nat_elim2 (\lambda n,m.\forall p.(le n (p+m)) \to (le (n-m) p))).
 208 intros.simplify.apply le_O_n.
 209 intros 2.rewrite < plus_n_O.intro.simplify.assumption.
 210 intros.simplify.apply H.
 211 apply le_S_S_to_le.rewrite > plus_n_Sm.assumption.
 212 qed.
 213
 214 (* the converse of le_plus_to_minus does not hold *)
 215 theorem le_plus_to_minus_r: \forall n,m,p. (le (n+m) p) \to (le n (p-m)).
 216 intros 3.apply (nat_elim2 (\lambda m,p.(le (n+m) p) \to (le n (p-m)))).
 217 intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
 218 intro.intro.cut (n=O).rewrite > Hcut.apply le_O_n.
 219 apply sym_eq. apply le_n_O_to_eq.
 220 apply (trans_le ? (n+(S n1))).
 221 rewrite < sym_plus.
 222 apply le_plus_n.assumption.
 223 intros.simplify.
 224 apply H.apply le_S_S_to_le.
 225 rewrite > plus_n_Sm.assumption.
 226 qed.
 227
 228
 229 theorem distributive_times_minus: distributive nat times minus.
 230 simplify.
 231 intros.
 232 apply ((leb_elim z y)).
 233   intro.cut (x*(y-z)+x*z = (x*y-x*z)+x*z).
 234     apply (inj_plus_l (x*z)).assumption.
 235     apply (trans_eq nat ? (x*y)).
 236       rewrite < distr_times_plus.rewrite < (plus_minus_m_m ? ? H).reflexivity.
 237       rewrite < plus_minus_m_m.
 238         reflexivity.
 239         apply le_times_r.assumption.
 240   intro.rewrite > eq_minus_n_m_O.
 241     rewrite > (eq_minus_n_m_O (x*y)).
 242       rewrite < sym_times.simplify.reflexivity.
 243         apply le_times_r.apply lt_to_le.apply not_le_to_lt.assumption.
 244         apply lt_to_le.apply not_le_to_lt.assumption.
 245 qed.
 246
 247 theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
 248 \def distributive_times_minus.
 249
 250 theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
 251 intros.
 252 cut (m+p \le n \or m+p \nleq n).
 253   elim Hcut.
 254     symmetry.apply plus_to_minus.
 255     rewrite > assoc_plus.rewrite > (sym_plus p).rewrite < plus_minus_m_m.
 256       rewrite > sym_plus.rewrite < plus_minus_m_m.
 257         reflexivity.
 258         apply (trans_le ? (m+p)).
 259           rewrite < sym_plus.apply le_plus_n.
 260           assumption.
 261       apply le_plus_to_minus_r.rewrite > sym_plus.assumption.
 262     rewrite > (eq_minus_n_m_O n (m+p)).
 263       rewrite > (eq_minus_n_m_O (n-m) p).
 264         reflexivity.
 265       apply le_plus_to_minus.apply lt_to_le. rewrite < sym_plus.
 266        apply not_le_to_lt. assumption.
 267     apply lt_to_le.apply not_le_to_lt.assumption.
 268   apply (decidable_le (m+p) n).
 269 qed.
 270
 271 theorem eq_plus_minus_minus_minus: \forall n,m,p:nat. p \le m \to m \le n \to
 272 p+(n-m) = n-(m-p).
 273 intros.
 274 apply sym_eq.
 275 apply plus_to_minus.
 276 rewrite < assoc_plus.
 277 rewrite < plus_minus_m_m.
 278 rewrite < sym_plus.
 279 rewrite < plus_minus_m_m.reflexivity.
 280 assumption.assumption.
 281 qed.