 Timestamp:
 Feb 18, 2013, 1:18:02 PM (7 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r2672 r2673 162 162 λn,v. nat_of_bitvector_aux n O v. 163 163 164 (* TODO: remove when standard library arithmetics/exp.ma is used in place 165 of definition in ASM/Util.ma *) 166 theorem lt_O_exp: ∀n,m:nat. O < n → O < n^m. 167 #n #m (elim m) normalize // #a #Hind #posn 168 @(le_times 1 ? 1) /2 by / qed. 169 theorem le_exp: ∀n,m,p:nat. O < p → 170 n ≤m → p^n ≤ p^m. 171 @nat_elim2 #n #m 172 [#ltm #len @lt_O_exp // 173 #_ #len @False_ind /2 by absurd/ 174 #Hind #p #posp #lenm normalize @le_times // @Hind /2 by monotonic_pred/ 175 ] 176 qed. 177 164 178 lemma nat_of_bitvector_aux_lt_bound: 165 179 ∀n.∀v:BitVector n. ∀m,l:nat. … … 168 182 #n #hd #tl #IH #m #l #B cases hd normalize nodelta 169 183 @(transitive_le … (IH ? (S l) …)) 170 [2,4: /2 by le_exp/184 [2,4: change with (?≤2^(S (n+l))) @le_exp /2 by le_n/ 171 185 1,3: @(transitive_le … (2 * (S m))) 172 [2,4: >commutative_times whd in ⊢ (??%); /2 by le_plus/186 [2,4: /2 by le_times/ 173 187 3: //  1: normalize <plus_n_O <plus_n_Sm // ]] 174 188 qed. 
src/ASM/Util.ma
r2314 r2673 1135 1135 qed. 1136 1136 1137 (* 1137 1138 let rec odd_p 1138 1139 (n: nat) … … 1261 1262 ] 1262 1263 qed. 1264 *) 1263 1265 1264 1266 lemma two_times_n_plus_one_refl_two_times_n_to_False: 1265 1267 ∀m, n: nat. 1266 1268 2 * m + 1 = 2 * n → False. 1267 #m #n 1268 #assm 1269 cut (even_p (2 * n) ∧ even_p ((2 * m) + 1)) 1270 [1: 1271 >assm 1272 @conj 1273 @two_times_n_even_p 1274 2: 1275 * #_ #absurd 1276 cases (even_p_to_not_odd_p … absurd) 1277 #assm @assm 1278 @two_times_n_plus_one_odd_p 1279 ] 1269 @nat_elim2 1270 [ * [2: #n ] normalize [ <plus_n_Sm ] 1271  #n normalize 1272  #n #m #IH >commutative_times >commutative_times in ⊢ (???%→?); normalize 1273 ] #EQ destruct @IH 1274 >commutative_times >commutative_times in ⊢ (???%); assumption 1280 1275 qed. 1281 1276
Note: See TracChangeset
for help on using the changeset viewer.