Changeset 2673 for src/ASM/Arithmetic.ma


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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r2672 r2673  
    162162  λn,v. nat_of_bitvector_aux n O v.
    163163
     164(* TODO: remove when standard library arithmetics/exp.ma is used in place
     165   of definition in ASM/Util.ma *)
     166theorem 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.
     169theorem 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  ]
     176qed.
     177
    164178lemma nat_of_bitvector_aux_lt_bound:
    165179 ∀n.∀v:BitVector n. ∀m,l:nat.
     
    168182 #n #hd #tl #IH #m #l #B cases hd normalize nodelta
    169183 @(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/
    171185 |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/
    173187  |3: // | 1: normalize <plus_n_O <plus_n_Sm // ]]
    174188qed. 
Note: See TracChangeset for help on using the changeset viewer.