Changeset 1516 for src/ASM/BitVector.ma
 Timestamp:
 Nov 19, 2011, 12:38:20 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/BitVector.ma
r990 r1516 29 29 30 30 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool. 31 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??)//31 #v lapply (refl … 0) cases v in ⊢ (??%? → ?%%??); // 32 32 #n #hd #tl #abs @⊥ destruct (abs) 33 33 qed. … … 35 35 lemma BitVector_Sn: ∀n.∀v:BitVector (S n). 36 36 ∃hd.∃tl.v ≃ VCons bool n hd tl. 37 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))37 #n #v lapply (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))); 38 38 [ #abs @⊥ destruct (abs) 39 39  #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ] … … 132 132 (x ≠ y → P false) → 133 133 P (eq_bv n x y). 134 #P #n #x #y #Ht #Hf whd in ⊢ (?%) @(eq_v_elim … Ht Hf)134 #P #n #x #y #Ht #Hf whd in ⊢ (?%); @(eq_v_elim … Ht Hf) 135 135 #Q * *; normalize /3/ 136 136 qed. … … 177 177 ∀n, v, q. 178 178 eq_bv n v q = true → v = q. 179 #n #v #q generalize in match v 179 #n #v #q generalize in match v; 180 180 elim q 181 181 [ #v #h @BitVector_O … … 184 184 #hd' * #tl' #jmeq >jmeq in h; 185 185 #new_h 186 change in new_h with ((andb ? ?) = ?);186 change in new_h; with ((andb ? ?) = ?); 187 187 cases(conjunction_true … new_h) 188 188 #eq_heads #eq_tails … … 190 190 cases(eq_b_eq … eq_heads) 191 191 whd in eq_tails:(??(?????(%))?); 192 change in eq_tails with (eq_bv ??? = ?);192 change in eq_tails; with (eq_bv ??? = ?); 193 193 <(ih tl') // 194 194 ]
Note: See TracChangeset
for help on using the changeset viewer.