source: src/Clight/frontend_misc.ma @ 2234

Last change on this file since 2234 was 2234, checked in by garnier, 7 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
3include "Clight/TypeComparison.ma".
4include "common/Pointers.ma".
5
6lemma eq_intsize_identity : ∀id. eq_intsize id id = true.
7* normalize //
8qed.
9
10lemma sz_eq_identity : ∀s. sz_eq_dec s s = inl ?? (refl ? s).
11* normalize //
12qed.
13
14lemma 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
19lemma 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
24lemma eq_block_identity : ∀b. eq_block b b = true. // qed.
Note: See TracBrowser for help on using the repository browser.