matita/matita/contribs/lambda_delta/Ground_2/arith.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "arithmetics/nat.ma".
  16 include "Ground_2/star.ma".
  17
  18 (* ARITHMETICAL PROPERTIES **************************************************)
  19
  20 lemma false_lt_to_le: ∀x,y. (x < y → False) → y ≤ x.
  21 #x #y #H elim (decidable_lt x y) /2 width=1/
  22 #Hxy elim (H Hxy)
  23 qed-.
  24
  25 axiom eq_nat_dec: ∀n1,n2:nat. Decidable (n1 = n2).
  26
  27 axiom lt_dec: ∀n1,n2. Decidable (n1 < n2).
  28
  29 lemma plus_S_eq_O_false: ∀n,m. n + S m = 0 → False.
  30 #n #m <plus_n_Sm #H destruct
  31 qed-.
  32
  33 lemma plus_S_le_to_pos: ∀n,m,p. n + S m ≤ p → 0 < p.
  34 #n #m #p <plus_n_Sm #H @(lt_to_le_to_lt … H) //
  35 qed.
  36
  37 lemma minus_le: ∀m,n. m - n ≤ m.
  38 /2 width=1/ qed.
  39
  40 lemma le_O_to_eq_O: ∀n. n ≤ 0 → n = 0.
  41 /2 width=1/ qed.
  42
  43 lemma lt_to_le: ∀a,b. a < b → a ≤ b.
  44 /2 width=2/ qed.
  45
  46 lemma lt_refl_false: ∀n. n < n → False.
  47 #n #H elim (lt_to_not_eq … H) -H /2 width=1/
  48 qed-.
  49
  50 lemma lt_zero_false: ∀n. n < 0 → False.
  51 #n #H elim (lt_to_not_le … H) -H /2 width=1/
  52 qed-.
  53
  54 lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
  55 #m #n elim (decidable_lt m n) /2 width=1/ /3 width=1/
  56 qed.
  57
  58 lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
  59 #m elim m -m
  60 [ * /2 width=1/
  61 | #m #IHm * /2 width=1/
  62   #n elim (IHm n) -IHm #H
  63   [ @or3_intro0 | @or3_intro1 destruct | @or3_intro2 ] // /2 width=1/ (**) (* /3 width=1/ is slow *)
  64 qed.
  65
  66 lemma le_to_lt_or_eq: ∀m,n. m ≤ n → m < n ∨ m = n.
  67 /2 width=1/ qed. (**) (* REMOVE: this is le_to_or_lt_eq *)
  68
  69 lemma plus_le_weak: ∀m,n,p. m + n ≤ p → n ≤ p.
  70 /2 width=2/ qed.
  71
  72 lemma plus_lt_false: ∀m,n. m + n < m → False.
  73 #m #n #H1 lapply (le_plus_n_r n m) #H2
  74 lapply (le_to_lt_to_lt … H2 H1) -H2 -H1 #H
  75 elim (lt_refl_false … H)
  76 qed-.
  77
  78 lemma le_fwd_plus_plus_ge: ∀m1,m2. m2 ≤ m1 → ∀n1,n2. m1 + n1 ≤ m2 + n2 → n1 ≤ n2.
  79 #m1 #m2 #H elim H -m1
  80 [ /2 width=2/
  81 | #m1 #_ #IHm1 #n1 #n2 #H @IHm1 /2 width=1/
  82 ]
  83 qed.
  84
  85 lemma monotonic_lt_minus_l: ∀p,q,n. n ≤ q → q < p → q - n < p - n.
  86 #p #q #n #H1 #H2
  87 @lt_plus_to_minus_r <plus_minus_m_m //.
  88 qed.
  89
  90 lemma plus_le_minus: ∀a,b,c. a + b ≤ c → a ≤ c - b.
  91 /2 width=1/ qed.
  92
  93 lemma lt_plus_minus: ∀i,u,d. u ≤ i → i < d + u → i - u < d.
  94 /2 width=1/ qed.
  95
  96 lemma plus_plus_comm_23: ∀m,n,p. m + n + p = m + p + n.
  97 // qed.
  98
  99 lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n.
 100 #n #m #p #lepm @plus_to_minus <associative_plus
 101 >(commutative_plus p) <plus_minus_m_m //
 102 qed.
 103
 104 lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
 105 #b elim b -b
 106 [ #c #a #H >(le_O_to_eq_O … H) -H //
 107 | #b #IHb #c elim c -c //
 108   #c #_ #a #Hcb
 109   lapply (le_S_S_to_le … Hcb) -Hcb #Hcb
 110   <plus_n_Sm normalize /2 width=1/
 111 ]
 112 qed.
 113
 114 lemma minus_plus_comm: ∀a,b,c. a - b - c = a - (c + b).
 115 // qed.
 116
 117 lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
 118 /3 width=1/ qed.
 119
 120 lemma le_plus_minus: ∀a,b,c. c ≤ b → a + b - c = a + (b - c).
 121 /2 width=1/ qed.
 122
 123 lemma plus_minus_m_m_comm: ∀n,m. m ≤ n → n = m + (n - m).
 124 /2 width=1/ qed.
 125
 126 lemma minus_plus_m_m_comm: ∀n,m. n = (m + n) - m.
 127 /2 width=1/ qed.
 128
 129 lemma arith_a2: ∀a,c1,c2. c1 + c2 ≤ a → a - c1 - c2 + (c1 + c2) = a.
 130 /2 width=1/ qed.
 131
 132 lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
 133 #a #b #c1 #H >minus_plus @eq_f2 /2 width=1/
 134 qed.
 135
 136 lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
 137 #a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1/
 138 qed.
 139
 140 lemma arith_c1: ∀a,b,c1. a + c1 - (b + c1) = a - b.
 141 // qed.
 142
 143 lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b.
 144 #x #a #b #c1 >plus_plus_comm_23 //
 145 qed.
 146
 147 lemma arith_d1: ∀a,b,c1. c1 ≤ b → a + c1 + (b - c1) = a + b.
 148 /2 width=1/ qed.
 149
 150 lemma arith_e2: ∀a,c1,c2. a ≤ c1 → c1 + c2 - (c1 - a + c2) = a.
 151 /3 width=1/ qed.
 152
 153 lemma arith_f1: ∀a,b,c1. a + b ≤ c1 → c1 - (c1 - a - b) = a + b.
 154 #a #b #c1 #H >minus_plus <minus_minus //
 155 qed.
 156
 157 lemma arith_g1: ∀a,b,c1. c1 ≤ b → a - (b - c1) - c1 = a - b.
 158 /2 width=1/ qed.
 159
 160 lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b →
 161                 a1 - c1 + a2 - (b - c1) = a1 + a2 - b.
 162 #a1 #a2 #b #c1 #H1 #H2 <le_plus_minus_comm /2 width=1/
 163 qed.
 164
 165 lemma arith_i2: ∀a,c1,c2. c1 + c2 ≤ a → c1 + c2 + (a - c1 - c2) = a.
 166 /2 width=1/ qed.
 167
 168 lemma arith_z1: ∀a,b,c1. a + c1 - b - c1 = a - b.
 169 // qed.
 170
 171 (* unstable *****************************************************************)
 172
 173 lemma arith1: ∀n,h,m,p. n + h + m ≤ p + h → n + m ≤ p.
 174 /2 width=2/ qed.
 175
 176 lemma arith2: ∀j,i,e,d. d + e ≤ i → d ≤ i - e + j.
 177 #j #i #e #d #H lapply (plus_le_minus … H) -H /2 width=3/
 178 qed.
 179
 180 lemma arith3: ∀a1,a2,b,c1. a1 + a2 ≤ b → a1 + c1 + a2 ≤ b + c1.
 181 /2 width=1/ qed.
 182
 183 lemma arith4: ∀h,d,e1,e2. d ≤ e1 + e2 → d + h ≤ e1 + h + e2.
 184 /2 width=1/ qed.
 185
 186 lemma arith5: ∀a,b1,b2,c1. c1 ≤ b1 → c1 ≤ a → a < b1 + b2 → a - c1 < b1 - c1 + b2.
 187 #a #b1 #b2 #c1 #H1 #H2 #H3
 188 <le_plus_minus_comm // @monotonic_lt_minus_l //
 189 qed.
 190
 191 lemma arith8: ∀a,b. a < a + b + 1.
 192 // qed.
 193
 194 lemma arith9: ∀a,b,c. c < a + (b + c + 1) + 1.
 195 // qed.
 196
 197 lemma arith10: ∀a,b,c,d,e. a ≤ b → c + (a - d - e) ≤ c + (b - d - e).
 198 #a #b #c #d #e #H
 199 >minus_plus >minus_plus @monotonic_le_plus_r @monotonic_le_minus_l //
 200 qed.