# Changeset 2565 for src/Clight/frontend_misc.ma

Ignore:
Timestamp:
Dec 19, 2012, 6:11:23 PM (7 years ago)
Message:

Cl to Cm progress.

File:
1 edited

Unmodified
Removed
• ## src/Clight/frontend_misc.ma

 r2510 | 2: * #Habsurd @(False_ind … (Habsurd … (refl ? i))) ] qed. lemma intsize_eq_inversion : ∀sz,sz'. ∀A:Type[0]. ∀ok,not_ok. intsize_eq_elim' sz sz' (λsz,sz'. res A) (OK ? ok) (Error ? not_ok) = (OK ? ok) → sz = sz'. * * try // normalize #A #ok #not_ok #Habsurd destruct qed. lemma intsize_eq_elim_dec : ∀sz1,sz2. ∀P: ∀sz1,sz2. Type[0]. ((∀ifok,iferr. intsize_eq_elim' sz1 sz1 P ifok iferr = ifok) ∧ sz1 = sz2) ∨ ((∀ifok,iferr. intsize_eq_elim' sz1 sz2 P ifok iferr = iferr) ∧ sz1 ≠ sz2). * * #P normalize try /3 by or_introl, conj, refl/ %2 @conj try // % #H destruct qed. lemma typ_eq_elim : ∀t1,t2. ∀(P: (t1=t2)+(t1≠t2) → Prop). (∀H:t1 = t2. P (inl ?? H)) → (∀H:t1 ≠ t2. P (inr ?? H)) → P (typ_eq t1 t2). #t1 #t2 #P #Hl #Hr @(match typ_eq t1 t2 with [ inl H ⇒ Hl H | inr H ⇒ Hr H ]) qed. lemma eq_nat_dec_true : ∀n. eq_nat_dec n n = inl ?? (refl ? n). #n elim n try // #n' #Hind whd in ⊢ (??%?); >Hind @refl qed. lemma type_eq_dec_true : ∀ty. type_eq_dec ty ty = inl ?? (refl ? ty). #ty cases (type_eq_dec ty ty) #H destruct (H) try @refl @False_ind cases H #J @J @refl qed. lemma typ_eq_refl : ∀t. typ_eq t t = inl ?? (refl ? t). * [ * * normalize @refl | @refl ] qed. lemma intsize_eq_elim_inversion : ∀A:Type[0]. ∀sz1,sz2. ∀elt1,f,errmsg,res. intsize_eq_elim ? sz1 sz2 bvint elt1 f (Error A errmsg) = OK ? res → ∃H:sz1 = sz2. OK ? res = (f (eq_rect_r ? sz1 sz2 (sym_eq ??? H) ? elt1)). #A * * #elt1 #f #errmsg #res normalize #H destruct (H) %{(refl ??)} normalize nodelta >H @refl qed. lemma inttyp_eq_elim_true' : ∀sz,sg,P,p1,p2. inttyp_eq_elim' sz sz sg sg P p1 p2 = p1. * * #P #p1 #p2 normalize try @refl qed. (* --------------------------------------------------------------------------- *) ] qed. axiom commutative_multiplication : ∀n. ∀v1,v2:BitVector n. multiplication ? v1 v2 = multiplication ? v2 v1. lemma commutative_short_multiplication : ∀n. ∀v1,v2:BitVector n. short_multiplication ? v1 v2 = short_multiplication ? v2 v1. #n #v1 #v2 whd in ⊢ (??%%); >commutative_multiplication @refl qed. lemma sign_ext_same_size : ∀n,v. sign_ext n n v = v. #n #v whd in match (sign_ext ???); >nat_compare_eq @refl qed. axiom sign_ext_zero : ∀sz1,sz2. sign_ext sz1 sz2 (zero sz1) = zero sz2. axiom zero_ext_zero : ∀sz1,sz2. zero_ext sz1 sz2 (zero sz1) = zero sz2. axiom multiplication_zero : ∀n:nat. ∀v : BitVector n. multiplication … (zero ?) v = (zero ?). axiom short_multiplication_zero : ∀n. ∀v:BitVector n. short_multiplication ? (zero ?) v = (zero ?).
Note: See TracChangeset for help on using the changeset viewer.