Changeset 350 for Deliverables/D4.1/Matita/Nat.ma
 Timestamp:
 Dec 1, 2010, 1:10:53 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/Nat.ma
r349 r350 37 37 38 38 interpretation "Nat less than or equal prop" 'less_than_or_equal n m = (less_than_or_equal_p n m). 39 interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m). 39 (*interpretation "Nat less than or equal bool" 'less_than_or_equal n m = (less_than_or_equal_b n m). 40 *) 40 41 41 42 ndefinition greater_than_or_equal_p: Nat → Nat → Prop ≝ … … 45 46 ndefinition greater_than_or_equal_b: ∀m, n: Nat. Bool ≝ 46 47 λm, n: Nat. 47 n ≤m.48 less_than_or_equal_b n m. 48 49 49 50 notation "hvbox(n break ≥ m)" … … 53 54 54 55 interpretation "Nat greater than or equal prop" 'greater_than_or_equal n m = (greater_than_or_equal_p n m). 55 interpretation "Nat greater than or equal bool" 'greater_than_or_equal n m = (greater_than_or_equal_b n m). 56 (*interpretation "Nat greater than or equal bool" 'greater_than_or_equal n m = (greater_than_or_equal_b n m). 57 *) 56 58 57 59 (* Add Boolean versions. *) … … 76 78 77 79 interpretation "Nat greater than prop" 'greater_than n m = (greater_than_p n m). 80 81 nlet rec less_than_b (m: Nat) (n: Nat) on m ≝ 82 match m with 83 [ Z ⇒ 84 match n with 85 [ Z ⇒ false 86  S o ⇒ true 87 ] 88  S o ⇒ 89 match n with 90 [ Z ⇒ false 91  S p ⇒ less_than_b o p 92 ] 93 ]. 94 95 (* interpretation "Nat less than bool" 'less_than n m = (less_than_b n m). *) 96 97 ndefinition greater_than_b ≝ 98 λm, n: Nat. 99 less_than_b n m. 100 101 (* interpretation "Nat greater than bool" 'greater_than n m = (greater_than_b n m). *) 78 102 79 103 (* ===================================== *) … … 125 149 126 150 nlet rec division_aux (m: Nat) (n : Nat) (p: Nat) ≝ 127 match n ≤p with151 match less_than_or_equal_b n p with 128 152 [ true ⇒ Z 129 153  false ⇒ … … 148 172 149 173 nlet rec modulus_aux (m: Nat) (n: Nat) (p: Nat) ≝ 150 match n ≤p with174 match less_than_or_equal_b n p with 151 175 [ true ⇒ n 152 176  false ⇒ … … 216 240 (m + n)  n = m. 217 241 218 n axiom less_than_or_equal_monotone:242 ntheorem less_than_or_equal_monotone: 219 243 ∀m, n: Nat. 220 244 m ≤ n → (S m) ≤ (S n). 221 222 naxiom succ_less_than_or_equal_injective: 245 #m n H; nelim H; /2/. 246 nqed. 247 248 nlemma trans_le: ∀n,m,l. n ≤ m → m ≤ l → n ≤ l. 249 #n m l H H1; nelim H1; /2/. 250 nqed. 251 252 ntheorem succ_less_than_or_equal_injective: 223 253 ∀m, n: Nat. 224 254 (S m) ≤ (S n) → m ≤ n. 255 #m n H; 256 nchange with (match S m with [ Z ⇒ Z  S x ⇒ x] ≤ match S n with [ Z ⇒ Z  S x ⇒ x]); 257 napply (match H return λx.λ_. m ≤ match x with [Z ⇒ Z  S x ⇒ x] with [ ltoe_refl ⇒ ?  ltoe_step y H ⇒ ? ]); 258 nnormalize; /3/. 259 nqed. 225 260 226 261 naxiom plus_minus_inverse_right: … … 228 263 (m  n) + n = m. 229 264 230 naxiom greater_than_b: Nat → Nat → Bool. 231 naxiom less_than_b: Nat → Nat → Bool. 232 233 naxiom succ_less_than_injective: 265 ntheorem succ_less_than_injective: 234 266 ∀m, n: Nat. 235 267 less_than_p (S m) (S n) → m < n. 236 237 naxiom nothing_less_than_Z: 268 /2/. 269 nqed. 270 271 nlemma not_less_than_S_Z: 272 ∀m,n: Nat. S m ≤ n → ¬ (n = Z). 273 #m n H; nelim H [ @; #K; ndestruct  #y H1 H2; @; #K; ndestruct ] 274 nqed. 275 276 ntheorem nothing_less_than_Z: 238 277 ∀m: Nat. 239 278 ¬(m < Z). 279 #m; @; #H; nlapply (not_less_than_S_Z m Z H); /2/; 280 nqed. 240 281 241 282 (* ===================================== *)
Note: See TracChangeset
for help on using the changeset viewer.