Last change
on this file since 2327 was
2234,
checked in by garnier, 8 years ago

Progress on proving semantics preservation under memory injections.

File size:
768 bytes

Line  

1  (* Various small results used in at least two files in the frontend. *) 

2  

3  include "Clight/TypeComparison.ma". 

4  include "common/Pointers.ma". 

5  

6  lemma eq_intsize_identity : ∀id. eq_intsize id id = true. 

7  * normalize // 

8  qed. 

9  

10  lemma sz_eq_identity : ∀s. sz_eq_dec s s = inl ?? (refl ? s). 

11  * normalize // 

12  qed. 

13  

14  lemma type_eq_identity : ∀t. type_eq t t = true. 

15  #t normalize elim (type_eq_dec t t) 

16  [ 1: #Heq normalize // 

17   2: #H destruct elim H #Hcontr elim (Hcontr (refl ? t)) ] qed. 

18  

19  lemma type_neq_not_identity : ∀t1, t2. t1 ≠ t2 → type_eq t1 t2 = false. 

20  #t1 #t2 #Hneq normalize elim (type_eq_dec t1 t2) 

21  [ 1: #Heq destruct elim Hneq #Hcontr elim (Hcontr (refl ? t2)) 

22   2: #Hneq' normalize // ] qed. 

23  

24  lemma eq_block_identity : ∀b. eq_block b b = true. // qed. 

Note: See
TracBrowser
for help on using the repository browser.