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

Cl to Cm progress.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2510 r2565  
    149149| 2: * #Habsurd @(False_ind … (Habsurd … (refl ? i))) ]
    150150qed.
     151
     152lemma 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
     162qed.
     163
     164lemma 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
     170try /3 by or_introl, conj, refl/
     171%2 @conj try //
     172% #H destruct
     173qed.
     174
     175lemma 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 ])
     184qed.
     185
     186
     187lemma 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
     190qed.
     191
     192lemma type_eq_dec_true : ∀ty. type_eq_dec ty ty = inl ?? (refl ? ty).
     193#ty cases (type_eq_dec ty ty) #H
     194destruct (H) try @refl @False_ind cases H #J @J @refl qed.
     195
     196lemma typ_eq_refl : ∀t. typ_eq t t = inl ?? (refl ? t).
     197*
     198[ * * normalize @refl
     199| @refl ]
     200qed.
     201
     202lemma 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
     210qed.
     211
     212lemma 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
     216qed.
     217
    151218
    152219(* --------------------------------------------------------------------------- *)
     
    575642  ]
    576643qed.
     644
     645axiom commutative_multiplication :
     646  ∀n. ∀v1,v2:BitVector n.
     647  multiplication ? v1 v2 = multiplication ? v2 v1.
     648 
     649lemma 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
     653qed.
     654
     655lemma sign_ext_same_size : ∀n,v. sign_ext n n v = v.
     656#n #v whd in match (sign_ext ???); >nat_compare_eq @refl
     657qed.
     658
     659axiom sign_ext_zero : ∀sz1,sz2. sign_ext sz1 sz2 (zero sz1) = zero sz2.
     660
     661axiom zero_ext_zero : ∀sz1,sz2. zero_ext sz1 sz2 (zero sz1) = zero sz2.
     662
     663axiom multiplication_zero : ∀n:nat. ∀v : BitVector n. multiplication … (zero ?) v = (zero ?).
     664
     665axiom short_multiplication_zero : ∀n. ∀v:BitVector n. short_multiplication ? (zero ?) v = (zero ?).
     666
    577667
    578668
Note: See TracChangeset for help on using the changeset viewer.