Last change
on this file since 2231 was
2231,
checked in by garnier, 9 years ago
|
Various tiny lemmas used in at least two files in the fornt-end.
|
File size:
676 bytes
|
Line | |
---|
1 | (* Various small results used in at least two files in the front-end. *) |
---|
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.