Changeset 330
 Timestamp:
 Nov 29, 2010, 2:08:52 PM (9 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVector.ma
r320 r330 195 195 false) b c. 196 196 197 naxiom plus_minus_inverse_left:198 ∀m, n: Nat.199 (m + n)  n = m.200 201 naxiom plus_minus_inverse_right:202 ∀m, n: Nat.203 (m  n) + n = m.204 205 naxiom greater_than_b: Nat → Nat → Bool.206 207 197 nlet rec bitvector_of_nat (n: Nat) (m: Nat): BitVector n ≝ 208 198 let biglist ≝ reverse ? (bitvector_of_nat_aux m) in 
Deliverables/D4.1/Matita/List.ma
r329 r330 103 103 #K; 104 104 ncases (K absd); 105 ## ncases (less_than_monoton); 106 107 105 ## nnormalize in p; 106 nnormalize; 107 napply (succ_less_than_or_equal_injective ? ?); 108 nassumption; 109 ##] 110 nqed. 111 108 112 nlet rec get_index_weak (A: Type[0]) (l: List A) (n: Nat) on n ≝ 109 113 match n with … … 116 120 match l with 117 121 [ Empty ⇒ Nothing A 118  Cons hd tl ⇒ get_index A tl o122  Cons hd tl ⇒ get_index_weak A tl o 119 123 ] 120 124 ]. 
Deliverables/D4.1/Matita/Nat.ma
r329 r330 209 209 210 210 (* ===================================== *) 211 (* Lemmas. *) 212 (* ===================================== *) 211 (* Axioms. *) 212 (* ===================================== *) 213 214 naxiom plus_minus_inverse_left: 215 ∀m, n: Nat. 216 (m + n)  n = m. 217 218 naxiom less_than_or_equal_monotone: 219 ∀m, n: Nat. 220 m ≤ n → (S m) ≤ (S n). 221 222 naxiom succ_less_than_or_equal_injective: 223 ∀m, n: Nat. 224 (S m) ≤ (S n) → m ≤ n. 225 226 naxiom plus_minus_inverse_right: 227 ∀m, n: Nat. 228 (m  n) + n = m. 229 230 naxiom greater_than_b: Nat → Nat → Bool. 213 231 214 232 naxiom succ_less_than_injective: … … 219 237 ∀m: Nat. 220 238 ¬(m < Z). 239 240 (* ===================================== *) 241 (* Lemmas. *) 242 (* ===================================== *) 221 243 222 244 nlemma less_than_or_equal_zero: … … 347 369 nnormalize. 348 370 nrewrite > H. 349 napply Ssucc_plus.371 napply succ_plus. 350 372 nqed. 351 373
Note: See TracChangeset
for help on using the changeset viewer.