Changeset 2673


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)

Location:
src
Files:
3 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. 
  • src/ASM/Util.ma

    r2314 r2673  
    11351135qed.
    11361136
     1137(*
    11371138let rec odd_p
    11381139  (n: nat)
     
    12611262  ]
    12621263qed.
     1264*)
    12631265
    12641266lemma two_times_n_plus_one_refl_two_times_n_to_False:
    12651267  ∀m, n: nat.
    12661268    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
    12801275qed.
    12811276
  • src/common/PositiveMap.ma

    r2599 r2673  
    22include "utilities/binary/positive.ma".
    33include "ASM/Util.ma". (* bool_to_Prop *)
     4include "utilities/option.ma".
    45
    56inductive positive_map (A:Type[0]) : Type[0] ≝
     
    419420  ]
    420421] qed.
    421 
    422 include "utilities/option.ma".
    423422
    424423definition is_none : ∀A.option A → bool ≝ λA,o.match o with [ None ⇒ true | _ ⇒ false ].
Note: See TracChangeset for help on using the changeset viewer.