|
Last change
on this file since 2304 was
2234,
checked in by garnier, 9 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 front-end. *) |
|---|
| 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.
