Context Navigation

SimplifyCasts.ma @ 2304

Last change on this file since 2304 was 2219, checked in by campbell, 9 years ago
Speed up cast simplification proof checking a bit.
File size: 151.4 KB

Line
1	include "Clight/Csyntax.ma".
2	include "Clight/TypeComparison.ma".
3
4	(* IG: used to prove preservation of the semantics. *)
5	include "Clight/Cexec.ma".
6	include "Clight/casts.ma".
7	include "Clight/CexecSound.ma".
8
9
10	(* include "ASM/AssemblyProof.ma". ) ( I had to manually copy some of the lemmas in this file, including an axiom ... *)
11
12	(* Attempt to remove unnecessary integer casts in Clight programs.
13
14	This differs from the OCaml prototype by attempting to recursively determine
15	whether subexpressions can be changed rather than using a fixed size pattern.
16	As a result more complex expressions such as (char)((int)x + (int)y + (int)z)
17	where x,y and z are chars can be simplified.
18
19	A possible improvement that doesn't quite fit into this scheme would be to
20	spot that casts can be removed in expressions like (int)x == (int)y where
21	x and y have some smaller integer type.
22	*)
23
24	(* Attempt to squeeze integer constant into a given type.
25
26	This might be too conservative --- if we're going to cast it anyway, can't
27	I just ignore the fact that the integer doesn't fit?
28	*)
29
30	(* [reduce_bits n m exp v] takes avector of size n + m + 1 and returns (if all goes well) a vector of size
31	* m+1 (an empty vector of bits makes no sense). It proceeds by removing /all/ the [n] leading bits equal
32	* to [exp]. If it fails, it returns None. *)
33	let rec reduce_bits (n,m:nat) (exp:bool) (v:BitVector (plus n (S m))) on n : option (BitVector (S m)) ≝
34	match n return λn. BitVector (n+S m) → option (BitVector (S m)) with
35	[ O ⇒ λv. Some ? v
36	\| S n' ⇒ λv. if eq_b (head' ?? v) exp then reduce_bits ?? exp (tail ?? v) else None ?
37	] v.
38
39	lemma reduce_bits_ok : ∀n,m.∀exp.∀v,v'. reduce_bits (S n) m exp v = Some ? v'→ reduce_bits n m exp (tail ?? v) = Some ? v'.
40	#n #m #exp #v #v' #H whd in H:(??%?); lapply H -H
41	cases (eq_b ? exp)
42	[ 1: #H whd in H:(??%?); //
43	\| 2: #H normalize in H; destruct ] qed.
44
45	lemma reduce_bits_trunc : ∀n,m.∀exp.∀v:(BitVector (plus n (S m))).∀v'.
46	reduce_bits n m exp v = Some ? v' → v' = truncate n (S m) v.
47	#n #m elim n
48	[ 1: #exp #v #v' #H normalize in v v' H; destruct normalize >vsplit_O_n //
49	\| 2: #n' #Hind #exp #v #v' #H >truncate_tail
50	> (Hind ??? (reduce_bits_ok ?? exp v v' H)) // ] qed.
51
52	lemma reduce_bits_dec : ∀n,m.∀exp.∀v. (∃v'.reduce_bits n m exp v = Some ? v') ∨ reduce_bits n m exp v = None ?.
53	#n #m #exp #v elim (reduce_bits n m exp v)
54	[ 1: %2 //
55	\| 2: #v' %1 @(ex_intro … v') // ] qed.
56
57	(* pred_bitsize_of_intsize I32 = 31, … *)
58	definition pred_bitsize_of_intsize : intsize → nat ≝
59	λsz. pred (bitsize_of_intsize sz).
60
61	definition signed : signedness → bool ≝
62	λsg. match sg with [ Unsigned ⇒ false \| Signed ⇒ true ].
63
64	(* [simplify_int sz sz' sg sg' i] tries to convert an integer [i] of width [sz] and signedness [sg]
65	* into an integer of size [sz'] of signedness [sg'].
66	* - It first proceeds by comparing the source and target width: if the target width is strictly superior
67	* to the source width, the conversion fails.
68	* - If the size is equal, the argument is returned as-is.
69	* - If the target type is strictly smaller than the source, it tries to squeeze the integer to
70	* the desired size.
71	*)
72	let rec simplify_int (sz,sz':intsize) (sg,sg':signedness) (i:bvint sz) : option (bvint sz') ≝
73	let bit ≝ signed sg ∧ head' … i in
74	(* [nat_compare] does more than an innocent post-doc might think. It also computes the difference between the two args.
75	* if x < y, nat_compare x y = lt(x, y-(x+1))
76	* if x = y, nat_compare x y = eq x
77	* if x > y, nat_compare x y = gt(x-(y+1), y) *)
78	match nat_compare (pred_bitsize_of_intsize sz) (pred_bitsize_of_intsize sz')
79	return λn,m,x.BitVector (S n) → option (BitVector (S m)) with
80	[ nat_lt _ _ ⇒ λi. None ? (* refuse to make constants larger *)
81	\| nat_eq _ ⇒ λi. Some ? i
82	\| nat_gt x y ⇒ λi.
83	(* Here, we have [x]=31-([y]+1) and [y] ∈ {15; 7} OR [x] = 15-(7+1) and [y] = 7. I.e.: x=15,y=15 or x=23,y=7 or x=7,y=7.
84	* In [reduce_bits n m bit i], [i] is supposed to have type BitVector n + (S m). Since its type is here (S x) + (S y),
85	* we deduce that the actual arguments of [reduce_bits] are (S x) and (S y), which is consistent.
86	* If [i] is of signed type and if it is negative, then it tries to remove the (S x) first "1" bits.
87	* Otherwise, it tries to remove the (S x) first "0" bits.
88	*)
89	match reduce_bits ?? bit (i⌈BitVector (S (y+S x))↦BitVector ((S x) + (S y))⌉) with
90	[ Some i' ⇒
91	if signed sg' then
92	if eq_b bit (head' … i') then
93	Some ? i'
94	else None ?
95	else Some ? i'
96	\| None ⇒ None ?
97	]
98	] i.
99	>(commutative_plus_faster (S x)) @refl
100	qed.
101
102
103	lemma eq_intsize_identity : ∀id. eq_intsize id id = true.
104	* normalize //
105	qed.
106
107	lemma sz_eq_identity : ∀s. sz_eq_dec s s = inl ?? (refl ? s).
108	* normalize //
109	qed.
110
111	lemma type_eq_identity : ∀t. type_eq t t = true.
112	#t normalize elim (type_eq_dec t t)
113	[ 1: #Heq normalize //
114	\| 2: #H destruct elim H #Hcontr elim (Hcontr (refl ? t)) ] qed.
115
116	lemma type_neq_not_identity : ∀t1, t2. t1 ≠ t2 → type_eq t1 t2 = false.
117	#t1 #t2 #Hneq normalize elim (type_eq_dec t1 t2)
118	[ 1: #Heq destruct elim Hneq #Hcontr elim (Hcontr (refl ? t2))
119	\| 2: #Hneq' normalize // ] qed.
120
121	definition size_le ≝ λsz1,sz2.
122	match sz1 with
123	[ I8 ⇒ True
124	\| I16 ⇒
125	match sz2 with
126	[ I16 ⇒ True \| I32 ⇒ True \| _ ⇒ False ]
127	\| I32 ⇒
128	match sz2 with
129	[ I32 ⇒ True \| _ ⇒ False ]
130	].
131
132	definition size_lt ≝ λsz1,sz2.
133	match sz1 with
134	[ I8 ⇒
135	match sz2 with
136	[ I16 ⇒ True \| I32 ⇒ True \| _ ⇒ False ]
137	\| I16 ⇒
138	match sz2 with
139	[ I32 ⇒ True \| _ ⇒ False ]
140	\| I32 ⇒ False
141	].
142
143	lemma size_lt_to_le : ∀sz1,sz2. size_lt sz1 sz2 → size_le sz1 sz2.
144	#sz1 #sz2 elim sz1 elim sz2 normalize // qed.
145
146	lemma size_lt_dec : ∀sz1,sz2. size_lt sz1 sz2 + (¬ (size_lt sz1 sz2)).
147	* * normalize /2/ /3/
148	qed.
149
150	lemma size_not_lt_to_ge : ∀sz1,sz2. ¬(size_lt sz1 sz2) → (sz1 = sz2) + (size_lt sz2 sz1).
151	* * normalize /2/ /3/
152	qed.
153
154	(* This function already exists in prop, we want it in type. *)
155	definition sign_eq_dect : ∀sg1,sg2:signedness. (sg1 = sg2) + (sg1 ≠ sg2).
156	* * normalize // qed.
157
158	lemma size_absurd : ∀a,b. size_le a b → size_lt b a → False.
159	* * normalize
160	#H1 #H2 try (@(False_ind … H1)) try (@(False_ind … H2)) qed.
161
162	(* This defines necessary conditions for [src_expr] to be coerced to "target_ty".
163	* Again, these are /not/ sufficient conditions. See [simplify_inv] for the rest. *)
164	definition necessary_conditions ≝ λsrc_sz.λsrc_sg.λtarget_sz.λtarget_sg.
165	match size_lt_dec target_sz src_sz with
166	[ inl Hlt ⇒ true
167	\| inr Hnlt ⇒
168	match sz_eq_dec target_sz src_sz with
169	[ inl Hsz_eq ⇒
170	match sign_eq_dect src_sg target_sg with
171	[ inl Hsg_eq ⇒ false
172	\| inr Hsg_neq ⇒ true
173	]
174	\| inr Hsz_neq ⇒ false
175	]
176	].
177
178	(* Inversion on necessary_conditions *)
179	lemma necessary_conditions_spec :
180	∀src_sz,src_sg,target_sz, target_sg. (necessary_conditions src_sz src_sg target_sz target_sg = true) →
181	((size_lt target_sz src_sz) ∨ (src_sz = target_sz ∧ src_sg ≠ target_sg)).
182	#src_sz #src_sg #target_sz #target_sg
183	whd in match (necessary_conditions ????);
184	cases (size_lt_dec target_sz src_sz) normalize nodelta
185	[ 1: #Hlt #_ %1 //
186	\| 2: #Hnlt
187	cases (sz_eq_dec target_sz src_sz) normalize nodelta
188	[ 2: #_ #Hcontr destruct
189	\| 1: #Heq cases (sign_eq_dect src_sg target_sg) normalize nodelta
190	[ 1: #_ #Hcontr destruct
191	\| 2: #Hsg_neq #_ %2 destruct /2/ ]
192	]
193	] qed.
194
195	(* Compare the results [r1,r2] of the evaluation of two expressions. If [r1] is an
196	* integer value smaller but containing the same stuff than [r2] then all is well.
197	* If the first evaluation is erroneous, we don't care about anything else. *)
198	definition smaller_integer_val ≝ λsrc_sz,dst_sz,sg. λr1,r2:res(val×trace).
199	match r1 with
200	[ OK res1 ⇒
201	let 〈val1, tr1〉 ≝ res1 in
202	∀v1. val1 = Vint src_sz v1 →
203	match r2 with
204	[ OK res2 ⇒
205	let 〈val2, tr2〉 ≝ res2 in
206	∃v2. (val2 = Vint dst_sz v2 ∧
207	v2 = cast_int_int src_sz sg dst_sz v1 ∧ tr1 = tr2 ∧ size_le dst_sz src_sz)
208	\| _ ⇒ False ]
209	\| Error errmsg1 ⇒ True
210	].
211
212	(* Simulation relation used for expression evaluation. *)
213	inductive res_sim (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝
214	\| SimOk : (∀a:A. r1 = OK ? a → r2 = OK ? a) → res_sim A r1 r2
215	\| SimFail : (∃err. r1 = Error ? err) → res_sim A r1 r2.
216
217	(* Trick to reduce checking time by eliminating a load of costly automation.
218	It would be nice to do this by refactoring the type and code instead, but we
219	don't want to spend lots of time on something that already works. *)
220
221	lemma SimFailNicely : ∀A,err,r2. res_sim A (Error ? err) r2.
222	#A #err #r2 @SimFail %{err} %
223	qed.
224
225	(* Invariant of simplify_expr *)
226	inductive simplify_inv (ge : genv) (en : env) (m : mem) (e1 : expr) (e2 : expr) (target_sz : intsize) (target_sg : signedness) : bool → Prop ≝
227	(* Inv_eq states a standard simulation result. We enforce some needed equations on types to prove the cast cases. *)
228	\| Inv_eq : ∀result_flag.
229	result_flag = false →
230	typeof e1 = typeof e2 →
231	res_sim ? (exec_expr ge en m e1) (exec_expr ge en m e2) →
232	res_sim ? (exec_lvalue ge en m e1) (exec_lvalue ge en m e2) →
233	simplify_inv ge en m e1 e2 target_sz target_sg result_flag
234	(* Inv_coerce_ok states that we successfuly squeezed the source expression to [target_sz]. The details are hidden in [smaller_integer_val]. *)
235	\| Inv_coerce_ok : ∀src_sz,src_sg.
236	(typeof e1) = (Tint src_sz src_sg) →
237	(typeof e2) = (Tint target_sz target_sg) →
238	(smaller_integer_val src_sz target_sz src_sg (exec_expr ge en m e1) (exec_expr ge en m e2)) →
239	simplify_inv ge en m e1 e2 target_sz target_sg true.
240
241	(* Invariant of simplify_inside *)
242	definition conservation ≝ λe,result:expr.
243	∀ge,en,m. res_sim ? (exec_expr ge en m e) (exec_expr ge en m result)
244	∧ res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge en m result)
245	∧ typeof e = typeof result.
246
247	(* This lemma proves that simplify_int actually implements an integer cast. *)
248	(* The case 4 can be merged with cases 7 and 8. *)
249
250	lemma simplify_int_implements_cast : ∀sz,sz'.∀sg,sg'.∀i,i'. simplify_int sz sz' sg sg' i = Some ? i' → i' = cast_int_int sz sg sz' i.
251	* *
252	[ 1: #sg #sg' #i #i' #Hsimp normalize in Hsimp ⊢ %; elim sg normalize destruct //
253	\| 2,3,6: #sg #sg' #i #i' #Hsimp normalize in Hsimp; destruct (* ⊢ %; destruct destruct whd in Hsimp:(??%?); destruct *)
254	\| 4: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); normalize nodelta in Hsimp; normalize in i i' ⊢ %;
255	normalize in match (signed ?) in Hsimp;
256	normalize in match (S (plus ??)) in Hsimp;
257	normalize in match (plus 7 8) in Hsimp;
258	lapply Hsimp -Hsimp
259	cases (head' bool 15 i)
260	normalize in match (andb ??);
261	[ 1,3: elim (reduce_bits_dec 8 7 true i)
262	[ 1,3: * #v' #Heq >Heq letin Heq_trunc ≝ (reduce_bits_trunc … Heq) normalize nodelta
263	[ 1: cases (eq_b true ?) normalize #H destruct normalize @refl
264	\| 2: #H destruct normalize @refl ]
265	\| 2,4: #Heq >Heq normalize nodelta #H destruct ]
266	\| 2,4,5,6,7,8:
267	elim (reduce_bits_dec 8 7 false i)
268	[ 1,3,5,7,9,11: * #v' #Heq >Heq normalize nodelta letin Heq_trunc ≝ (reduce_bits_trunc … Heq)
269	[ 1,3,4: cases (eq_b false ?) normalize nodelta
270	#H destruct normalize @refl
271	\| 2,5,6: #H destruct normalize @refl ]
272	\| 2,4,6,8,10,12: #Heq >Heq normalize nodelta #H destruct
273	]
274	]
275	\| 5,9: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); destruct @refl
276	\| 7, 8: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); normalize nodelta in Hsimp; normalize in i i' ⊢ %;
277	normalize in match (signed ?) in Hsimp;
278	normalize in match (S (plus ??)) in Hsimp;
279	normalize in match (plus 7 24) in Hsimp;
280	lapply Hsimp -Hsimp
281	cases (head' bool ? i)
282	normalize in match (andb ??);
283	[ 1,3,9,11:
284	[ 1,2: (elim (reduce_bits_dec 24 7 true i)) \| 3,4: (elim (reduce_bits_dec 16 15 true i)) ]
285	[ 1,3,5,7: * #v' #Heq >Heq letin Heq_trunc ≝ (reduce_bits_trunc … Heq) normalize nodelta
286	[ 1,3: cases (eq_b true ?) normalize #H destruct normalize @refl
287	\| 2,4: #H destruct normalize @refl ]
288	\| 2,4,6,8: #Heq >Heq normalize nodelta #H destruct ]
289	\| 2,4,5,6,7,8,10,12,13,14,15,16:
290	[ 1,2,3,4,5,6: elim (reduce_bits_dec 24 7 false i)
291	\| 6,7,8,9,10,11,12: elim (reduce_bits_dec 16 15 false i) ]
292	[ 1,3,5,7,9,11,13,15,17,19,21,23:
293	* #v' #Heq >Heq normalize nodelta letin Heq_trunc ≝ (reduce_bits_trunc … Heq)
294	[ 1,3,4,7,9,10:
295	cases (eq_b false ?) normalize nodelta #H destruct normalize @refl
296	\| 2,5,6,8,11,12: #H destruct normalize @refl ]
297	\| 2,4,6,8,10,12,14,16,18,20,22,24: #Heq >Heq normalize nodelta #H destruct
298	]
299	]
300	] qed.
301
302	(* Facts about cast_int_int *)
303
304	(* copied from AssemblyProof *)
305	lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A.
306	#A #v generalize in match (refl … 0); cases v in ⊢ (??%? → ?%%??); //
307	#n #hd #tl #abs @⊥ destruct (abs)
308	qed.
309
310	lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n).
311	∃hd.∃tl.v ≃ VCons A n hd tl.
312	#A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
313	[ #abs @⊥ destruct (abs)
314	\| #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
315	qed.
316
317	lemma vector_append_zero:
318	∀A,m.
319	∀v: Vector A m.
320	∀q: Vector A 0.
321	v = q@@v.
322	#A #m #v #q
323	>(Vector_O A q) %
324	qed.
325
326	corollary prod_vector_zero_eq_left:
327	∀A, n.
328	∀q: Vector A O.
329	∀r: Vector A n.
330	〈q, r〉 = 〈[[ ]], r〉.
331	#A #n #q #r
332	generalize in match (Vector_O A q …);
333	#hyp
334	>hyp in ⊢ (??%?);
335	%
336	qed.
337
338	lemma vsplit_eq : ∀A. ∀m,n. ∀v : Vector A ((S m) + n). ∃v1:Vector A (S m). ∃v2:Vector A n. v = v1 @@ v2.
339	# A #m #n elim m
340	[ 1: normalize #v
341	elim (Vector_Sn ?? v) #hd * #tl #Eq
342	@(ex_intro … (hd ::: [[]])) @(ex_intro … tl)
343	>Eq normalize //
344	\| 2: #n' #Hind #v
345	elim (Vector_Sn ?? v) #hd * #tl #Eq
346	elim (Hind tl)
347	#tl1 * #tl2 #Eq_tl
348	@(ex_intro … (hd ::: tl1))
349	@(ex_intro … tl2)
350	destruct normalize //
351	] qed.
352
353	lemma vsplit_eq2 : ∀A. ∀m,n : nat. ∀v : Vector A (m + n). ∃v1:Vector A m. ∃v2:Vector A n. v = v1 @@ v2.
354	# A #m #n elim m
355	[ 1: normalize #v @(ex_intro … (VEmpty ?)) @(ex_intro … v) normalize //
356	\| 2: #n' #Hind #v
357	elim (Vector_Sn ?? v) #hd * #tl #Eq
358	elim (Hind tl)
359	#tl1 * #tl2 #Eq_tl
360	@(ex_intro … (hd ::: tl1))
361	@(ex_intro … tl2)
362	destruct normalize //
363	] qed.
364
365	lemma vsplit_zero:
366	∀A,m.
367	∀v: Vector A m.
368	〈[[]], v〉 = vsplit A 0 m v.
369	#A #m #v
370	elim v
371	[ %
372	\| #n #hd #tl #ih
373	normalize in ⊢ (???%); %
374	]
375	qed.
376
377
378	lemma vsplit_zero2:
379	∀A,m.
380	∀v: Vector A m.
381	〈[[]], v〉 = vsplit' A 0 m v.
382	#A #m #v
383	elim v
384	[ %
385	\| #n #hd #tl #ih
386	normalize in ⊢ (???%); %
387	]
388	qed.
389
390	(* This is not very nice. Note that this axiom was copied verbatim from ASM/AssemblyProof.ma.
391	* TODO sync with AssemblyProof.ma, in a better world we shouldn't have to copy all of this. *)
392	axiom vsplit_succ:
393	∀A, m, n.
394	∀l: Vector A m.
395	∀r: Vector A n.
396	∀v: Vector A (m + n).
397	∀hd.
398	v = l@@r → (〈l, r〉 = vsplit ? m n v → 〈hd:::l, r〉 = vsplit ? (S m) n (hd:::v)).
399
400	axiom vsplit_succ2:
401	∀A, m, n.
402	∀l: Vector A m.
403	∀r: Vector A n.
404	∀v: Vector A (m + n).
405	∀hd.
406	v = l@@r → (〈l, r〉 = vsplit' ? m n v → 〈hd:::l, r〉 = vsplit' ? (S m) n (hd:::v)).
407
408	lemma vsplit_prod2:
409	∀A,m,n.
410	∀p: Vector A (m + n).
411	∀v: Vector A m.
412	∀q: Vector A n.
413	p = v@@q → 〈v, q〉 = vsplit' A m n p.
414	#A #m
415	elim m
416	[ #n #p #v #q #hyp
417	>hyp <(vector_append_zero A n q v)
418	>(prod_vector_zero_eq_left A …)
419	@vsplit_zero2
420	\| #r #ih #n #p #v #q #hyp
421	>hyp
422	cases (Vector_Sn A r v)
423	#hd #exists
424	cases exists
425	#tl #jmeq >jmeq
426	@vsplit_succ2 [1: % \|2: @ih % ]
427	]
428	qed.
429
430	lemma vsplit_prod:
431	∀A,m,n.
432	∀p: Vector A (m + n).
433	∀v: Vector A m.
434	∀q: Vector A n.
435	p = v@@q → 〈v, q〉 = vsplit A m n p.
436	#A #m
437	elim m
438	[ #n #p #v #q #hyp
439	>hyp <(vector_append_zero A n q v)
440	>(prod_vector_zero_eq_left A …)
441	@vsplit_zero
442	\| #r #ih #n #p #v #q #hyp
443	>hyp
444	cases (Vector_Sn A r v)
445	#hd #exists
446	cases exists
447	#tl #jmeq >jmeq
448	@vsplit_succ [1: % \|2: @ih % ]
449	]
450	qed.
451
452	lemma cast_decompose : ∀s1, v. cast_int_int I32 s1 I8 v = (cast_int_int I16 s1 I8 (cast_int_int I32 s1 I16 v)).
453	#s1 #v normalize elim s1 normalize nodelta
454	normalize in v;
455	elim (vsplit_eq ??? (v⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉))
456	[ 2,4: //
457	\| 1,3: #l * #r normalize nodelta #Eq1
458	<(vsplit_prod bool 16 16 … Eq1)
459	elim (vsplit_eq ??? (r⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉))
460	[ 2,4: //
461	\| 1,3: #lr * #rr normalize nodelta #Eq2
462	<(vsplit_prod bool 8 8 … Eq2)
463	cut (v = (l @@ lr) @@ rr)
464	[ 1,3 : destruct >(vector_associative_append ? 16 8) //
465	\| 2,4: #Hrewrite destruct
466	<(vsplit_prod bool 24 8 … Hrewrite) @refl
467	]
468	]
469	] qed.
470
471	lemma cast_idempotent : ∀s1,s2,sz1,sz2,v. size_lt sz1 sz2 → cast_int_int sz2 s1 sz1 (cast_int_int sz1 s2 sz2 v) = v.
472	#s1 #s2 * * #v elim s1 elim s2
473	normalize #H try @refl
474	@(False_ind … H)
475	qed.
476
477	lemma cast_identity : ∀sz,sg,v. cast_int_int sz sg sz v = v.
478	* * #v normalize // qed.
479
480	lemma cast_collapse : ∀s1,s2,v. cast_int_int I32 s1 I8 (cast_int_int I16 s2 I32 v) = (cast_int_int I16 s1 I8 v).
481	#s1 #s2 #v >cast_decompose >cast_idempotent
482	[ 1: @refl \| 2: // ]
483	qed.
484
485	lemma cast_composition_lt : ∀a_sz,a_sg, b_sz, b_sg, c_sz, val.
486	size_lt c_sz a_sz → size_lt c_sz b_sz →
487	(cast_int_int a_sz a_sg c_sz val =
488	cast_int_int b_sz b_sg c_sz (cast_int_int a_sz a_sg b_sz val)).
489	* #a_sg * #b_sg * #val whd in match (size_lt ??); whd in match (size_lt ??);
490	#Hlt1 #Hlt2
491	[ 1,2,3,4,5,6,7,8,9,10,11,12,14,15,17,18,19,20,21,23,24,27:
492	@(False_ind … Hlt1) @(False_ind … Hlt2)
493	\| 13,25,26: >cast_identity elim a_sg elim b_sg normalize //
494	\| 22: normalize elim b_sg elim a_sg normalize
495	normalize in val;
496	elim (vsplit_eq ??? (val⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉))
497	[ 2,4,6,8: normalize //
498	\| 1,3,5,7: #left * #right normalize #Eq1
499	<(vsplit_prod bool 16 16 … Eq1)
500	elim (vsplit_eq ??? (right⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉))
501	[ 2,4,6,8: //
502	\| 1,3,5,7: #rightleft * #rightright normalize #Eq2
503	<(vsplit_prod bool 8 8 … Eq2)
504	cut (val = (left @@ rightleft) @@ rightright)
505	[ 1,3,5,7: destruct >(vector_associative_append ? 16 8) //
506	\| 2,4,6,8: #Hrewrite destruct
507	<(vsplit_prod bool 24 8 … Hrewrite) @refl
508	]
509	]
510	]
511	\| 16: elim b_sg elim a_sg >cast_collapse @refl
512	] qed.
513
514	lemma cast_composition : ∀a_sz,a_sg, b_sz, b_sg, c_sz, val.
515	size_le c_sz a_sz → size_le c_sz b_sz →
516	(cast_int_int a_sz a_sg c_sz val =
517	cast_int_int b_sz b_sg c_sz (cast_int_int a_sz a_sg b_sz val)).
518	#a_sz #a_sg #b_sz #b_sg #c_sz #val #Hle_c_a #Hle_c_b
519	cases (size_lt_dec c_sz a_sz)
520	cases (size_lt_dec c_sz b_sz)
521	[ 1: #Hltb #Hlta @(cast_composition_lt … Hlta Hltb)
522	\| 2: #Hnltb #Hlta
523	cases (size_not_lt_to_ge … Hnltb)
524	[ 1: #Heq destruct >cast_identity //
525	\| 2: #Hltb @(False_ind … (size_absurd ?? Hle_c_b Hltb))
526	]
527	\| 3: #Hltb #Hnlta
528	cases (size_not_lt_to_ge … Hnlta)
529	[ 1: #Heq destruct >cast_idempotent //
530	\| 2: #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta))
531	]
532	\| 4: #Hnltb #Hnlta
533	cases (size_not_lt_to_ge … Hnlta)
534	cases (size_not_lt_to_ge … Hnltb)
535	[ 1: #Heq_b #Heq_a destruct >cast_identity >cast_identity //
536	\| 2: #Hltb #Heq @(False_ind … (size_absurd ?? Hle_c_b Hltb))
537	\| 3: #Eq #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta))
538	\| 4: #Hltb #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta))
539	]
540	] qed.
541
542	let rec assert_int_value (v : option val) (expected_size : intsize) : option (BitVector (bitsize_of_intsize expected_size)) ≝
543	match v with
544	[ None ⇒ None ?
545	\| Some v ⇒
546	match v with
547	[ Vint sz i ⇒
548	match sz_eq_dec sz expected_size with
549	[ inl Heq ⇒ Some ??
550	\| inr _ ⇒ None ?
551	]
552	\| _ ⇒ None ?
553	]
554	].
555	>Heq in i; #i @i qed.
556
557	(* cast_int_int behaves as truncate (≃ vsplit) when downsizing *)
558	(* ∀src_sz,target_sz,sg. ∀i. size_le target_sz src_sz → cast_int_int src_sz sg target_sz i = truncate *)
559
560	lemma vsplit_to_truncate : ∀m,n,i. (\snd (vsplit bool m n i)) = truncate m n i.
561	#m #n #i normalize // qed.
562
563	(* Somme lemmas on how "simplifiable" operations behave under cast_int_int. *)
564
565	lemma integer_add_cast_lt : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_lt target_sz src_sz →
566	(addition_n (bitsize_of_intsize target_sz)
567	(cast_int_int src_sz sg target_sz lhs_int)
568	(cast_int_int src_sz sg target_sz rhs_int)
569	= cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)).
570	#src_sz #target_sz #sg #lhs_int #rhs_int #Hlt
571	elim src_sz in Hlt lhs_int rhs_int; elim target_sz
572	[ 1,2,3,5,6,9: normalize #H @(False_ind … H)
573	\| *: elim sg #_
574	normalize in match (bitsize_of_intsize ?);
575	normalize in match (bitsize_of_intsize ?);
576	#lint #rint
577	normalize in match (cast_int_int ????);
578	normalize in match (cast_int_int ????);
579	whd in match (addition_n ???);
580	whd in match (addition_n ???) in ⊢ (???%);
581	>vsplit_to_truncate >vsplit_to_truncate
582	<truncate_add_with_carries
583	[ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint rint false);
584	\| 3,4: normalize in match (plus 24 8); generalize in match (add_with_carries ? lint rint false);
585	\| 5,6: normalize in match (plus 16 16); generalize in match (add_with_carries ? lint rint false);
586	]
587	* #result #carry
588	normalize nodelta //
589	qed.
590
591	lemma integer_add_cast_eq : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. target_sz = src_sz →
592	(addition_n (bitsize_of_intsize target_sz)
593	(cast_int_int src_sz sg target_sz lhs_int)
594	(cast_int_int src_sz sg target_sz rhs_int)
595	= cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)).
596	#src_sz #target_sz #sg #lhs_int #rhs_int #Heq destruct
597	>cast_identity >cast_identity >cast_identity // qed.
598
599	lemma integer_add_cast_le : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_le target_sz src_sz →
600	(addition_n (bitsize_of_intsize target_sz)
601	(cast_int_int src_sz sg target_sz lhs_int)
602	(cast_int_int src_sz sg target_sz rhs_int)
603	= cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)).
604	#src_sz #target_sz #sg #lhs_int #rhs_int #Hle
605	cases (sz_eq_dec target_sz src_sz)
606	[ 1: #Heq @(integer_add_cast_eq … Heq)
607	\| 2: #Hneq cut (size_lt target_sz src_sz)
608	[ 1: elim target_sz in Hle Hneq; elim src_sz normalize //
609	#_ * #H @(H … (refl ??))
610	\| 2: #Hlt @(integer_add_cast_lt … Hlt)
611	]
612	] qed.
613
614	lemma truncate_eat : ∀l,n,m,v. l = n → ∃tl. truncate (S n) m v = truncate l m tl.
615	#l #n #m #v #len elim (Vector_Sn … v) #hd * #tl #Heq >len
616	@(ex_intro … tl)
617	>Heq >Heq
618	elim (vsplit_eq2 … tl) #l * #r #Eq
619	normalize
620	<(vsplit_prod bool n m tl l r Eq)
621	<(vsplit_prod2 bool n m tl l r Eq)
622	normalize //
623	qed.
624
625
626	lemma integer_neg_trunc : ∀m,n. ∀i: BitVector (m+n). two_complement_negation n (truncate m n i) = truncate m n (two_complement_negation (m+n) i).
627	#m elim m
628	[ 1: #n #i normalize in i;
629	whd in match (truncate ???);
630	whd in match (truncate ???) in ⊢ (???%);
631	<vsplit_zero <vsplit_zero //
632	\| 2: #m' #Hind #n #i normalize in i;
633	elim (Vector_Sn … i) #hd * #tl #Heq
634	whd in match (two_complement_negation (S ?) ?);
635	>Heq in ⊢ (??%?); >truncate_tail whd in match (tail ???) in ⊢ (??%?);
636	whd in match (two_complement_negation ??) in ⊢ (??%?);
637	lapply (Hind ? tl) #H
638	whd in match (two_complement_negation ??) in H;
639	(* trying to reduce add_with_carries *)
640	normalize in match (S m'+n);
641	whd in match (zero ?) in ⊢ (???%);
642	>Heq in match (negation_bv ??) in ⊢ (???%);
643	whd in match (negation_bv ??) in ⊢ (???%);
644	>add_with_carries_unfold in ⊢ (???%);
645	normalize in ⊢ (???%);
646	cases hd normalize nodelta
647	[ 1,2: <add_with_carries_unfold in ⊢ (???%); (* Good. Some progress. *)
648	(* try to transform the rhs of H into what we need. *)
649	whd in match (two_complement_negation ??) in H:(???%);
650	lapply H -H
651	generalize in match (add_with_carries (m'+n) (negation_bv (m'+n) tl) (zero (m'+n)) true);
652	* #Left #Right normalize nodelta
653	#H generalize in ⊢ (???(???(????(???(match % with [ _ ⇒ ? \| _ ⇒ ?])))));
654	#b >(vsplit_to_truncate (S m')) >truncate_tail
655	cases b
656	normalize nodelta
657	normalize in match (tail ???); @H
658	]
659	] qed. (* This was painful. *)
660
661	lemma integer_sub_cast_lt : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_lt target_sz src_sz →
662	(subtraction (bitsize_of_intsize target_sz)
663	(cast_int_int src_sz sg target_sz lhs_int)
664	(cast_int_int src_sz sg target_sz rhs_int)
665	= cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)).
666	#src_sz #target_sz #sg #lhs_int #rhs_int #Hlt
667	elim src_sz in Hlt lhs_int rhs_int; elim target_sz
668	[ 1,2,3,5,6,9: normalize #H @(False_ind … H)
669	\| *: elim sg #_
670	normalize in match (bitsize_of_intsize ?);
671	normalize in match (bitsize_of_intsize ?);
672	#lint #rint
673	normalize in match (cast_int_int ????);
674	normalize in match (cast_int_int ????);
675	whd in match (subtraction ???);
676	whd in match (subtraction ???) in ⊢ (???%);
677	>vsplit_to_truncate >vsplit_to_truncate
678	>integer_neg_trunc <truncate_add_with_carries
679	[ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint ? false);
680	\| 3,4: normalize in match (plus 24 8); generalize in match (add_with_carries ? lint ? false);
681	\| 5,6: normalize in match (plus 16 16); generalize in match (add_with_carries ? lint ? false);
682	]
683	* #result #carry
684	normalize nodelta //
685	qed.
686
687	lemma integer_sub_cast_eq : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. target_sz = src_sz →
688	(subtraction (bitsize_of_intsize target_sz)
689	(cast_int_int src_sz sg target_sz lhs_int)
690	(cast_int_int src_sz sg target_sz rhs_int)
691	= cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)).
692	#src_sz #target_sz #sg #lhs_int #rhs_int #Heq destruct
693	>cast_identity >cast_identity >cast_identity //
694	qed.
695
696	lemma integer_sub_cast_le : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_le target_sz src_sz →
697	(subtraction (bitsize_of_intsize target_sz)
698	(cast_int_int src_sz sg target_sz lhs_int)
699	(cast_int_int src_sz sg target_sz rhs_int)
700	= cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)).
701	#src_sz #target_sz #sg #lhs_int #rhs_int #Hle
702	cases (sz_eq_dec target_sz src_sz)
703	[ 1: #Heq @(integer_sub_cast_eq … Heq)
704	\| 2: #Hneq cut (size_lt target_sz src_sz)
705	[ 1: elim target_sz in Hle Hneq; elim src_sz normalize //
706	#_ * #H @(H … (refl ??))
707	\| 2: #Hlt @(integer_sub_cast_lt … Hlt)
708	]
709	] qed.
710
711	lemma simplify_int_success_lt : ∀sz,sg,sz',sg',i,i'. (simplify_int sz sz' sg sg' i=Some (bvint sz') i') → size_le sz' sz.
712	* #sg * #sg' #i #i' #H whd in H:(??%?); try destruct normalize // qed.
713
714	lemma smaller_integer_val_identity : ∀sz,sg,x.
715	smaller_integer_val sz sz sg x x.
716	#sz #sg *
717	[ 2: #error //
718	\| 1: * #val #trace whd in match (smaller_integer_val ?????);
719	#v1 #Hval %{v1} @conj try @conj try @conj //
720	elim sz //
721	] qed.
722
723	(* Inversion on exec_cast *)
724	lemma exec_cast_inv : ∀castee_val,src_sz,src_sg,cast_sz,cast_sg,m,result.
725	exec_cast m castee_val (Tint src_sz src_sg) (Tint cast_sz cast_sg) = OK ? result →
726	∃i. castee_val = Vint src_sz i ∧ result = Vint cast_sz (cast_int_int src_sz src_sg cast_sz i).
727	#castee_val #src_sz #src_sg #cast_sz #cast_sg #m #result
728	elim castee_val
729	[ 1: \| 2: #sz' #i \| 3: #f \| 4: \| 5: #ptr ]
730	[ 2: \| *: whd in ⊢ ((??%?) → ?); #Habsurd destruct ]
731	whd in ⊢ ((??%?) → ?);
732	cases (sz_eq_dec sz' src_sz)
733	[ 1: #Heq destruct >intsize_eq_elim_true normalize nodelta #Heq destruct
734	%{i} /2/
735	\| 2: #Hneq >intsize_eq_elim_false; try assumption #H destruct ]
736	qed.
737
738
739	(* Lemmas related to the Ebinop case *)
740
741	lemma classify_add_int : ∀sz,sg. classify_add (Tint sz sg) (Tint sz sg) = add_case_ii sz sg.
742	* * // qed.
743
744	lemma classify_sub_int : ∀sz,sg. classify_sub (Tint sz sg) (Tint sz sg) = sub_case_ii sz sg.
745	* * // qed.
746
747	lemma bool_conj_inv : ∀a,b : bool. (a ∧ b) = true → a = true ∧ b = true.
748	* * normalize #H @conj // qed.
749
750	(* Operations where it is safe to use a smaller integer type on the assumption
751	that we would cast it down afterwards anyway. *)
752	definition binop_simplifiable ≝
753	λop. match op with [ Oadd ⇒ true \| Osub ⇒ true \| _ ⇒ false ].
754
755	(* Inversion principle for integer addition *)
756	lemma iadd_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r →
757	∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (addition_n (bitsize_of_intsize dsz) i1 i2)).
758	#sz #sg #v1 #v2 #m #r
759	elim v1
760	[ 1: \| 2: #sz' #i \| 3: #f \| 4: \| 5: #ptr ]
761	whd in ⊢ ((??%?) → ?); normalize nodelta
762	>classify_add_int normalize nodelta #H destruct
763	elim v2 in H;
764	[ 1: \| 2: #sz'' #i' \| 3: #f' \| 4: \| 5: #ptr' ]
765	whd in ⊢ ((??%?) → ?); #H destruct
766	elim (sz_eq_dec sz' sz'')
767	[ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/
768	\| 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct
769	] qed.
770
771	(* Inversion principle for integer subtraction. *)
772	lemma isub_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r →
773	∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (subtraction ? i1 i2)).
774	#sz #sg #v1 #v2 #m #r
775	elim v1
776	[ 1: \| 2: #sz' #i \| 3: #f \| 4: \| 5: #ptr ]
777	whd in ⊢ ((??%?) → ?); normalize nodelta
778	>classify_sub_int normalize nodelta #H destruct
779	elim v2 in H;
780	[ 1: \| 2: #sz'' #i' \| 3: #f' \| 4: \| 5: #ptr' ]
781	whd in ⊢ ((??%?) → ?); #H destruct
782	elim (sz_eq_dec sz' sz'')
783	[ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/
784	\| 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct
785	] qed.
786
787	definition is_int : val → Prop ≝
788	λv.
789	match v with
790	[ Vint _ _ ⇒ True
791	\| _ ⇒ False ].
792
793	(* "negative" (in the sense of ¬ Some) inversion principle for integer addition *)
794	lemma neg_iadd_inv : ∀sz,sg,v1,v2,m. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m = None ? →
795	¬ (is_int v1) ∨ ¬ (is_int v2) ∨
796	∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2.
797	#sz #sg #v1 #v2 #m
798	elim v1
799	[ 1: \| 2: #sz' #i \| 3: #f \| 4: \| 5: #ptr ]
800	[ 2: \| *: #_ %1 %1 % #H @H ]
801	elim v2
802	[ 1: \| 2: #sz'' #i' \| 3: #f' \| 4: \| 5: #ptr' ]
803	[ 2: \| *: #_ %1 %2 % #H @H ]
804	whd in ⊢ ((??%?) → ?); normalize nodelta
805	>classify_add_int normalize nodelta
806	elim (sz_eq_dec sz' sz'')
807	[ 1: #Heq destruct >intsize_eq_elim_true #Habsurd destruct (Habsurd)
808	\| 2: #Hneq >intsize_eq_elim_false try assumption #_
809	%2 %{sz'} %{sz''} %{i} %{i'} try @conj try @conj //
810	] qed.
811
812	(* "negative" inversion principle for integer subtraction *)
813	lemma neg_isub_inv : ∀sz,sg,v1,v2,m. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = None ? →
814	¬ (is_int v1) ∨ ¬ (is_int v2) ∨
815	∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2.
816	#sz #sg #v1 #v2 #m
817	elim v1
818	[ 1: \| 2: #sz' #i \| 3: #f \| 4: \| 5: #ptr ]
819	[ 2: \| *: #_ %1 %1 % #H @H ]
820	elim v2
821	[ 1: \| 2: #sz'' #i' \| 3: #f' \| 4: \| 5: #ptr' ]
822	[ 2: \| *: #_ %1 %2 % #H @H ]
823	whd in ⊢ ((??%?) → ?); normalize nodelta
824	>classify_sub_int normalize nodelta
825	elim (sz_eq_dec sz' sz'')
826	[ 1: #Heq destruct >intsize_eq_elim_true #Habsurd destruct (Habsurd)
827	\| 2: #Hneq >intsize_eq_elim_false try assumption #_
828	%2 %{sz'} %{sz''} %{i} %{i'} try @conj try @conj //
829	] qed.
830
831
832	lemma simplifiable_op_inconsistent : ∀op,sz,sg,v1,v2,m.
833	¬ (is_int v1) → binop_simplifiable op = true → sem_binary_operation op v1 (Tint sz sg) v2 (Tint sz sg) m = None ?.
834	#op #sz #sg #v1 #v2 #m #H
835	elim op normalize in match (binop_simplifiable ?); #H destruct
836	elim v1 in H;
837	[ 1,6: \| 2,7: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I)) \| 3,8: #f \| 4,9: \| 5,10: #ptr ]
838	#_
839	whd in match (sem_binary_operation ??????); normalize nodelta
840	>classify_add_int normalize nodelta //
841	>classify_sub_int normalize nodelta //
842	qed.
843
844	notation > "hvbox('let' «ident x,ident y» 'as' ident E ≝ t 'in' s)"
845	with precedence 10
846	for @{ match $t return λx.x = $t → ? with [ mk_Sig ${ident x} ${ident y} ⇒ λ${ident E}.$s ] (refl ? $t) }.
847
848	notation > "hvbox('let' « 〈ident x1,ident x2〉, ident y» 'as' ident E, ident F ≝ t 'in' s)"
849	with precedence 10
850	for @{ match $t return λx.x = $t → ? with
851	[ mk_Sig ${fresh a} ${ident y} ⇒ λ${ident E}.
852	match ${fresh a} return λx.x = ${fresh a} → ? with
853	[ mk_Prod ${ident x1} ${ident x2} ⇒ λ${ident F}. $s ] (refl ? ${fresh a})
854	] (refl ? $t)
855	}.
856
857	(* This function will make your eyes bleed. You've been warned.
858	* Implements a correct-by-construction version of Brian's original cast-removal code. Does so by
859	* threading an invariant defined in [simplify_inv], which says roughly "simplification yields either
860	what you hoped for, i.e. an integer value of the right size, OR something equivalent to the original
861	expression". [simplify_expr] is not to be called directly: simplify inside is the proper wrapper.
862	* TODO: proper doc. Some cases are simplifiable. Some type equality tests are maybe dispensable.
863	* This function is slightly more conservative than the original one, but this should be incrementally
864	* modifiable (replacing calls to simplify_inside by calls to simplify_expr, + proving correction).
865	* Also, I think that the proofs are factorizable to a great deal, but I'd rather have something
866	* more or less "modular", case-by-case wise.
867	*)
868	let rec simplify_expr (e:expr) (target_sz:intsize) (target_sg:signedness)
869	: Σresult:bool×expr. ∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result) ≝
870	match e return λx. x = e → ? with
871	[ Expr ed ty ⇒ λHexpr_eq.
872	match ed return λx. ed = x → ? with
873	[ Econst_int cst_sz i ⇒ λHdesc_eq.
874	match ty return λx. x=ty → ? with
875	[ Tint ty_sz sg ⇒ λHexprtype_eq.
876	(* Ensure that the displayed type size [cst_sz] and actual size [sz] are equal ... *)
877	match sz_eq_dec cst_sz ty_sz with
878	[ inl Hsz_eq ⇒
879	match type_eq_dec ty (Tint target_sz target_sg) with
880	[ inl Hdonothing ⇒ «〈true, e〉, ?»
881	\| inr Hdosomething ⇒
882	(* Do the actual useful work *)
883	match simplify_int cst_sz target_sz sg target_sg i return λx. (simplify_int cst_sz target_sz sg target_sg i) = x → ? with
884	[ Some i' ⇒ λHsimpl_eq.
885	«〈true, Expr (Econst_int target_sz i') (Tint target_sz target_sg)〉, ?»
886	\| None ⇒ λ_.
887	«〈false, e〉, ?»
888	] (refl ? (simplify_int cst_sz target_sz sg target_sg i))
889	]
890	\| inr _ ⇒ (* The expression is ill-typed. *)
891	«〈false, e〉, ?»
892	]
893	\| _ ⇒ λ_.
894	«〈false, e〉, ?»
895	] (refl ? ty)
896	\| Ederef e1 ⇒ λHdesc_eq.
897	let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in
898	«〈false, Expr (Ederef e2) ty〉, ?»
899	\| Eaddrof e1 ⇒ λHdesc_eq.
900	let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in
901	«〈false, Expr (Eaddrof e2) ty〉, ?»
902	\| Eunop op e1 ⇒ λHdesc_eq.
903	let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in
904	«〈false, Expr (Eunop op e2) ty〉, ?»
905	\| Ebinop op lhs rhs ⇒ λHdesc_eq.
906	(* Type equality is enforced to prove the equalities needed in return by the invariant. *)
907	match binop_simplifiable op
908	return λx. (binop_simplifiable op) = x → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)))
909	with
910	[ true ⇒ λHop_simplifiable_eq.
911	match assert_type_eq ty (typeof lhs) with
912	[ OK Hty_eq_lhs ⇒
913	match assert_type_eq (typeof lhs) (typeof rhs) with
914	[ OK Htylhs_eq_tyrhs ⇒
915	let «〈desired_type_lhs, lhs1〉, Hinv_lhs» as Hsimplify_lhs, Hpair_lhs ≝ simplify_expr lhs target_sz target_sg in
916	let «〈desired_type_rhs, rhs1〉, Hinv_rhs» as Hsimplify_rhs, Hpair_rhs ≝ simplify_expr rhs target_sz target_sg in
917	match desired_type_lhs ∧ desired_type_rhs
918	return λx. (desired_type_lhs ∧ desired_type_rhs) = x → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)))
919	with
920	[ true ⇒ λHdesired_eq.
921	«〈true, Expr (Ebinop op lhs1 rhs1) (Tint target_sz target_sg)〉, ?»
922	\| false ⇒ λHdesired_eq.
923	let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in
924	let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in
925	«〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?»
926	] (refl ? (desired_type_lhs ∧ desired_type_rhs))
927	\| Error _ ⇒
928	let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in
929	let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in
930	«〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?»
931	]
932	\| Error _ ⇒
933	let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in
934	let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in
935	«〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?»
936	]
937	\| false ⇒ λHop_simplifiable_eq.
938	let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in
939	let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in
940	«〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?»
941	] (refl ? (binop_simplifiable op))
942	\| Ecast cast_ty castee ⇒ λHdesc_eq.
943	match cast_ty return λx. x = cast_ty → ? with
944	[ Tint cast_sz cast_sg ⇒ λHcast_ty_eq.
945	match type_eq_dec ty cast_ty with
946	[ inl Hcast_eq ⇒
947	match necessary_conditions cast_sz cast_sg target_sz target_sg
948	return λx. x = (necessary_conditions cast_sz cast_sg target_sz target_sg) → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)))
949	with
950	[ true ⇒ λHconditions.
951	let «〈desired_type, castee1〉, Hcastee_inv» as Hsimplify1, Hpair1 ≝ simplify_expr castee target_sz target_sg in
952	match desired_type return λx. desired_type = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result))
953	with
954	[ true ⇒ λHdesired_eq.
955	«〈true, castee1〉, ?»
956	\| false ⇒ λHdesired_eq.
957	let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr castee cast_sz cast_sg in
958	match desired_type2 return λx. desired_type2 = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result))
959	with
960	[ true ⇒ λHdesired2_eq.
961	«〈false, castee2〉, ?»
962	\| false ⇒ λHdesired2_eq.
963	«〈false, Expr (Ecast ty castee2) cast_ty〉, ?»
964	] (refl ? desired_type2)
965	] (refl ? desired_type)
966	\| false ⇒ λHconditions.
967	let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr castee cast_sz cast_sg in
968	match desired_type2 return λx. desired_type2 = x → Σresult:bool×expr. (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result))
969	with
970	[ true ⇒ λHdesired2_eq.
971	«〈false, castee2〉, ?»
972	\| false ⇒ λHdesired2_eq.
973	«〈false, Expr (Ecast ty castee2) cast_ty〉, ?»
974	] (refl ? desired_type2)
975	] (refl ? (necessary_conditions cast_sz cast_sg target_sz target_sg))
976	\| inr Hcast_neq ⇒
977	(* inconsistent types ... *)
978	let «castee1, Hcastee_equiv» as Hsimplify ≝ simplify_inside castee in
979	«〈false, Expr (Ecast cast_ty castee1) ty〉, ?»
980	]
981	\| _ ⇒ λHcast_ty_eq.
982	let «castee1, Hcastee_equiv» as Hsimplify ≝ simplify_inside castee in
983	«〈false, Expr (Ecast cast_ty castee1) ty〉, ?»
984	] (refl ? cast_ty)
985	\| Econdition cond iftrue iffalse ⇒ λHdesc_eq.
986	let «cond1, Hcond_equiv» as Hsimplify ≝ simplify_inside cond in
987	match assert_type_eq ty (typeof iftrue) with
988	[ OK Hty_eq_iftrue ⇒
989	match assert_type_eq (typeof iftrue) (typeof iffalse) with
990	[ OK Hiftrue_eq_iffalse ⇒
991	let «〈desired_true, iftrue1〉, Htrue_inv» as Hsimplify_iftrue, Hpair_iftrue ≝ simplify_expr iftrue target_sz target_sg in
992	let «〈desired_false, iffalse1〉, Hfalse_inv» as Hsimplify_iffalse, Hpair_iffalse ≝ simplify_expr iffalse target_sz target_sg in
993	match desired_true ∧ desired_false
994	return λx. (desired_true ∧ desired_false) = x → (Σresult:(bool × expr). (∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result)))
995	with
996	[ true ⇒ λHdesired_eq.
997	«〈true, Expr (Econdition cond1 iftrue1 iffalse1) (Tint target_sz target_sg)〉, ?»
998	\| false ⇒ λHdesired_eq.
999	let «iftrue1, Htrue_equiv» as Hsimplify_iftrue ≝ simplify_inside iftrue in
1000	let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in
1001	«〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?»
1002	] (refl ? (desired_true ∧ desired_false))
1003	\| _ ⇒
1004	let «iftrue1, Htrue_equiv» as Hsimplify_iftrue ≝ simplify_inside iftrue in
1005	let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in
1006	«〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?»
1007	]
1008	\| _ ⇒
1009	let «iftrue1, Htrue_equiv» as Hsimplify_iftrue ≝ simplify_inside iftrue in
1010	let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in
1011	«〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?»
1012	]
1013	(* Could probably do better with these, too. *)
1014	\| Eandbool lhs rhs ⇒ λHdesc_eq.
1015	let «lhs1, Hlhs_equiv» as Eq1 ≝ simplify_inside lhs in
1016	let «rhs1, Hrhs_equiv» as Eq2 ≝ simplify_inside rhs in
1017	«〈false, Expr (Eandbool lhs1 rhs1) ty〉, ?»
1018	\| Eorbool lhs rhs ⇒ λHdesc_eq.
1019	let «lhs1, Hlhs_equiv» as Eq1 ≝ simplify_inside lhs in
1020	let «rhs1, Hrhs_equiv» as Eq2 ≝ simplify_inside rhs in
1021	«〈false, Expr (Eorbool lhs1 rhs1) ty〉,?»
1022	(* Could also improve Esizeof *)
1023	\| Efield rec_expr f ⇒ λHdesc_eq.
1024	let «rec_expr1, Hrec_expr_equiv» as Hsimplify ≝ simplify_inside rec_expr in
1025	«〈false,Expr (Efield rec_expr1 f) ty〉, ?»
1026	\| Ecost l e1 ⇒ λHdesc_eq.
1027	(* The invariant requires that the toplevel [ty] type matches the type of [e1]. *)
1028	(* /!\ XXX /!\ We assume that the type of a cost-labelled expr is the type of the underlying expr. *)
1029	match type_eq_dec ty (typeof e1) with
1030	[ inl Heq ⇒
1031	let «〈desired_type, e2〉, Hinv» as Hsimplify, Hpair ≝ simplify_expr e1 target_sz target_sg in
1032	«〈desired_type, Expr (Ecost l e2) (typeof e2)〉, ?»
1033	\| inr Hneq ⇒
1034	let «e2, Hexpr_equiv» as Eq ≝ simplify_inside e1 in
1035	«〈false, Expr (Ecost l e2) ty〉, ?»
1036	]
1037	\| Econst_float f ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?»
1038	(* \| Evar id ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?» *)
1039	(* In order for the simplification function to be less dymp, we would have to use this line, which would in fact
1040	require to alter the semantics of [load_value_of_type]. *)
1041	\| Evar id ⇒ λHdesc_eq. «〈type_eq ty (Tint target_sz target_sg), Expr ed ty〉, ?»
1042	\| Esizeof t ⇒ λHdesc_eq. «〈type_eq ty (Tint target_sz target_sg), Expr ed ty〉, ?»
1043	] (refl ? ed)
1044	] (refl ? e)
1045
1046	and simplify_inside (e:expr) : Σresult:expr. conservation e result ≝
1047	match e return λx. x = e → ? with
1048	[ Expr ed ty ⇒ λHexpr_eq.
1049	match ed return λx. x = ed → ? with
1050	[ Ederef e1 ⇒ λHdesc_eq.
1051	let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in
1052	«Expr (Ederef e2) ty, ?»
1053	\| Eaddrof e1 ⇒ λHdesc_eq.
1054	let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in
1055	«Expr (Eaddrof e2) ty, ?»
1056	\| Eunop op e1 ⇒ λHdesc_eq.
1057	let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in
1058	«Expr (Eunop op e2) ty, ?»
1059	\| Ebinop op lhs rhs ⇒ λHdesc_eq.
1060	let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in
1061	let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in
1062	«Expr (Ebinop op lhs1 rhs1) ty, ?»
1063	\| Ecast cast_ty castee ⇒ λHdesc_eq.
1064	match type_eq_dec ty cast_ty with
1065	[ inl Hcast_eq ⇒
1066	match cast_ty return λx. x = cast_ty → Σresult:expr. conservation e result
1067	with
1068	[ Tint cast_sz cast_sg ⇒ λHcast_ty_eq.
1069	let «〈success, castee1〉, Htrans_inv» as Hsimplify, Hpair ≝ simplify_expr castee cast_sz cast_sg in
1070	match success return λx. x = success → Σresult:expr. conservation e result
1071	with
1072	[ true ⇒ λHsuccess_eq.
1073	«castee1, ?»
1074	\| false ⇒ λHsuccess_eq.
1075	«Expr (Ecast cast_ty castee1) ty, ?»
1076	] (refl ? success)
1077	\| _ ⇒ λHcast_ty_eq.
1078	«e, ?»
1079	] (refl ? cast_ty)
1080	\| inr Hcast_neq ⇒
1081	«e, ?»
1082	]
1083	\| Econdition cond iftrue iffalse ⇒ λHdesc_eq.
1084	let «cond1, Hequiv_cond» as Eq_cond ≝ simplify_inside cond in
1085	let «iftrue1, Hequiv_iftrue» as Eq_iftrue ≝ simplify_inside iftrue in
1086	let «iffalse1, Hequiv_iffalse» as Eq_iffalse ≝ simplify_inside iffalse in
1087	«Expr (Econdition cond1 iftrue1 iffalse1) ty, ?»
1088	\| Eandbool lhs rhs ⇒ λHdesc_eq.
1089	let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in
1090	let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in
1091	«Expr (Eandbool lhs1 rhs1) ty, ?»
1092	\| Eorbool lhs rhs ⇒ λHdesc_eq.
1093	let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in
1094	let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in
1095	«Expr (Eorbool lhs1 rhs1) ty, ?»
1096	\| Efield rec_expr f ⇒ λHdesc_eq.
1097	let «rec_expr1, Hequiv_rec» as Eq_rec ≝ simplify_inside rec_expr in
1098	«Expr (Efield rec_expr1 f) ty, ?»
1099	\| Ecost l e1 ⇒ λHdesc_eq.
1100	let «e2, Hequiv» as Eq ≝ simplify_inside e1 in
1101	«Expr (Ecost l e2) ty, ?»
1102	\| _ ⇒ λHdesc_eq.
1103	«e, ?»
1104	] (refl ? ed)
1105	] (refl ? e).
1106	#ge #en #m
1107	[ 1,3,5,6,7,8,9,10,11,12: %1 try @refl
1108	cases (exec_expr ge en m e) #res
1109	try (@(SimOk ???) //)
1110	\| 2: @(Inv_coerce_ok ge en m … target_sz target_sg target_sz target_sg) destruct /by refl/
1111	(*
1112	whd in match (exec_expr ????); >eq_intsize_identity whd
1113	>sz_eq_identity normalize % [ 1: @conj // \| 2: elim target_sz in i; normalize #i @I ]
1114	*)
1115	\| 4: destruct @(Inv_coerce_ok ge en m ???? ty_sz sg) / by refl/
1116	whd in match (exec_expr ????);
1117	whd in match (exec_expr ????);
1118	>eq_intsize_identity >eq_intsize_identity whd
1119	#v1 #Heq destruct (Heq) %{i'} try @conj try @conj try @conj //
1120	[ 1: @(simplify_int_implements_cast … Hsimpl_eq)
1121	\| 2: @(simplify_int_success_lt … Hsimpl_eq) ]
1122	\| 13: %1 // >Hexpr_eq cases (exec_expr ge en m e) #res
1123	try (@(SimOk ???) //)
1124	\| 14: elim (type_eq_dec ty (Tint target_sz target_sg))
1125	[ 1: #Heq >Heq >type_eq_identity @(Inv_coerce_ok ??????? target_sz target_sg)
1126	destruct
1127	[ 1,2: //
1128	\| 3: @smaller_integer_val_identity ]
1129	\| 2: #Hneq >(type_neq_not_identity … Hneq) %1 // destruct
1130	@(SimOk ???) //
1131	]
1132	\| 15: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
1133	[ 1: (* Proving preservation of the semantics for expressions. *)
1134	cases Hexpr_sim
1135	[ 2: (* Case where the evaluation of e1 as an expression fails *)
1136	normalize * #err #Hfail >Hfail normalize nodelta @SimFailNicely
1137	\| 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
1138	#Hsim %1 * #val #trace normalize #Hstep
1139	cut (∃ptr. (exec_expr ge en m e1 = OK ? 〈Vptr ptr, trace〉) ∧
1140	(load_value_of_type ty m (pblock ptr) (poff ptr) = Some ? val))
1141	[ 1: lapply Hstep -Hstep
1142	cases (exec_expr ge en m e1)
1143	[ 1: * #val' #trace' normalize nodelta
1144	cases val' normalize nodelta
1145	[ 1,2,3,4: #H1 destruct #H2 destruct #H3 destruct
1146	\| 5: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *)
1147	cases (load_value_of_type ty m (pblock pointer) (poff pointer)) in Heq;
1148	normalize nodelta
1149	[ 1: #Heq destruct \| 2: #val2 #Heq destruct @conj // ]
1150	]
1151	\| 2: normalize nodelta #errmesg #Hcontr destruct
1152	]
1153	\| 2: * #e1_ptr * #He1_eq_ptr #Hloadptr
1154	cut (∃ptr1. (exec_expr ge en m e2 = OK ? 〈Vptr ptr1, trace〉)
1155	∧ (load_value_of_type ty m (pblock ptr1) (poff ptr1) = Some ? val))
1156	[ 1: @(ex_intro … e1_ptr) @conj
1157	[ 1: @Hsim // \| 2: // ]
1158	\| 2: * #e2_ptr * #He2_exec #Hload_e2_ptr
1159	normalize >He2_exec normalize nodelta >Hload_e2_ptr normalize nodelta @refl
1160	]
1161	]
1162	]
1163	\| 2: (* Proving the preservation of the semantics for lvalues. *)
1164	cases Hexpr_sim
1165	[ 2: (* Case where the evaluation of e1 as an lvalue fails *)
1166	normalize * #err #Hfail >Hfail normalize nodelta @SimFailNicely
1167	\| 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
1168	#Hsim %1 * * #block #offset #trace normalize #Hstep
1169	cut (∃ptr. (exec_expr ge en m e1 = OK ? 〈Vptr ptr, trace〉) ∧ pblock ptr = block ∧ poff ptr = offset)
1170	[ 1: lapply Hstep -Hstep
1171	cases (exec_expr ge en m e1)
1172	[ 1: * #val' #trace' normalize nodelta
1173	cases val' normalize nodelta
1174	[ 1,2,3,4: #H1 destruct #H2 destruct #H3 destruct
1175	\| 5: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *)
1176	destruct try @conj try @conj //
1177	]
1178	\| 2: normalize nodelta #errmesg #Hcontr destruct
1179	]
1180	\| 2: * #e1_ptr * * #He1_eq_ptr #Hblock #Hoffset
1181	cut (∃ptr1. (exec_expr ge en m e2 = OK ? 〈Vptr ptr1, trace〉) ∧ pblock ptr1 = block ∧ poff ptr1 = offset)
1182	[ 1: @(ex_intro … e1_ptr) @conj try @conj // @Hsim //
1183	\| 2: * #e2_ptr * * #He2_exec #Hblock #Hoffset
1184	normalize >He2_exec normalize nodelta //
1185	]
1186	]
1187	]
1188	]
1189	\| 16: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
1190	[ 1: (* Proving preservation of the semantics for expressions. *)
1191	cases Hlvalue_sim
1192	[ 2: (* Case where the evaluation of e1 as an expression fails *)
1193	* #err #Hfail whd in match (exec_expr ????); >Hfail @SimFailNicely
1194	\| 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
1195	#Hsim %1 * #val #trace whd in match (exec_expr ????); #Hstep
1196	cut (∃block,offset,ptype. (exec_lvalue ge en m e1 = OK ? 〈block, offset, trace〉) ∧
1197	(ty = Tpointer ptype) ∧
1198	val = Vptr (mk_pointer block offset))
1199	[ 1: lapply Hstep -Hstep
1200	cases (exec_lvalue ge en m e1)
1201	[ 1: * * #block #offset #trace' normalize nodelta
1202	cases ty
1203	[ 2: #sz #sg \| 3: #fsz \| 4: #ptr_ty \| 5: #array_ty #array_sz \| 6: #domain #codomain
1204	\| 7: #structname #fieldspec \| 8: #unionname #fieldspec \| 9: #id ]
1205	normalize nodelta try (#Heq destruct)
1206	@(ex_intro … block) @(ex_intro … offset) @(ex_intro … ptr_ty)
1207	try @conj try @conj destruct //
1208	\| 2: normalize nodelta #errmesg #Hcontr destruct
1209	]
1210	\| 2: * #block * #offset * #ptype * * #Hexec_lvalue #Hty_eq #Hval_eq
1211	whd in match (exec_expr ????); >(Hsim … Hexec_lvalue) normalize nodelta destruct normalize nodelta
1212	//
1213	]
1214	]
1215	\| 2: (* Proving preservation of the semantics of lvalues. *)
1216	@SimFailNicely
1217	]
1218	\| 17: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
1219	[ 1: whd in match (exec_expr ge en m (Expr ??));
1220	whd in match (exec_expr ge en m (Expr ??));
1221	cases Hexpr_sim
1222	[ 2: * #error #Hexec >Hexec normalize nodelta @SimFailNicely
1223	\| 1: cases (exec_expr ge en m e1)
1224	[ 2: #error #Hexec normalize nodelta @SimFailNicely
1225	\| 1: * #val #trace #Hexec
1226	>(Hexec ? (refl ? (OK ? 〈val,trace〉)))
1227	normalize nodelta @SimOk #a >Htype_eq #H @H
1228	]
1229	]
1230	\| 2: @SimFailNicely
1231	]
1232	\| 18: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_lhs #Hdesired_rhs -Hdesired_eq
1233	inversion (Hinv_lhs ge en m)
1234	[ 1: #result_flag_lhs #Hresult_lhs #Htype_lhs #Hsim_expr_lhs #Hsim_lvalue_lhs #Hresult_flag_lhs_eq_true
1235	#Hinv <Hresult_flag_lhs_eq_true in Hresult_lhs; >Hdesired_lhs #Habsurd destruct
1236	\| 2: #lhs_src_sz #lhs_src_sg #Htype_lhs #Htype_lhs1 #Hsmaller_lhs #Hdesired_type_lhs #_
1237	inversion (Hinv_rhs ge en m)
1238	[ 1: #result_flag_rhs #Hresult_rhs #Htype_rhs #Hsim_expr_rhs #Hsim_lvalue_rhs #Hdesired_type_rhs_eq #_
1239	<Hdesired_type_rhs_eq in Hresult_rhs; >Hdesired_rhs #Habsurd destruct
1240	\| 2: #rhs_src_sz #rhs_src_sg #Htype_rhs #Htype_rhs1 #Hsmaller_rhs #Hdesired_type_rhs #_
1241	@(Inv_coerce_ok ge en m … target_sz target_sg lhs_src_sz lhs_src_sg)
1242	[ 1: >Htype_lhs //
1243	\| 2: //
1244	\| 3: whd in match (exec_expr ??? (Expr ??));
1245	whd in match (exec_expr ??? (Expr ??));
1246	(* Tidy up the type equations *)
1247	>Htype_lhs in Htylhs_eq_tyrhs; >Htype_rhs #Heq destruct
1248	lapply Hsmaller_rhs lapply Hsmaller_lhs
1249	generalize in match rhs_src_sz; #src_sz
1250	generalize in match rhs_src_sg; #src_sg
1251	-Hsmaller_lhs -Hsmaller_rhs -Htype_lhs -Htype_rhs -Hinv_lhs -Hinv_rhs
1252	>Htype_lhs1 >Htype_rhs1 -Htype_lhs1 -Htype_rhs1
1253	(* Enumerate all the cases for the evaluation of the source expressions ... *)
1254	cases (exec_expr ge en m lhs);
1255	try // * #val_lhs #trace_lhs normalize nodelta
1256	cases (exec_expr ge en m rhs);
1257	try // * #val_rhs #trace_rhs normalize nodelta
1258	whd in match (m_bind ?????);
1259	(* specialize to the actual simplifiable operations. *)
1260	cases op in Hop_simplifiable_eq;
1261	[ 1,2: \| *: normalize in ⊢ (% → ?); #H destruct (H) ] #_
1262	[ 1: lapply (iadd_inv src_sz src_sg val_lhs val_rhs m)
1263	\| 2: lapply (isub_inv src_sz src_sg val_lhs val_rhs m) ]
1264	cases (sem_binary_operation ? val_lhs (Tint src_sz src_sg) val_rhs (Tint src_sz src_sg) m)
1265	[ 1,3: #_ #_ #_ normalize @I ]
1266	#src_result #Hinversion_src elim (Hinversion_src src_result (refl ? (Some ? src_result)))
1267	#src_result_sz * #i1 * #i2 * * #Hval_lhs_eq #Hval_rhs_eq #Hsrc_result_eq
1268	whd in match (opt_to_res ???); whd in match (m_bind ?????); normalize nodelta
1269	>Hval_lhs_eq >Hval_rhs_eq #Hsmaller_rhs #Hsmaller_lhs
1270	whd
1271	#result_int #Hsrc_result >Hsrc_result in Hsrc_result_eq; #Hsrc_result_eq
1272	lapply (sym_eq ??? Hsrc_result_eq) -Hsrc_result_eq #Hsrc_result_eq
1273	cut (src_result_sz = src_sz) [ 1,3: destruct // ] #Hsz_eq
1274	lapply Hsmaller_lhs lapply Hsmaller_rhs
1275	cases (exec_expr ge en m lhs1) normalize nodelta
1276	[ 2,4: destruct #error normalize in ⊢ (% → ?); #H @(False_ind … (H i1 (refl ? (Vint src_sz i1)))) ]
1277	* #val_lhs1 #trace_lhs1
1278	cases (exec_expr ge en m rhs1)
1279	[ 2,4: destruct #error #_ normalize in ⊢ (% → ?); #H @(False_ind … (H i2 (refl ? (Vint src_sz i2)))) ]
1280	* #val_rhs1 #trace_rhs1
1281	whd in match (m_bind ?????); normalize nodelta
1282	[ 1: lapply (neg_iadd_inv target_sz target_sg val_lhs1 val_rhs1 m)
1283	lapply (iadd_inv target_sz target_sg val_lhs1 val_rhs1 m)
1284	\| 2: lapply (neg_isub_inv target_sz target_sg val_lhs1 val_rhs1 m)
1285	lapply (isub_inv target_sz target_sg val_lhs1 val_rhs1 m) ]
1286	cases (sem_binary_operation ? val_lhs1 (Tint target_sz target_sg) val_rhs1 (Tint target_sz target_sg) m)
1287	[ 1,3: destruct #_ #Hneg_inversion elim (Hneg_inversion (refl ? (None ?)))
1288	(* Proceed by case analysis on Hneg_inversion to prove the absurdity of this branch *)
1289	*
1290	[ 1,4: whd in ⊢ (? → % → ?); normalize nodelta
1291	#Habsurd #Hcounterexample elim (Hcounterexample i1 (refl ? (Vint src_sz i1)))
1292	#i * * * #Hlhs1_is_int >Hlhs1_is_int in Habsurd; * #Habsurd
1293	@(False_ind … (Habsurd I))
1294	\| 2,5: whd in ⊢ (? → ? → % → ?); normalize nodelta
1295	#Habsurd #_ #Hcounterexample elim (Hcounterexample i2 (refl ? (Vint src_sz i2)))
1296	#i * * * #Hlhs1_is_int >Hlhs1_is_int in Habsurd; * #Habsurd
1297	@(False_ind … (Habsurd I))
1298	\| 3,6: #dsz1 * #dsz2 * #j1 * #j2 * * #Hval_lhs1 #Hval_rhs1 #Hsz_neq
1299	whd in ⊢ (% → % → ?); normalize nodelta
1300	#Hsmaller_lhs #Hsmaller_rhs
1301	elim (Hsmaller_lhs … i1 (refl ? (Vint src_sz i1)))
1302	#li * * * #Hval_lhs1_alt #H_lhs_cast_eq #Htrace_eq_lhs #Hsize_le
1303	elim (Hsmaller_rhs … i2 (refl ? (Vint src_sz i2)))
1304	#ri * * * #Hval_rhs1_alt #H_rhs_cast_eq #Htrace_eq_rhs #_
1305	destruct elim Hsz_neq #Habsurd @(Habsurd (refl ? target_sz))
1306	]
1307	\| 2,4: destruct #result #Hinversion #_ #Hsmaller_lhs #Hsmaller_rhs normalize nodelta
1308	elim (Hinversion result (refl ? (Some ? result)))
1309	#result_sz * #lhs_int * #rhs_int * * #Hlhs1_eq #Hrhs1_eq #Hop_eq
1310	elim (Hsmaller_lhs … i1 (refl ? (Vint src_sz i1)))
1311	#li * * * #Hval_lhs1_alt #H_lhs_cast_eq #Htrace_eq_lhs #Hsize_le
1312	elim (Hsmaller_rhs … i2 (refl ? (Vint src_sz i2)))
1313	#ri * * * #Hval_rhs1_alt #H_rhs_cast_eq #Htrace_eq_rhs #_
1314	destruct
1315	[ 1: %{(addition_n (bitsize_of_intsize target_sz)
1316	(cast_int_int src_sz src_sg target_sz i1)
1317	(cast_int_int src_sz src_sg target_sz i2))}
1318	try @conj try @conj try @conj //
1319	>integer_add_cast_le try //
1320	\| 2: %{(subtraction (bitsize_of_intsize target_sz)
1321	(cast_int_int src_sz src_sg target_sz i1)
1322	(cast_int_int src_sz src_sg target_sz i2))}
1323	try @conj try @conj try @conj //
1324	>integer_sub_cast_le try //
1325	]
1326	] ] ] ]
1327	\| 19,20,21,22: destruct %1 try @refl
1328	elim (Hequiv_lhs ge en m) * #Hexpr_sim_lhs #Hlvalue_sim_lhs #Htype_eq_lhs
1329	elim (Hequiv_rhs ge en m) * #Hexpr_sim_rhs #Hlvalue_sim_rhs #Htype_eq_rhs
1330	[ 1,3,5,7:
1331	whd in match (exec_expr ????); whd in match (exec_expr ????);
1332	cases Hexpr_sim_lhs
1333	[ 2,4,6,8: * #error #Herror >Herror @SimFailNicely
1334	\| *: cases (exec_expr ge en m lhs)
1335	[ 2,4,6,8: #error #_ @SimFailNicely
1336	\| : #lval #ltrace #Hsim_lhs normalize nodelta
1337	cases Hexpr_sim_rhs
1338	[ 2,4,6,8: * #error #Herror >Herror @SimFailNicely
1339	\| *: cases (exec_expr ge en m rhs)
1340	[ 2,4,6,8: #error #_ @SimFailNicely
1341	\| : #rval #rtrace #Hsim_rhs
1342	whd in match (exec_expr ??? (Expr (Ebinop ???) ?));
1343	>(Hsim_lhs 〈lval,ltrace〉 (refl ? (OK ? 〈lval,ltrace〉)))
1344	>(Hsim_rhs 〈rval,rtrace〉 (refl ? (OK ? 〈rval,rtrace〉)))
1345	normalize nodelta
1346	>Htype_eq_lhs >Htype_eq_rhs
1347	@SimOk * #val #trace #H @H
1348	]
1349	]
1350	]
1351	]
1352	\| *: @SimFailNicely
1353	]
1354	(* Jump to the cast cases *)
1355	\| 23,30,31,32,33,34,35,36: %1 try @refl
1356	[ 1,4,7,10,13,16,19,22: destruct // ]
1357	elim (Hcastee_equiv ge en m) * #Hexec_sim #Hlvalue_sim #Htype_eq
1358	(* exec_expr simulation *)
1359	[ 1,3,5,7,9,11,13,15: cases Hexec_sim
1360	[ 2,4,6,8,10,12,14,16: destruct * #error #Hexec_fail whd in match (exec_expr ge en m ?);
1361	>Hexec_fail @SimFailNicely
1362	\| 1,3,5,7,9,11,13,15: #Hsim @SimOk * #val #trace <Hexpr_eq >Hdesc_eq
1363	whd in match (exec_expr ge en m ?); #Hstep
1364	cut (∃v1. exec_expr ge en m castee = OK ? 〈v1,trace〉
1365	∧ exec_cast m v1 (typeof castee) cast_ty = OK ? val)
1366	[ 1,3,5,7,9,11,13,15:
1367	lapply Hstep -Hstep cases (exec_expr ge en m castee)
1368	[ 2,4,6,8,10,12,14,16: #error1 normalize nodelta #Hcontr destruct
1369	\| 1,3,5,7,9,11,13,15: * #val1 #trace1 normalize nodelta
1370	#Hstep @(ex_intro … val1)
1371	cases (exec_cast m val1 (typeof castee) cast_ty) in Hstep;
1372	[ 2,4,6,8,10,12,14,16: #error #Hstep normalize in Hstep; destruct
1373	\| 1,3,5,7,9,11,13,15: #result #Hstep normalize in Hstep; destruct
1374	@conj @refl
1375	]
1376	]
1377	\| 2,4,6,8,10,12,14,16: * #v1 * #Hexec_expr #Hexec_cast
1378	whd in match (exec_expr ge en m ?);
1379	>(Hsim … Hexec_expr ) normalize nodelta
1380	<Htype_eq >Hexec_cast //
1381	]
1382	]
1383	\| 2,4,6,8,10,12,14,16: destruct @SimFailNicely
1384	]
1385	\| 24: destruct inversion (Hcastee_inv ge en m)
1386	[ 1: #result_flag #Hresult_flag #Htype_eq #Hexpr_sim #Hlvalue_sim #Hresult_flag_2
1387	<Hresult_flag_2 in Hresult_flag; #Hcontr destruct
1388	\| 2: #src_sz #src_sg #Htype_castee #Htype_castee1 #Hsmaller_eval #_ #Hinv_eq
1389	@(Inv_coerce_ok ??????? cast_sz cast_sg)
1390	[ 1: // \| 2: <Htype_castee1 //
1391	\| 3: whd in match (exec_expr ??? (Expr ??));
1392	>Htype_castee
1393	(* Simplify the goal by culling impossible cases, using Hsmaller_val *)
1394	cases (exec_expr ge en m castee) in Hsmaller_eval;
1395	[ 2: #error //
1396	\| 1: * #castee_val #castee_trace #Hsmaller normalize nodelta
1397	lapply (exec_cast_inv castee_val src_sz src_sg cast_sz cast_sg m)
1398	cases (exec_cast m castee_val (Tint src_sz src_sg) (Tint cast_sz cast_sg))
1399	[ 2: #error #_ @I
1400	\| 1: #result #Hinversion elim (Hinversion result (refl ? (OK ? result)))
1401	#castee_int * #Hcastee_val_eq #Hresult_eq
1402	whd in match (m_bind ?????);
1403	#result_int #Hresult_eq2
1404	cases (exec_expr ge en m castee1) in Hsmaller;
1405	[ 2: #error normalize in ⊢ (% → ?); #Habsurd
1406	@(False_ind … (Habsurd castee_int Hcastee_val_eq))
1407	\| 1: * #val1 #trace1 whd in ⊢ (% → ?); normalize nodelta
1408	#Hsmaller elim (Hsmaller castee_int Hcastee_val_eq)
1409	#val1_int * * * #Hval1_eq #Hval1_int_eq #Hcastee_trace_eq
1410	destruct #Hle %{(cast_int_int src_sz src_sg target_sz castee_int)}
1411	try @conj try @conj try @conj try //
1412	[ 1: @cast_composition ] try assumption
1413	elim (necessary_conditions_spec … (sym_eq … Hconditions))
1414	[ 2,4: * #Heq >Heq #_ elim target_sz //
1415	\| 1,3: #Hlt @(size_lt_to_le ?? Hlt) ]
1416	] ] ] ] ]
1417	\| 25,27: destruct
1418	inversion (Hcast2 ge en m)
1419	[ 1,3: (* Impossible case. *)
1420	#result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #Hresult_contr <Hresult_contr in Hresult;
1421	#Hcontr destruct
1422	\| 2,4: (* We successfuly cast the expression to the desired type. We can thus get rid of the "cast" itself.
1423	We did not successfuly cast the subexpression to target_sz, though. *)
1424	#src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #_ #Hinv_eq
1425	@(Inv_eq ???????) //
1426	[ 1,3: >Htype_castee2 //
1427	\| 2,4: (* Prove simulation for exec_expr *)
1428	whd in match (exec_expr ??? (Expr ??));
1429	cases (exec_expr ge en m castee) in Hsmaller_eval;
1430	[ 2,4: (* erroneous evaluation of the original expression *)
1431	#error #Hsmaller_eval @SimFailNicely
1432	\| 1,3: * #val #trace normalize nodelta >Htype_castee
1433	lapply (exec_cast_inv val src_sz src_sg cast_sz cast_sg m)
1434	cases (exec_cast m val (Tint src_sz src_sg) (Tint cast_sz cast_sg))
1435	[ 2,4: #error #_ #_ @SimFailNicely
1436	\| 1,3: #result #Hinversion elim (Hinversion result (refl ??))
1437	#val_int * #Hval_eq #Hresult_eq
1438	cases (exec_expr ge en m castee2)
1439	[ 2,4: #error #Hsmaller_eval normalize in Hsmaller_eval; @(False_ind … (Hsmaller_eval val_int Hval_eq))
1440	\| 1,3: * #val1 #trace1 #Hsmaller elim (Hsmaller val_int Hval_eq)
1441	#val1_int * * * #Hval1_eq #Hcast_eq #Htrace_eq #Hle
1442	destruct @SimOk normalize #a #H @H ]
1443	] ]
1444	] ]
1445	\| 26,28: destruct
1446	inversion (Hcast2 ge en m)
1447	[ 2,4: (* Impossible case. *)
1448	#src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #Habsurd #Hinv_eq
1449	(* Do some gymnastic to transform the Habsurd jmeq into a proper, 'destruct'able eq *)
1450	letin Habsurd_eq ≝ (jmeq_to_eq ??? Habsurd) lapply Habsurd_eq
1451	-Habsurd_eq -Habsurd #Habsurd destruct
1452	\| 1,3: (* All our attempts at casting down the expression have failed. We still use the
1453	resulting expression, as we may have discovered and simplified unrelated casts. *)
1454	#result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #_ #Hinv
1455	@(Inv_eq ???????) //
1456	whd in match (exec_expr ??? (Expr ??));
1457	whd in match (exec_expr ??? (Expr ??));
1458	cases Hsim_expr
1459	[ 2,4: * #error #Hexec_err >Hexec_err @SimFailNicely
1460	\| 1,3: #Hexec_ok
1461	cases (exec_expr ge en m castee) in Hexec_ok;
1462	[ 2,4: #error #Hsim @SimFailNicely
1463	\| 1,3: * #val #trace #Hsim normalize nodelta
1464	>Htype_eq >(Hsim 〈val,trace〉 (refl ? (OK ? 〈val,trace〉))) normalize nodelta
1465	@SimOk #a #H @H
1466	]
1467	]
1468	]
1469	\| 29: destruct elim (Hcastee_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
1470	@(Inv_eq ???????) //
1471	whd in match (exec_expr ??? (Expr ??));
1472	whd in match (exec_expr ??? (Expr ??));
1473	cases Hsim_expr
1474	[ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
1475	\| 1: #Hexec_ok @SimOk * #val #trace
1476	cases (exec_expr ge en m castee) in Hexec_ok;
1477	[ 2: #error #Habsurd normalize in Habsurd; normalize nodelta #H destruct
1478	\| 1: * #val #trace #Hexec_ok normalize nodelta
1479	>(Hexec_ok … 〈val, trace〉 (refl ? (OK ? 〈val, trace〉)))
1480	>Htype_eq
1481	normalize nodelta #H @H
1482	]
1483	]
1484	\| 37: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_true #Hdesired_false -Hdesired_eq
1485	inversion (Htrue_inv ge en m)
1486	[ 1: #result_flag_true #Hresult_true #Htype_true #Hsim_expr_true #Hsim_lvalue_true #Hresult_flag_true_eq_false
1487	#Hinv <Hresult_flag_true_eq_false in Hresult_true; >Hdesired_true #Habsurd destruct
1488	\| 2: #true_src_sz #true_src_sg #Htype_eq_true #Htype_eq_true1 #Hsmaller_true #_ #Hinv_true
1489	inversion (Hfalse_inv ge en m)
1490	[ 1: #result_flag_false #Hresult_false #Htype_false #Hsim_expr_false #Hsim_lvalue_false #Hresult_flag_false_eq_false
1491	#Hinv <Hresult_flag_false_eq_false in Hresult_false; >Hdesired_false #Habsurd destruct
1492	\| 2: #false_src_sz #false_src_sg #Htype_eq_false #Htype_eq_false1 #Hsmaller_false #_ #Hinv_false
1493	>Htype_eq_true @(Inv_coerce_ok ??????? true_src_sz true_src_sg)
1494	[ 1,2: //
1495	\| 3: whd in match (exec_expr ????); whd in match (exec_expr ??? (Expr ??));
1496	elim (Hcond_equiv ge en m) * #Hexec_cond_sim #_ #Htype_cond_eq
1497	cases Hexec_cond_sim
1498	[ 2: * #error #Herror >Herror normalize @I
1499	\| 1: cases (exec_expr ge en m cond)
1500	[ 2: #error #_ normalize @I
1501	\| 1: * #cond_val #cond_trace #Hcond_sim
1502	>(Hcond_sim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉)))
1503	normalize nodelta
1504	>Htype_cond_eq
1505	cases (exec_bool_of_val cond_val (typeof cond1)) *
1506	[ 3,4: normalize //
1507	\| 1,2: normalize in match (m_bind ?????);
1508	normalize in match (m_bind ?????);
1509	-Hexec_cond_sim -Hcond_sim -cond_val
1510	[ 1: (* true branch taken *)
1511	cases (exec_expr ge en m iftrue) in Hsmaller_true;
1512	[ 2: #error #_ @I
1513	\| 1: * #val_true_branch #trace_true_branch #Hsmaller
1514	#val_true_branch #Hval_true_branch lapply Hsmaller -Hsmaller
1515	cases (exec_expr ge en m iftrue1)
1516	[ 2: #error normalize in ⊢ (% → ?); #Hsmaller
1517	@(False_ind … (Hsmaller val_true_branch Hval_true_branch))
1518	\| 1: * #val_true1_branch #trace_true1_branch #Hsmaller normalize nodelta
1519	elim (Hsmaller val_true_branch Hval_true_branch)
1520	#val_true1_int * * * #val_true1_branch #Hval_cast_eq #Htrace_eq #Hle
1521	%{val_true1_int} try @conj try @conj try @conj //
1522	] ]
1523	\| 2: (* false branch taken. Same proof as above, different arguments ... *)
1524	cut (false_src_sz = true_src_sz ∧ false_src_sg = true_src_sg)
1525	[ 1: >Htype_eq_true in Hiftrue_eq_iffalse; >Htype_eq_false #Htype_eq
1526	destruct (Htype_eq) @conj @refl ] * #Hsz_eq #Hsg_eq destruct
1527	cases (exec_expr ge en m iffalse) in Hsmaller_false;
1528	[ 2: #error #_ @I
1529	\| 1: destruct * #val_false_branch #trace_false_branch #Hsmaller
1530	#val_false_branch #Hval_false_branch lapply Hsmaller -Hsmaller
1531	cases (exec_expr ge en m iffalse1)
1532	[ 2: #error normalize in ⊢ (% → ?); #Hsmaller
1533	@(False_ind … (Hsmaller val_false_branch Hval_false_branch))
1534	\| 1: * #val_false1_branch #trace_false1_branch #Hsmaller normalize nodelta
1535	elim (Hsmaller val_false_branch Hval_false_branch)
1536	#val_false1_int * * * #val_false1_branch #Hval_cast_eq #Htrace_eq #Hle
1537	%{val_false1_int} try @conj try @conj try @conj //
1538	] ]
1539	] ] ] ] ] ] ]
1540	\| 38,39,40: destruct
1541	elim (Hcond_equiv ge en m) * #Hsim_expr_cond #Hsim_vlalue_cond #Htype_cond_eq
1542	elim (Htrue_equiv ge en m) * #Hsim_expr_true #Hsim_vlalue_true #Htype_true_eq
1543	elim (Hfalse_equiv ge en m) * #Hsim_expr_false #Hsim_vlalue_false #Htype_false_eq
1544	%1 try @refl
1545	[ 1,3,5: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
1546	cases (exec_expr ge en m cond) in Hsim_expr_cond;
1547	[ 2,4,6: #error #_ @SimFailNicely
1548	\| 1,3,5: * #cond_val #cond_trace normalize nodelta
1549	cases (exec_expr ge en m cond1)
1550	[ 2,4,6: #error *
1551	[ 1,3,5: #Hsim lapply (Hsim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉)))
1552	#Habsurd destruct
1553	\| : #error #Habsurd destruct ]
1554	\| 1,3,5: * #cond_val1 #cond_trace1 *
1555	[ 2,4,6: * #error #Habsurd destruct
1556	\| 1,3,5: #Hsim lapply (Hsim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉)))
1557	#Hcond_eq normalize nodelta destruct (Hcond_eq)
1558	>Htype_cond_eq cases (exec_bool_of_val cond_val (typeof cond1))
1559	[ 2,4,6: #error @SimFailNicely
1560	\| 1,3,5: * (* true branch *)
1561	[ 1,3,5:
1562	normalize in match (m_bind ?????);
1563	normalize in match (m_bind ?????);
1564	cases Hsim_expr_true
1565	[ 2,4,6: * #error #Hexec_fail >Hexec_fail @SimFailNicely
1566	\| 1,3,5: cases (exec_expr ge en m iftrue)
1567	[ 2,4,6: #error #_ normalize nodelta @SimFailNicely
1568	\| 1,3,5: * #val_true #trace_true normalize nodelta #Hsim
1569	>(Hsim 〈val_true,trace_true〉 (refl ? (OK ? 〈val_true,trace_true〉)))
1570	normalize nodelta @SimOk #a #H @H
1571	]
1572	]
1573	\| 2,4,6:
1574	normalize in match (m_bind ?????);
1575	normalize in match (m_bind ?????);
1576	cases Hsim_expr_false
1577	[ 2,4,6: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFailNicely
1578	\| 1,3,5: cases (exec_expr ge en m iffalse)
1579	[ 2,4,6: #error #_ normalize nodelta @SimFailNicely
1580	\| 1,3,5: * #val_false #trace_false normalize nodelta #Hsim
1581	>(Hsim 〈val_false,trace_false〉 (refl ? (OK ? 〈val_false,trace_false〉)))
1582	normalize nodelta @SimOk #a #H @H
1583	]
1584	]
1585	]
1586	]
1587	]
1588	]
1589	]
1590	\| 2,4,6: @SimFailNicely
1591	]
1592	\| 41,42: destruct
1593	elim (Hlhs_equiv ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs
1594	elim (Hrhs_equiv ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs
1595	%1 try @refl
1596	[ 1,3: whd in match (exec_expr ??? (Expr ??));
1597	whd in match (exec_expr ??? (Expr ??));
1598	cases Hsim_expr_lhs
1599	[ 2,4: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFailNicely
1600	\| 1,3: cases (exec_expr ge en m lhs)
1601	[ 2,4: #error #_ @SimFailNicely
1602	\| 1,3: * #lhs_val #lhs_trace #Hsim normalize nodelta
1603	>(Hsim 〈lhs_val,lhs_trace〉 (refl ? (OK ? 〈lhs_val,lhs_trace〉)))
1604	normalize nodelta >Htype_eq_lhs
1605	cases (exec_bool_of_val lhs_val (typeof lhs1))
1606	[ 2,4: #error normalize @SimFailNicely
1607	\| 1,3: *
1608	whd in match (m_bind ?????);
1609	whd in match (m_bind ?????);
1610	[ 2,3: (* lhs evaluates to true *)
1611	@SimOk #a #H @H
1612	\| 1,4: cases Hsim_expr_rhs
1613	[ 2,4: * #error #Hexec >Hexec @SimFailNicely
1614	\| 1,3: cases (exec_expr ge en m rhs)
1615	[ 2,4: #error #_ @SimFailNicely
1616	\| 1,3: * #rhs_val #rhs_trace -Hsim #Hsim
1617	>(Hsim 〈rhs_val,rhs_trace〉 (refl ? (OK ? 〈rhs_val,rhs_trace〉)))
1618	normalize nodelta >Htype_eq_rhs
1619	@SimOk #a #H @H
1620	]
1621	]
1622	]
1623	]
1624	]
1625	]
1626	\| 2,4: @SimFailNicely
1627	]
1628	\| 43: destruct
1629	cases (type_eq_dec ty (Tint target_sz target_sg))
1630	[ 1: #Htype_eq >Htype_eq >type_eq_identity
1631	@(Inv_coerce_ok ??????? target_sz target_sg)
1632	[ 1,2: //
1633	\| 3: @smaller_integer_val_identity ]
1634	\| 2: #Hneq >(type_neq_not_identity … Hneq)
1635	%1 // @SimOk #a #H @H
1636	]
1637	\| 44: destruct elim (Hrec_expr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
1638	%1 try @refl
1639	[ 1: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
1640	whd in match (exec_lvalue ????) in Hsim_lvalue;
1641	whd in match (exec_lvalue' ?????);
1642	whd in match (exec_lvalue' ?????);
1643	>Htype_eq
1644	cases (typeof rec_expr1) normalize nodelta
1645	[ 2: #sz #sg \| 3: #fl \| 4: #ty \| 5: #ty #n \| 6: #tl #ty \| 7: #id #fl \| 8: #id #fl \| 9: #ty ]
1646	[ 1,2,3,4,5,8,9: @SimFailNicely
1647	\| 6,7: cases Hsim_lvalue
1648	[ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFailNicely
1649	\| 1,3: cases (exec_lvalue ge en m rec_expr)
1650	[ 2,4: #error #_ normalize in ⊢ (??%?); @SimFailNicely
1651	\| 1,3: #a #Hsim >(Hsim a (refl ? (OK ? a)))
1652	whd in match (m_bind ?????);
1653	@SimOk #a #H @H
1654	]
1655	]
1656	]
1657	\| 2: whd in match (exec_lvalue ??? (Expr ??)); whd in match (exec_lvalue ??? (Expr ??));
1658	>Htype_eq
1659	cases (typeof rec_expr1) normalize nodelta
1660	[ 2: #sz #sg \| 3: #fl \| 4: #ty \| 5: #ty #n \| 6: #tl #ty \| 7: #id #fl \| 8: #id #fl \| 9: #ty ]
1661	[ 1,2,3,4,5,8,9: @SimFailNicely
1662	\| 6,7: cases Hsim_lvalue
1663	[ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFailNicely
1664	\| 1,3: cases (exec_lvalue ge en m rec_expr)
1665	[ 2,4: #error #_ normalize in ⊢ (??%?); @SimFailNicely
1666	\| 1,3: #a #Hsim >(Hsim a (refl ? (OK ? a)))
1667	whd in match (m_bind ?????);
1668	@SimOk #a #H @H
1669	]
1670	]
1671	]
1672	]
1673	\| 45: destruct
1674	inversion (Hinv ge en m)
1675	[ 2: #src_sz #src_sg #Htypeof_e1 #Htypeof_e2 #Hsmaller #Hdesired_eq #_
1676	@(Inv_coerce_ok ??????? src_sz src_sg)
1677	[ 1: >Htypeof_e1 //
1678	\| 2: >Htypeof_e2 //
1679	\| 3: whd in match (exec_expr ??? (Expr ??));
1680	whd in match (exec_expr ??? (Expr ??));
1681	cases (exec_expr ge en m e1) in Hsmaller;
1682	[ 2: #error normalize //
1683	\| 1: * #val1 #trace1 #Hsmaller #val1_int #Hval1_eq
1684	cases (exec_expr ge en m e2) in Hsmaller;
1685	[ 2: #error normalize in ⊢ (% → ?); #Habsurd @(False_ind … (Habsurd val1_int Hval1_eq))
1686	\| 1: * #val2 #trace #Hsmaller elim (Hsmaller val1_int Hval1_eq)
1687	#val2_int * * * #Hval2_eq #Hcast #Htrace #Hle normalize nodelta
1688	%{val2_int} try @conj try @conj try @conj //
1689	]
1690	]
1691	]
1692	\| 1: #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #Hdesired_typ #_
1693	>Hresult %1 try @refl
1694	[ 1: >Htype_eq //
1695	\| 2: whd in match (exec_expr ??? (Expr ??));
1696	whd in match (exec_expr ??? (Expr ??));
1697	cases Hsim_expr
1698	[ 2: * #error #Hexec_error >Hexec_error @SimFailNicely
1699	\| 1: cases (exec_expr ge en m e1)
1700	[ 2: #error #_ @SimFailNicely
1701	\| 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #He2_exec >He2_exec
1702	@SimOk #a #H @H
1703	]
1704	]
1705	\| 3: @SimFailNicely
1706	]
1707	]
1708	\| 46: destruct elim (Hexpr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
1709	%1 try @refl
1710	[ 1: whd in match (exec_expr ??? (Expr ??));
1711	whd in match (exec_expr ??? (Expr ??));
1712	cases Hsim_expr
1713	[ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
1714	\| 1: cases (exec_expr ge en m e1)
1715	[ 2: #error #_ @SimFailNicely
1716	\| 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hsim2 >Hsim2 @SimOk #a #H @H ]
1717	]
1718	\| 2: @SimFail /2 by ex_intro/ ]
1719	(* simplify_inside cases. Amounts to propagate a simulation result, except for the /cast/ case which actually calls
1720	* simplify_expr *)
1721	\| 47, 48, 49: (* trivial const_int, const_float and var cases *)
1722	try @conj try @conj try @refl
1723	@SimOk #a #H @H
1724	\| 50: (* Deref case *) destruct
1725	elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
1726	try @conj try @conj
1727	[ 1:
1728	whd in match (exec_expr ??? (Expr ??));
1729	whd in match (exec_expr ??? (Expr ??));
1730	whd in match (exec_lvalue' ?????);
1731	whd in match (exec_lvalue' ?????);
1732	\| 2:
1733	whd in match (exec_lvalue ??? (Expr ??));
1734	whd in match (exec_lvalue ??? (Expr ??));
1735	]
1736	[ 1,2:
1737	cases Hsim_expr
1738	[ 2,4: * #error #Hexec_fail >Hexec_fail @SimFailNicely
1739	\| 1,3: cases (exec_expr ge en m e1)
1740	[ 2,4: #error #_ @SimFailNicely
1741	\| 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ]
1742	\| 3: // ]
1743	\| 51: (* Addrof *) destruct
1744	elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
1745	try @conj try @conj
1746	[ 1:
1747	whd in match (exec_expr ??? (Expr ??));
1748	whd in match (exec_expr ??? (Expr ??));
1749	cases Hsim_lvalue
1750	[ 2: * #error #Hlvalue_fail >Hlvalue_fail @SimFailNicely
1751	\| 1: cases (exec_lvalue ge en m e1)
1752	[ 2: #error #_ @SimFailNicely
1753	\| 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ]
1754	\| 2: @SimFailNicely
1755	\| 3: // ]
1756	\| 52: (* Unop *) destruct
1757	elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
1758	try @conj try @conj
1759	[ 1:
1760	whd in match (exec_expr ??? (Expr ??));
1761	whd in match (exec_expr ??? (Expr ??));
1762	cases Hsim_expr
1763	[ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
1764	\| 1: cases (exec_expr ge en m e1)
1765	[ 2: #error #_ @SimFailNicely
1766	\| 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk
1767	>Htype_eq #a #H @H ] ]
1768	\| 2: @SimFailNicely
1769	\| 3: // ]
1770	\| 53: (* Binop *) destruct
1771	elim (Hequiv_lhs ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs
1772	elim (Hequiv_rhs ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs
1773	try @conj try @conj
1774	[ 1:
1775	whd in match (exec_expr ??? (Expr ??));
1776	whd in match (exec_expr ??? (Expr ??));
1777	cases Hsim_expr_lhs
1778	[ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
1779	\| 1: cases (exec_expr ge en m lhs)
1780	[ 2: #error #_ @SimFailNicely
1781	\| 1: #lhs_value #Hsim_lhs cases Hsim_expr_rhs
1782	[ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
1783	\| 1: cases (exec_expr ge en m rhs)
1784	[ 2: #error #_ @SimFailNicely
1785	\| 1: #rhs_value #Hsim_rhs
1786	lapply (Hsim_lhs lhs_value (refl ? (OK ? lhs_value)))
1787	lapply (Hsim_rhs rhs_value (refl ? (OK ? rhs_value)))
1788	#Hrhs >Hrhs #Hlhs >Hlhs >Htype_eq_rhs >Htype_eq_lhs
1789	@SimOk #a #H @H
1790	]
1791	]
1792	]
1793	]
1794	\| 2: @SimFailNicely
1795	\| 3: //
1796	]
1797	\| 54: (* Cast, fallback case *)
1798	try @conj try @conj try @refl
1799	@SimOk #a #H @H
1800	\| 55: (* Cast, success case *) destruct
1801	inversion (Htrans_inv ge en m)
1802	[ 1: (* contradiction *)
1803	#result_flag #Hresult_flag #Htype_eq #Hsim_epr #Hsim_lvalue #Hresult_flag_true
1804	<Hresult_flag_true in Hresult_flag; #Habsurd destruct
1805	\| 2: #src_sz #src_sg #Hsrc_type_eq #Htarget_type_eq #Hsmaller #_ #_
1806	try @conj try @conj try @conj
1807	[ 1: whd in match (exec_expr ??? (Expr ??));
1808	cases (exec_expr ge en m castee) in Hsmaller;
1809	[ 2: #error #_ @SimFailNicely
1810	\| 1: * #val #trace normalize nodelta >Hsrc_type_eq
1811	lapply (exec_cast_inv val src_sz src_sg cast_sz cast_sg m)
1812	cases (exec_cast m val ??)
1813	[ 2: #error #_ #_ @SimFailNicely
1814	\| 1: #result #Hinversion elim (Hinversion result (refl ??))
1815	#val_int * #Hval_eq #Hcast
1816	cases (exec_expr ge en m castee1)
1817	[ 2: #error #Habsurd normalize in Habsurd; @(False_ind … (Habsurd val_int Hval_eq))
1818	\| 1: * #val1 #trace1 #Hsmaller elim (Hsmaller val_int Hval_eq)
1819	#val1_int * * * #Hval1_int #Hval18int #Htrace #Hle
1820	@SimOk destruct normalize // ]
1821	]
1822	]
1823	\| 2: @SimFailNicely
1824	\| 3: >Htarget_type_eq //
1825	]
1826	]
1827	\| 56: (* Cast, "failure" case *) destruct
1828	inversion (Htrans_inv ge en m)
1829	[ 2: (* contradiction *)
1830	#src_sz #src_sg #Htype_castee #Htype_castee1 #Hsmaller #Habsurd
1831	lapply (jmeq_to_eq ??? Habsurd) -Habsurd #Herror destruct
1832	\| 1: #result_flag #Hresult_flag #Htype_eq #Hsim_expr #Hsim_lvalue #_ #_
1833	try @conj try @conj try @conj
1834	[ 1: whd in match (exec_expr ????);
1835	whd in match (exec_expr ??? (Expr ??));
1836	cases Hsim_expr
1837	[ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
1838	\| 1: cases (exec_expr ??? castee)
1839	[ 2: #error #_ @SimFailNicely
1840	\| 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec_ok >Hexec_ok
1841	@SimOk >Htype_eq #a #H @H ]
1842	]
1843	\| 2: @SimFailNicely
1844	\| 3: //
1845	]
1846	]
1847	\| 57,58,59,60,61,62,63,64,68:
1848	try @conj try @conj try @refl
1849	@SimOk #a #H @H
1850	\| 65: destruct
1851	elim (Hequiv_cond ge en m) * #Hsim_exec_cond #Hsim_lvalue_cond #Htype_eq_cond
1852	elim (Hequiv_iftrue ge en m) * #Hsim_exec_true #Hsim_lvalue_true #Htype_eq_true
1853	elim (Hequiv_iffalse ge en m) * #Hsim_exec_false #Hsim_lvalue_false #Htype_eq_false
1854	try @conj try @conj
1855	[ 1: whd in match (exec_expr ??? (Expr ??));
1856	whd in match (exec_expr ??? (Expr ??));
1857	cases Hsim_exec_cond
1858	[ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
1859	\| 1: cases (exec_expr ??? cond)
1860	[ 2: #error #_ @SimFailNicely
1861	\| 1: * #condb #condtrace #Hcond_sim lapply (Hcond_sim 〈condb, condtrace〉 (refl ? (OK ? 〈condb, condtrace〉)))
1862	#Hcond_ok >Hcond_ok >Htype_eq_cond
1863	normalize nodelta
1864	cases (exec_bool_of_val condb (typeof cond1))
1865	[ 2: #error @SimFailNicely
1866	\| 1: * whd in match (m_bind ?????); whd in match (m_bind ?????);
1867	normalize nodelta
1868	[ 1: (* true branch taken *)
1869	cases Hsim_exec_true
1870	[ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
1871	\| 1: cases (exec_expr ??? iftrue)
1872	[ 2: #error #_ @SimFailNicely
1873	\| 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H
1874	@SimOk #a #H @H
1875	]
1876	]
1877	\| 2: (* false branch taken *)
1878	cases Hsim_exec_false
1879	[ 2: * #error #Hexec_fail >Hexec_fail @SimFailNicely
1880	\| 1: cases (exec_expr ??? iffalse)
1881	[ 2: #error #_ @SimFailNicely
1882	\| 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H
1883	@SimOk #a #H @H
1884	]
1885	]
1886	]
1887	]
1888	]
1889	]
1890	\| 2: @SimFailNicely
1891	\| 3: //
1892	]
1893	\| 66,67: destruct
1894	elim (Hequiv_lhs ge en m) * #Hsim_exec_lhs #Hsim_lvalue_lhs #Htype_eq_lhs
1895	elim (Hequiv_rhs ge en m) * #Hsim_exec_rhs #Hsim_lvalue_rhs #Htype_eq_rhs
1896	try @conj try @conj
1897	whd in match (exec_expr ??? (Expr ??));
1898	whd in match (exec_expr ??? (Expr ??));
1899	[ 1,4: cases Hsim_exec_lhs
1900	[ 2,4: * #error #Hexec_fail >Hexec_fail @SimFailNicely
1901	\| 1,3: cases (exec_expr ??? lhs)
1902	[ 2,4: #error #_ @SimFailNicely
1903	\| 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hlhs >Hlhs >Htype_eq_lhs
1904	normalize nodelta elim a #lhs_val #lhs_trace
1905	cases (exec_bool_of_val lhs_val (typeof lhs1))
1906	[ 2,4: #error @SimFailNicely
1907	\| 1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????);
1908	[ 2,3: @SimOk //
1909	\| 1,4: cases Hsim_exec_rhs
1910	[ 2,4: * #error #Hexec_fail >Hexec_fail @SimFailNicely
1911	\| 1,3: cases (exec_expr ??? rhs)
1912	[ 2,4: #error #_ @SimFailNicely
1913	\| 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrhs >Hrhs >Htype_eq_rhs
1914	@SimOk #a #H @H
1915	]
1916	]
1917	]
1918	]
1919	]
1920	]
1921	\| 2,5: @SimFailNicely
1922	\| 3,6: //
1923	]
1924	\| 69: (* record field *) destruct
1925	elim (Hequiv_rec ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
1926	try @conj try @conj
1927	whd in match (exec_expr ??? (Expr ??));
1928	whd in match (exec_expr ??? (Expr ??));
1929	whd in match (exec_lvalue' ??? (Efield rec_expr f) ty);
1930	whd in match (exec_lvalue' ??? (Efield rec_expr1 f) ty);
1931	[ 1: >Htype_eq cases (typeof rec_expr1) normalize nodelta
1932	[ 2: #sz #sg \| 3: #fl \| 4: #ty' \| 5: #ty #n \| 6: #tl #ty'
1933	\| 7: #id #fl \| 8: #id #fl \| 9: #id ]
1934	try (@SimFailNicely)
1935	cases Hsim_lvalue
1936	[ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFailNicely
1937	\| 1,3: cases (exec_lvalue ge en m rec_expr)
1938	[ 2,4: #error #_ @SimFailNicely
1939	\| 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec >Hexec
1940	@SimOk #a #H @H ]
1941	]
1942	\| 2: (* Note: identical to previous case. Too lazy to merge and manually shift indices. *)
1943	>Htype_eq cases (typeof rec_expr1) normalize nodelta
1944	[ 2: #sz #sg \| 3: #fl \| 4: #ty' \| 5: #ty #n \| 6: #tl #ty'
1945	\| 7: #id #fl \| 8: #id #fl \| 9: #id ]
1946	try (@SimFailNicely)
1947	cases Hsim_lvalue
1948	[ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFailNicely
1949	\| 1,3: cases (exec_lvalue ge en m rec_expr)
1950	[ 2,4: #error #_ @SimFailNicely
1951	\| 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec >Hexec
1952	@SimOk #a #H @H ]
1953	]
1954	\| 3: // ]
1955	\| 70: (* cost label *) destruct
1956	elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
1957	try @conj try @conj
1958	whd in match (exec_expr ??? (Expr ??));
1959	whd in match (exec_expr ??? (Expr ??));
1960	[ 1:
1961	cases Hsim_expr
1962	[ 2: * #error #Hexec >Hexec @SimFailNicely
1963	\| 1: cases (exec_expr ??? e1)
1964	[ 2: #error #_ @SimFailNicely
1965	\| 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H
1966	@SimOk #a #H @H ]
1967	]
1968	\| 2: @SimFail /2 by ex_intro/
1969	\| 3: //
1970	]
1971	] qed.
1972
1973	(* Propagate cast simplification through statements and programs. *)
1974
1975	definition simplify_e ≝ λe. pi1 … (simplify_inside e).
1976
1977	let rec simplify_statement (s:statement) : statement ≝
1978	match s with
1979	[ Sskip ⇒ Sskip
1980	\| Sassign e1 e2 ⇒ Sassign (simplify_e e1) (simplify_e e2)
1981	\| Scall eo e es ⇒ Scall (option_map ?? simplify_e eo) (simplify_e e) (map ?? simplify_e es)
1982	\| Ssequence s1 s2 ⇒ Ssequence (simplify_statement s1) (simplify_statement s2)
1983	\| Sifthenelse e s1 s2 ⇒ Sifthenelse (simplify_e e) (simplify_statement s1) (simplify_statement s2) (* TODO: try to reduce size of e *)
1984	\| Swhile e s1 ⇒ Swhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *)
1985	\| Sdowhile e s1 ⇒ Sdowhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *)
1986	\| Sfor s1 e s2 s3 ⇒ Sfor (simplify_statement s1) (simplify_e e) (simplify_statement s2) (simplify_statement s3) (* TODO: reduce size of e *)
1987	\| Sbreak ⇒ Sbreak
1988	\| Scontinue ⇒ Scontinue
1989	\| Sreturn eo ⇒ Sreturn (option_map ?? simplify_e eo)
1990	\| Sswitch e ls ⇒ Sswitch (simplify_e e) (simplify_ls ls)
1991	\| Slabel l s1 ⇒ Slabel l (simplify_statement s1)
1992	\| Sgoto l ⇒ Sgoto l
1993	\| Scost l s1 ⇒ Scost l (simplify_statement s1)
1994	]
1995	and simplify_ls ls ≝
1996	match ls with
1997	[ LSdefault s ⇒ LSdefault (simplify_statement s)
1998	\| LScase sz i s ls' ⇒ LScase sz i (simplify_statement s) (simplify_ls ls')
1999	].
2000
2001	definition simplify_function : function → function ≝
2002	λf. mk_function (fn_return f) (fn_params f) (fn_vars f) (simplify_statement (fn_body f)).
2003
2004	definition simplify_fundef : clight_fundef → clight_fundef ≝
2005	λf. match f with
2006	[ CL_Internal f ⇒ CL_Internal (simplify_function f)
2007	\| _ ⇒ f
2008	].
2009
2010	definition simplify_program : clight_program → clight_program ≝
2011	λp. transform_program … p (λ_.simplify_fundef).
2012
2013	(* Simulation on statement continuations. Stolen from labelSimulation and adapted to our setting. *)
2014	inductive cont_cast : cont → cont → Prop ≝
2015	\| cc_stop : cont_cast Kstop Kstop
2016	\| cc_seq : ∀s,k,k'. cont_cast k k' → cont_cast (Kseq s k) (Kseq (simplify_statement s) k')
2017	\| cc_while : ∀e,s,k,k'.
2018	cont_cast k k' →
2019	cont_cast (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k')
2020	\| cc_dowhile : ∀e,s,k,k'.
2021	cont_cast k k' →
2022	cont_cast (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k')
2023	\| cc_for1 : ∀e,s1,s2,k,k'.
2024	cont_cast k k' →
2025	cont_cast (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip (simplify_e e) (simplify_statement s1) (simplify_statement s2)) k')
2026	\| cc_for2 : ∀e,s1,s2,k,k'.
2027	cont_cast k k' →
2028	cont_cast (Kfor2 e s1 s2 k) (Kfor2 (simplify_e e) (simplify_statement s1) (simplify_statement s2) k')
2029	\| cc_for3 : ∀e,s1,s2,k,k'.
2030	cont_cast k k' →
2031	cont_cast (Kfor3 e s1 s2 k) (Kfor3 (simplify_e e) (simplify_statement s1) (simplify_statement s2) k')
2032	\| cc_switch : ∀k,k'.
2033	cont_cast k k' → cont_cast (Kswitch k) (Kswitch k')
2034	\| cc_call : ∀r,f,en,k,k'.
2035	cont_cast k k' →
2036	cont_cast (Kcall r f en k) (Kcall r (simplify_function f) en k').
2037
2038	lemma call_cont_cast : ∀k,k'.
2039	cont_cast k k' →
2040	cont_cast (call_cont k) (call_cont k').
2041	#k0 #k0' #K elim K /2/
2042	qed.
2043
2044	inductive state_cast : state → state → Prop ≝
2045	\| swc_state : ∀f,s,k,k',e,m.
2046	cont_cast k k' →
2047	state_cast (State f s k e m) (State (simplify_function f) (simplify_statement s ) k' e m)
2048	\| swc_callstate : ∀fd,args,k,k',m.
2049	cont_cast k k' → state_cast (Callstate fd args k m) (Callstate (simplify_fundef fd) args k' m)
2050	\| swc_returnstate : ∀res,k,k',m.
2051	cont_cast k k' → state_cast (Returnstate res k m) (Returnstate res k' m)
2052	\| swc_finalstate : ∀r.
2053	state_cast (Finalstate r) (Finalstate r)
2054	.
2055
2056	record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
2057	rg_find_symbol: ∀s.
2058	find_symbol ? ge s = find_symbol ? ge' s;
2059	rg_find_funct: ∀v,f.
2060	find_funct ? ge v = Some ? f →
2061	find_funct ? ge' v = Some ? (t f);
2062	rg_find_funct_ptr: ∀b,f.
2063	find_funct_ptr ? ge b = Some ? f →
2064	find_funct_ptr ? ge' b = Some ? (t f)
2065	}.
2066
2067	(* The return type of any function is invariant under cast simplification *)
2068	lemma fn_return_simplify : ∀f. fn_return (simplify_function f) = fn_return f.
2069	// qed.
2070
2071
2072	definition expr_lvalue_ind_combined ≝
2073	λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
2074	conj ??
2075	(expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx)
2076	(lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
2077
2078	lemma simulation_transitive : ∀A,r0,r1,r2. res_sim A r0 r1 → res_sim A r1 r2 → res_sim A r0 r2.
2079	#A #r0 #r1 #r2 *
2080	[ 2: * #error #H >H #_ @SimFail /2 by ex_intro/
2081	\| 1: cases r0
2082	[ 2: #error #_ #_ @SimFail /2 by ex_intro/
2083	\| 1: #elt #Hsim lapply (Hsim elt (refl ? (OK ? elt))) #H >H // ]
2084	] qed.
2085
2086	lemma sim_related_globals : ∀ge,ge',en,m. related_globals ? simplify_fundef ge ge' →
2087	(∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧
2088	(∀ed, ty. res_sim ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)).
2089	#ge #ge' #en #m #Hrelated @expr_lvalue_ind_combined
2090	[ 1: #sz #ty #i @SimOk #a normalize //
2091	\| 2: #ty #f @SimOk #a normalize //
2092	\| 3: *
2093	[ 1: #sz #i \| 2: #fl \| 3: #id \| 4: #e1 \| 5: #e1 \| 6: #op #e1 \| 7: #op #e1 #e2 \| 8: #cast_ty #e1
2094	\| 9: #cond #iftrue #iffalse \| 10: #e1 #e2 \| 11: #e1 #e2 \| 12: #sizeofty \| 13: #e1 #field \| 14: #cost #e1 ]
2095	#ty #Hsim_lvalue try //
2096	whd in match (Plvalue ???);
2097	whd in match (exec_expr ????);
2098	whd in match (exec_expr ????);
2099	cases Hsim_lvalue
2100	[ 2,4,6: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/
2101	\| *: cases (exec_lvalue' ge en m ? ty)
2102	[ 2,4,6: #error #_ @SimFail /2 by ex_intro/
2103	\| *: #a #Hsim_lvalue lapply (Hsim_lvalue a (refl ? (OK ? a))) #Hrewrite >Hrewrite
2104	@SimOk // ]
2105	]
2106	\| 4: #v #ty whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????);
2107	cases (lookup SymbolTag block en v) normalize nodelta
2108	[ 2: #block @SimOk //
2109	\| 1: elim Hrelated #Hsymbol #_ #_ >(Hsymbol v) @SimOk //
2110	]
2111	\| 5: #e #ty #Hsim_expr whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????);
2112	cases Hsim_expr
2113	[ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2114	\| 1: cases (exec_expr ge en m e)
2115	[ 2: #error #_ @SimFail /2 by ex_intro/
2116	\| 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
2117	@SimOk // ]
2118	]
2119	\| 6: #ty #ed #ty' #Hsim_lvalue
2120	whd in match (exec_expr ????); whd in match (exec_expr ????);
2121	whd in match (exec_lvalue ????); whd in match (exec_lvalue ????);
2122	cases Hsim_lvalue
2123	[ 2: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/
2124	\| 1: cases (exec_lvalue' ge en m ed ty')
2125	[ 2: #error #_ @SimFail /2 by ex_intro/
2126	\| *: #a #Hsim_lvalue lapply (Hsim_lvalue a (refl ? (OK ? a))) #Hrewrite >Hrewrite
2127	@SimOk // ]
2128	]
2129	\| 7: #ty #op #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
2130	cases Hsim
2131	[ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2132	\| 1: cases (exec_expr ge en m e)
2133	[ 2: #error #_ @SimFail /2 by ex_intro/
2134	\| 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
2135	@SimOk // ]
2136	]
2137	\| 8: #ty #op #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
2138	cases Hsim1
2139	[ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2140	\| 1: cases (exec_expr ge en m e1)
2141	[ 2: #error #_ @SimFail /2 by ex_intro/
2142	\| 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
2143	cases Hsim2
2144	[ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2145	\| 1: cases (exec_expr ge en m e2)
2146	[ 2: #error #_ @SimFail /2 by ex_intro/
2147	\| 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
2148	@SimOk // ]
2149	]
2150	]
2151	]
2152	\| 9: #ty #cast_ty #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
2153	cases Hsim
2154	[ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2155	\| 1: cases (exec_expr ge en m e)
2156	[ 2: #error #_ @SimFail /2 by ex_intro/
2157	\| 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
2158	@SimOk // ]
2159	] (* mergeable with 7 modulo intros *)
2160	\| 10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
2161	cases Hsim1
2162	[ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2163	\| 1: cases (exec_expr ge en m e1)
2164	[ 2: #error #_ @SimFail /2 by ex_intro/
2165	\| 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite normalize nodelta
2166	cases (exec_bool_of_val (\fst a) (typeof e1))
2167	[ 2: #error @SimFail /2 by ex_intro/
2168	\| 1: *
2169	[ 1: (* true branch *) cases Hsim2
2170	\| 2: (* false branch *) cases Hsim3 ]
2171	[ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2172	\| 1: cases (exec_expr ge en m e2) \| 3: cases (exec_expr ge en m e3) ]
2173	[ 2,4: #error #_ @SimFail /2 by ex_intro/
2174	\| 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite @SimOk // ]
2175	]
2176	]
2177	]
2178	\| 11,12: #ty #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
2179	cases Hsim1
2180	[ 2,4: * #error #Hfail >Hfail @SimFailNicely
2181	\| 1,3: cases (exec_expr ge en m e1)
2182	[ 2,4: #error #_ @SimFailNicely
2183	\| 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite normalize nodelta
2184	cases (exec_bool_of_val ??)
2185	[ 2,4: #erro @SimFailNicely
2186	\| 1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????);
2187	[ 2,3: @SimOk //
2188	\| 1,4: cases Hsim2
2189	[ 2,4: * #error #Hfail >Hfail normalize nodelta @SimFail /2 by ex_intro/
2190	\| 1,3: cases (exec_expr ge en m e2)
2191	[ 2,4: #error #_ @SimFail /2 by ex_intro/
2192	\| 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
2193	@SimOk // ]
2194	]
2195	]
2196	]
2197	]
2198	]
2199	\| 13: #ty #sizeof_ty @SimOk normalize //
2200	\| 14: #ty #e #ty' #field #Hsim_lvalue
2201	whd in match (exec_lvalue' ? en m (Efield ??) ty);
2202	whd in match (exec_lvalue' ge' en m (Efield ??) ty);
2203	normalize in match (typeof (Expr ??));
2204	cases ty' in Hsim_lvalue; normalize nodelta
2205	[ 2: #sz #sg \| 3: #fsz \| 4: #ptr_ty \| 5: #array_ty #array_sz \| 6: #domain #codomain
2206	\| 7: #structname #fieldspec \| 8: #unionname #fieldspec \| 9: #id ]
2207	#Hsim_lvalue
2208	try (@SimFail /2 by ex_intro/)
2209	normalize in match (exec_lvalue ge en m ?);
2210	normalize in match (exec_lvalue ge' en m ?);
2211	cases Hsim_lvalue
2212	[ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2213	\| 1,3: cases (exec_lvalue' ge en m e ?)
2214	[ 2,4: #error #_ @SimFail /2 by ex_intro/
2215	\| 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
2216	@SimOk /2 by ex_intro/ ]
2217	]
2218	\| 15: #ty #lab #e #Hsim
2219	whd in match (exec_expr ??? (Expr ??));
2220	whd in match (exec_expr ??? (Expr ??));
2221	cases Hsim
2222	[ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
2223	\| 1: cases (exec_expr ge en m e)
2224	[ 2: #error #_ @SimFail /2 by ex_intro/
2225	\| 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
2226	@SimOk // ]
2227	] (* cf case 7, again *)
2228	\| 16: *
2229	[ 1: #sz #i \| 2: #fl \| 3: #id \| 4: #e1 \| 5: #e1 \| 6: #op #e1 \| 7: #op #e1 #e2 \| 8: #cast_ty #e1
2230	\| 9: #cond #iftrue #iffalse \| 10: #e1 #e2 \| 11: #e1 #e2 \| 12: #sizeofty \| 13: #e1 #field \| 14: #cost #e1 ]
2231	#ty normalize in match (is_not_lvalue ?);
2232	[ 3,4,13: #Habsurd @(False_ind … Habsurd) ] #_
2233	@SimFailNicely
2234	] qed.
2235
2236	lemma related_globals_expr_simulation : ∀ge,ge',en,m.
2237	related_globals ? simplify_fundef ge ge' →
2238	∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m (simplify_e e)) ∧
2239	typeof e = typeof (simplify_e e).
2240	#ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?);
2241	cases e #ed #ty cases ed
2242	[ 1: #sz #i \| 2: #fl \| 3: #id \| 4: #e1 \| 5: #e1 \| 6: #op #e1 \| 7: #op #e1 #e2 \| 8: #cast_ty #e1
2243	\| 9: #cond #iftrue #iffalse \| 10: #e1 #e2 \| 11: #e1 #e2 \| 12: #sizeofty \| 13: #e1 #field \| 14: #cost #e1 ]
2244	elim (simplify_inside (Expr ??)) #e' #Hconservation whd in Hconservation; @conj lapply (Hconservation ge en m)
2245	* * try //
2246	cases (exec_expr ge en m (Expr ??))
2247	try (#error #_ #_ #_ @SimFailNicely)
2248	* #val #trace #Hsim_expr #Hsim_lvalue #Htype_eq
2249	try @(simulation_transitive ???? Hsim_expr (proj1 ?? (sim_related_globals ge ge' en m Hrelated) ?))
2250	qed.
2251
2252	lemma related_globals_lvalue_simulation : ∀ge,ge',en,m.
2253	related_globals ? simplify_fundef ge ge' →
2254	∀e. res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge' en m (simplify_e e)) ∧
2255	typeof e = typeof (simplify_e e).
2256	#ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?);
2257	cases e #ed #ty cases ed
2258	[ 1: #sz #i \| 2: #fl \| 3: #id \| 4: #e1 \| 5: #e1 \| 6: #op #e1 \| 7: #op #e1 #e2 \| 8: #cast_ty #e1
2259	\| 9: #cond #iftrue #iffalse \| 10: #e1 #e2 \| 11: #e1 #e2 \| 12: #sizeofty \| 13: #e1 #field \| 14: #cost #e1 ]
2260	elim (simplify_inside (Expr ??)) #e' #Hconservation whd in Hconservation; @conj lapply (Hconservation ge en m)
2261	* * try //
2262	cases (exec_lvalue ge en m (Expr ??))
2263	try (#error #_ #_ #_ @SimFailNicely)
2264	* #val #trace #Hsim_expr #Hsim_lvalue #Htype_eq
2265	(* Having to distinguish between exec_lvalue' and exec_lvalue is /ugly/. *)
2266	cases e' in Hsim_lvalue ⊢ %; #ed' #ty' whd in match (exec_lvalue ????); whd in match (exec_lvalue ????);
2267	lapply (proj2 ?? (sim_related_globals ge ge' en m Hrelated) ed' ty') #Hsim_lvalue2 #Hsim_lvalue1
2268	try @(simulation_transitive ???? Hsim_lvalue1 Hsim_lvalue2)
2269	qed.
2270
2271	lemma related_globals_exprlist_simulation : ∀ge,ge',en,m.
2272	related_globals ? simplify_fundef ge ge' →
2273	∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m (map expr expr simplify_e args)).
2274	#ge #ge' #en #m #Hrelated #args
2275	elim args
2276	[ 1: /3/
2277	\| 2: #hd #tl #Hind normalize
2278	elim (related_globals_expr_simulation ge ge' en m Hrelated hd)
2279	*
2280	[ 2: * #error #Hfail >Hfail #_ @SimFail /2 by refl, ex_intro/
2281	\| 1: cases (exec_expr ge en m hd)
2282	[ 2: #error #_ #_ @SimFail /2 by refl, ex_intro/
2283	\| 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Heq >Heq #Htype_eq >Htype_eq
2284	cases Hind normalize
2285	[ 2: * #error #Hfail >Hfail @SimFail /2 by refl, ex_intro/
2286	\| 1: cases (exec_exprlist ??? tl)
2287	[ 2: #error #_ @SimFail /2 by refl, ex_intro/
2288	\| 1: * #values #trace #Hsim lapply (Hsim 〈values, trace〉 (refl ? (OK ? 〈values, trace〉)))
2289	#Heq >Heq @SimOk // ]
2290	]
2291	]
2292	]
2293	] qed.
2294
2295	lemma simplify_type_of_fundef_eq : ∀clfd. (type_of_fundef (simplify_fundef clfd)) = (type_of_fundef clfd).
2296	* // qed.
2297
2298	lemma simplify_typeof_eq : ∀ge:genv.∀en:env.∀m:mem. ∀func. typeof (simplify_e func) = typeof func.
2299	#ge #en #m #func whd in match (simplify_e func); elim (simplify_inside func)
2300	#func' #H lapply (H ge en m) * * #_ #_ //
2301	qed.
2302
2303	lemma simplify_fun_typeof_eq : ∀ge:genv.∀en:env.∀m:mem. ∀func. fun_typeof (simplify_e func) = fun_typeof func.
2304	#ge #en #m #func whd in match (simplify_e func); whd in match (fun_typeof ?) in ⊢ (??%%);
2305	>simplify_typeof_eq whd in match (simplify_e func); // qed.
2306
2307	lemma simplify_is_not_skip: ∀s.s ≠ Sskip → ∃pf. is_Sskip (simplify_statement s) = inr … pf.
2308	*
2309	[ 1: * #Habsurd elim (Habsurd (refl ? Sskip))
2310	\| *: #a try #b try #c try #d try #e
2311	whd in match (simplify_statement ?);
2312	whd in match (is_Sskip ?);
2313	try /2 by refl, ex_intro/
2314	] qed.
2315
2316	lemma call_cont_simplify : ∀k,k'.
2317	cont_cast k k' →
2318	cont_cast (call_cont k) (call_cont k').
2319	#k0 #k0' #K elim K /2/
2320	qed.
2321
2322	lemma simplify_ls_commute : ∀l. (simplify_statement (seq_of_labeled_statement l)) = (seq_of_labeled_statement (simplify_ls l)).
2323	#l @(labeled_statements_ind … l)
2324	[ 1: #default_statement //
2325	\| 2: #sz #i #s #tl #Hind
2326	whd in match (seq_of_labeled_statement ?) in ⊢ (??%?);
2327	whd in match (simplify_ls ?) in ⊢ (???%);
2328	whd in match (seq_of_labeled_statement ?) in ⊢ (???%);
2329	whd in match (simplify_statement ?) in ⊢ (??%?);
2330	>Hind //
2331	] qed.
2332
2333	lemma select_switch_commute : ∀sz,i,l.
2334	select_switch sz i (simplify_ls l) = simplify_ls (select_switch sz i l).
2335	#sz #i #l @(labeled_statements_ind … l)
2336	[ 1: #default_statement //
2337	\| 2: #sz' #i' #s #tl #Hind
2338	whd in match (simplify_ls ?) in ⊢ (??%?);
2339	whd in match (select_switch ???) in ⊢ (??%%);
2340	cases (sz_eq_dec sz sz')
2341	[ 1: #Hsz_eq destruct >intsize_eq_elim_true >intsize_eq_elim_true
2342	cases (eq_bv (bitsize_of_intsize sz') i' i) normalize nodelta
2343	whd in match (simplify_ls ?) in ⊢ (???%);
2344	[ 1: // \| 2: @Hind ]
2345	\| 2: #Hneq >(intsize_eq_elim_false ? sz sz' ???? Hneq) >(intsize_eq_elim_false ? sz sz' ???? Hneq)
2346	@Hind
2347	]
2348	] qed.
2349
2350	lemma elim_IH_aux :
2351	∀lab. ∀s:statement.∀k,k'. cont_cast k k' →
2352	∀Hind:(∀k:cont.∀k':cont.
2353	cont_cast k k' →
2354	match find_label lab s k with
2355	[ None ⇒ find_label lab (simplify_statement s) k'=None (statement×cont)
2356	\| Some (r:(statement×cont))⇒
2357	let 〈s',ks〉 ≝r in
2358	∃ks':cont. find_label lab (simplify_statement s) k' = Some (statement×cont) 〈simplify_statement s',ks'〉
2359	∧ cont_cast ks ks']).
2360	(find_label lab s k = None ? ∧ find_label lab (simplify_statement s) k' = None ?) ∨
2361	(∃st,kst,kst'. find_label lab s k = Some ? 〈st,kst〉 ∧ find_label lab (simplify_statement s) k' = Some ? 〈simplify_statement st,kst'〉 ∧ cont_cast kst kst').
2362	#lab #s #k #k' #Hcont_cast #Hind
2363	lapply (Hind k k' Hcont_cast)
2364	cases (find_label lab s k)
2365	[ 1: normalize nodelta #Heq >Heq /3/
2366	\| 2: * #st #kst normalize nodelta * #kst' * #Heq #Hcont_cast' >Heq %2
2367	%{st} %{kst} %{kst'} @conj try @conj //
2368	] qed.
2369
2370
2371	lemma cast_find_label : ∀lab,s,k,k'.
2372	cont_cast k k' →
2373	match find_label lab s k with
2374	[ Some r ⇒
2375	let 〈s',ks〉 ≝ r in
2376	∃ks'. find_label lab (simplify_statement s) k' = Some ? 〈simplify_statement s', ks'〉
2377	∧ cont_cast ks ks'
2378	\| None ⇒
2379	find_label lab (simplify_statement s) k' = None ?
2380	].
2381	#lab #s @(statement_ind2 ? (λls.
2382	∀k:cont
2383	.∀k':cont
2384	.cont_cast k k'
2385	→match find_label_ls lab ls k with
2386	[None⇒
2387	find_label_ls lab (simplify_ls ls) k' = None ?
2388	\|Some r ⇒
2389	let 〈s',ks〉 ≝r in
2390	∃ks':cont
2391	.find_label_ls lab (simplify_ls ls) k'
2392	=Some (statement×cont) 〈simplify_statement s',ks'〉
2393	∧cont_cast ks ks']
2394	) … s)
2395	[ 1: #k #k' #Hcont_cast
2396	whd in match (find_label ? Sskip ?); normalize nodelta @refl
2397	\| 2: #e1 #e2 #k #k' #Hcont_cast
2398	whd in match (find_label ? (Sassign e1 e2) ?); normalize nodelta @refl
2399	\| 3: #e0 #e #args #k #k' #Hcont_cast
2400	whd in match (find_label ? (Scall e0 e args) ?); normalize nodelta @refl
2401	\| 4: #s1 #s2 #Hind_s1 #Hind_s2 #k #k' #Hcont_cast
2402	whd in match (find_label ? (Ssequence s1 s2) ?);
2403	whd in match (find_label ? (simplify_statement (Ssequence s1 s2)) ?);
2404	elim (elim_IH_aux lab s1 (Kseq s2 k) (Kseq (simplify_statement s2) k') ? Hind_s1)
2405	[ 3: try ( @cc_seq // )
2406	\| 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
2407	normalize nodelta %{kst'} /2/
2408	\| 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
2409	elim (elim_IH_aux lab s2 k k' Hcont_cast Hind_s2)
2410	[ 2: * #st * #kst * #kst' * * #Hrewrite2 >Hrewrite2 #Hrewrite3 >Hrewrite3 #Hcont_cast'
2411	normalize nodelta %{kst'} /2/
2412	\| 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
2413	] ]
2414	\| 5: #e #s1 #s2 #Hind_s1 #Hind_s2 #k #k' #Hcont_cast
2415	whd in match (find_label ???);
2416	whd in match (find_label ? (simplify_statement ?) ?);
2417	elim (elim_IH_aux lab s1 k k' Hcont_cast Hind_s1)
2418	[ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
2419	normalize nodelta %{kst'} /2/
2420	\| 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
2421	elim (elim_IH_aux lab s2 k k' Hcont_cast Hind_s2)
2422	[ 2: * #st * #kst * #kst' * * #Hrewrite2 >Hrewrite2 #Hrewrite3 >Hrewrite3 #Hcont_cast'
2423	normalize nodelta %{kst'} /2/
2424	\| 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
2425	] ]
2426	\| 6: #e #s #Hind_s #k #k' #Hcont_cast
2427	whd in match (find_label ???);
2428	whd in match (find_label ? (simplify_statement ?) ?);
2429	elim (elim_IH_aux lab s (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k') ? Hind_s)
2430	[ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
2431	normalize nodelta %{kst'} /2/
2432	\| 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
2433	\| 3: @cc_while // ]
2434	\| 7: #e #s #Hind_s #k #k' #Hcont_cast
2435	whd in match (find_label ???);
2436	whd in match (find_label ? (simplify_statement ?) ?);
2437	elim (elim_IH_aux lab s (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k') ? Hind_s)
2438	[ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
2439	normalize nodelta %{kst'} /2/
2440	\| 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
2441	\| 3: @cc_dowhile // ]
2442	\| 8: #s1 #cond #s2 #s3 #Hind_s1 #Hind_s2 #Hind_s3 #k #k' #Hcont_cast
2443	whd in match (find_label ???);
2444	whd in match (find_label ? (simplify_statement ?) ?);
2445	elim (elim_IH_aux lab s1
2446	(Kseq (Sfor Sskip cond s2 s3) k)
2447	(Kseq (Sfor Sskip (simplify_e cond) (simplify_statement s2) (simplify_statement s3)) k')
2448	? Hind_s1)
2449	[ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
2450	normalize nodelta %{kst'} /2/
2451	\| 3: @cc_for1 //
2452	\| 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
2453	elim (elim_IH_aux lab s3
2454	(Kfor2 cond s2 s3 k)
2455	(Kfor2 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k')
2456	? Hind_s3)
2457	[ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
2458	normalize nodelta %{kst'} /2/
2459	\| 3: @cc_for2 //
2460	\| 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
2461	elim (elim_IH_aux lab s2
2462	(Kfor3 cond s2 s3 k)
2463	(Kfor3 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k')
2464	? Hind_s2)
2465	[ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
2466	normalize nodelta %{kst'} /2/
2467	\| 3: @cc_for3 //
2468	\| 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
2469	] ] ]
2470	\| 9,10: #k #k' #Hcont_cast normalize in match (find_label ???); normalize nodelta //
2471	\| 11: #e #k #k' #Hcont_cast normalize in match (find_label ???); normalize nodelta //
2472	\| 12: #e #ls #Hind #k #k' #Hcont_cast
2473	whd in match (find_label ???);
2474	whd in match (find_label ? (simplify_statement ?) ?);
2475	(* We can't elim the Hind on a list of labeled statements. We must proceed more manually. *)
2476	lapply (Hind (Kswitch k) (Kswitch k') ?)
2477	[ 1: @cc_switch //
2478	\| 2: cases (find_label_ls lab ls (Kswitch k)) normalize nodelta
2479	[ 1: //
2480	\| 2: * #st #kst normalize nodelta // ] ]
2481	\| 13: #lab' #s0 #Hind #k #k' #Hcont_cast
2482	whd in match (find_label ???);
2483	whd in match (find_label ? (simplify_statement ?) ?);
2484	cases (ident_eq lab lab') normalize nodelta
2485	[ 1: #_ %{k'} /2/
2486	\| 2: #_ elim (elim_IH_aux lab s0 k k' Hcont_cast Hind)
2487	[ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
2488	normalize nodelta %{kst'} /2/
2489	\| 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ]
2490	]
2491	\| 14: #l #k #k' #Hcont_cast //
2492	\| 15: #l #s0 #Hind #k #k' #Hcont_cast
2493	whd in match (find_label ???);
2494	whd in match (find_label ? (simplify_statement ?) ?);
2495	elim (elim_IH_aux lab s0 k k' Hcont_cast Hind)
2496	[ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
2497	normalize nodelta %{kst'} /2/
2498	\| 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ]
2499	\| 16: #s0 #Hind #k #k' #Hcont_cast
2500	whd in match (find_label ???);
2501	whd in match (find_label ? (simplify_statement ?) ?);
2502	elim (elim_IH_aux lab s0 k k' Hcont_cast Hind)
2503	[ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
2504	normalize nodelta %{kst'} /2/
2505	\| 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ]
2506	\| 17: #sz #i #s0 #t #Hind_s0 #Hind_ls #k #k' #Hcont_cast
2507	whd in match (simplify_ls ?);
2508	whd in match (find_label_ls ???);
2509	lapply Hind_ls
2510	@(labeled_statements_ind … t)
2511	[ 1: #default_case #Hind_ls whd in match (seq_of_labeled_statement ?);
2512	elim (elim_IH_aux lab s0
2513	(Kseq default_case k)
2514	(Kseq (simplify_statement default_case) k') ? Hind_s0)
2515	[ 2: * #st * #kst * #kst' * * #Hrewrite #Hrewrite1 #Hcont_cast'
2516	>Hrewrite >Hrewrite1
2517	normalize nodelta whd in match (find_label_ls ???);
2518	>Hrewrite >Hrewrite1 normalize nodelta
2519	%{kst'} /2/
2520	\| 3: @cc_seq //
2521	\| 1: * #Hrewrite #Hrewrite1 >Hrewrite normalize nodelta
2522	lapply (Hind_ls k k' Hcont_cast)
2523	cases (find_label_ls lab (LSdefault default_case) k)
2524	[ 1: normalize nodelta #Heq1
2525	whd in match (simplify_ls ?);
2526	whd in match (find_label_ls lab ??);
2527	whd in match (seq_of_labeled_statement ?);
2528	whd in match (find_label_ls lab ??);
2529	>Hrewrite1 normalize nodelta @Heq1
2530	\| 2: * #st #kst normalize nodelta #H
2531	whd in match (find_label_ls lab ??);
2532	whd in match (simplify_ls ?);
2533	whd in match (seq_of_labeled_statement ?);
2534	>Hrewrite1 normalize nodelta @H
2535	]
2536	]
2537	\| 2: #sz' #i' #s' #tl' #Hind #A
2538
2539	whd in match (seq_of_labeled_statement ?);
2540	elim (elim_IH_aux lab s0
2541	(Kseq (Ssequence s' (seq_of_labeled_statement tl')) k)
2542	(Kseq (simplify_statement (Ssequence s' (seq_of_labeled_statement tl'))) k')
2543	?
2544	Hind_s0)
2545	[ 3: @cc_seq //
2546	\| 1: * #Heq #Heq2 >Heq >Heq2 normalize nodelta
2547	lapply (A k k' Hcont_cast)
2548	cases (find_label_ls lab (LScase sz' i' s' tl') k) normalize nodelta
2549	[ 1: #H whd in match (find_label_ls ???);
2550	<simplify_ls_commute
2551	whd in match (seq_of_labeled_statement ?);
2552	>Heq2 normalize nodelta
2553	assumption
2554	\| 2: * #st #kst normalize nodelta #H
2555	whd in match (find_label_ls ???);
2556	<simplify_ls_commute >Heq2 normalize nodelta @H
2557	]
2558	\| 2: * #st * #kst * #kst' * * #Hrewrite #Hrewrite1 #Hcont_cast'
2559	>Hrewrite normalize nodelta
2560	%{kst'} @conj try //
2561	whd in match (find_label_ls ???);
2562	<simplify_ls_commute >Hrewrite1 //
2563	]
2564	]
2565	] qed.
2566
2567	lemma cast_find_label_fn : ∀lab,f,k,k',s,ks.
2568	cont_cast k k' →
2569	find_label lab (fn_body f) k = Some ? 〈s,ks〉 →
2570	∃ks'. find_label lab (fn_body (simplify_function f)) k' = Some ? 〈simplify_statement s,ks'〉
2571	∧ cont_cast ks ks'.
2572	#lab * #rettype #args #vars #body #k #k' #s #ks #Hcont_cast #Hfind_lab
2573	whd in match (simplify_function ?);
2574	lapply (cast_find_label lab body ?? Hcont_cast)
2575	>Hfind_lab normalize nodelta //
2576	qed.
2577
2578	theorem cast_correction : ∀ge, ge'.
2579	related_globals ? simplify_fundef ge ge' →
2580	∀s1, s1', tr, s2.
2581	state_cast s1 s1' →
2582	exec_step ge s1 = Value … 〈tr,s2〉 →
2583	∃s2'. exec_step ge' s1' = Value … 〈tr,s2'〉 ∧
2584	state_cast s2 s2'.
2585	#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hs1_sim_s1' #Houtcome
2586	inversion Hs1_sim_s1'
2587	[ 1: (* regular state *)
2588	#f #stm #k #k' #en #m #Hcont_cast
2589	lapply (related_globals_expr_simulation ge ge' en m Hrelated) #Hsim_related
2590	lapply (related_globals_lvalue_simulation ge ge' en m Hrelated) #Hsim_lvalue_related
2591	cases stm
2592	(* Perform the intros for the statements*)
2593	[ 1: \| 2: #lhs #rhs \| 3: #ret #func #args \| 4: #stm1 #stm2 \| 5: #cond #iftrue #iffalse \| 6: #cond #body
2594	\| 7: #cond #body \| 8: #init #cond #step #body \| 9,10: \| 11: #retval \| 12: #cond #switchcases \| 13: #lab #body
2595	\| 14: #lab \| 15: #cost #body ]
2596	[ 1: (* Skip *)
2597	#Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1
2598	whd in match (exec_step ??); whd in match (exec_step ??);
2599	inversion Hcont_cast
2600	[ 1: (* Kstop *)
2601	#Hk #Hk' #_ >fn_return_simplify cases (fn_return f) normalize nodelta
2602	[ 1: >Heq_s1 in Hs1_sim_s1'; >Heq_s1' #Hsim inversion Hsim
2603	[ 1: #f0 #s #k0 #k0' #e #m0 #Hcont_cast0 #Hstate_eq #Hstate_eq' #_
2604	#Eq whd in match (ret ??) in Eq; destruct (Eq)
2605	%{(Returnstate Vundef Kstop (free_list m (blocks_of_env en)))} @conj
2606	[ 1: // \| 2: %3 %1 ]
2607	\| 2: #fd #args #k0 #k0' #m0 #Hcont_cast0 #Habsurd destruct (Habsurd)
2608	\| 3: #res #k0 #k0' #m0 #Hcont_cast #Habsurd destruct (Habsurd)
2609	\| 4: #r #Habsurd destruct (Habsurd) ]
2610	\| 3,4,9: #irrelevant #Habsurd destruct
2611	\| *: #irrelevant1 #irrelevant2 #Habsurd destruct ]
2612	\| 2: (* Kseq stm' k' *)
2613	#stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
2614	whd in match (ret ??) in Eq; destruct (Eq)
2615	%{(State (simplify_function f) (simplify_statement stm') k0' en m)} @conj
2616	[ 1: // \| 2: %1 // ]
2617	\| 3: (* Kwhile *)
2618	#cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
2619	whd in match (ret ??) in Eq; destruct (Eq)
2620	%{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)} @conj
2621	[ 1: // \| 2: %1 // ]
2622	\| 4: (* Kdowhile *)
2623	#cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
2624	elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq cases Hsim_cond
2625	[ 2: * #error #Hfail >Hfail in Eq; #Habsurd normalize in Habsurd; destruct
2626	\| 1: cases (exec_expr ge en m cond) in Eq;
2627	[ 2: #error whd in match (m_bind ?????) in ⊢ (% → ?); #Habsurd destruct
2628	\| 1: * #val #trace whd in match (m_bind ?????) in ⊢ (% → ?); <Htype_cond_eq
2629	#Eq #Hsim_cond lapply (Hsim_cond 〈val,trace〉 (refl ? (OK ? 〈val,trace〉)))
2630	#Hrewrite_cond >Hrewrite_cond whd in match (m_bind ?????);
2631	(* case analysis on the outcome of the conditional *)
2632	cases (exec_bool_of_val val (typeof cond)) in Eq ⊢ %;
2633	[ 2: (* evaluation of the conditional fails *)
2634	#error normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
2635	\| 1: * whd in match (bindIO ??????);
2636	whd in match (bindIO ??????);
2637	#Eq destruct (Eq)
2638	[ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) (simplify_statement body)) k0' en m)}
2639	@conj [ 1: // \| 2: %1 // ]
2640	\| 2: %{(State (simplify_function f) Sskip k0' en m)}
2641	@conj [ 1: // \| 2: %1 // ]
2642	]
2643	]
2644	]
2645	]
2646	\| 5,6,7:
2647	#cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
2648	whd in match (ret ??) in Eq ⊢ %; destruct (Eq)
2649	[ 1: %{(State (simplify_function f)
2650	(Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body))
2651	k0' en m)} @conj
2652	[ 1: // \| 2: %1 // ]
2653	\| 2: %{(State (simplify_function f)
2654	(simplify_statement step)
2655	(Kfor3 (simplify_e cond) (simplify_statement step) (simplify_statement body) k0')
2656	en m)} @conj
2657	[ 1: // \| 2: %1 @cc_for3 // ]
2658	\| 3: %{(State (simplify_function f)
2659	(Sfor Sskip (simplify_e cond) (simplify_statement step)
2660	(simplify_statement body))
2661	k0' en m)} @conj
2662	[ 1: // \| 2: %1 // ]
2663	]
2664	\| 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
2665	whd in match (ret ??) in Eq ⊢ %; destruct (Eq)
2666	%{(State (simplify_function f) Sskip k0' en m)} @conj
2667	[ 1: // \| 2: %1 // ]
2668	\| 9: (* Call *)
2669	#r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ #Eq
2670	>fn_return_simplify cases (fn_return f) in Eq; normalize nodelta
2671	[ 1: #Eq whd in match (ret ??) in Eq ⊢ %; destruct (Eq)
2672	%{(Returnstate Vundef (Kcall r (simplify_function f0) en0 k0')
2673	(free_list m (blocks_of_env en)))} @conj
2674	[ 1: // \| 2: %3 @cc_call // ]
2675	\| 3,4,9: #irrelevant #Habsurd destruct (Habsurd)
2676	\| *: #irrelevant1 #irrelevant2 #Habsurd destruct (Habsurd) ]
2677	]
2678	\| 2: (* Assign *)
2679	#Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1
2680	whd in match (simplify_statement ?); #Heq
2681	whd in match (exec_step ??) in Heq ⊢ %;
2682	(* Begin by making the simplify_e disappear using Hsim_related *)
2683	elim (Hsim_lvalue_related lhs) *
2684	[ 2: * #error #Hfail >Hfail in Heq; #Habsurd normalize in Habsurd; destruct (Habsurd)
2685	\| 1: cases (exec_lvalue ge en m lhs) in Heq;
2686	[ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
2687	\| 1: * * #block #offset #trace
2688	whd in match (bindIO ??????); #Heq #Hsim #Htype_eq_lhs
2689	lapply (Hsim 〈block, offset, trace〉 (refl ? (OK ? 〈block, offset, trace〉)))
2690	#Hrewrite >Hrewrite -Hrewrite whd in match (bindIO ??????);
2691	(* After [lhs], treat [rhs] *)
2692	elim (Hsim_related rhs) *
2693	[ 2: * #error #Hfail >Hfail in Heq; #Habsurd normalize in Habsurd; destruct (Habsurd)
2694	\| 1: cases (exec_expr ge en m rhs) in Heq;
2695	[ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
2696	\| 1: * #val #trace
2697	whd in match (bindIO ??????); #Heq #Hsim #Htype_eq_rhs
2698	lapply (Hsim 〈val, trace〉 (refl ? (OK ? 〈val, trace〉)))
2699	#Hrewrite >Hrewrite -Hrewrite whd in match (bindIO ??????);
2700	<Htype_eq_lhs <Htype_eq_rhs
2701	cases (opt_to_io ?????) in Heq;
2702	[ 1: #o #resumption whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
2703	\| 3: #error whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
2704	\| 2: #mem whd in match (bindIO ??????); #Heq destruct (Heq)
2705	%{(State (simplify_function f) Sskip k' en mem)} @conj
2706	[ 1: // \| 2: %1 // ]
2707	]
2708	]
2709	]
2710	]
2711	]
2712	\| 3: (* Call *)
2713	#Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1
2714	whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
2715	whd in match (exec_step ??) in Heq ⊢ %;
2716	elim (Hsim_related func) in Heq; *
2717	[ 2: * #error #Hfail >Hfail #Htype_eq #Habsurd normalize in Habsurd; destruct (Habsurd)
2718	\| 1: cases (exec_expr ??? func)
2719	[ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2720	\| 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Heq >Heq #Htype_eq >Htype_eq
2721	whd in match (bindIO ??????) in ⊢ (% → %);
2722	elim (related_globals_exprlist_simulation ge ge' en m Hrelated args)
2723	[ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
2724	\| 1: cases (exec_exprlist ge en m args)
2725	[ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2726	\| 1: #l -Hsim #Hsim lapply (Hsim l (refl ? (OK ? l))) #Heq >Heq
2727	whd in match (bindIO ??????) in ⊢ (% → %);
2728	elim Hrelated #_ #Hfunct #_ lapply (Hfunct (\fst a))
2729	cases (find_funct clight_fundef ge (\fst a));
2730	[ 1: #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2731	\| 2: #clfd -Hsim #Hsim lapply (Hsim clfd (refl ? (Some ? clfd))) #Heq >Heq
2732	whd in match (bindIO ??????) in ⊢ (% → %);
2733	>simplify_type_of_fundef_eq >(simplify_fun_typeof_eq ge en m)
2734	cases (assert_type_eq (type_of_fundef clfd) (fun_typeof func))
2735	[ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
2736	\| 1: #Htype_eq cases ret
2737	[ 1: whd in match (bindIO ??????) in ⊢ (% → %);
2738	#Eq destruct (Eq)
2739	%{(Callstate (simplify_fundef clfd) (\fst l)
2740	(Kcall (None (block×offset×type)) (simplify_function f) en k') m)}
2741	@conj
2742	[ 1: // \| 2: %2 @cc_call // ]
2743	\| 2: #fptr whd in match (bindIO ??????) in ⊢ (% → %);
2744	elim (Hsim_lvalue_related fptr) *
2745	[ 2: * #error #Hfail >Hfail #_
2746	#Habsurd normalize in Habsurd; destruct (Habsurd)
2747	\| 1: cases (exec_lvalue ge en m fptr)
2748	[ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2749	\| 1: #a #Hsim #Htype_eq_fptr >(Hsim a (refl ? (OK ? a)))
2750	whd in match (bindIO ??????) in ⊢ (% → %);
2751	#Heq destruct (Heq)
2752	%{(Callstate (simplify_fundef clfd) (\fst l)
2753	(Kcall (Some (block×offset×type) 〈\fst a,typeof (simplify_e fptr)〉)
2754	(simplify_function f) en k') m)}
2755	@conj [ 1: // \| 2: >(simplify_typeof_eq ge en m) %2 @cc_call // ]
2756	] ] ] ] ] ] ] ] ]
2757	\| 4: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
2758	whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
2759	whd in match (exec_step ??) in Heq ⊢ %;
2760	destruct (Heq)
2761	%{(State (simplify_function f) (simplify_statement stm1) (Kseq (simplify_statement stm2) k') en m)}
2762	@conj
2763	[ 1: // \| 2: %1 @cc_seq // ]
2764	\| 5: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
2765	whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
2766	whd in match (exec_step ??) in Heq ⊢ %;
2767	elim (Hsim_related cond) in Heq; *
2768	[ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2769	\| 1: cases (exec_expr ge en m cond)
2770	[ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2771	\| 1: * #condval #condtrace #Hsim lapply (Hsim 〈condval, condtrace〉 (refl ? (OK ? 〈condval, condtrace〉))) #Heq >Heq
2772	#Htype_eq_cond
2773	whd in match (bindIO ??????) in ⊢ (% → %);
2774	>(simplify_typeof_eq ge en m)
2775	cases (exec_bool_of_val condval (typeof cond))
2776	[ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
2777	\| 1: * whd in match (bindIO ??????) in ⊢ (% → %); #Heq normalize nodelta in Heq ⊢ %;
2778	[ 1: destruct skip (condtrace)
2779	%{(State (simplify_function f) (simplify_statement iftrue) k' en m)} @conj
2780	[ 1: // \| 2: <e0 %1 // ]
2781	\| 2: destruct skip (condtrace)
2782	%{(State (simplify_function f) (simplify_statement iffalse) k' en m)} @conj
2783	[ 1: // \| 2: <e0 %1 // ]
2784	] ] ] ]
2785	\| 6: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
2786	whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
2787	whd in match (exec_step ??) in Heq ⊢ %;
2788	elim (Hsim_related cond) in Heq; *
2789	[ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2790	\| 1: cases (exec_expr ge en m cond)
2791	[ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2792	\| 1: * #condval #condtrace #Hsim lapply (Hsim 〈condval, condtrace〉 (refl ? (OK ? 〈condval, condtrace〉))) #Heq >Heq
2793	#Htype_eq_cond
2794	whd in match (bindIO ??????) in ⊢ (% → %);
2795	>(simplify_typeof_eq ge en m)
2796	cases (exec_bool_of_val condval (typeof cond))
2797	[ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
2798	\| 1: * whd in match (bindIO ??????) in ⊢ (% → %); #Heq normalize nodelta in Heq ⊢ %;
2799	[ 1: destruct skip (condtrace)
2800	%{(State (simplify_function f) (simplify_statement body) (Kwhile (simplify_e cond) (simplify_statement body) k') en m)}
2801	@conj
2802	[ 1: // \| 2: <e0 %1 @cc_while // ]
2803	\| 2: destruct skip (condtrace)
2804	%{(State (simplify_function f) Sskip k' en m)} @conj
2805	[ 1: // \| 2: <e0 %1 // ]
2806	] ] ] ]
2807	\| 7: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
2808	whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
2809	whd in match (exec_step ??) in Heq ⊢ %;
2810	destruct (Heq)
2811	%{(State (simplify_function f) (simplify_statement body)
2812	(Kdowhile (simplify_e cond) (simplify_statement body) k') en m)} @conj
2813	[ 1: // \| 2: %1 @cc_dowhile // ]
2814	\| 8: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
2815	whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
2816	whd in match (exec_step ??) in Heq ⊢ %;
2817	cases (is_Sskip init) in Heq;
2818	[ 2: #Hinit_neq_Sskip elim (simplify_is_not_skip init Hinit_neq_Sskip) #pf #Hrewrite >Hrewrite
2819	normalize nodelta
2820	whd in match (ret ??) in ⊢ (% → %);
2821	#Eq destruct (Eq)
2822	%{(State (simplify_function f) (simplify_statement init)
2823	(Kseq (Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body)) k') en m)} @conj
2824	[ 1: // \| 2: %1 @cc_for1 // ]
2825	\| 1: #Hinit_eq_Sskip >Hinit_eq_Sskip
2826	whd in match (simplify_statement ?);
2827	whd in match (is_Sskip ?);
2828	normalize nodelta
2829	elim (Hsim_related cond) *
2830	[ 2: * #error #Hfail #_ >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
2831	\| 1: cases (exec_expr ge en m cond)
2832	[ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2833	\| 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite #Htype_eq_cond >Hrewrite
2834	whd in match (m_bind ?????); whd in match (m_bind ?????);
2835	<Htype_eq_cond
2836	cases (exec_bool_of_val ? (typeof cond))
2837	[ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
2838	\| 1: * whd in match (bindIO ??????); whd in match (bindIO ??????);
2839	normalize nodelta #Heq destruct (Heq)
2840	[ 1: %{(State (simplify_function f) (simplify_statement body)
2841	(Kfor2 (simplify_e cond) (simplify_statement step) (simplify_statement body) k') en m)}
2842	@conj [ 1: // \| 2: %1 @cc_for2 // ]
2843	\| 2: %{(State (simplify_function f) Sskip k' en m)} @conj
2844	[ 1: // \| 2: %1 // ]
2845	] ] ] ] ]
2846	\| 9: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
2847	whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
2848	whd in match (exec_step ??) in Heq ⊢ %;
2849	inversion Hcont_cast in Heq; normalize nodelta
2850	[ 1: #Hk #Hk' #_
2851	\| 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
2852	\| 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
2853	\| 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
2854	\| 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
2855	\| 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
2856	\| 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ]
2857	#H whd in match (ret ??) in H ⊢ %;
2858	destruct (H)
2859	[ 1,4: %{(State (simplify_function f) Sbreak k0' en m)} @conj [ 1,3: // \| 2,4: %1 // ]
2860	\| 2,3,5,6: %{(State (simplify_function f) Sskip k0' en m)} @conj try // %1 // ]
2861	\| 10: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
2862	whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
2863	whd in match (exec_step ??) in Heq ⊢ %;
2864	inversion Hcont_cast in Heq; normalize nodelta
2865	[ 1: #Hk #Hk' #_
2866	\| 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
2867	\| 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
2868	\| 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
2869	\| 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
2870	\| 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
2871	\| 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ]
2872	#H whd in match (ret ??) in H ⊢ %;
2873	destruct (H)
2874	[ 1,4,6: %{(State (simplify_function f) Scontinue k0' en m)} @conj try // %1 //
2875	\| 2: %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)}
2876	@conj try // %1 //
2877	\| 3: elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq elim Hsim_cond in H;
2878	[ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
2879	\| 1: cases (exec_expr ??? cond)
2880	[ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2881	\| 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
2882	whd in match (m_bind ?????) in ⊢ (% → %);
2883	<Htype_cond_eq
2884	cases (exec_bool_of_val ? (typeof cond))
2885	[ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
2886	\| 1: * whd in match (bindIO ??????); whd in match (bindIO ??????);
2887	normalize nodelta #Heq destruct (Heq)
2888	[ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) (simplify_statement body)) k0' en m)}
2889	@conj [ 1: // \| 2: %1 // ]
2890	\| 2: %{(State (simplify_function f) Sskip k0' en m)}
2891	@conj [ 1: // \| 2: %1 // ]
2892	] ] ] ]
2893	\| 5: %{(State (simplify_function f) (simplify_statement step)
2894	(Kfor3 (simplify_e cond) (simplify_statement step) (simplify_statement body) k0') en m)} @conj
2895	[ 1: // \| 2: %1 @cc_for3 // ]
2896	]
2897	\| 11: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
2898	whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
2899	whd in match (exec_step ??) in Heq ⊢ %;
2900	cases retval in Heq; normalize nodelta
2901	[ 1: >fn_return_simplify cases (fn_return f) normalize nodelta
2902	whd in match (ret ??) in ⊢ (% → %);
2903	[ 2: #sz #sg \| 3: #fl \| 4: #ty' \| 5: #ty #n \| 6: #tl #ty'
2904	\| 7: #id #fl \| 8: #id #fl \| 9: #id ]
2905	#H destruct (H)
2906	%{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env en)))}
2907	@conj [ 1: // \| 2: %3 @call_cont_simplify // ]
2908	\| 2: #e >fn_return_simplify cases (type_eq_dec (fn_return f) Tvoid) normalize nodelta
2909	[ 1: #_ #Habsurd destruct (Habsurd)
2910	\| 2: #_ elim (Hsim_related e) *
2911	[ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2912	\| 1: cases (exec_expr ??? e)
2913	[ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2914	\| 1: #a #Hsim #Htype_eq_e lapply (Hsim a (refl ? (OK ? a)))
2915	#Hrewrite >Hrewrite
2916	whd in match (m_bind ?????); whd in match (m_bind ?????);
2917	#Heq destruct (Heq)
2918	%{(Returnstate (\fst a) (call_cont k') (free_list m (blocks_of_env en)))}
2919	@conj [ 1: // \| 2: %3 @call_cont_simplify // ]
2920	] ] ] ]
2921	\| 12: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
2922	whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
2923	whd in match (exec_step ??) in Heq ⊢ %;
2924	elim (Hsim_related cond) in Heq; *
2925	[ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2926	\| 1: cases (exec_expr ??? cond)
2927	[ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
2928	\| 1: #a #Hsim #Htype_eq_cond lapply (Hsim a (refl ? (OK ? a)))
2929	#Hrewrite >Hrewrite
2930	whd in match (bindIO ??????); whd in match (bindIO ??????);
2931	cases (\fst a) normalize nodelta
2932	[ 1,3,4,5: #a destruct (a) #b destruct (b)
2933	\| 2: #sz #i whd in match (ret ??) in ⊢ (% → %); #Heq destruct (Heq)
2934	%{(State (simplify_function f)
2935	(seq_of_labeled_statement (select_switch sz i (simplify_ls switchcases)))
2936	(Kswitch k') en m)} @conj
2937	[ 1: //
2938	\| 2: @(labeled_statements_ind … switchcases)
2939	[ 1: #default_s
2940	whd in match (simplify_ls ?);
2941	whd in match (select_switch sz i ?) in ⊢ (?%%);
2942	whd in match (seq_of_labeled_statement ?) in ⊢ (?%%);
2943	%1 @cc_switch //
2944	\| 2: #sz' #i' #top_case #tail #Hind
2945	cut ((seq_of_labeled_statement (select_switch sz i (simplify_ls (LScase sz' i' top_case tail))))
2946	= (simplify_statement (seq_of_labeled_statement (select_switch sz i (LScase sz' i' top_case tail)))))
2947	[ 1: >select_switch_commute >simplify_ls_commute @refl
2948	\| 2: #Hrewrite >Hrewrite
2949	%1 @cc_switch //
2950	] ] ] ] ] ]
2951	\| 13: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
2952	whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
2953	whd in match (exec_step ??) in Heq ⊢ %;
2954	destruct (Heq)
2955	%{(State (simplify_function f) (simplify_statement body) k' en m)}
2956	@conj %1 //
2957	\| 14: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
2958	whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
2959	whd in match (exec_step ??) in Heq ⊢ %;
2960	lapply (cast_find_label_fn lab f (call_cont k) (call_cont k'))
2961	cases (find_label lab (fn_body f) (call_cont k)) in Heq;
2962	normalize nodelta
2963	[ 1: #Habsurd destruct (Habsurd)
2964	\| 2: * #st #kst normalize nodelta
2965	#Heq whd in match (ret ??) in Heq;
2966	#H lapply (H st kst (call_cont_simplify ???) (refl ? (Some ? 〈st,kst〉))) try //
2967	* #kst' * #Heq2 #Hcont_cast' >Heq2 normalize nodelta
2968	destruct (Heq)
2969	%{(State (simplify_function f) (simplify_statement st) kst' en m)} @conj
2970	[ 1: // \| 2: %1 // ]
2971	]
2972	\| 15: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
2973	whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
2974	whd in match (exec_step ??) in Heq ⊢ %;
2975	destruct (Heq)
2976	%{(State (simplify_function f) (simplify_statement body) k' en m)}
2977	@conj
2978	[ 1: // \| 2: %1 // ]
2979	]
2980	\| 2: (* Call state *)
2981	#fd #args #k #k' #m #Hcont_cast #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
2982	whd in match (exec_step ??) in ⊢ (% → %);
2983	elim fd in Heq_s1'; normalize nodelta
2984	[ 1: * #rettype #args #vars #body #Heq_s1'
2985	whd in match (simplify_function ?);
2986	cases (exec_alloc_variables empty_env ??)
2987	#local_env #new_mem normalize nodelta
2988	cases (exec_bind_parameters ????)
2989	[ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
2990	\| 1: #new_mem_init
2991	whd in match (m_bind ?????); whd in match (m_bind ?????);
2992	#Heq destruct (Heq)
2993	%{(State (mk_function rettype args vars (simplify_statement body))
2994	(simplify_statement body) k' local_env new_mem_init)} @conj
2995	[ 1: // \| 2: %1 // ]
2996	]
2997	\| 2: #id #argtypes #rettype #Heq_s1'
2998	cases (check_eventval_list args ?)
2999	[ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
3000	\| 1: #l whd in match (m_bind ?????); whd in match (m_bind ?????);
3001	#Habsurd destruct (Habsurd) ]
3002	]
3003	\| 3: (* Return state *)
3004	#res #k #k' #m #Hcont_cast #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
3005	whd in match (exec_step ??) in ⊢ (% → %);
3006	inversion Hcont_cast
3007	[ 1: #Hk #Hk' #_
3008	\| 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
3009	\| 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
3010	\| 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
3011	\| 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
3012	\| 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
3013	\| 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ]
3014	normalize nodelta
3015	[ 1: cases res normalize nodelta
3016	[ 2: * normalize nodelta #i
3017	[ 3: #Heq whd in match (ret ??) in Heq; destruct (Heq)
3018	%{(Finalstate i)} @conj [ 1: // \| 2: // ]
3019	\| * : #Habsurd destruct (Habsurd) ]
3020	\| *: #a try #b destruct ]
3021	\| 9: elim r normalize nodelta
3022	[ 2: * * #block #offset #typ normalize nodelta
3023	cases (opt_to_io io_out io_in mem ? (store_value_of_type' ????))
3024	[ 2: #mem whd in match (m_bind ?????); whd in match (m_bind ?????);
3025	#Heq destruct (Heq)
3026	%{(State (simplify_function f0) Sskip k0' en0 mem)} @conj
3027	[ 1: // \| 2: %1 // ]
3028	\| 1: #output #resumption
3029	whd in match (m_bind ?????); #Habsurd destruct (Habsurd)
3030	\| 3: #eror #Habsurd normalize in Habsurd; destruct (Habsurd) ]
3031	\| 1: #Heq whd in match (ret ??) in Heq; destruct (Heq)
3032	%{(State (simplify_function f0) Sskip k0' en0 m)} @conj
3033	[ 1: // \| 2: %1 // ]
3034	]
3035	\| *: #Habsurd destruct (Habsurd) ]
3036	\| 4: (* Final state *)
3037	#r #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
3038	whd in match (exec_step ??) in ⊢ (% → %);
3039	#Habsurd destruct (Habsurd)
3040	] qed.

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format