Changeset 2565 for src/Clight/frontend_misc.ma
 Timestamp:
 Dec 19, 2012, 6:11:23 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/frontend_misc.ma
r2510 r2565 149 149  2: * #Habsurd @(False_ind … (Habsurd … (refl ? i))) ] 150 150 qed. 151 152 lemma intsize_eq_inversion : 153 ∀sz,sz'. 154 ∀A:Type[0]. 155 ∀ok,not_ok. 156 intsize_eq_elim' sz sz' (λsz,sz'. res A) 157 (OK ? ok) 158 (Error ? not_ok) = (OK ? ok) → 159 sz = sz'. 160 * * try // normalize 161 #A #ok #not_ok #Habsurd destruct 162 qed. 163 164 lemma intsize_eq_elim_dec : 165 ∀sz1,sz2. 166 ∀P: ∀sz1,sz2. Type[0]. 167 ((∀ifok,iferr. intsize_eq_elim' sz1 sz1 P ifok iferr = ifok) ∧ sz1 = sz2) ∨ 168 ((∀ifok,iferr. intsize_eq_elim' sz1 sz2 P ifok iferr = iferr) ∧ sz1 ≠ sz2). 169 * * #P normalize 170 try /3 by or_introl, conj, refl/ 171 %2 @conj try // 172 % #H destruct 173 qed. 174 175 lemma typ_eq_elim : 176 ∀t1,t2. 177 ∀(P: (t1=t2)+(t1≠t2) → Prop). 178 (∀H:t1 = t2. P (inl ?? H)) → (∀H:t1 ≠ t2. P (inr ?? H)) → P (typ_eq t1 t2). 179 #t1 #t2 #P #Hl #Hr 180 @(match typ_eq t1 t2 181 with 182 [ inl H ⇒ Hl H 183  inr H ⇒ Hr H ]) 184 qed. 185 186 187 lemma eq_nat_dec_true : ∀n. eq_nat_dec n n = inl ?? (refl ? n). 188 #n elim n try // 189 #n' #Hind whd in ⊢ (??%?); >Hind @refl 190 qed. 191 192 lemma type_eq_dec_true : ∀ty. type_eq_dec ty ty = inl ?? (refl ? ty). 193 #ty cases (type_eq_dec ty ty) #H 194 destruct (H) try @refl @False_ind cases H #J @J @refl qed. 195 196 lemma typ_eq_refl : ∀t. typ_eq t t = inl ?? (refl ? t). 197 * 198 [ * * normalize @refl 199  @refl ] 200 qed. 201 202 lemma intsize_eq_elim_inversion : 203 ∀A:Type[0]. 204 ∀sz1,sz2. 205 ∀elt1,f,errmsg,res. 206 intsize_eq_elim ? sz1 sz2 bvint elt1 f (Error A errmsg) = OK ? res → 207 ∃H:sz1 = sz2. OK ? res = (f (eq_rect_r ? sz1 sz2 (sym_eq ??? H) ? elt1)). 208 #A * * #elt1 #f #errmsg #res normalize #H destruct (H) 209 %{(refl ??)} normalize nodelta >H @refl 210 qed. 211 212 lemma inttyp_eq_elim_true' : 213 ∀sz,sg,P,p1,p2. 214 inttyp_eq_elim' sz sz sg sg P p1 p2 = p1. 215 * * #P #p1 #p2 normalize try @refl 216 qed. 217 151 218 152 219 (*  *) … … 575 642 ] 576 643 qed. 644 645 axiom commutative_multiplication : 646 ∀n. ∀v1,v2:BitVector n. 647 multiplication ? v1 v2 = multiplication ? v2 v1. 648 649 lemma commutative_short_multiplication : 650 ∀n. ∀v1,v2:BitVector n. 651 short_multiplication ? v1 v2 = short_multiplication ? v2 v1. 652 #n #v1 #v2 whd in ⊢ (??%%); >commutative_multiplication @refl 653 qed. 654 655 lemma sign_ext_same_size : ∀n,v. sign_ext n n v = v. 656 #n #v whd in match (sign_ext ???); >nat_compare_eq @refl 657 qed. 658 659 axiom sign_ext_zero : ∀sz1,sz2. sign_ext sz1 sz2 (zero sz1) = zero sz2. 660 661 axiom zero_ext_zero : ∀sz1,sz2. zero_ext sz1 sz2 (zero sz1) = zero sz2. 662 663 axiom multiplication_zero : ∀n:nat. ∀v : BitVector n. multiplication … (zero ?) v = (zero ?). 664 665 axiom short_multiplication_zero : ∀n. ∀v:BitVector n. short_multiplication ? (zero ?) v = (zero ?). 666 577 667 578 668
Note: See TracChangeset
for help on using the changeset viewer.