|
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 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.
