Last change
on this file since 2231 was
2231,
checked in by garnier, 7 years ago

Various tiny lemmas used in at least two files in the forntend.

File size:
676 bytes

Line  

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

2  

3  include "Clight/TypeComparison.ma". 

4  

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

6  * normalize // 

7  qed. 

8  

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

10  * normalize // 

11  qed. 

12  

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

14  #t normalize elim (type_eq_dec t t) 

15  [ 1: #Heq normalize // 

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

17  

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

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

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

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

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