# Changeset 2673 for src/ASM

Ignore:
Timestamp:
Feb 18, 2013, 1:18:02 PM (7 years ago)
Message:

corrected some compilation errors (that might depend on some matita update)

Location:
src/ASM
Files:
2 edited

Unmodified
Added
Removed
• ## src/ASM/Arithmetic.ma

 r2672 λn,v. nat_of_bitvector_aux n O v. (* TODO: remove when standard library arithmetics/exp.ma is used in place of definition in ASM/Util.ma *) theorem lt_O_exp: ∀n,m:nat. O < n → O < n^m. #n #m (elim m) normalize // #a #Hind #posn @(le_times 1 ? 1) /2 by / qed. theorem le_exp: ∀n,m,p:nat. O < p → n ≤m → p^n ≤ p^m. @nat_elim2 #n #m [#ltm #len @lt_O_exp // |#_ #len @False_ind /2 by absurd/ |#Hind #p #posp #lenm normalize @le_times // @Hind /2 by monotonic_pred/ ] qed. lemma nat_of_bitvector_aux_lt_bound: ∀n.∀v:BitVector n. ∀m,l:nat. #n #hd #tl #IH #m #l #B cases hd normalize nodelta @(transitive_le … (IH ? (S l) …)) [2,4: /2 by le_exp/ [2,4: change with (?≤2^(S (n+l))) @le_exp /2 by le_n/ |1,3: @(transitive_le … (2 * (S m))) [2,4: >commutative_times whd in ⊢ (??%); /2 by le_plus/ [2,4: /2 by le_times/ |3: // | 1: normalize
• ## src/ASM/Util.ma

 r2314 qed. (* let rec odd_p (n: nat) ] qed. *) lemma two_times_n_plus_one_refl_two_times_n_to_False: ∀m, n: nat. 2 * m + 1 = 2 * n → False. #m #n #assm cut (even_p (2 * n) ∧ even_p ((2 * m) + 1)) [1: >assm @conj @two_times_n_even_p |2: * #_ #absurd cases (even_p_to_not_odd_p … absurd) #assm @assm @two_times_n_plus_one_odd_p ] @nat_elim2 [ * [2: #n ] normalize [ commutative_times >commutative_times in ⊢ (???%→?); normalize ] #EQ destruct @IH >commutative_times >commutative_times in ⊢ (???%); assumption qed.
Note: See TracChangeset for help on using the changeset viewer.