Changeset 961 for src/ASM/Vector.ma


Ignore:
Timestamp:
Jun 15, 2011, 4:15:52 PM (8 years ago)
Author:
campbell
Message:

Use precise bitvector sizes throughout the front end, rather than 32bits
everywhere.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Vector.ma

    r889 r961  
    477477] qed.
    478478
     479lemma eq_v_true : ∀A,f. (∀a. f a a = true) → ∀n,v. eq_v A n f v v = true.
     480#A #f #f_true #n #v elim v
     481[ //
     482| #m #h #t #IH whd in ⊢ (??%%) >f_true >IH @refl
     483] qed.
     484
     485lemma vector_neq_tail : ∀A,n,h. ∀t,t':Vector A n. h:::t≠h:::t' → t ≠ t'.
     486#A #n #h #t #t' * #NE % #E @NE >E @refl
     487qed.
     488
     489lemma  eq_v_false : ∀A,f. (∀a,a'. f a a' = true → a = a') → ∀n,v,v'. v≠v' → eq_v A n f v v' = false.
     490#A #f #f_true #n elim n
     491[ #v #v' @(vector_inv_n ??? v) @(vector_inv_n ??? v') * #H @False_ind @H @refl
     492| #m #IH #v #v' @(vector_inv_n ??? v) #h #t @(vector_inv_n ??? v') #h' #t'
     493  #NE normalize lapply (f_true h h') cases (f h h') // #E @IH >E in NE /2/
     494] qed.
     495
    479496(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    480497(* Subvectors.                                                                *)
Note: See TracChangeset for help on using the changeset viewer.