source: src/Clight/frontend_misc.ma @ 2332

Last change on this file since 2332 was 2332, checked in by garnier, 7 years ago

Some progress on switch removal. Small fix in the definition of free, in GenMem?.ma.

File size: 4.5 KB
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
24(* useful facts on various boolean operations *)
25lemma andb_lsimpl_true : ∀x. andb true x = x. // qed.
26lemma andb_lsimpl_false : ∀x. andb false x = false. normalize // qed.
27lemma andb_comm : ∀x,y. andb x y = andb y x. // qed.
28lemma notb_true : notb true = false. // qed.
29lemma notb_false : notb false = true. % #H destruct qed.
30lemma notb_fold : ∀x. if x then false else true = (¬x). // qed.
31
32(* useful facts on block *)
33lemma not_eq_block : ∀b1,b2. b1 ≠ b2 → eq_block b1 b2 = false.
34#b1 #b2 #Hneq
35@(eq_block_elim … b1 b2)
36[ 1: #Heq destruct elim Hneq #H @(False_ind … (H (refl ??)))
37| 2: #_ @refl ] qed.
38
39lemma not_eq_block_rev : ∀b1,b2. b2 ≠ b1 → eq_block b1 b2 = false.
40#b1 #b2 #Hneq
41@(eq_block_elim … b1 b2)
42[ 1: #Heq destruct elim Hneq #H @(False_ind … (H (refl ??)))
43| 2: #_ @refl ] qed.
44
45(* useful facts on Z *)
46lemma Zltb_to_Zleb_true : ∀a,b. Zltb a b = true → Zleb a b = true.
47#a #b #Hltb lapply (Zltb_true_to_Zlt … Hltb) #Hlt @Zle_to_Zleb_true
48/3 by Zlt_to_Zle, transitive_Zle/ qed.
49
50lemma Zle_to_Zle_to_eq : ∀a,b. Zle a b → Zle b a → a = b.
51#a #b elim b
52[ 1: elim a // #a' normalize [ 1: @False_ind | 2: #_ @False_ind ] ]
53#b' elim a normalize
54[ 1: #_ @False_ind
55| 2: #a' #H1 #H2 >(le_to_le_to_eq … H1 H2) @refl
56| 3: #a' #_ @False_ind
57| 4: @False_ind
58| 5: #a' @False_ind
59| 6: #a' #H2 #H1 >(le_to_le_to_eq … H1 H2) @refl
60] qed.
61
62lemma Zleb_true_to_Zleb_true_to_eq : ∀a,b. (Zleb a b = true) → (Zleb b a = true) → a = b.
63#a #b #H1 #H2
64/3 by Zle_to_Zle_to_eq, Zleb_true_to_Zle/
65qed.
66
67lemma Zltb_dec : ∀a,b. (Zltb a b = true) ∨ (Zltb a b = false ∧ Zleb b a = true).
68#a #b
69lapply (Z_compare_to_Prop … a b)
70cases a
71[ 1: | 2,3: #a' ]
72cases b
73whd in match (Z_compare OZ OZ); normalize nodelta
74[ 2,3,5,6,8,9: #b' ]
75whd in match (Zleb ? ?);
76try /3 by or_introl, or_intror, conj, I, refl/
77whd in match (Zltb ??);
78whd in match (Zleb ??); #_
79[ 1: cases (decidable_le (succ a') b')
80     [ 1: #H lapply (le_to_leb_true … H) #H %1 assumption
81     | 2:  #Hnotle lapply (not_le_to_lt … Hnotle) #Hlt %2  @conj try @le_to_leb_true
82           /2 by monotonic_pred/ @(not_le_to_leb_false … Hnotle) ]
83| 2: cases (decidable_le (succ b') a')
84     [ 1: #H lapply (le_to_leb_true … H) #H %1 assumption
85     | 2:  #Hnotle lapply (not_le_to_lt … Hnotle) #Hlt %2  @conj try @le_to_leb_true
86           /2 by monotonic_pred/ @(not_le_to_leb_false … Hnotle) ]
87] qed.
88
89lemma Zleb_unsigned_OZ : ∀bv. Zleb OZ (Z_of_unsigned_bitvector 16 bv) = true.
90#bv elim bv try // #n' * #tl normalize /2/ qed.
91
92lemma Zltb_unsigned_OZ : ∀bv. Zltb (Z_of_unsigned_bitvector 16 bv) OZ = false.
93#bv elim bv try // #n' * #tl normalize /2/ qed.
94
95lemma Z_of_unsigned_not_neg : ∀bv.
96  (Z_of_unsigned_bitvector 16 bv = OZ) ∨ (∃p. Z_of_unsigned_bitvector 16 bv = pos p).
97#bv elim bv
98[ 1: normalize %1 @refl
99| 2: #n #hd #tl #Hind cases hd
100     [ 1: normalize %2 /2 by ex_intro/
101     | 2: cases Hind normalize [ 1: #H %1 @H | 2: * #p #H >H %2 %{p} @refl ]
102     ]
103] qed.
104
105lemma free_not_in_bounds : ∀x. if Zleb (pos one) x
106                                then Zltb x OZ 
107                                else false = false.
108#x lapply (Zltb_to_Zleb_true x OZ)
109elim (Zltb_dec … x OZ)
110[ 1: #Hlt >Hlt #H lapply (H (refl ??)) elim x
111     [ 2,3: #x' ] normalize in ⊢ (% → ?);
112     [ 1: #Habsurd destruct (Habsurd)
113     | 2,3: #_ @refl ]
114| 2: * #Hlt #Hle #_ >Hlt cases (Zleb (pos one) x) @refl ]
115qed.
116
117lemma free_not_valid : ∀x. if Zleb (pos one) x
118                            then Zleb x OZ 
119                            else false = false.
120#x
121cut (Zle (pos one) x ∧ Zle x OZ → False)
122[ * #H1 #H2 lapply (transitive_Zle … H1 H2) #H @H ] #Hguard
123cut (Zleb (pos one) x = true ∧ Zleb x OZ = true → False)
124[ * #H1 #H2 @Hguard @conj /2 by Zleb_true_to_Zle/ ]
125cases (Zleb (pos one) x) cases (Zleb x OZ)
126/2 by refl/ #H @(False_ind … (H (conj … (refl ??) (refl ??))))
127qed.
Note: See TracBrowser for help on using the repository browser.