Ignore:
Timestamp:
Nov 7, 2012, 6:02:50 PM (8 years ago)
Author:
garnier
Message:

Moved general stuff on memories from switchRemoval to MemProperties?, e.g. on loading, storing and free, as an
attempt to reduce the typechecking time of switchRemoval.ma.
Moved some other generic stuff on vectors from SimplifyCasts? to frontend_misc.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SimplifyCasts.ma

    r2428 r2441  
    66include "Clight/casts.ma".
    77include "Clight/CexecSound.ma".
     8
     9include "Clight/frontend_misc.ma".
    810
    911
     
    302304(* Facts about cast_int_int *)
    303305
    304 (* copied from AssemblyProof *)
    305 lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A.
    306  #A #v generalize in match (refl … 0); cases v in ⊢ (??%? → ?%%??); //
    307  #n #hd #tl #abs @⊥ destruct (abs)
    308 qed.
    309 
    310 lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n).
    311  ∃hd.∃tl.v ≃ VCons A n hd tl.
    312  #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
    313  [ #abs @⊥ destruct (abs)
    314  | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
    315 qed.
    316 
    317 lemma vector_append_zero:
    318   ∀A,m.
    319   ∀v: Vector A m.
    320   ∀q: Vector A 0.
    321     v = q@@v.
    322   #A #m #v #q
    323   >(Vector_O A q) %
    324 qed.
    325 
    326 corollary prod_vector_zero_eq_left:
    327   ∀A, n.
    328   ∀q: Vector A O.
    329   ∀r: Vector A n.
    330     〈q, r〉 = 〈[[ ]], r〉.
    331   #A #n #q #r
    332   generalize in match (Vector_O A q …);
    333   #hyp
    334   >hyp in ⊢ (??%?);
    335   %
    336 qed.
    337  
    338 lemma vsplit_eq : ∀A. ∀m,n. ∀v : Vector A ((S m) + n).  ∃v1:Vector A (S m). ∃v2:Vector A n. v = v1 @@ v2.
    339 # A #m #n elim m
    340 [ 1: normalize #v
    341   elim (Vector_Sn ?? v) #hd * #tl #Eq
    342   @(ex_intro … (hd ::: [[]])) @(ex_intro … tl)
    343   >Eq normalize //
    344 | 2: #n' #Hind #v
    345   elim (Vector_Sn ?? v) #hd * #tl #Eq
    346   elim (Hind tl)
    347   #tl1 * #tl2 #Eq_tl
    348   @(ex_intro … (hd ::: tl1))
    349   @(ex_intro … tl2) 
    350   destruct normalize //
    351 ] qed.
    352 
    353 lemma vsplit_eq2 : ∀A. ∀m,n : nat. ∀v : Vector A (m + n).  ∃v1:Vector A m. ∃v2:Vector A n. v = v1 @@ v2.
    354 # A #m #n elim m
    355 [ 1: normalize #v @(ex_intro … (VEmpty ?)) @(ex_intro … v) normalize //
    356 | 2: #n' #Hind #v
    357   elim (Vector_Sn ?? v) #hd * #tl #Eq
    358   elim (Hind tl)
    359   #tl1 * #tl2 #Eq_tl
    360   @(ex_intro … (hd ::: tl1))
    361   @(ex_intro … tl2) 
    362   destruct normalize //
    363 ] qed.
    364 
    365 lemma vsplit_zero:
    366   ∀A,m.
    367   ∀v: Vector A m.
    368     〈[[]], v〉 = vsplit A 0 m v.
    369   #A #m #v
    370   elim v
    371   [ %
    372   | #n #hd #tl #ih
    373     normalize in ⊢ (???%); %
    374   ]
    375 qed.
    376 
    377 
    378 lemma vsplit_zero2:
    379   ∀A,m.
    380   ∀v: Vector A m.
    381     〈[[]], v〉 = vsplit' A 0 m v.
    382   #A #m #v
    383   elim v
    384   [ %
    385   | #n #hd #tl #ih
    386     normalize in ⊢ (???%); %
    387   ]
    388 qed.
    389 
    390 (* This is not very nice. Note that this axiom was copied verbatim from ASM/AssemblyProof.ma.
    391  * TODO sync with AssemblyProof.ma, in a better world we shouldn't have to copy all of this. *)
    392 axiom vsplit_succ:
    393   ∀A, m, n.
    394   ∀l: Vector A m.
    395   ∀r: Vector A n.
    396   ∀v: Vector A (m + n).
    397   ∀hd.
    398     v = l@@r → (〈l, r〉 = vsplit ? m n v → 〈hd:::l, r〉 = vsplit ? (S m) n (hd:::v)).
    399 
    400 axiom vsplit_succ2:
    401   ∀A, m, n.
    402   ∀l: Vector A m.
    403   ∀r: Vector A n.
    404   ∀v: Vector A (m + n).
    405   ∀hd.
    406     v = l@@r → (〈l, r〉 = vsplit' ? m n v → 〈hd:::l, r〉 = vsplit' ? (S m) n (hd:::v)).
    407      
    408 lemma vsplit_prod2:
    409   ∀A,m,n.
    410   ∀p: Vector A (m + n).
    411   ∀v: Vector A m.
    412   ∀q: Vector A n.
    413     p = v@@q → 〈v, q〉 = vsplit' A m n p.
    414   #A #m
    415   elim m
    416   [ #n #p #v #q #hyp
    417     >hyp <(vector_append_zero A n q v)
    418     >(prod_vector_zero_eq_left A …)
    419     @vsplit_zero2
    420   | #r #ih #n #p #v #q #hyp
    421     >hyp
    422     cases (Vector_Sn A r v)
    423     #hd #exists
    424     cases exists
    425     #tl #jmeq >jmeq
    426     @vsplit_succ2 [1: % |2: @ih % ]
    427   ]
    428 qed.
    429 
    430 lemma vsplit_prod:
    431   ∀A,m,n.
    432   ∀p: Vector A (m + n).
    433   ∀v: Vector A m.
    434   ∀q: Vector A n.
    435     p = v@@q → 〈v, q〉 = vsplit A m n p.
    436   #A #m
    437   elim m
    438   [ #n #p #v #q #hyp
    439     >hyp <(vector_append_zero A n q v)
    440     >(prod_vector_zero_eq_left A …)
    441     @vsplit_zero
    442   | #r #ih #n #p #v #q #hyp
    443     >hyp
    444     cases (Vector_Sn A r v)
    445     #hd #exists
    446     cases exists
    447     #tl #jmeq >jmeq
    448     @vsplit_succ [1: % |2: @ih % ]
    449   ]
    450 qed.
    451306
    452307lemma cast_decompose : ∀s1, v. cast_int_int I32 s1 I8 v = (cast_int_int I16 s1 I8 (cast_int_int I32 s1 I16 v)).
     
    746601
    747602lemma bool_conj_inv : ∀a,b : bool. (a ∧ b) = true → a = true ∧ b = true.
    748 * * normalize #H @conj // qed.
     603* * normalize #H @conj try @refl assumption qed.
    749604
    750605(* Operations where it is safe to use a smaller integer type on the assumption
Note: See TracChangeset for help on using the changeset viewer.