source: src/Clight/frontend_misc.ma @ 2231

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
3include "Clight/TypeComparison.ma".
4
5lemma eq_intsize_identity : ∀id. eq_intsize id id = true.
6* normalize //
7qed.
8
9lemma sz_eq_identity : ∀s. sz_eq_dec s s = inl ?? (refl ? s).
10* normalize //
11qed.
12
13lemma 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
18lemma 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.