Context Navigation

toCminorCorrectnessExpr.ma @ 2593

Last change on this file since 2593 was 2591, checked in by garnier, 8 years ago
Moved simulation proof for expressions in toCminorCorrectnessExpr.ma, for separate typechecking.
File size: 109.8 KB

Line
1	include "Clight/toCminor.ma".
2	include "Clight/CexecInd.ma".
3	include "common/Globalenvs.ma".
4	include "Clight/toCminorOps.ma".
5	include "Clight/memoryInjections.ma".
6	include "Clight/abstract.ma".
7	include "Cminor/abstract.ma".
8
9	record clight_cminor_inv : Type[0] ≝ {
10	globals : list (ident × region × type);
11	ge_cl : genv_t clight_fundef;
12	ge_cm : genv_t (fundef internal_function);
13	eq_sym : ∀s. find_symbol … ge_cl s = find_symbol … ge_cm s;
14	trans_fn : ∀v,f. find_funct … ge_cl v = Some ? f →
15	∃tmp_u,f',H1,H2.
16	translate_fundef tmp_u globals H1 f H2 = OK ? f' ∧
17	find_funct … ge_cm v = Some ? f'
18	}.
19
20	(* Perhaps we will have to be more precise on what is allocated, etc.
21	cf [exec_alloc_variables]. For now this is conveniently hidden in
22	the [value_eq E v v'] *)
23	definition memory_matching ≝
24	λE:embedding.
25	λm,m':mem.
26	λen:cl_env.
27	λvenv:cm_env.
28	λcminv:clight_cminor_inv.
29	λsp:block.
30	λvars:var_types.
31	∀id.
32	match lookup SymbolTag ? en id with
33	[ None ⇒
34	match find_symbol ? (ge_cl cminv) id with
35	[ None ⇒ True
36	\| Some cl_blo ⇒ E cl_blo = Some ? 〈cl_blo, zero_offset〉
37	]
38	\| Some cl_blo ⇒
39	match lookup ?? vars id with
40	[ Some kind ⇒
41	let 〈vtype, type〉 ≝ kind in
42	match vtype with
43	[ Stack n ⇒
44	E cl_blo = Some ? 〈sp, mk_offset (repr I16 n)〉
45	\| Local ⇒
46	∀v. load_value_of_type type m cl_blo zero_offset = Some ? v →
47	∃v'. lookup ?? venv id = Some ? v' ∧
48	value_eq E v v'
49	\| _ ⇒ False ]
50	\| None ⇒ False ]
51	].
52
53
54	(* Local variables show up in the variable characterisation as local. *)
55
56	lemma characterise_vars_localid : ∀globals,f,vartypes,stacksize,id.
57	characterise_vars globals f = 〈vartypes, stacksize〉 →
58	Exists ? (λx. \fst x = id) (fn_params f @ fn_vars f) →
59	∃t. local_id vartypes id t.
60	#globals * #ret #args #vars #body
61	whd in match (characterise_vars ??); elim (args@vars)
62	[ #vartypes #stacksize #id #_ *
63	\| * #hd #ty #tl #IH
64	#vartypes #stacksize #id
65	whd in match (foldr ?????);
66	cases (foldr ? (Prod ??) ???) in IH ⊢ %;
67	#vartypes' #stackspace' #IH
68	whd in ⊢ (??(match % with [_⇒?])? → ?);
69	cases (orb ??)
70	#E whd in E:(??%?); destruct *
71	[ 1,3: #E destruct %{(typ_of_type ty)}
72	whd whd in match (lookup' ??); >lookup_add_hit //
73	\| 2,4: #TL cases (IH … (refl ??) TL) #ty' #LC
74	cases (identifier_eq ? id hd)
75	[ 1,3: #E destruct %{(typ_of_type ty)} whd whd in match (lookup' ??); >lookup_add_hit //
76	\| 2,4: #NE %{ty'} whd whd in match (lookup' ??); >lookup_add_miss //
77	]
78	]
79	] qed.
80
81
82	(* ---------------------------------- *)
83	(* Auxilliary lemmas and definitions. *)
84
85
86
87
88	lemma exec_alloc_fail_antimonotonic : ∀variables,env,env',var_id.
89	(∃m,m'.exec_alloc_variables env m variables=〈env',m'〉) →
90	lookup ?? env' var_id = None ? →
91	lookup ?? env var_id = None ? ∧
92	¬(Exists (ident×type) (λx:ident×type.\fst x=var_id) variables).
93	#vars elim vars
94	[ #env #env' #var_id normalize * #m * #m' #Heq destruct (Heq)
95	#H @conj try @H % //
96	\| * #id' #ty' #tl #Hind #env #env' #var * #m * #m'
97	whd in ⊢ ((??%?) → ? → ?);
98	cases (alloc m 0 (sizeof ty') XData) #m0 * #b #Hregion
99	normalize nodelta #Hexec #Hlookup
100	lapply (Hind … (ex_intro … (ex_intro … Hexec)) Hlookup)
101	cases env #env cases id' #id' cases var #var normalize
102	@(eqb_elim … id' var)
103	[ 2: #Hneq * #Hlookup' #Hexists' lapply (lookup_opt_pm_set_miss ? (Some ? b) … env (sym_neq ??? Hneq))
104	#Heq <Heq @conj try @Hlookup' % *
105	[ #Heq' destruct (Heq') cases Hneq #H @H @refl
106	\| cases Hexists' #H @H ]
107	\| 1: #Heq destruct (Heq) * #Hlookup' #Hexists'
108	lapply (lookup_opt_pm_set_hit … (Some ? b) var … env) #H1
109	>H1 in Hlookup'; #Heq destruct
110	]
111	] qed.
112
113	lemma variable_not_in_env_but_in_vartypes_is_global :
114	∀env,env',f,vars,stacksize,globals,var_id.
115	(∃m,m'.exec_alloc_variables env m (fn_params f@fn_vars f) =〈env',m'〉) →
116	characterise_vars globals f =〈vars,stacksize〉 →
117	lookup ?? env' var_id = None ? →
118	∀allocty,ty. lookup' vars var_id = OK ? 〈allocty, ty〉 →
119	∃r.allocty = Global r.
120	#env #env' #f #vars #stacksize #globals #var_id#Hexec_alloc
121	#Hcharacterise #Hlookup_fail #allocty #ty #Hlookup_type_ok
122	lapply (characterise_vars_src … Hcharacterise var_id ?)
123	[ whd % cases (res_inversion ?????? Hlookup_type_ok) * #vt #t *
124	#Hlookup >Hlookup #_ #Habsurd destruct ]
125	*
126	[ 1: * #r * #ty' * #Hlookup' #Hex %{r}
127	>Hlookup' in Hlookup_type_ok; #Heq destruct @refl ]
128	* #t whd in ⊢ (% → ?); >Hlookup_type_ok whd normalize nodelta
129	@(match allocty
130	return λx. allocty = x → ?
131	with
132	[ Global r ⇒ λ_. ?
133	\| Stack st' ⇒ λHalloc. ?
134	\| Local ⇒ λHalloc. ?
135	] (refl ? allocty))
136	[ @False_ind ] normalize nodelta
137	#Heq_typ
138	(* Halloc is in contradiction with Hlookup_fail *)
139	lapply (exec_alloc_fail_antimonotonic … Hexec_alloc … Hlookup_fail)
140	* #Hlookup' #Hnot_exists
141	lapply (characterise_vars_all … Hcharacterise var_id t ?)
142	[ 1,3: whd destruct (Halloc) >Hlookup_type_ok // ]
143	#Hexists @False_ind
144	cut (Exists (ident×type) (λx:ident×type.\fst x=var_id) (fn_params f@fn_vars f))
145	[ 1,3: elim (fn_params f @ fn_vars f) in Hexists; //
146	* #id' #ty' #tl #Hind *
147	[ 1,3: * #Heq #_ %1 @Heq
148	\| *: #H %2 @Hind @H ] ]
149	#H cases Hnot_exists #H' @H' @H
150	qed.
151
152	(* avoid a case analysis on type inside of a big proof *)
153	lemma match_type_inversion_aux : ∀ty,e,f.
154	match ty in type return λty':type.(res (expr (typ_of_type ty'))) with
155	[Tvoid⇒Error (expr (ASTint I32 Unsigned)) (msg TypeMismatch)
156	\|Tint (sz:intsize) (sg:signedness)⇒ f sz sg
157	\|Tpointer (x:type)⇒
158	Error (expr (typ_of_type (Tpointer x))) (msg TypeMismatch)
159	\|Tarray (x:type) (y:ℕ)⇒
160	Error (expr (typ_of_type (Tarray x y))) (msg TypeMismatch)
161	\|Tfunction (x:typelist) (y:type)⇒
162	Error (expr (typ_of_type (Tfunction x y))) (msg TypeMismatch)
163	\|Tstruct (x:ident) (y:fieldlist)⇒
164	Error (expr (ASTint I32 Unsigned)) (msg TypeMismatch)
165	\|Tunion (x:ident) (y:fieldlist)⇒
166	Error (expr (ASTint I32 Unsigned)) (msg TypeMismatch)
167	\|Tcomp_ptr (x:ident)⇒
168	Error (expr (typ_of_type (Tcomp_ptr x))) (msg TypeMismatch)]
169	= OK ? e →
170	∃sz,sg. ty = Tint sz sg ∧ (f sz sg ≃ OK ? e).
171	*
172	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
173	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
174	whd in match (typ_of_type Tvoid);
175	#e #f normalize nodelta #Heq destruct
176	%{sz} %{sg} % try @refl >Heq %
177	qed.
178
179
180	(* The two following lemmas are just noise. *)
181
182	lemma expr_vars_fix_ptr_type :
183	∀ty',optlen.
184	∀e:expr (typ_of_type (ptr_type ty' optlen)).
185	∀P.
186	expr_vars ASTptr (fix_ptr_type ty' optlen e) P →
187	expr_vars
188	(typ_of_type
189	match optlen
190	in option
191	return λ_:(option ℕ).type with
192	[None⇒Tpointer ty'
193	\|Some (n':ℕ)⇒ Tarray ty' n']) e P.
194	#ty' * normalize
195	[ 2: #n ]
196	#e #P
197	@expr_vars_mp //
198	qed.
199
200	lemma eval_expr_rewrite_aux :
201	∀genv.
202	∀optlen.
203	∀ty'.
204	∀e.
205	∀cm_env.
206	∀H.
207	∀sp.
208	∀m.
209	∀res.
210	(eval_expr genv
211	(typ_of_type
212	match optlen in option return λ_:(option ℕ).type with
213	[None⇒Tpointer ty'\|Some (n':ℕ)⇒Tarray ty' n'])
214	e cm_env (expr_vars_fix_ptr_type ty' optlen e (λid:ident.λty0:typ.present SymbolTag val cm_env id) H) sp m) = OK ? res →
215	eval_expr genv ASTptr (fix_ptr_type ty' optlen e) cm_env H sp m = OK ? res.
216	#genv * [ 2: #n ] normalize nodelta
217	#ty' normalize in match (typ_of_type ?);
218	#e #cm_env whd in match (fix_ptr_type ???);
219	#H #sp #m #res #H @H
220	qed.
221
222	lemma sign_ext_sign_ext_reduce :
223	∀i. sign_ext 32 16 (sign_ext 16 32 i) = i.
224	#i @refl
225	qed.
226
227	lemma sign_ext_zero_ext_reduce :
228	∀i. sign_ext 32 16 (zero_ext 16 32 i) = i.
229	#i @refl
230	qed.
231
232	(* There are two zero_ext, and this causes the "disambiguator" to fail. So we do
233	* the cleanup ourselves. *)
234
235	definition zero_ext_bv : ∀n1,n2. ∀bv:BitVector n1. BitVector n2 ≝ zero_ext.
236	definition zero_ext_val : ∀target_sz:intsize. val → val ≝ zero_ext.
237
238	(* CM code uses 8 bit constants and upcasts them to target_size, CL uses 32 bit and
239	* downcasts them to target_size. In the end, these are equal. We directly state what
240	* we need. *)
241	lemma value_eq_cl_cm_true :
242	∀E,sz.
243	value_eq E
244	(Vint sz (zero_ext_bv ? (bitsize_of_intsize sz) (repr I32 1)))
245	(zero_ext_val sz (Vint I8 (repr I8 1))).
246	#E * %2 qed.
247
248	lemma value_eq_cl_cm_false :
249	∀E,sz.
250	value_eq E
251	(Vint sz (zero_ext_bv ? (bitsize_of_intsize sz) (repr I32 0)))
252	(zero_ext_val sz (Vint I8 (repr I8 0))).
253	#E * %2 qed.
254
255	lemma exec_bool_of_val_inversion : ∀v,ty,b.
256	exec_bool_of_val v ty = OK ? b →
257	(∃sz,sg,i. v = Vint sz i ∧ ty = Tint sz sg ∧ b = (¬eq_bv (bitsize_of_intsize sz) i (zero (bitsize_of_intsize sz)))) ∨
258	(∃ty'. v = Vnull ∧ ty = Tpointer ty' ∧ b = false) ∨
259	(∃ptr,ty'. v = Vptr ptr ∧ ty = Tpointer ty' ∧ b = true).
260	#v #ty #b #Hexec
261	cases v in Hexec;
262	[ \| #vsz #i \| \| #p ]
263	cases ty
264	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain \| #structname #fieldspec \| #unionname #fieldspec \| #id
265	\| \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain \| #structname #fieldspec \| #unionname #fieldspec \| #id
266	\| \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain \| #structname #fieldspec \| #unionname #fieldspec \| #id
267	\| \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain \| #structname #fieldspec \| #unionname #fieldspec \| #id ]
268	whd in ⊢ ((??%%) → ?);
269	#Heq destruct (Heq)
270	[ 2: %1 %2 %{ptr_ty} @conj try @conj try @refl
271	\| 3: %2 %{p} %{ptr_ty} @conj try @conj try @refl
272	\| 1: %1 %1 %{sz} %{sg} lapply Heq -Heq
273	cases vsz in i; #i cases sz whd in ⊢ ((??%?) → ?);
274	#Heq destruct %{i} @conj try @conj try @refl
275	] qed.
276
277	(* This lemma is noise I extracted from the proof below, even though it is used only once.
278	Better that than an ugly cut.
279	We need the following lemma to feed another one down in the deref case. In essence,
280	it says that the variables present in a cminor expression resulting from converting
281	a clight deref are transmitted to the cminor counterpart of the dereferenced pointer.
282	This is made messy by the fact that clight to cminor implements different deref
283	strategies for different kind of variables.
284	*)
285	lemma translate_expr_deref_present:
286	∀vars:var_types.
287	∀ptrdesc:expr_descr.
288	∀ptrty:type.
289	∀derefty:type.
290	∀cm_deref.
291	∀Hcm_deref.
292	∀cm_ptr.
293	∀Hcm_ptr.
294	∀cm_env:env.
295	translate_expr vars (Expr (Ederef (Expr ptrdesc ptrty)) derefty) =OK ? «cm_deref,Hcm_deref» →
296	expr_vars (typ_of_type derefty) cm_deref (λid:ident.λty0:typ.present SymbolTag ? cm_env id) →
297	translate_expr vars (Expr ptrdesc ptrty) =OK ? «cm_ptr,Hcm_ptr» →
298	expr_vars ? cm_ptr (λid:ident.λty0:typ.present SymbolTag ? cm_env id).
299	#cut_vars #ptrdesc #ptrty #derefty
300	cases ptrty
301	[ \| #sz1 #sg1 \| #ptr_ty1 \| #array_ty1 #array_sz1 \| #domain1 #codomain1
302	\| #structname1 #fieldspec1 \| #unionname1 #fieldspec1 \| #id1 ]
303	#cut_cm_deref #Hcut_cm_deref #cut_cm_ptr #Hcut_cm_ptr #cut_cm_env
304	whd in match (translate_expr ??);
305	cases (translate_expr cut_vars (Expr ptrdesc ?)) normalize nodelta
306	[ 1,2,3,4,6,8,10,11,12,13,14,16: #err #Habsurd destruct (Habsurd) ]
307	normalize in match (typ_of_type ?);
308	* #cut_e' #Hcut_local_e'
309	lapply Hcut_cm_deref -Hcut_cm_deref lapply cut_cm_deref -cut_cm_deref
310	cases (access_mode derefty) normalize nodelta
311	[ #invert_ty \| \| #invert_ty
312	\| #invert_ty \| \| #invert_ty
313	\| #invert_ty \| \| #invert_ty
314	\| #invert_ty \| \| #invert_ty ]
315	[ 3,6,9,12: #cut_cm_deref #Hcut_cm_deref #Habsurd destruct (Habsurd) ]
316	#cut_cm_deref #Hcut_cm_deref #Heq destruct (Heq)
317	[ 1,3,5,7: whd in ⊢ (% → ?); ]
318	#Hgoal #Heq destruct @Hgoal
319	qed.
320
321	lemma load_value_of_type_by_ref :
322	∀ty,m,b,off,val.
323	load_value_of_type ty m b off = Some ? val →
324	typ_of_type ty ≃ ASTptr →
325	access_mode ty ≃ By_reference →
326	val = Vptr (mk_pointer b off).
327	*
328	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
329	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
330	#m #b #off #val
331	[ 1,6,7: normalize #Habsurd destruct (Habsurd)
332	\| 4,5: normalize #Heq #_ #_ destruct @refl
333	\| 2: #_ normalize #Heq destruct
334	\| *: #Hload normalize #_ #H
335	lapply (jmeq_to_eq ??? H) #Heq destruct
336	] qed.
337
338	lemma load_value_of_type_by_value :
339	∀ty,m,b,off,val.
340	access_mode ty = By_value (typ_of_type ty) →
341	load_value_of_type ty m b off = Some ? val →
342	loadv (typ_of_type ty) m (Vptr (mk_pointer b off)) = Some ? val.
343	*
344	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
345	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
346	#m #b #off #val
347	normalize in match (access_mode ?);
348	[ 1,4,5,6,7: #Habsurd destruct ]
349	#_
350	#H @H
351	qed.
352
353	lemma lookup_exec_alloc :
354	∀source_variables, initial_env, env, var_id, clb, m, m'.
355	lookup ?? env var_id = Some ? clb →
356	exec_alloc_variables initial_env m source_variables = 〈env,m'〉 →
357	lookup ?? initial_env var_id = Some ? clb ∨
358	Exists ? (λx. \fst x = var_id) source_variables.
359	#source_variables
360	elim source_variables
361	[ 1: #init_env #env #var #clb #m #m' #Hlookup #Hexec_alloc normalize in Hexec_alloc;
362	destruct (Hexec_alloc) %1 @Hlookup
363	\| 2: * #id #ty #tail #Hind
364	#init_env #env #var #clb #m #m' #Hlookup
365	whd in ⊢ (??%? → ?);
366	cases (alloc m 0 (sizeof ty) XData) #m0 * #blo #Hreg normalize nodelta
367	#Hexec_alloc
368	@(match identifier_eq ? id var with [ inl Heq ⇒ ? \| inr Hneq ⇒ ? ])
369	[ 1: destruct (Heq) %2 %1 @refl ]
370	cases (Hind … Hlookup Hexec_alloc)
371	[ #Hlookup %1 <(lookup_add_miss SymbolTag ? init_env ?? blo (sym_neq ??? Hneq)) @Hlookup
372	\| #Hexists %2 %2 @Hexists ]
373	] qed.
374
375	lemma characterise_vars_lookup_local :
376	∀globals,f,vartypes,stacksize,id,clb,env.
377	characterise_vars globals f = 〈vartypes, stacksize〉 →
378	lookup ?? env id = Some ? clb →
379	(∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈env,m'〉) →
380	∃t. local_id vartypes id t.
381	#globals #f #vartypes #stacksize #id #clb #env
382	#Hchar #Hlookup * #m * #m' #Hexec
383	cases (lookup_exec_alloc … Hlookup Hexec)
384	[ normalize in ⊢ (% → ?); #Heq destruct
385	\| @(characterise_vars_localid … Hchar) ]
386	qed.
387
388
389	(* -------------------------------------------------------------------- *)
390	(* Simulation proof for expression evaluation between Clight and Cminor *)
391
392	lemma eval_expr_sim :
393	(* [cl_cm_inv] maps CL globals to CM globals, including functions *)
394	∀cl_cm_inv : clight_cminor_inv.
395	(* current function (defines local environment) *)
396	∀f : function.
397	(* [alloctype] maps variables to their allocation type (global, stack, register) *)
398	∀alloctype : var_types.
399	∀stacksize : ℕ.
400	∀alloc_hyp : characterise_vars (globals cl_cm_inv) f = 〈alloctype, stacksize〉.
401	(* environments *)
402	∀cl_env : cl_env.
403	∀cm_env : cm_env.
404	(* Characterise clight environment. Needed to prove that some variable is either a parameter or a local. *)
405	∀cl_env_hyp : ∃m,m'. exec_alloc_variables empty_env m (fn_params f @ fn_vars f) = 〈cl_env,m'〉.
406	(* CL and CM memories *)
407	∀cl_m : mem.
408	∀cm_m : mem.
409	(* memory injection and matching *)
410	∀embed : embedding.
411	∀injection : memory_inj embed cl_m cm_m.
412	∀stackptr : block.
413	∀matching : memory_matching embed cl_m cm_m cl_env cm_env cl_cm_inv stackptr alloctype.
414	(* clight expr to cminor expr *)
415	(∀(e:expr).
416	∀(e':CMexpr (typ_of_type (typeof e))).
417	∀Hexpr_vars.
418	translate_expr alloctype e = OK ? («e', Hexpr_vars») →
419	∀cl_val,trace,Hyp_present.
420	exec_expr (ge_cl … cl_cm_inv) cl_env cl_m e = OK ? 〈cl_val, trace〉 →
421	∃cm_val. eval_expr (ge_cm cl_cm_inv) (typ_of_type (typeof e)) e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
422	value_eq embed cl_val cm_val) ∧
423	(* clight /lvalue/ to cminor /expr/ *)
424	(∀ed,ty.
425	∀(e':CMexpr ASTptr).
426	∀Hexpr_vars.
427	translate_addr alloctype (Expr ed ty) = OK ? («e', Hexpr_vars») →
428	∀cl_blo,cl_off,trace,Hyp_present.
429	exec_lvalue' (ge_cl … cl_cm_inv) cl_env cl_m ed ty = OK ? 〈cl_blo, cl_off, trace〉 →
430	∃cm_val. eval_expr (ge_cm cl_cm_inv) ASTptr e' cm_env Hyp_present stackptr cm_m = OK ? 〈trace, cm_val〉 ∧
431	value_eq embed (Vptr (mk_pointer cl_blo cl_off)) cm_val).
432	#inv #f #vars #stacksize #Hcharacterise #cl_env #cm_env #Hexec_alloc #cl_m #cm_m #E #Hinj #sp #Hlocal_matching
433	@expr_lvalue_ind_combined
434	[ 7: (* binary ops *)
435	#ty
436	#op #e1 #e2
437	#Hind1 #Hind2 #e' #Hexpr_vars #Htranslate
438	cases (bind_inversion ????? Htranslate) -Htranslate
439	* #lhs #Hexpr_vars_lhs * #Htranslate_lhs #Htranslate
440	cases (bind_inversion ????? Htranslate) -Htranslate
441	* #rhs #Hexpr_vars_rhs * #Htranslate_rhs
442	whd in ⊢ ((??%?) → ?);
443	#Htranslate_binop
444	cases (bind_as_inversion ????? Htranslate_binop) -Htranslate_binop
445	#translated_binop * #Htranslated_binop whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
446	#cl_val #trace #Hyp_present #Hexec
447	(* dump all the useless stuff after the turnstyle, in order to perform rewrites and so on. *)
448	lapply (Hind1 lhs Hexpr_vars_lhs Htranslate_lhs) -Hind1
449	lapply (Hind2 rhs Hexpr_vars_rhs Htranslate_rhs) -Hind2
450	lapply Hyp_present -Hyp_present
451	lapply Htranslate_lhs -Htranslate_lhs
452	lapply Htranslate_rhs -Htranslate_rhs
453	lapply Hexpr_vars_lhs -Hexpr_vars_lhs
454	lapply Hexpr_vars_rhs -Hexpr_vars_rhs
455	lapply Hexec -Hexec
456	lapply Htranslated_binop -Htranslated_binop
457	lapply rhs -rhs lapply lhs -lhs
458	(* end of dump *)
459	cases op
460	whd in ⊢ (? → ? → (??%?) → ?);
461	[ 1: (* add *)
462	lapply (classify_add_inversion (typeof e1) (typeof e2))
463	* [ 2: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
464	(* trying to factorise as much stuff as possible ... *)
465	lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 whd in match (typeof ?); #e'
466	* [ 1: * ]
467	[ 1: * #sz * #sg * *
468	\| 2: * #optlen * #ty' * #sz * #sg * *
469	\| 3: * #optlen * #sz * #sg * #ty' * * ]
470	whd in match (typeof ?) in ⊢ (% → % → ?);
471	#Htypeof_e1 #Htypeof_e2
472	>Htypeof_e1 >Htypeof_e2
473	#Hclassify
474	lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
475	normalize nodelta
476	whd in match (typeof ?) in ⊢ (% → % → %);
477	whd in match (typ_of_type (Tint ??));
478	#lhs #rhs #Htyp_should_eq
479	[ 1: cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
480	\| 2,3: cases (typ_should_eq_inversion ASTptr (typ_of_type ty) … Htyp_should_eq) ]
481	-Htyp_should_eq
482	#Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
483	<Heq_e' -Heq_e'
484	#Hexec
485	#Hexpr_vars_rhs #Hexpr_vars_lhs
486	#Htranslate_rhs #Htranslate_lhs
487	* [ #Hyp_present_lhs #Hyp_present_rhs
488	\| #Hyp_present_lhs * #Hyp_present_rhs #Hyp_present_cst
489	\| * #Hyp_present_lhs #Hyp_present_cst #Hyp_present_rhs ]
490	whd in match (typeof ?);
491	#Hind_rhs #Hind_lhs
492	cases (bind_inversion ????? Hexec) -Hexec
493	* #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
494	cases (bind_inversion ????? Hexec) -Hexec
495	* #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
496	cases (bind_inversion ????? Hexec) -Hexec
497	#val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
498	lapply (opt_to_res_inversion ???? Hsem) -Hsem
499	whd in match (typeof ?); whd in match (typeof ?);
500	#Hsem_binary
501	[ 1,2: lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
502	\| 3: lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs) ]
503	* #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
504	[ 1,3: lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
505	\| 2: lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs) ]
506	* #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
507	whd in match (eval_expr ???????);
508	whd in match (proj1 ???);
509	[ 3: lapply (eval_expr_rewrite_aux … Heval_lhs) -Heval_lhs #Heval_lhs ]
510	[ 1,2: >Heval_lhs normalize nodelta
511	whd in match (eval_expr ???????);
512	whd in match (eval_expr ???????);
513	>Heval_rhs normalize nodelta
514	whd in match (m_bind ?????);
515	\| 3: >(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta
516	whd in match (eval_expr ???????);
517	whd in match (eval_expr ???????);
518	>Heval_lhs normalize nodelta
519	]
520	whd in match (proj1 ???); whd in match (proj2 ???);
521	[ 2: (* standard int/int addition. *)
522	whd in match (eval_binop ???????);
523	whd in Hsem_binary:(??%?);
524	lapply (add_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
525	* #cm_val * #Hsem_binary_translated #Hvalue_eq_res
526	cases (sem_add_ii_inversion … Hsem_binary_translated)
527	#cm_vsz * #cm_lhs_v * #cm_rhs_v * *
528	#Hcm_lhs #Hcm_rhs #Hcm_val
529	destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
530	>intsize_eq_elim_true normalize nodelta
531	%{(Vint cm_vsz (addition_n (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))}
532	@conj try @refl lapply Hsem_binary_translated
533	whd in ⊢ ((??%?) → ?); normalize nodelta normalize in match (classify_add ??);
534	>inttyp_eq_elim_true' normalize nodelta
535	>intsize_eq_elim_true #H destruct (H) @Hvalue_eq_res
536	\| : ( pointer/int int/pointer addition *)
537	whd in Hsem_binary:(??%?);
538	lapply (add_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
539	* #cm_val * #Hsem_binary_translated #Hvalue_eq_res
540	(* >> *)
541	[ lapply (sem_add_pi_inversion … Hsem_binary_translated)
542	* #cm_vsz * #cm_rhs_v * #Hcm_rhs *
543	[ * #lhs_ptr * #Hcm_lhs_ptr #Hcm_val_shptr
544	\| * * #lhs_null #Hcm_rhs_zero #Hcm_val_null ]
545	\| lapply (sem_add_ip_inversion … Hsem_binary_translated)
546	* #cm_vsz * #cm_lhs_v * #Hcm_lhs *
547	[ * #rhs_ptr * #Hcm_rhs_ptr #Hcm_val_shptr
548	\| * * #rhs_null #Hcm_lhs_zero #Hcm_val_null ]
549	]
550	destruct
551	whd in match (eval_unop ????);
552	@(match sg
553	return λs. sg = s → ?
554	with
555	[ Unsigned ⇒ λHsg. ?
556	\| Signed ⇒ λHsg. ?
557	] (refl ??)) normalize nodelta
558	whd in match (eval_binop ???????);
559	whd in match (m_bind ?????);
560	[ 1: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr
561	(short_multiplication (bitsize_of_intsize I16)
562	(sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
563	(repr I16 (sizeof ty')))))}
564	\| 2: %{(Vptr (shift_pointer (bitsize_of_intsize I16) lhs_ptr
565	(short_multiplication (bitsize_of_intsize I16)
566	(zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
567	(repr I16 (sizeof ty')))))}
568	\| 5: %{(Vptr (shift_pointer (bitsize_of_intsize I16) rhs_ptr
569	(short_multiplication (bitsize_of_intsize I16)
570	(sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_lhs_v)
571	(repr I16 (sizeof ty')))))}
572	\| 6: %{(Vptr (shift_pointer (bitsize_of_intsize I16) rhs_ptr
573	(short_multiplication (bitsize_of_intsize I16)
574	(zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_lhs_v)
575	(repr I16 (sizeof ty')))))}
576	]
577	[ 1,2,3,4: @conj whd in match (E0);
578	whd in match (Eapp trace_rhs ?);
579	whd in match (Eapp trace_lhs ?);
580	>(append_nil … trace_rhs) try @refl
581	>(append_nil … trace_lhs) try @refl
582	@(value_eq_triangle_diagram … Hvalue_eq_res)
583	whd in match (shift_pointer_n ?????);
584	whd in match (shift_offset_n ?????);
585	>Hsg normalize nodelta
586	>commutative_short_multiplication
587	whd in match (shift_pointer ???);
588	whd in match (shift_offset ???);
589	>sign_ext_same_size @refl
590	\| 5,7: >(sign_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
591	\| 6,8: >(zero_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16)) ]
592	>(short_multiplication_zero 16 (repr I16 (sizeof ty')))
593	>(eq_bv_true … (zero 16)) normalize nodelta %{Vnull} @conj try assumption
594	normalize >append_nil try @refl
595	]
596	\| 2: (* subtraction cases: not quite identical to add. *)
597	lapply (classify_sub_inversion (typeof e1) (typeof e2))
598	* [ 2: #Hclassify >Hclassify normalize nodelta #lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
599	lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2 whd in match (typeof ?); #e'
600	* [ 1: * ]
601	[ 1: * #sz * #sg * *
602	\| 2: * #optlen * #ty' * #sz * #sg * *
603	\| 3: * #t1 * #t2 * #n1 * #n2 * * ]
604	whd in match (typeof ?) in ⊢ (% → % → ?);
605	#Htypeof_e1 #Htypeof_e2
606	>Htypeof_e1 >Htypeof_e2
607	#Hclassify
608	lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
609	normalize nodelta
610	whd in match (typeof ?) in ⊢ (% → % → %);
611	whd in match (typ_of_type (Tint ??));
612	#lhs #rhs
613	[ 1: #Htyp_should_eq cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
614	-Htyp_should_eq
615	\| 2: #Htyp_should_eq cases (typ_should_eq_inversion ASTptr (typ_of_type ty) … Htyp_should_eq)
616	-Htyp_should_eq
617	\| 3: #Haux cases (match_type_inversion_aux … Haux) #ty_sz * #ty_sg * -Haux
618	#Hty_eq #Heq_aux destruct (Hty_eq) lapply (jmeq_to_eq ??? Heq_aux) -Heq_aux
619	#Heq_e' destruct (Heq_e') ]
620	[ 1,2: #Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
621	<Heq_e' -Heq_e' \| ]
622	#Hexec
623	#Hexpr_vars_rhs #Hexpr_vars_lhs
624	#Htranslate_rhs #Htranslate_lhs
625	* [ #Hyp_present_lhs #Hyp_present_rhs
626	\| #Hyp_present_lhs * #Hyp_present_rhs #Hyp_present_cst
627	\| * #Hyp_present_lhs #Hyp_present_rhs #Hyp_present_cst ]
628	whd in match (typeof ?);
629	#Hind_rhs #Hind_lhs
630	cases (bind_inversion ????? Hexec) -Hexec
631	* #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
632	cases (bind_inversion ????? Hexec) -Hexec
633	* #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
634	cases (bind_inversion ????? Hexec) -Hexec
635	#val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
636	lapply (opt_to_res_inversion ???? Hsem) -Hsem
637	whd in match (typeof ?); whd in match (typeof ?);
638	#Hsem_binary
639	whd in match (eval_expr ???????);
640	whd in match (proj1 ???);
641	whd in match (eval_expr ???????);
642	whd in match (eval_expr ???????);
643	whd in match (proj1 ???);
644	[ 1: lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
645	\| 2,3: lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs) ]
646	* #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
647	[ 1,2: lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
648	\| 3: lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs) ]
649	* #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
650	[ 3: lapply (eval_expr_rewrite_aux … Heval_lhs) -Heval_lhs #Heval_lhs ]
651	[ 1,2: >Heval_lhs normalize nodelta
652	whd in match (eval_expr ???????);
653	whd in match (eval_expr ???????);
654	whd in match (proj2 ???);
655	[ >(eval_expr_rewrite_aux … Heval_rhs)
656	\| >Heval_rhs ]
657	whd in match (m_bind ?????);
658	normalize nodelta
659	\| 3: >(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta
660	whd in match (eval_expr ???????);
661	whd in match (proj2 ???);
662	whd in match (eval_expr ???????);
663	whd in match (proj1 ???);
664	whd in match (eval_expr ???????);
665	>Heval_rhs normalize nodelta
666	whd in match (eval_unop ????);
667	]
668	[ 1:
669	(* ptr/ptr sub *)
670	whd in Hsem_binary:(??%?);
671	lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
672	-Hsem_binary
673	* #cm_val * #Hsem_binary_translated #Hvalue_eq_res
674	lapply (sem_sub_pp_inversion … Hsem_binary_translated)
675	* #ty_sz' * #ty_sg' * #Heq destruct (Heq) *
676	[ (* regular pointers case *)
677	* #lhs_ptr * #rhs_ptr * #resulting_offset * * * *
678	#Hcm_lhs #Hcm_rhs #Hblocks_eq #Hoffset_eq #Hcm_val_eq
679	whd in match (eval_binop ???????);
680	>Hcm_lhs >Hcm_rhs normalize nodelta >Hblocks_eq >eq_block_b_b
681	normalize nodelta
682	whd in match (eval_expr ???????);
683	whd in match (m_bind ?????);
684	whd in match (eval_binop ???????);
685	normalize in match (bitsize_of_intsize ?);
686	normalize in match (S (7+pred_size_intsize I16*8)) in Hoffset_eq;
687	>Hoffset_eq
688	(* whd in match (pred_size_intsize ?); normalize in match (7+18); )
689	(* size mismatch between CL and CM. TODO *)
690	>Hoffset_eq normalize nodelta
691	whd in match (eval_unop ????);
692	%{cm_val} >Hcm_val_eq
693	whd in match (opt_to_res ???);
694	whd in match (m_bind ?????); @conj
695	[ 2: destruct assumption
696	\| 1: whd in match (zero_ext ? (Vint ??));
697	whd in match E0; whd in match (Eapp ? []); >append_nil
698	normalize in match (bitsize_of_intsize ?); try @refl ]
699	\| (* null pointers case *)
700	* * #Hcm_lhs #Hcm_rhs #Hcm_val destruct
701	whd in match (eval_binop ???????); normalize nodelta
702	whd in match (eval_expr ???????);
703	whd in match (m_bind ?????);
704	whd in match (eval_binop ???????); normalize nodelta
705	>division_u_zero normalize nodelta
706	whd in match (eval_unop ????);
707	whd in match (opt_to_res ???);
708	whd in match (m_bind ?????);
709	whd in match (pred_size_intsize ?);
710	%{(zero_ext ty_sz' (Vint I32 (zero (S (7+3*8)))))} @conj
711	[ whd in match (Eapp ??); whd in match E0; >append_nil try @refl ]
712	whd in Hsem_binary_translated:(??%?);
713	normalize nodelta in Hsem_binary_translated:(??%?);
714	lapply Hsem_binary_translated; -Hsem_binary_translated
715	cases n1 cases n2
716	[ \| 2,3: #n \| #n1 #n2 ] normalize nodelta
717	#Heq destruct (Heq)
718	whd in match (zero_ext ??);
719	cases ty_sz' in Hvalue_eq_res; try //
720	]
721	\| 2: (* int/int sub *)
722	whd in match (eval_binop ???????);
723	whd in Hsem_binary:(??%?);
724	lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
725	* #cm_val * #Hsem_binary_translated #Hvalue_eq_res
726	cases (sem_sub_ii_inversion … Hsem_binary_translated)
727	#cm_vsz * #cm_lhs_v * #cm_rhs_v * *
728	#Hcm_lhs #Hcm_rhs #Hcm_val
729	destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
730	>intsize_eq_elim_true normalize nodelta
731	%{(Vint cm_vsz (subtraction (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))}
732	@conj try @refl lapply Hsem_binary_translated
733	whd in ⊢ ((??%?) → ?); normalize nodelta whd in match (classify_sub ??);
734	>type_eq_dec_true normalize nodelta
735	>intsize_eq_elim_true #H destruct (H) @Hvalue_eq_res
736	\| 3: (* ptr/int sub *)
737	whd in Hsem_binary:(??%?);
738	lapply (sub_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary) -Hsem_binary
739	* #cm_val * #Hsem_binary_translated #Hvalue_eq_res
740	lapply (sem_sub_pi_inversion … Hsem_binary_translated) -Hsem_binary_translated
741	* #cm_vsz * #cm_rhs_v * #Hcm_rhs *
742	[ * #lhs_ptr * #Hcm_lhs_ptr #Hcm_val_shptr
743	\| * * #lhs_null #Hcm_rhs_zero #Hcm_val_null ]
744	whd in match (eval_unop ????);
745	-Heval_lhs -Heval_rhs destruct
746	whd in match (proj2 ???);
747	whd in match (proj1 ???);
748	whd in match (proj2 ???);
749	whd in match (eval_expr ???????);
750	@(match sg
751	return λs. sg = s → ?
752	with
753	[ Unsigned ⇒ λHsg. ?
754	\| Signed ⇒ λHsg. ?
755	] (refl ??)) normalize nodelta
756	whd in match (eval_unop ????);
757	whd in match (m_bind ?????);
758	whd in match (eval_binop ???????);
759	[ 1,2:
760	whd in match (neg_shift_pointer_n ?????) in Hvalue_eq_res;
761	whd in match (neg_shift_offset_n ?????) in Hvalue_eq_res;
762	whd in match (neg_shift_pointer ???);
763	whd in match (neg_shift_offset ???);
764	destruct (Hsg) normalize nodelta in Hvalue_eq_res;
765	[ >sign_ext_sign_ext_reduce
766	%{(Vptr
767	(mk_pointer (pblock lhs_ptr)
768	(mk_offset
769	(subtraction offset_size (offv (poff lhs_ptr))
770	(short_multiplication (bitsize_of_intsize I16)
771	(sign_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
772	(repr I16 (sizeof ty')))))))}
773	@conj
774	[ whd in match E0; whd in match (Eapp ? []); >append_nil try @refl
775	\| >commutative_short_multiplication @Hvalue_eq_res ]
776	\| >sign_ext_zero_ext_reduce
777	%{(Vptr
778	(mk_pointer (pblock lhs_ptr)
779	(mk_offset
780	(subtraction offset_size (offv (poff lhs_ptr))
781	(short_multiplication (bitsize_of_intsize I16)
782	(zero_ext (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16) cm_rhs_v)
783	(repr I16 (sizeof ty')))))))}
784	@conj
785	[ whd in match E0; whd in match (Eapp ? []); >append_nil try @refl
786	\| >commutative_short_multiplication @Hvalue_eq_res ]
787	]
788	]
789	[ >(sign_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
790	>(short_multiplication_zero 16 (repr I16 (sizeof ty')))
791	>(sign_ext_zero (bitsize_of_intsize I16) (bitsize_of_intsize I32))
792	\| >(zero_ext_zero (bitsize_of_intsize cm_vsz) (bitsize_of_intsize I16))
793	>(short_multiplication_zero 16 (repr I16 (sizeof ty')))
794	>(zero_ext_zero (bitsize_of_intsize I16) (bitsize_of_intsize I32)) ]
795	>(eq_bv_true … (zero 32)) normalize nodelta
796	%{Vnull} @conj try assumption
797	normalize >append_nil try @refl
798	]
799	\| 3: (* mul *)
800	lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
801	[ 2,4: #Hclassify >Hclassify normalize nodelta
802	#lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
803	lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
804	whd in match (typeof ?); #e'
805	* #sz * #sg * *
806	whd in match (typeof ?) in ⊢ (% → % → ?);
807	#Htypeof_e1 #Htypeof_e2
808	>Htypeof_e1 >Htypeof_e2
809	whd in match (typeof ?) in ⊢ (% → % → % → ?);
810	#Hclassify
811	lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
812	normalize nodelta
813	whd in match (typ_of_type (Tint ??));
814	#lhs #rhs #Htyp_should_eq
815	cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
816	-Htyp_should_eq
817	#Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
818	<Heq_e' -Heq_e'
819	#Hexec
820	#Hexpr_vars_rhs #Hexpr_vars_lhs
821	#Htranslate_rhs #Htranslate_lhs
822	* #Hyp_present_lhs #Hyp_present_rhs
823	#Hind_rhs #Hind_lhs
824	cases (bind_inversion ????? Hexec) -Hexec
825	* #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
826	cases (bind_inversion ????? Hexec) -Hexec
827	* #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
828	cases (bind_inversion ????? Hexec) -Hexec
829	#val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
830	lapply (opt_to_res_inversion ???? Hsem) -Hsem
831	whd in match (typeof ?); whd in match (typeof ?);
832	#Hsem_binary
833	lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
834	* #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
835	lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
836	* #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
837	whd in match (eval_expr ???????);
838	whd in match (proj1 ???);
839	>Heval_lhs normalize nodelta
840	>Heval_rhs normalize nodelta
841	whd in match (m_bind ?????);
842	whd in match (eval_binop ???????);
843	whd in Hsem_binary:(??%?);
844	lapply (mul_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
845	* #cm_val * #Hsem_binary_translated #Hvalue_eq_res
846	cases (sem_mul_inversion … Hsem_binary)
847	#cm_vsz * #cm_lhs_v * #cm_rhs_v * *
848	#Hcm_lhs #Hcm_rhs #Hcm_val
849	destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
850	>(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
851	>(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
852	>intsize_eq_elim_true normalize nodelta
853	%{(Vint cm_vsz (short_multiplication (bitsize_of_intsize cm_vsz) cm_lhs_v cm_rhs_v))}
854	@conj try @refl
855	whd in Hsem_binary:(??%?);
856	whd in match (classify_aop ??) in Hsem_binary:(??%?);
857	>type_eq_dec_true in Hsem_binary; normalize nodelta
858	>intsize_eq_elim_true #Heq destruct (Heq)
859	%2
860	\| 4,5: (* div *)
861	lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
862	[ 2,4: #Hclassify >Hclassify normalize nodelta
863	#lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
864	lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
865	whd in match (typeof ?); #e'
866	* #sz * * * *
867	whd in match (typeof ?) in ⊢ (% → % → ?);
868	#Htypeof_e1 #Htypeof_e2
869	>Htypeof_e1 >Htypeof_e2
870	whd in match (typeof ?) in ⊢ (% → % → % → ?);
871	#Hclassify
872	lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
873	normalize nodelta
874	whd in match (typ_of_type (Tint ??));
875	#lhs #rhs #Htyp_should_eq
876	[ 1,3: cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq)
877	\| 2,4: cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ]
878	-Htyp_should_eq
879	#Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
880	<Heq_e' -Heq_e'
881	#Hexec
882	#Hexpr_vars_rhs #Hexpr_vars_lhs
883	#Htranslate_rhs #Htranslate_lhs
884	* #Hyp_present_lhs #Hyp_present_rhs
885	#Hind_rhs #Hind_lhs
886	cases (bind_inversion ????? Hexec) -Hexec
887	* #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
888	cases (bind_inversion ????? Hexec) -Hexec
889	* #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
890	cases (bind_inversion ????? Hexec) -Hexec
891	#val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
892	lapply (opt_to_res_inversion ???? Hsem) -Hsem
893	whd in match (typeof ?); whd in match (typeof ?);
894	#Hsem_binary
895	lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
896	* #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
897	lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
898	* #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
899	whd in match (eval_expr ???????);
900	whd in match (proj1 ???);
901	>Heval_lhs normalize nodelta
902	>Heval_rhs normalize nodelta
903	whd in match (m_bind ?????);
904	whd in match (eval_binop ???????);
905	whd in Hsem_binary:(??%?);
906	[ 1,3: (* div*)
907	lapply (div_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
908	* #cm_val * #Hsem_binary_translated #Hvalue_eq_res
909	[ cases (sem_div_inversion_s … Hsem_binary)
910	\| cases (sem_div_inversion_u … Hsem_binary) ]
911	\| 2,4: (* mod *)
912	lapply (mod_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
913	* #cm_val * #Hsem_binary_translated #Hvalue_eq_res
914	[ cases (sem_mod_inversion_s … Hsem_binary)
915	\| cases (sem_mod_inversion_u … Hsem_binary) ]
916	]
917	#cm_vsz * #cm_lhs_v * #cm_rhs_v * *
918	#Hcm_lhs #Hcm_rhs #Hcm_val
919	destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
920	>(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
921	>(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
922	>intsize_eq_elim_true normalize nodelta
923	[ cases (division_s ???) in Hcm_val;
924	\| cases (division_u ???) in Hcm_val;
925	\| cases (modulus_s ???) in Hcm_val;
926	\| cases (modulus_u ???) in Hcm_val; ]
927	normalize nodelta
928	[ 1,3,5,7: @False_ind ]
929	#i #Hcl_val destruct (Hcl_val) %{(Vint cm_vsz i)} @conj try @refl %2
930	\| 6,7,8: (* and,or,xor *)
931	lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
932	[ 2,4,6: #Hclassify >Hclassify normalize nodelta
933	#lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
934	lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
935	whd in match (typeof ?); #e'
936	* #sz * #sg * *
937	whd in match (typeof ?) in ⊢ (% → % → ?);
938	#Htypeof_e1 #Htypeof_e2
939	>Htypeof_e1 >Htypeof_e2
940	whd in match (typeof ?) in ⊢ (% → % → % → ?);
941	#Hclassify
942	lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
943	normalize nodelta
944	whd in match (typ_of_type (Tint ??));
945	#lhs #rhs #Htyp_should_eq
946	cases (typ_should_eq_inversion (ASTint sz sg) (typ_of_type ty) … Htyp_should_eq)
947	-Htyp_should_eq
948	#Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
949	<Heq_e' -Heq_e'
950	#Hexec
951	#Hexpr_vars_rhs #Hexpr_vars_lhs
952	#Htranslate_rhs #Htranslate_lhs
953	* #Hyp_present_lhs #Hyp_present_rhs
954	#Hind_rhs #Hind_lhs
955	cases (bind_inversion ????? Hexec) -Hexec
956	* #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
957	cases (bind_inversion ????? Hexec) -Hexec
958	* #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
959	cases (bind_inversion ????? Hexec) -Hexec
960	#val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
961	lapply (opt_to_res_inversion ???? Hsem) -Hsem
962	whd in match (typeof ?); whd in match (typeof ?);
963	#Hsem_binary
964	lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
965	* #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
966	lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
967	* #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
968	whd in match (eval_expr ???????);
969	whd in match (proj1 ???);
970	>Heval_lhs normalize nodelta
971	>Heval_rhs normalize nodelta
972	whd in match (m_bind ?????);
973	whd in match (eval_binop ???????);
974	whd in Hsem_binary:(??%?);
975	[ 1: (* and *)
976	lapply (and_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
977	* #cm_val * #Hsem_binary_translated #Hvalue_eq_res
978	cases (sem_and_inversion … Hsem_binary)
979	\| 2: (* or *)
980	lapply (or_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
981	* #cm_val * #Hsem_binary_translated #Hvalue_eq_res
982	cases (sem_or_inversion … Hsem_binary)
983	\| 3: (* xor *)
984	lapply (xor_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
985	* #cm_val * #Hsem_binary_translated #Hvalue_eq_res
986	cases (sem_xor_inversion … Hsem_binary)
987	]
988	#cm_vsz * #cm_lhs_v * #cm_rhs_v * *
989	#Hcm_lhs #Hcm_rhs #Hcm_val
990	destruct (Hcm_lhs) destruct (Hcm_rhs) normalize nodelta
991	>(value_eq_int_inversion … Hvalue_eq_lhs) normalize nodelta
992	>(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
993	>intsize_eq_elim_true normalize nodelta
994	[ 1: %{(Vint cm_vsz (conjunction_bv … cm_lhs_v cm_rhs_v))}
995	\| 2: %{(Vint cm_vsz (inclusive_disjunction_bv … cm_lhs_v cm_rhs_v))}
996	\| 3: %{(Vint cm_vsz (exclusive_disjunction_bv … cm_lhs_v cm_rhs_v))}
997	]
998	@conj try @refl >Hcm_val %2
999	\| 9,10: (* shl, shr *)
1000	lapply (classify_aop_inversion (typeof e1) (typeof e2)) *
1001	[ 2,4: #Hclassify >Hclassify normalize nodelta
1002	#lhs #rhs whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
1003	lapply e' -e' cases e1 #ed1 #ety1 cases e2 #ed2 #ety2
1004	whd in match (typeof ?); #e'
1005	* #sz * * * *
1006	whd in match (typeof ?) in ⊢ (% → % → ?);
1007	#Htypeof_e1 #Htypeof_e2
1008	>Htypeof_e1 >Htypeof_e2
1009	whd in match (typeof ?) in ⊢ (% → % → % → ?);
1010	#Hclassify
1011	lapply (jmeq_to_eq ??? Hclassify) -Hclassify #Hclassify >Hclassify
1012	normalize nodelta
1013	whd in match (typ_of_type (Tint ??));
1014	#lhs #rhs #Htyp_should_eq
1015	[ 1,3: cases (typ_should_eq_inversion (ASTint sz Signed) (typ_of_type ty) … Htyp_should_eq)
1016	\| 2,4: cases (typ_should_eq_inversion (ASTint sz Unsigned) (typ_of_type ty) … Htyp_should_eq) ]
1017	-Htyp_should_eq
1018	#Heq_type <Heq_type in e'; #e' #Heq_e' lapply (jmeq_to_eq ??? Heq_e') -Heq_e' #Heq_e'
1019	<Heq_e' -Heq_e'
1020	#Hexec
1021	#Hexpr_vars_rhs #Hexpr_vars_lhs
1022	#Htranslate_rhs #Htranslate_lhs
1023	* #Hyp_present_lhs #Hyp_present_rhs
1024	#Hind_rhs #Hind_lhs
1025	cases (bind_inversion ????? Hexec) -Hexec
1026	* #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1027	cases (bind_inversion ????? Hexec) -Hexec
1028	* #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1029	cases (bind_inversion ????? Hexec) -Hexec
1030	#val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1031	lapply (opt_to_res_inversion ???? Hsem) -Hsem
1032	whd in match (typeof ?); whd in match (typeof ?);
1033	#Hsem_binary
1034	lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1035	* #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1036	lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1037	* #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1038	whd in match (eval_expr ???????);
1039	whd in match (proj1 ???);
1040	>Heval_lhs normalize nodelta
1041	>Heval_rhs normalize nodelta
1042	whd in match (m_bind ?????);
1043	whd in match (eval_binop ???????);
1044	whd in Hsem_binary:(??%?);
1045	[ 1,3: (* shl *)
1046	lapply (shl_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1047	* #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1048	cases (sem_shl_inversion … Hsem_binary)
1049	#sz1 * #sz2 * #lhs_i * #rhs_i * * *
1050	#Hcl_lhs #Hcl_rhs #Hcl_val #Hshift_ok
1051	destruct (Hcl_lhs Hcl_rhs)
1052	>(value_eq_int_inversion … Hvalue_eq_lhs)
1053	>(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1054	>Hshift_ok normalize nodelta
1055	%{(Vint sz1
1056	(shift_left bool (bitsize_of_intsize sz1)
1057	(nat_of_bitvector (bitsize_of_intsize sz2) rhs_i) lhs_i false))}
1058	@conj try @refl >Hcl_val %2
1059	\| : ( shr, translated to mod /!\ *)
1060	lapply (shr_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs … Hsem_binary)
1061	* #cm_val * #Hsem_binary_translated #Hvalue_eq_res
1062	cases (sem_shr_inversion … Hsem_binary) normalize nodelta
1063	#sz1 * #sz2 * #lhs_i * #rhs_i * * *
1064	#Hcl_lhs #Hcl_rhs #Hshift_ok #Hcl_val
1065	destruct (Hcl_lhs Hcl_rhs)
1066	>(value_eq_int_inversion … Hvalue_eq_lhs)
1067	>(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1068	>Hshift_ok normalize nodelta >Hcl_val
1069	/3 by ex_intro, conj, vint_eq/ ]
1070	\| : ( comparison operators *)
1071	lapply e' -e'
1072	cases e1 #ed1 #ety1
1073	cases e2 #ed2 #ety2
1074	whd in match (typeof ?) in ⊢ (% → % → % → %);
1075	#cm_expr whd in match (typeof ?);
1076	inversion (classify_cmp ety1 ety2)
1077	[ 3,6,9,12,15,18: #ety1' #ety2' #Hety1 #Hety2
1078	lapply (jmeq_to_eq ??? Hety1) #Hety1'
1079	lapply (jmeq_to_eq ??? Hety1) #Hety2'
1080	destruct #Hclassify >Hclassify normalize nodelta
1081	#cmexpr1 #cmexpr2
1082	whd in ⊢ ((???%) → ?);
1083	#Heq destruct (Heq)
1084	\| 1,4,7,10,13,16:
1085	#sz #sg #Hety1 #Hety2 #Hclassify
1086	lapply (jmeq_to_eq ??? Hety1) #Hety1'
1087	lapply (jmeq_to_eq ??? Hety1) #Hety2' destruct
1088	>(jmeq_to_eq ??? Hclassify) -Hclassify normalize nodelta
1089	whd in match (typeof ?) in ⊢ (% → % → % → %);
1090	whd in match (typ_of_type ?) in ⊢ (% → % → ?);
1091	cases sg #cmexpr1 #cmexpr2 normalize nodelta
1092	#Hcast_to_bool #Hexec_expr
1093	cases (complete_cmp_inversion … Hcast_to_bool) -Hcast_to_bool
1094	#tysz * #tysg * #Htyis_int #Hcm_expr_aux
1095	destruct (Htyis_int)
1096	lapply (jmeq_to_eq ??? Hcm_expr_aux) #Hcm_expr -Hcm_expr_aux
1097	destruct (Hcm_expr)
1098	cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1099	* #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1100	cases (bind_inversion ????? Hexec) -Hexec
1101	* #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1102	cases (bind_inversion ????? Hexec) -Hexec
1103	#val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1104	lapply (opt_to_res_inversion ???? Hsem) -Hsem
1105	whd in match (typeof ?); whd in match (sem_binary_operation ???????);
1106	normalize nodelta
1107	#Hsem_cmp cases (some_inversion ????? Hsem_cmp) -Hsem_cmp
1108	#cl_val' * #Hsem_cmp #Hcl_val_cast
1109	destruct (Hcl_val_cast)
1110	lapply (sem_cmp_int_inversion … Hsem_cmp) -Hsem_cmp
1111	* #vsz * #lhs_val * #rhs_val * * #Hcl_lhs #Hcl_rhs normalize nodelta
1112	destruct (Hcl_lhs) destruct (Hcl_rhs)
1113	#Heq_bool whd in match (typ_of_type ?) in ⊢ (% → % → % → %);
1114	#Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs
1115	* #Hyp_present_lhs #Hyp_present_rhs
1116	#Hind_rhs #Hind_lhs
1117	lapply (Hind_rhs … Hyp_present_rhs Hexec_rhs)
1118	* #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs
1119	lapply (Hind_lhs … Hyp_present_lhs Hexec_lhs)
1120	* #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs
1121	whd in match (eval_expr ???????);
1122	whd in match (eval_expr ???????);
1123	>Heval_lhs normalize nodelta
1124	>Heval_rhs normalize nodelta
1125	whd in match (m_bind ?????);
1126	whd in match (eval_binop ???????);
1127	>(value_eq_int_inversion … Hvalue_eq_lhs)
1128	>(value_eq_int_inversion … Hvalue_eq_rhs) normalize nodelta
1129	>intsize_eq_elim_true normalize nodelta
1130	destruct (Heq_bool)
1131	whd in match (eval_unop ????);
1132	whd in match (opt_to_res ???);
1133	whd in match (m_bind ?????);
1134	whd in match (of_bool ?);
1135	[ %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Ceq lhs_val rhs_val)))}
1136	\| %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Ceq lhs_val rhs_val)))}
1137	\| %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Cne lhs_val rhs_val)))}
1138	\| %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Cne lhs_val rhs_val)))}
1139	\| %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Clt lhs_val rhs_val)))}
1140	\| %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Clt lhs_val rhs_val)))}
1141	\| %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Cgt lhs_val rhs_val)))}
1142	\| %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Cgt lhs_val rhs_val)))}
1143	\| %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Cle lhs_val rhs_val)))}
1144	\| %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Cle lhs_val rhs_val)))}
1145	\| %{(zero_ext tysz (FE_of_bool (cmp_int (bitsize_of_intsize vsz) Cge lhs_val rhs_val)))}
1146	\| %{(zero_ext tysz (FE_of_bool (cmpu_int (bitsize_of_intsize vsz) Cge lhs_val rhs_val)))} ]
1147	@conj try @refl
1148	whd in match (FE_of_bool ?); whd in match FEtrue; whd in match FEfalse;
1149	[ 1,3,5,7,9,11:
1150	cases (cmp_int ????) normalize nodelta
1151	\| *:
1152	cases (cmpu_int ????) normalize nodelta ]
1153	try @value_eq_cl_cm_true
1154	try @value_eq_cl_cm_false
1155	\| : ( ptr comparison *)
1156	#n #ty' #Hety1 #Hety2 #Hclassify
1157	lapply (jmeq_to_eq ??? Hety1) #Hety1'
1158	lapply (jmeq_to_eq ??? Hety1) #Hety2' destruct
1159	>(jmeq_to_eq ??? Hclassify) -Hclassify normalize nodelta
1160	whd in match (typeof ?) in ⊢ (% → % → % → %);
1161	#cmexpr1 #cmexpr2
1162	#Hcast_to_bool #Hexec_expr
1163	cases (complete_cmp_inversion … Hcast_to_bool) -Hcast_to_bool
1164	#tysz * #tysg * #Htyis_int #Hcm_expr_aux
1165	destruct (Htyis_int)
1166	lapply (jmeq_to_eq ??? Hcm_expr_aux) #Hcm_expr -Hcm_expr_aux
1167	destruct (Hcm_expr)
1168	cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1169	* #cl_lhs #trace_lhs * #Hexec_lhs #Hexec
1170	cases (bind_inversion ????? Hexec) -Hexec
1171	* #cl_rhs #trace_rhs * #Hexec_rhs #Hexec
1172	cases (bind_inversion ????? Hexec) -Hexec
1173	#val_cl * #Hsem whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1174	lapply (opt_to_res_inversion ???? Hsem) -Hsem
1175	whd in match (typeof ?); whd in match (sem_binary_operation ???????);
1176	#Hsem_cmp
1177	cases (some_inversion ????? Hsem_cmp) -Hsem_cmp normalize nodelta
1178	#cl_val' * #Hsem_cmp #Hcl_val_cast destruct (Hcl_val_cast);
1179	#Hexpr_vars_rhs #Hexpr_vars_lhs #Htranslate_rhs #Htranslate_lhs
1180	* #Hyp_present_lhs #Hyp_present_rhs
1181	#Hind_rhs #Hind_lhs
1182	lapply (Hind_rhs … (expr_vars_fix_ptr_type … Hyp_present_rhs) Hexec_rhs)
1183	* #cm_rhs * #Heval_rhs #Hvalue_eq_rhs -Hind_rhs -Hexec_rhs
1184	lapply (Hind_lhs … (expr_vars_fix_ptr_type … Hyp_present_lhs) Hexec_lhs)
1185	* #cm_lhs * #Heval_lhs #Hvalue_eq_lhs -Hind_lhs -Hexec_lhs
1186	lapply (cmp_value_eq … Hvalue_eq_lhs Hvalue_eq_rhs Hinj … Hsem_cmp) -Hsem_cmp
1187	-Hvalue_eq_lhs -Hvalue_eq_rhs
1188	* #cm_val * #Hsem_cmp_cm #Hvalue_eq_res
1189	whd in match (eval_expr ???????);
1190	whd in match (eval_expr ???????);
1191	>(eval_expr_rewrite_aux … Heval_lhs) normalize nodelta
1192	>(eval_expr_rewrite_aux … Heval_rhs) normalize nodelta
1193	whd in match (m_bind ?????);
1194	lapply (sem_cmp_ptr_inversion … Hsem_cmp_cm) -Hsem_cmp_cm
1195	*
1196	[ 2,4,6,8,10,12:
1197	* * #Hcl_lhs #Hcl_rhs #Hsem_cmp
1198	whd in Hsem_cmp:(??%?); destruct
1199	\| :
1200	[ 2,4,6,8,10,12:
1201	* #p2 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp
1202	whd in Hsem_cmp:(??%?); destruct
1203	\| :
1204	[ 2,4,6,8,10,12:
1205	* #p1 * * #Hcl_lhs #Hcl_rhs #Hsem_cmp
1206	whd in Hsem_cmp:(??%?); destruct
1207	\| : #p1 * #p2 * * * * #Hcl_lhs #Hcl_rhs #Hvalid_p1 #Hvalid_p2 #Heq_block_outcome
1208	whd in Hsem_cmp:(??%?); destruct
1209	]
1210	]
1211	]
1212	whd in match (eval_binop ???????);
1213	normalize nodelta
1214	whd in match (eval_unop ????);
1215	whd in match (opt_to_res ???);
1216	whd in match (m_bind ?????);
1217	[ 1,2,3,4,5,6:
1218	[ 1,4,6:
1219	%{(zero_ext tysz FEtrue)} @conj try @refl
1220	>(value_eq_int_inversion' … Hvalue_eq_res) normalize nodelta
1221	@value_eq_cl_cm_true
1222	\| 2,3,5:
1223	%{(zero_ext tysz FEfalse)} @conj try @refl
1224	>(value_eq_int_inversion' … Hvalue_eq_res) normalize nodelta
1225	@value_eq_cl_cm_false
1226	]
1227	\| *: >Hvalid_p1 >Hvalid_p2 normalize nodelta
1228	lapply Heq_block_outcome -Heq_block_outcome
1229	@(eq_block_elim … (pblock p1) (pblock p2))
1230	normalize nodelta
1231	whd in match (eval_unop ????);
1232	whd in match (opt_to_res ???);
1233	whd in match (m_bind ?????);
1234	[ 1,3,5,7,9,11:
1235	#Hbocks_eq #Heq_cmp destruct (Heq_cmp)
1236	whd in match (eval_unop ????);
1237	whd in match (m_bind ?????);
1238	cases (cmp_offset ???) in Hvalue_eq_res; normalize nodelta
1239	#Hvalue_eq_res >(value_eq_int_inversion' … Hvalue_eq_res) normalize nodelta
1240	[ 1,3,5,7,9,11: %{(zero_ext tysz (FE_of_bool true))} @conj try @refl
1241	@value_eq_cl_cm_true
1242	\| 2,4,6,8,10,12: %{(zero_ext tysz (FE_of_bool false))} @conj try @refl
1243	@value_eq_cl_cm_false
1244	]
1245	\| *:
1246	#_ whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)
1247	>(value_eq_int_inversion' … Hvalue_eq_res) normalize nodelta
1248	[ %{(zero_ext tysz (FE_of_bool false))} @conj try @refl
1249	@value_eq_cl_cm_false
1250	\| %{(zero_ext tysz (FE_of_bool true))} @conj try @refl
1251	@value_eq_cl_cm_true
1252	]
1253	]
1254	]
1255	]
1256	]
1257	\| 1: (* Integer constant *)
1258	#csz #ty cases ty
1259	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
1260	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
1261	#i whd in match (typeof ?); #e' #Hexpr_vars #Htranslate
1262	#val #trace #Hpresent #Hexec_cl
1263	whd in Htranslate:(??%?);
1264	[ 1,3,4,5,6,7,8: destruct ]
1265	cases (intsize_eq_elim_dec csz sz (λsz0.λsz0'.res (Σe0':expr (typ_of_type (Tint sz0' sg)).expr_vars (typ_of_type (Tint sz0' sg)) e0' (local_id vars))))
1266	[ 2: * #H_err #H_neq_sz
1267	lapply (H_err (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
1268	>Htranslate #Habsurd destruct (Habsurd) ]
1269	* #H_ok #Heq_sz lapply (H_ok (OK ? «Cst (ASTint csz sg) (Ointconst csz sg i),I») (Error ? (msg TypeMismatch)))
1270	destruct (Heq_sz)
1271	>Htranslate -Htranslate -H_ok #Heq destruct (Heq)
1272	whd in Hexec_cl:(??%?); >eq_intsize_true in Hexec_cl; normalize nodelta
1273	#Heq destruct (Heq) %{(Vint sz i)} @conj try @refl //
1274	\| 2: *
1275	[ #sz #i \| #var_id \| * #ed1 #ty1 \| #e1 \| #op #e1 \| #op #e1 #e2 \| #cast_ty #e1
1276	\| #cond #iftrue #iffalse \| #e1 #e2 \| #e1 #e2 \| #sizeofty \| #e1 #field \| #cost #e1 ]
1277	try /2 by I/
1278	#ty whd in ⊢ (% → ?); #Hind
1279	whd in match (Plvalue ???);
1280	whd in match (typeof ?);
1281	#cm_expr #Hexpr_vars #Htranslate_expr #val #trace #Hyp_present #Hexec
1282	whd in Hexec:(??%?);
1283	whd in match (exec_lvalue' ?????) in Hexec:(??%?);
1284	cases (bind_inversion ????? Hexec) -Hexec * * #cl_b #cl_o #cl_t * #Hcl_success #Hcl_load_success
1285	whd in Hcl_success:(???%);
1286	[ 1: (* var case *)
1287	lapply Hcl_success -Hcl_success -Hind
1288	(* Peform case analysis on presence of variable in local Clight env.
1289	* if success, exec_expr/exec_lvalue tells us that it shoud be local. *)
1290	@(match lookup SymbolTag block cl_env var_id
1291	return λx.(lookup SymbolTag block cl_env var_id = x) → ?
1292	with
1293	[ None ⇒ λHcl_lookup. ?
1294	\| Some loc ⇒ λHcl_lookup. ?
1295	] (refl ? (lookup SymbolTag block cl_env var_id)))
1296	normalize nodelta
1297	[ 1: (* global case *)
1298	#Hlookup_global
1299	cases (bind_inversion ????? Hlookup_global) -Hlookup_global #global_block
1300	* #Hopt lapply (opt_to_res_inversion ???? Hopt) #Hfind_symbol
1301	#Heq whd in Heq:(???%); destruct (Heq)
1302	lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
1303	* #var_id_alloctype * #var_id_type * #Heq
1304	cases (variable_not_in_env_but_in_vartypes_is_global …
1305	Hexec_alloc Hcharacterise Hcl_lookup ?? Heq)
1306	#r #Heq' destruct (Heq') normalize nodelta
1307	lapply Hcl_load_success -Hcl_load_success
1308	lapply Hyp_present -Hyp_present
1309	lapply Hexpr_vars -Hexpr_vars
1310	lapply cm_expr -cm_expr inversion (access_mode ty)
1311	[ #typ_of_ty \| \| #typ_of_ty ]
1312	#Heq_typ_of_type #Heq_access_mode
1313	#cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success normalize nodelta
1314	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1315	whd in match (eval_expr ???????);
1316	whd in match (eval_expr ???????);
1317	whd in match (eval_constant ????);
1318	<(eq_sym … inv) >Hfind_symbol normalize nodelta
1319	cases (bind_inversion ????? Hcl_load_success) #x *
1320	#Hopt_to_res whd in ⊢ (???% → ?); #Heq_val destruct (Heq_val)
1321	lapply (opt_to_res_inversion ???? Hopt_to_res)
1322	#Hcl_load_success
1323	[ 2: %{(Vptr (mk_pointer cl_b (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
1324	@conj try @refl
1325	whd in Hcm_load_success:(??%?);
1326	lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq_ty
1327	>(load_value_of_type_by_ref … Hcl_load_success)
1328	try assumption %4
1329	lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
1330	>Hfind_symbol normalize nodelta #Heq_embedding
1331	whd in match (shift_offset ???);
1332	>addition_n_0 whd in match (pointer_translation ??); >Heq_embedding
1333	normalize nodelta @refl
1334	\| 1: cut (access_mode ty=By_value (typ_of_type ty))
1335	[ @jmeq_to_eq lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heqt
1336	lapply Heq_access_mode <Heqt // ] #Haccess
1337	lapply (load_by_value_success_valid_pointer … Haccess … Hcl_load_success)
1338	#Hvalid_ptr
1339	lapply (mi_inj … Hinj ?? cl_b zero_offset … Hvalid_ptr … Hcl_load_success)
1340	[ whd in ⊢ (??%?);
1341	lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
1342	>Hfind_symbol normalize nodelta #Heq_embedding >Heq_embedding @refl ]
1343	* #val' * #Hcm_load_success #Hvalue_eq
1344	lapply (load_value_of_type_by_value … Haccess … Hcm_load_success)
1345	#Hloadv lapply (jmeq_to_eq ??? Heq_typ_of_type) #Htypeq <Htypeq >Hloadv
1346	normalize %{val'} @conj try @refl assumption ]
1347	\| 2: (* local case *)
1348	#Heq destruct (Heq)
1349	lapply (bind2_eq_inversion ?????? Htranslate_expr) -Htranslate_expr
1350	* #var_id_alloc_type * #var_id_type *
1351	generalize in match var_id_alloc_type; * normalize nodelta
1352	[ 1: #r #Hlookup_vartype
1353	lapply (characterise_vars_lookup_local … Hcharacterise … Hcl_lookup … Hexec_alloc)
1354	* #typ whd in match (local_id ???);
1355	>Hlookup_vartype normalize nodelta @False_ind
1356	\| 2: (* Stack local *)
1357	lapply Hcl_load_success -Hcl_load_success
1358	lapply Hyp_present -Hyp_present
1359	lapply Hexpr_vars -Hexpr_vars
1360	lapply cm_expr -cm_expr inversion (access_mode ty)
1361	[ #typ_of_ty \| \| #typ_of_ty ]
1362	#Heq_typ_of_type #Heq_access_mode
1363	#cm_expr #Hexpr_vars #Hyp_present #Hcl_load_success
1364	#stack_depth #Hlookup_vartype_success normalize nodelta
1365	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1366	lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
1367	cases (res_inversion ?????? Hlookup_vartype_success) -Hlookup_vartype_success
1368	* #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
1369	>Hlookup' normalize nodelta #Hembedding_eq
1370	cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
1371	#loaded_val * #Hload_val
1372	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1373	lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
1374	#Hload_success whd in match (eval_expr ???????);
1375	cut (pointer_translation (mk_pointer cl_b zero_offset) E =
1376	Some ? (mk_pointer sp (mk_offset (repr I16 stack_depth))))
1377	[ 1,3: whd in ⊢ (??%?); >Hembedding_eq normalize nodelta
1378	>offset_plus_0 @refl ]
1379	#Hpointer_translation
1380	[ 2: (* By-ref *)
1381	whd in Hload_success:(??%?);
1382	lapply (load_value_of_type_by_ref … Hload_success … Heq_typ_of_type Heq_access_mode)
1383	#Heq_val
1384	>Heq_val
1385	%{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stack_depth))))}
1386	@conj try @refl
1387	%4 whd in match (shift_offset ???);
1388	whd in match zero_offset;
1389	>commutative_addition_n >addition_n_0 @Hpointer_translation
1390	\| 1: (* By value *)
1391	lapply (jmeq_to_eq ??? Heq_typ_of_type) #Heq0
1392	lapply (mi_inj … Hinj … Hpointer_translation … Hload_success)
1393	[ @(load_by_value_success_valid_pointer … Hload_success)
1394	lapply Heq_access_mode <Heq0 /2 by jmeq_to_eq/ ]
1395	* #cm_val * #Hload_in_cm #Hvalue_eq
1396	%{cm_val} @conj try assumption
1397	lapply (load_value_of_type_by_value … Hload_in_cm)
1398	[ lapply Heq_access_mode <Heq0 #Heq1
1399	@(jmeq_to_eq ??? Heq1) ]
1400	#Hloadv <Heq0
1401	whd in match (shift_offset ???); >commutative_addition_n >addition_n_0
1402	>Hloadv @refl ]
1403	\| 3: (* Register local variable *)
1404	#Hlookup_eq
1405	lapply (res_inversion ?????? Hlookup_eq)
1406	* * #var_id_alloc_type' #var_id_type' * #Hlookup' #Heq destruct (Heq)
1407	#Htype_eq
1408	cases (type_should_eq_inversion
1409	var_id_type
1410	ty
1411	(λt0:type.Σe':expr (typ_of_type t0).expr_vars (typ_of_type t0) e' (local_id vars))
1412	… Htype_eq) -Htype_eq
1413	(* Reverting all premises in order to perform type rewrite *)
1414	#Htype_eq
1415	lapply Hlookup' -Hlookup' lapply Hlookup_eq -Hlookup_eq
1416	lapply Hcl_load_success -Hcl_load_success
1417	lapply Hcl_lookup -Hcl_lookup
1418	lapply Hyp_present -Hyp_present
1419	lapply Hexpr_vars -Hexpr_vars
1420	lapply cm_expr
1421	destruct (Htype_eq)
1422	#cm_expr #Hexpr_vars #Hyp_present #Hcl_lookup #Hcl_load_success #Hlookup_eq #Hlookup'
1423	#Hexpr_eq lapply (jmeq_to_eq ??? Hexpr_eq) -Hexpr_eq #Hexpr_eq
1424	destruct (Hexpr_eq)
1425	whd in match (eval_expr ???????);
1426	whd in match (lookup_present ?????);
1427	lapply (Hlocal_matching var_id) >Hcl_lookup normalize nodelta
1428	>Hlookup' normalize nodelta #Hmatching
1429	cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
1430	#loaded_val * #Hload_val
1431	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1432	lapply (opt_to_res_inversion ???? Hload_val) -Hload_val
1433	#Hload_success
1434	cases (Hmatching … Hload_success) #val'
1435	* #Hlookup_in_cm #Hvalue_eq %{val'}
1436	cases Hyp_present
1437	>Hlookup_in_cm normalize nodelta #_ @conj try @refl try assumption
1438	(* seems ok *)
1439	]
1440	]
1441	\| 2: lapply Hcl_success -Hcl_success
1442	lapply Htranslate_expr -Htranslate_expr
1443	lapply Hind -Hind cases ty1
1444	[ \| #sz1 #sg1 \| #ptr_ty1 \| #array_ty1 #array_sz1 \| #domain1 #codomain1
1445	\| #structname1 #fieldspec1 \| #unionname1 #fieldspec1 \| #id1 ]
1446	#Hind #Htranslate_expr #Hexec_cl
1447	cases (bind_inversion ????? Htranslate_expr) (* -Htranslate_expr *)
1448	* whd in match (typ_of_type ?); normalize nodelta
1449	#cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind
1450	whd in ⊢ ((???%) → ?);
1451	[ 1,2,6,7: #Heq destruct (Heq) ]
1452	lapply (Hind cm_expr_ind Hexpr_vars_ind) -Hind
1453	whd in match (translate_addr ??); >Htranslate_expr_ind normalize nodelta
1454	#Hind lapply (Hind (refl ??) cl_b cl_o cl_t ?) -Hind
1455	[ 1,3,5,7: @(translate_expr_deref_present … Htranslate_expr … Hyp_present … Htranslate_expr_ind) ]
1456	whd in match (exec_lvalue' ?????); >Hexec_cl normalize nodelta
1457	cases (bind_inversion ????? Hexec_cl) * #cl_ptr #cl_trace0 *
1458	#Hexec_cl_ind #Hcl_ptr
1459	cut (∃ptr. cl_ptr = Vptr ptr)
1460	[ 1,3,5,7: cases cl_ptr in Hcl_ptr; normalize
1461	#H1 destruct #H2 destruct try /2 by ex_intro, refl/ #H3 destruct ]
1462	* * #cl_ptr_block #cl_ptr_off -Hcl_ptr
1463	#Hcl_ptr destruct (Hcl_ptr) normalize nodelta -Hexec_cl
1464	#Hind lapply (Hind (refl ??)) -Hind
1465	* #cm_ptr * #Hexec_cm_ind #Hvalue_eq_ind
1466	lapply (value_eq_ptr_inversion … Hvalue_eq_ind) * * #cm_ptr_block #cm_ptr_off * #Hcm_ptr
1467	destruct (Hcm_ptr) #Hpointer_translation
1468	cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success #cl_val * #Hopt_to_res
1469	whd in ⊢ ((???%) → ?); #Heq destruct (Heq) lapply (opt_to_res_inversion ???? Hopt_to_res)
1470	-Hopt_to_res
1471	lapply Hexec_cm_ind -Hexec_cm_ind
1472	lapply Hyp_present -Hyp_present
1473	lapply Htranslate_expr -Htranslate_expr
1474	lapply Hexpr_vars -Hexpr_vars
1475	lapply cm_expr -cm_expr
1476	cases ty (* Inversion (access_mode ty) fails for whatever reason. *)
1477	[ \| #sz2 #sg2 \| #ptr_ty2 \| #array_ty2 #array_sz2 \| #domain2 #codomain2 \| #structname2 #fieldspec2 \| #unionname2 #fieldspec2 \| #id2
1478	\| \| #sz2 #sg2 \| #ptr_ty2 \| #array_ty2 #array_sz2 \| #domain2 #codomain2 \| #structname2 #fieldspec2 \| #unionname2 #fieldspec2 \| #id2
1479	\| \| #sz2 #sg2 \| #ptr_ty2 \| #array_ty2 #array_sz2 \| #domain2 #codomain2 \| #structname2 #fieldspec2 \| #unionname2 #fieldspec2 \| #id2
1480	\| \| #sz2 #sg2 \| #ptr_ty2 \| #array_ty2 #array_sz2 \| #domain2 #codomain2 \| #structname2 #fieldspec2 \| #unionname2 #fieldspec2 \| #id2 ]
1481	whd in match (typ_of_type ?); whd in match (access_mode ?); normalize nodelta
1482	#cm_expr #Hexpr_vars #Htranslate_expr #Hyp_present #Hexec_cm_ind #Hcl_load_success
1483	#Heq destruct (Heq)
1484	[ 3,4,8,9,13,14,18,19: (* By reference *)
1485	>Hexec_cm_ind %{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
1486	lapply (load_value_of_type_by_ref … Hcl_load_success ??)
1487	try @refl_jmeq
1488	#Hval >Hval %4 assumption
1489	\| : ( By_value *)
1490	(* project Hcl_load_success in Cminor through memory_inj *)
1491	lapply (mi_inj ??? Hinj cl_b cl_o cm_ptr_block cm_ptr_off … Hpointer_translation … Hcl_load_success)
1492	try @(load_by_value_success_valid_pointer … Hcl_load_success)
1493	try @jmeq_to_eq
1494	try assumption try @refl_jmeq
1495	* #cm_val * #Hcm_load_success #Hvalue_eq
1496	lapply (load_value_of_type_by_value … Hcm_load_success)
1497	try @refl
1498	#Hloadv_cm
1499	whd in match (eval_expr ???????); >Hexec_cm_ind normalize nodelta
1500	>Hloadv_cm normalize %{cm_val} @conj try @refl assumption ]
1501	\| 3: lapply Hcl_load_success -Hcl_load_success lapply Hcl_success -Hcl_success
1502	lapply (refl ? (typeof e1))
1503	cases (typeof e1) in ⊢ ((???%) → %);
1504	[ \| #sz1 #sg1 \| #ptr_ty1 \| #array_ty1 #array_sz1 \| #domain1 #codomain1
1505	\| #structname1 #fieldspec1 \| #unionname1 #fieldspec1 \| #id1 ] normalize nodelta
1506	#Heq_typeof normalize nodelta
1507	[ 1,2,3,4,5,8: #Habsurd destruct ] #Hexec_cl #Hcl_load_success
1508	whd in Htranslate_expr:(??%?); >Heq_typeof in Htranslate_expr;
1509	normalize nodelta #Htranslate_expr
1510	cases (bind_inversion ????? Htranslate_expr) -Htranslate_expr
1511	* whd in match (typ_of_type ?); normalize nodelta
1512	#cm_expr_ind #Hexpr_vars_ind * #Htranslate_expr_ind #Htranslate_expr2
1513	[ cases (bind_inversion ????? Htranslate_expr2) -Htranslate_expr2
1514	#cm_field_off * #Hcm_field_off
1515	\| lapply Htranslate_expr2 -Htranslate_expr2 ]
1516	cases (bind_inversion ????? Hexec_cl) -Hexec_cl
1517	* * #block_cl #offset_cl #trace0 * #Hexec_lvalue #Hexec_cl
1518	whd in Hexec_lvalue:(???%);
1519	[ cases (bind_inversion ????? Hexec_cl) -Hexec_cl
1520	#cl_field_off * #Hcl_field_off #Hoffset_eq ]
1521	cases (bind_inversion ????? Hcl_load_success) -Hcl_load_success
1522	#cl_val * #Hopt_cl_val whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1523	lapply (opt_to_res_inversion ???? Hopt_cl_val) -Hopt_cl_val #Hcl_load_value
1524	[ (* Struct case *)
1525	lapply Hcl_load_value -Hcl_load_value
1526	lapply Hyp_present -Hyp_present
1527	lapply Hexpr_vars -Hexpr_vars
1528	lapply cm_expr -cm_expr
1529	lapply Hind -Hind
1530	cases ty
1531	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
1532	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
1533	#Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
1534	normalize nodelta
1535	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1536	whd in match (eval_expr ???????);
1537	(* applying the arguments of the induction hypothesis progressively *)
1538	lapply (Hind (Op2 ASTptr (ASTint I16 Signed) ASTptr (Oaddpi I16) cm_expr_ind
1539	(Cst (ASTint I16 Signed) (Ointconst I16 Signed (repr I16 cm_field_off)))) ?)
1540	[ 1,3,5,7,9: whd @conj try assumption whd @I ] -Hind #Hind
1541	lapply (Hind ?)
1542	[ 1,3,5,7,9:
1543	whd in ⊢ (??%?); >Heq_typeof normalize nodelta
1544	>Htranslate_expr_ind whd in match (m_bind ?????);
1545	>Hcm_field_off normalize nodelta @refl ] -Hind #Hind
1546	whd in Hoffset_eq:(???%); destruct (offset_eq)
1547	cut (cl_field_off = cm_field_off)
1548	[ 1,3,5,7,9: lapply Hcl_field_off >Hcm_field_off
1549	normalize #Heq destruct (Heq) @refl ]
1550	#Heq destruct (Heq)
1551	lapply (Hind cl_b cl_o trace ?)
1552	[ 1,3,5,7,9: @Hyp_present ] -Hind #Hind
1553	lapply (Hind ?) -Hind
1554	[ 1,3,5,7,9: whd in ⊢ (??%?); >Heq_typeof normalize nodelta
1555	>Hexec_lvalue whd in match (m_bind ?????); >Hcm_field_off normalize nodelta
1556	@Hoffset_eq ]
1557	* #cm_val' * #Heval_expr #Hvalue_eq
1558	lapply (value_eq_ptr_inversion … Hvalue_eq) * * #cm_ptr_block #cm_ptr_off
1559	* #Heq_cm_val_ptr destruct (Heq_cm_val_ptr) #Hpointer_trans
1560	[ 1,2,5: (* by-value *)
1561	lapply (mi_inj … Hinj cl_b cl_o ?? … Hpointer_trans … Hcl_load_value)
1562	[ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
1563	* #cm_val * #Hcm_load_value #Hvalue_eq
1564	lapply (load_value_of_type_by_value … Hcm_load_value)
1565	[ 1,3,5: @refl ]
1566	#Hcm_loadv %{cm_val} >Heval_expr normalize nodelta >Hcm_loadv normalize @conj
1567	try @refl try assumption
1568	\| 3,4: (* by-ref *)
1569	whd in match (eval_expr ???????) in Heval_expr; >Heval_expr
1570	%{(Vptr (mk_pointer cm_ptr_block cm_ptr_off))} @conj try @refl
1571	whd in Hcl_load_value:(??%?); destruct (Hcl_load_value) assumption
1572	]
1573	\| (* union case *)
1574	lapply Hcl_load_value -Hcl_load_value
1575	lapply Hyp_present -Hyp_present
1576	lapply Hexpr_vars -Hexpr_vars
1577	lapply cm_expr -cm_expr
1578	lapply Hind -Hind
1579	cases ty
1580	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
1581	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
1582	whd in match (typ_of_type ?); normalize nodelta
1583	#Hind #cm_expr #Hexpr_vars #Hyp_present #Hcl_load_value
1584	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1585	[ 1,2,5: (* by-value *)
1586	whd in match (eval_expr ???????);
1587	lapply (Hind cm_expr_ind Hexpr_vars ?)
1588	[ 1,3,5: whd in ⊢ (??%?); >Heq_typeof normalize nodelta @Htranslate_expr_ind ]
1589	whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
1590	-Hind #Hind
1591	lapply (Hind block_cl offset_cl trace0 Hyp_present) -Hind >Hexec_lvalue normalize nodelta
1592	whd in match (m_bind ?????); #Hind
1593	cases (Hind (refl ??)) -Hind
1594	#cm_val * #Heval_expr #Hvalue_eq >Heval_expr normalize nodelta
1595	cases (value_eq_ptr_inversion … Hvalue_eq) * #cm_block #cm_offset * #Hcm_val #Hpointer_trans
1596	destruct (Hcm_val) whd in Hexec_cl:(???%); destruct (Hexec_cl)
1597	lapply (mi_inj … Hinj cl_b cl_o cm_block cm_offset … Hpointer_trans … Hcl_load_value)
1598	[ 1,3,5: @(load_by_value_success_valid_pointer … Hcl_load_value) // ]
1599	* #cm_val * #Hcm_load_value #Hvalue_eq
1600	lapply (load_value_of_type_by_value … Hcm_load_value)
1601	[ 1,3,5: @refl ]
1602	#Hcm_loadv %{cm_val} >Hcm_loadv normalize @conj
1603	try @refl assumption
1604	\| 3,4:
1605	whd in Hexec_cl:(???%); destruct (Hexec_cl)
1606	lapply (Hind cm_expr Hexpr_vars)
1607	whd in match (translate_addr ??); >Heq_typeof normalize nodelta -Hind #Hind
1608	lapply (Hind Htranslate_expr_ind) -Hind
1609	whd in match (exec_lvalue' ?????); >Heq_typeof normalize nodelta
1610	>Hexec_lvalue whd in match (m_bind ?????);
1611	#Hind cases (Hind … Hyp_present (refl ??))
1612	#cm_val * #Heval_expr #Hvalue_eq >Heval_expr %{cm_val} @conj
1613	try @refl whd in Hcl_load_value:(??%?); destruct (Hcl_load_value)
1614	assumption ]
1615	]
1616	]
1617	\| 3: #var #ty #cmexpr #Hexpr_vars #Htranslate_var #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue_var
1618	whd in Hexec_lvalue_var:(??%?);
1619	(* check whether var is local or global *)
1620	lapply (Hlocal_matching var)
1621	lapply (variable_not_in_env_but_in_vartypes_is_global … var Hexec_alloc … Hcharacterise)
1622	cases (lookup ?? cl_env var) in Hexec_lvalue_var;
1623	normalize nodelta
1624	[ 1: (* global *)
1625	#Hexec_opt #H lapply (H (refl ??)) -H #Hvar_is_global
1626	cases (bind_inversion ????? Hexec_opt) -Hexec_opt #varblock * #Hopt_to_res #Heq
1627	whd in Heq:(???%) Hopt_to_res:(???%); destruct (Heq)
1628	lapply (opt_to_res_inversion ???? Hopt_to_res) -Hopt_to_res #Hfind_symbol >Hfind_symbol normalize nodelta
1629	#Hembed
1630	cases (bind_inversion ????? Htranslate_var) -Htranslate_var
1631	* #var_alloctype #var_type * #Hlookup_vartype #Hvar_alloctype
1632	cases (Hvar_is_global … Hlookup_vartype) #r #Halloctype >Halloctype in Hvar_alloctype;
1633	normalize nodelta whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1634	whd in match (eval_expr ???????);
1635	whd in match (eval_constant ????);
1636	<(eq_sym inv var) >Hfind_symbol normalize nodelta
1637	%{(Vptr (mk_pointer cl_blo (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 O))))}
1638	@conj try @refl %4 whd in match (pointer_translation ??);
1639	>Hembed normalize nodelta whd in match (shift_offset ???);
1640	>addition_n_0 @refl
1641	\| 2: (* local *)
1642	#BL #Heq destruct (Heq) #_
1643	@(match (lookup ?? vars var)
1644	return λx. (lookup ?? vars var = x) → ?
1645	with
1646	[ None ⇒ ?
1647	\| Some kind ⇒ ?
1648	] (refl ??))
1649	normalize nodelta
1650	#Hlookup [ @False_ind ]
1651	cases kind in Hlookup; #var_alloctype #var_type normalize nodelta
1652	#Hlookup
1653	lapply (refl ? var_alloctype)
1654	cases var_alloctype in ⊢ ((???%) → %); normalize nodelta
1655	[ #reg #Heq @False_ind \| #stacksize #Hvar_alloc #Hembed \| #Hvar_alloc #Hlookup' ]
1656	[ (* stack alloc*)
1657	cases (bind_inversion ????? Htranslate_var) -Htranslate_var
1658	* #var_alloctype' #var_type' * #Hlookup_vartype'
1659	whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
1660	whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
1661	whd in ⊢ ((???%) → ?); #Heq destruct (Heq) whd in match (eval_expr ???????);
1662	%{(Vptr (mk_pointer sp (shift_offset (bitsize_of_intsize I16) zero_offset (repr I16 stacksize))))}
1663	@conj try @refl %4 whd in match (pointer_translation ??);
1664	>Hembed @refl
1665	\| (* local alloc *)
1666	cases (bind_inversion ????? Htranslate_var) -Htranslate_var
1667	* #var_alloctype' #var_type' * #Hlookup_vartype'
1668	whd in Hlookup_vartype':(??%?); >Hlookup in Hlookup_vartype'; normalize nodelta
1669	whd in ⊢ ((???%) → ?); #Heq destruct (Heq) >Hvar_alloc normalize nodelta
1670	whd in ⊢ ((???%) → ?); #Heq destruct (Heq) ] ]
1671	(\| 4: #e #ty)
1672	\| 4:
1673	* #ed #ety cases ety
1674	[ \| #sz1 #sg1 \| #ptr_ty1 \| #array_ty1 #array_sz1 \| #domain1 #codomain1
1675	\| #structname1 #fieldspec1 \| #unionname1 #fieldspec1 \| #id1 ] normalize nodelta
1676	whd in match (typeof ?);
1677	#ty #Hind #e' #Hexpr_vars #Htranslate #cl_blo #cl_off #trace #Hyp_present #Hexec_lvalue
1678	cases (bind_inversion ????? Htranslate) -Htranslate
1679	* #cm_expr #Hexpr_vars_cm * #Htranslate_ind
1680	cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
1681	* #cl_val #trace0 * #Hexec_expr #Hcl_val
1682	whd in match (typeof ?); whd in match (typ_of_type ?); normalize nodelta
1683	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1684	cut (cl_val = Vptr (mk_pointer cl_blo cl_off) ∧ trace = trace0)
1685	[ 1,3,5,7: cases cl_val in Hcl_val; normalize
1686	[ 1,5,9,13: #Heq destruct (Heq)
1687	\| 2,6,10,14: #sz #vec #Heq destruct (Heq)
1688	\| 3,7,11,15: #Heq destruct (Heq)
1689	\| 4,8,12,16: * #BL #OFF #Heq destruct (Heq) @conj try @refl ] ]
1690	* #Heq_cl_val destruct (Heq_cl_val) #Htrace_eq destruct (Htrace_eq)
1691	cases (Hind e' Hexpr_vars Htranslate_ind … Hyp_present … Hexec_expr)
1692	#cm_val * #Heval_expr_cm #Hvalue_eq >Heval_expr_cm
1693	%{cm_val} @conj try @refl try assumption
1694	\| 5:
1695	#ty cases ty
1696	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
1697	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
1698	#ed #ty' #Hind
1699	whd in match (typeof ?); whd in match (typ_of_type ?); #cm_expr
1700	#Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
1701	cases (bind_inversion ????? Htranslate) -Htranslate
1702	* #cm_expr #Hexpr_vars_cm * #Htranslate_ind
1703	cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1704	* * #cl_blo #cl_off #trace0 * #Hexec_lvalue normalize nodelta
1705	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1706	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1707	cases (Hind cm_expr Hexpr_vars Htranslate_ind ??? Hyp_present Hexec_lvalue)
1708	#cm_val * #Hexec_cm #Hvalue_eq >Hexec_cm
1709	%{cm_val} @conj try @refl assumption
1710	\| 6:
1711	#ty *
1712	[ cases ty
1713	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
1714	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
1715	#e #Hind
1716	whd in match (typeof ?);
1717	#e' whd in match (typ_of_type ?); #Hexpr_vars whd in ⊢ ((??%?) → ?);
1718	#Htranslate
1719	[ 3,4,5,8: destruct (Htranslate)
1720	\| 2: lapply Htranslate -Htranslate lapply Hexpr_vars -Hexpr_vars lapply e' -e'
1721	cases sz normalize nodelta
1722	#e' #Hexpr_vars #Htranslate
1723	[ 1, 2: destruct (Htranslate) ] ]
1724	#cl_val #trace #Hyp_present #Hexec_expr
1725	cases (bind_inversion ????? Htranslate) -Htranslate
1726	#cmop * #Htranslate_unop #Hexec_arg
1727	cases (bind_inversion ????? Hexec_arg) -Hexec_arg
1728	* #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1729	cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1730	* #cl_arg #cl_trace * #Hexec_cl
1731	whd in ⊢ ((???%) → ?); #Hexec_unop
1732	cases (bind_inversion ????? Hexec_unop) -Hexec_unop
1733	#v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1734	lapply (opt_to_res_inversion ???? Hopt) -Hopt
1735	#Hsem_cl whd in match (eval_expr ???????);
1736	cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
1737	#cm_val * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
1738	lapply (unary_operation_value_eq … Hvalue_eq … Hsem_cl)
1739	* #cl_val' * #Hcl_unop #Hvalue_eq %{cl_val'} @conj try assumption
1740	whd in match (typ_of_type Tvoid);
1741	lapply (translate_notbool_to_cminor … Htranslate_unop … Hcl_unop)
1742	#H >H @refl
1743	\| *:
1744	cases ty
1745	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain \| #structname #fieldspec \| #unionname #fieldspec \| #id
1746	\| \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain \| #structname #fieldspec \| #unionname #fieldspec \| #id ]
1747	#e #Hind whd in match (typeof ?); whd in match (typ_of_type ?);
1748	#e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec
1749	whd in Htranslate:(??%?);
1750	[ 3,4,5,8,11,12,13,16: destruct (Htranslate) ]
1751	cases (bind_inversion ????? Htranslate) -Htranslate
1752	#cmop * #Htranslate_unop #Hexec_arg
1753	cases (bind_inversion ????? Hexec_arg) -Hexec_arg
1754	* #cm_arg #Hexpr_vars_arg * #Htranslate whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1755	cases (bind_inversion ????? Hexec) -Hexec
1756	* #cl_arg #cl_trace * #Hexec_cl
1757	whd in ⊢ ((???%) → ?); #Hexec_unop
1758	cases (bind_inversion ????? Hexec_unop) -Hexec_unop
1759	#v * #Hopt whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1760	lapply (opt_to_res_inversion ???? Hopt) -Hopt
1761	#Hcl_unop whd in match (eval_expr ???????);
1762	cases (Hind cm_arg Hexpr_vars Htranslate … Hyp_present Hexec_cl)
1763	#op_arg * #Heval_cm #Hvalue_eq >Heval_cm normalize nodelta
1764	lapply (unary_operation_value_eq … Hvalue_eq … Hcl_unop)
1765	* #op_res * #Hcl_sem #Hvalue_eq
1766	[ 1,2,3,4: >(translate_notint_to_cminor … Htranslate_unop … Hcl_sem)
1767	%{op_res} @conj try @refl assumption
1768	\| 5,6,7,8: >(translate_negint_to_cminor … Htranslate_unop … Hcl_sem)
1769	%{op_res} @conj try @refl assumption
1770	]
1771	]
1772	\| 8: #ty #ty' * #ed #ety
1773	cases ety
1774	[ \| #esz #esg \| #eptr_ty \| #earray_ty #earray_sz \| #edomain #ecodomain
1775	\| #estructname #efieldspec \| #eunionname #efieldspec \| #eid ]
1776	whd in match (typeof ?); whd in match (typ_of_type ?);
1777	#Hind whd in match (typeof ?);
1778	#cm_expr #Hexpr_vars #Htranslate
1779	cases (bind_inversion ????? Htranslate) -Htranslate
1780	* #cm_castee #Hexpr_vars_castee * #Htranslate_expr #Htranslate
1781	cases (bind_inversion ????? Htranslate) -Htranslate
1782	* #cm_cast #Hexpr_vars_cast * #Htranslate_cast #Htranslate
1783	[ 1,5,6,7,8: whd in Htranslate_cast:(??%%); destruct (Htranslate_cast) ]
1784	cases (bind_inversion ????? Htranslate) -Htranslate
1785	* #cm_cast' #Hexpr_vars' * #Htyp_should_eq whd in ⊢ ((??%%) → ?);
1786	#Heq destruct (Heq)
1787	#cl_val #trace #Hyp_present #Hexec_cm
1788	cases (bind_inversion ????? Hexec_cm) -Hexec_cm
1789	* #cm_val #trace0 * #Hexec_cm #Hexec_cast
1790	cases (bind_inversion ????? Hexec_cast) -Hexec_cast
1791	#cast_val * #Hexec_cast
1792	whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1793	cases (typ_should_eq_inversion (typ_of_type ty') (typ_of_type ty) … Htyp_should_eq) -Htyp_should_eq
1794	#Htype_eq
1795	lapply Hexec_cast -Hexec_cast
1796	(* lapply Htyp_should_eq -Htyp_should_eq *)
1797	lapply Htranslate_cast -Htranslate_cast
1798	lapply Hexpr_vars_cast -Hexpr_vars_cast
1799	lapply cm_cast -cm_cast
1800	lapply Hyp_present -Hyp_present
1801	lapply Hexpr_vars -Hexpr_vars
1802	lapply cm_expr -cm_expr
1803	<Htype_eq -Htype_eq
1804	whd in ⊢ (? → ? → ? → ? → ? → ? → (??%%) → ?);
1805	whd in match (typeof ?); normalize nodelta
1806	cases ty'
1807	[ \| #sz' #sg' \| #ptr_ty' \| #array_ty' #array_sz' \| #domain' #codomain' \| #structname' #fieldspec' \| #unionname' #fieldspec' \| #id'
1808	\| \| #sz' #sg' \| #ptr_ty' \| #array_ty' #array_sz' \| #domain' #codomain' \| #structname' #fieldspec' \| #unionname' #fieldspec' \| #id'
1809	\| \| #sz' #sg' \| #ptr_ty' \| #array_ty' #array_sz' \| #domain' #codomain' \| #structname' #fieldspec' \| #unionname' #fieldspec' \| #id' ]
1810	#cm_expr #Hexpr_vars #Hyp_present #cm_cast #Hexpr_vars_cast #Htranslate_cast normalize nodelta #Hexec_cast
1811	#Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
1812	whd in Htranslate_cast:(??%%);
1813	whd in Hexpr_vars;
1814	destruct (Htranslate_cast)
1815	[ 1,2,3,4,7:
1816	lapply (Hind cm_castee Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
1817	* #cm_val' * #Heval_castee
1818	lapply Hexec_cm -Hexec_cm
1819	whd in Hexec_cast:(??%%);
1820	cases cm_val in Hexec_cast; normalize nodelta
1821	[ \| #vsz #vi \| \| #vp
1822	\| \| #vsz #vi \| \| #vp
1823	\| \| #vsz #vi \| \| #vp
1824	\| \| #vsz #vi \| \| #vp
1825	\| \| #vsz #vi \| \| #vp ]
1826	[ 2,6,10,14,18:
1827	\| *: #Habsurd destruct (Habsurd) ]
1828	#Hexec_cast #Hexec_cm #Hvalue_eq
1829	[ 1,2,3:
1830	cases (intsize_eq_elim_inversion ??????? Hexec_cast) -Hexec_cast
1831	#Hsz_eq destruct (Hsz_eq) #Hcl_val_eq ]
1832	[ 2,3: lapply (sym_eq ??? Hcl_val_eq) -Hcl_val_eq #Hexec_cast ]
1833	[ 1,2,4,5:
1834	cases (bind_inversion ????? Hexec_cast)
1835	whd in match (typeof ?);
1836	#cast_val * whd in ⊢ ((??%%) → ?); normalize nodelta
1837	whd in match (eq_rect_r ??????);
1838	[ 3,4: cases (eq_bv ???) normalize nodelta #Heq destruct (Heq) ]
1839	@(eq_bv_elim … vi (zero (bitsize_of_intsize esz))) normalize nodelta
1840	[ 2,4: #foo #Habsurd destruct (Habsurd) ]
1841	#Heq_vi >eq_intsize_true normalize nodelta #Heq destruct (Heq)
1842	whd in ⊢ ((??%%) → ?); #Heq destruct (Heq)
1843	whd in match (typ_of_type ?); whd in match (eval_expr ???????);
1844	>Heval_castee normalize nodelta whd in match (eval_unop ????);
1845	>(value_eq_int_inversion … Hvalue_eq) normalize nodelta
1846	>Heq_vi >eq_bv_true normalize
1847	%{Vnull} @conj try @refl %3
1848	\| 3: destruct (Hcl_val_eq)
1849	whd in match (eval_expr ???????);
1850	>Heval_castee normalize nodelta
1851	whd in match (eval_unop ????);
1852	cases esg normalize nodelta
1853	whd in match (opt_to_res ???); whd in match (m_bind ?????);
1854	[ %{(sign_ext sz' cm_val')} \| %{(zero_ext sz' cm_val')} ] @conj try @refl
1855	whd in match (eq_rect_r ??????);
1856	-Hexpr_vars -Hyp_present -Hind -Hexec_cm -cm_castee
1857	(* cast_int_int is defined as a let rec on its first argument, we have to eliminate esz for
1858	this reason. *)
1859	lapply Hvalue_eq -Hvalue_eq lapply vi -vi
1860	cases esz normalize nodelta
1861	#vi #Hvalue_eq >(value_eq_int_inversion … Hvalue_eq)
1862	whd in match (sign_ext ??); whd in match (zero_ext ??);
1863	%2
1864	]
1865	\| *:
1866	lapply (Hind cm_expr Hexpr_vars Htranslate_expr … Hyp_present Hexec_cm)
1867	* #cm_val' * #Heval_expr #Hvalue_eq >Heval_expr
1868	%{cm_val'} @conj try @refl
1869	lapply Hexec_cast -Hexec_cast lapply Hvalue_eq -Hvalue_eq
1870	-Hind -Hexpr_vars -Hyp_present lapply Hexec_cm -Hexec_cm
1871	cases cm_val
1872	[ \| #vsz #vi \| \| #vp
1873	\| \| #vsz #vi \| \| #vp
1874	\| \| #vsz #vi \| \| #vp
1875	\| \| #vsz #vi \| \| #vp ]
1876	#Hexec_cm #Hvalue_eq #Hexec_cast
1877	whd in Hexec_cast:(??%%);
1878	[ 1,5,9,13: destruct (Hexec_cast) ]
1879	[ 2,3,5,6,8,9,11,12: destruct (Hexec_cast) try assumption ]
1880	lapply Hexec_cast -Hexec_cast
1881	normalize cases (eq_v ?????) normalize
1882	#Habsurd destruct (Habsurd)
1883	]
1884	\| 9: (* Econdition *)
1885	#ty #e1 #e2 #e3 #Hind1 #Hind2 #Hind3 whd in match (typeof ?);
1886	#cm_expr #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present
1887	#Hexec_cm
1888	cases (bind_inversion ????? Hexec_cm) -Hexec_cm
1889	* #cm_cond_val #trace_cond0 * #Hexec_cond #Hexec_cm
1890	cases (bind_inversion ????? Hexec_cm) -Hexec_cm
1891	#bool_of_cm_cond_val * #Hexec_bool_of_val #Hexec_cm
1892	cases (bind_inversion ????? Hexec_cm) -Hexec_cm
1893	* #cm_ifthenelse_val #cm_ifthenelse_trace * #Hcm_ifthenelse
1894	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1895	cases (bind_inversion ????? Htranslate) -Htranslate
1896	* #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
1897	cases (bind_inversion ????? Htranslate) -Htranslate
1898	* #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 #Htranslate
1899	cases (bind_inversion ????? Htranslate) -Htranslate
1900	* #cm_expr_e2_welltyped #Hexpr2_vars_wt * #Htypecheck
1901	lapply (typ_should_eq_inversion (typ_of_type (typeof e2)) (typ_of_type ty) … Htypecheck) -Htypecheck
1902	* #Htypeof_e2_eq_ty
1903	lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
1904	lapply Hexpr_vars_e2 -Hexpr_vars_e2 lapply cm_expr_e2 -cm_expr_e2
1905	>Htypeof_e2_eq_ty #cm_expr_e2 #Hexpr_vars_e2 #Hind2
1906	#Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
1907	#Hcmexpr_eq2 destruct (Hcm_expr_eq2) #Htranslate
1908	cases (bind_inversion ????? Htranslate) -Htranslate
1909	* #cm_expr_e3 #Hexpr_vars_e3 * #Htranslate_e3 #Htranslate
1910	cases (bind_inversion ????? Htranslate) -Htranslate
1911	* #cm_expr_e3_welltyped #Hexpr3_vars_wt * #Htypecheck
1912	lapply (typ_should_eq_inversion (typ_of_type (typeof e3)) (typ_of_type ty) … Htypecheck) -Htypecheck
1913	* #Htypeof_e3_eq_ty
1914	lapply (Hind3 cm_expr_e3 Hexpr_vars_e3 Htranslate_e3) -Hind3
1915	lapply Hexpr_vars_e3 -Hexpr_vars_e3 lapply cm_expr_e3 -cm_expr_e3
1916	>Htypeof_e3_eq_ty #cm_expr_e3 #Hexpr_vars_e3 #Hind3
1917	#Hjm_type_eq lapply (jmeq_to_eq ??? Hjm_type_eq) -Hjm_type_eq
1918	#Hcmexpr_eq3 destruct (Hcm_expr_eq2)
1919	lapply (Hind1 cm_expr_e1 Hexpr_vars_e1 Htranslate_e1) -Hind1
1920	lapply Hexpr_vars_e1 -Hexpr_vars_e1 lapply cm_expr_e1 -cm_expr_e1
1921	lapply Hexec_bool_of_val -Hexec_bool_of_val
1922	cases (typeof e1) normalize nodelta
1923	[ \| #esz #esg \| #eptr_ty \| #earray_ty #earray_sz \| #edomain #ecodomain
1924	\| #estructname #efieldspec \| #eunionname #efieldspec \| #eid ]
1925	#Hexec_bool_of_val #cm_expr_e1 #Hexpr_vars_e1 #Hind1 #Heq
1926	whd in Heq:(???%); destruct (Heq)
1927	whd in match (eval_expr ???????);
1928	whd in Hyp_present; cases Hyp_present * #Hyp1 #Hyp2 #Hyp3 -Hyp_present
1929	lapply (Hind1 … Hyp1 Hexec_cond) -Hind1 * #cm_val_e1 * #Heval_e1 #Hvalue_eq1
1930	>Heval_e1 normalize nodelta
1931	lapply Hcm_ifthenelse -Hcm_ifthenelse
1932	lapply Hexec_cond -Hexec_cond
1933	lapply Hexec_bool_of_val -Hexec_bool_of_val
1934	lapply Hvalue_eq1 -Hvalue_eq1
1935	cases cm_cond_val
1936	[ \| #vsz #vi \| \| #vp
1937	\| \| #vsz #vi \| \| #vp
1938	\| \| #vsz #vi \| \| #vp
1939	\| \| #vsz #vi \| \| #vp ]
1940	whd in ⊢ (? → (??%%) → ?);
1941	[ 6:
1942	\| *: #_ #Habsurd destruct (Habsurd) ]
1943	#Hvalue_eq1 #Hsz_check
1944	lapply (intsize_eq_elim_inversion ??????? Hsz_check) -Hsz_check
1945	* #Hsz_eq destruct (Hsz_eq) whd in match (eq_rect_r ??????);
1946	#Heq destruct (Heq)
1947	#Hexec_expr_e1
1948	@(match (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))
1949	return λx. ((eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz))) = x) → ?
1950	with
1951	[ true ⇒ λHeq. ?
1952	\| false ⇒ λHeq. ?
1953	] (refl ? (eq_bv (bitsize_of_intsize esz) vi (zero (bitsize_of_intsize esz)))))
1954	normalize nodelta
1955	>(value_eq_int_inversion … Hvalue_eq1) #Hexec_expr_body
1956	whd in match (eval_bool_of_val ?); whd in match (m_bind ?????);
1957	>Heq normalize nodelta
1958	[ -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq3)
1959	cases (Hind3 … Hyp3 Hexec_expr_body) #cm_val3 * #Heval_expr >Heval_expr #Hvalue_eq
1960	normalize %{cm_val3} @conj try @refl assumption
1961	\| -Heq -Hexec_expr_e1 -Hvalue_eq1 -Heval_e1 -cm_val_e1 -Hexpr_vars_e1 destruct (Hcmexpr_eq2)
1962	cases (Hind2 … Hyp2 Hexec_expr_body) #cm_val2 * #Heval_expr >Heval_expr #Hvalue_eq
1963	normalize %{cm_val2} @conj try @refl assumption ]
1964	\| 10: (* andbool *)
1965	#ty
1966	#e1 #e2 #Hind1 #Hind2 whd in match (typeof ?);
1967	cases ty
1968	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
1969	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
1970	#cm_expr #Hexpr_vars #Htranslate #cl_final_val #trace #Hyp_present #Hexec_expr
1971	(* decompose first slice of clight execution *)
1972	cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1973	* #cl_val_e1 #cm_trace_e1 * #Hexec_e1 #Hexec_expr
1974	cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1975	(* cut *)
1976	* * normalize nodelta #Hexec_bool_of_val
1977	[ 2,4,6,8,10,12,14:
1978	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
1979	\| 16: whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd)
1980	\| *:
1981	#Hexec_expr
1982	cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1983	* #cl_val_e2 #cm_trace_e2 * #Hexec_e2 #Hexec_expr
1984	cases (bind_inversion ????? Hexec_expr) -Hexec_expr
1985	#b2 * #Hexec_bool_of_val_e2
1986	whd in ⊢ ((???%) → ?); #Heq
1987	destruct (Heq) ]
1988	cases (bind_inversion ????? Htranslate) -Htranslate normalize nodelta
1989	* #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
1990	cases (bind_inversion ????? Htranslate) -Htranslate
1991	* #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 #Htranslate
1992	cases (bind_inversion ????? Htranslate) -Htranslate
1993	* #cm_expr_e2_welltyped #Hexpr_vars_wt * #Htype_coercion
1994	lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htype_coercion) -Htype_coercion
1995	* #Htypeof_e2_eq_ty
1996	(* cleanup the type coercion *)
1997	lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
1998	lapply Hexpr_vars_wt -Hexpr_vars_wt
1999	lapply cm_expr_e2_welltyped -cm_expr_e2_welltyped whd in match (typ_of_type ?);
2000	lapply Hexpr_vars_e2 -Hexpr_vars_e2
2001	lapply cm_expr_e2 -cm_expr_e2
2002	>Htypeof_e2_eq_ty normalize nodelta -Htypeof_e2_eq_ty
2003	#cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2
2004	#Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
2005	lapply (Hind1 cm_expr_e1 … Hexpr_vars_e1 Htranslate_e1) -Hind1
2006	lapply Hexpr_vars_e1 -Hexpr_vars_e1
2007	lapply cm_expr_e1 -cm_expr_e1
2008	cases (exec_bool_of_val_inversion … Hexec_bool_of_val)
2009	[ 2,4: * #ptr1 * #ptr_ty1 * * #Hcl_val_e1 #Htypeof_e1 #Habsurd destruct (Habsurd)
2010	destruct >(Htypeof_e1) whd in match (typ_of_type ?);
2011	#cm_expr_e1 #Hexpr_vars_e1 #Hind1 normalize nodelta
2012	whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
2013	*
2014	[ 2,4: * #ptr_ty * * #Hcl_val_e1 #Htypeof_e1 #Habsurd destruct (Habsurd)
2015	destruct >Htypeof_e1 whd in match (typ_of_type ?); normalize nodelta
2016	#cm_expr #Hexpr_vars #Hind whd in ⊢ ((???%) → ?);
2017	#Habsurd destruct (Habsurd) ]
2018	* #sz1 * #sg1 * #i1 * * #Hcl_val_e1 #Htypeof_e1 -Hexec_bool_of_val
2019	destruct >Htypeof_e1 #Heq_bv
2020	whd in match (typ_of_type ?) in ⊢ (% → % → % → % → ?);
2021	#cm_expr_e1 #Hexpr_vars_e1 #Hind1 normalize nodelta
2022	whd in match (typ_of_type ?);
2023	whd in ⊢ ((???%) → ?); #Heq
2024	destruct (Heq) cases Hyp_present -Hyp_present
2025	* #Hyp_present_e1 * * #Hyp_present_e2 normalize in ⊢ (% → % → % → ?);
2026	* * *
2027	lapply (Hind1 … Hyp_present_e1 Hexec_e1)
2028	* #cm_val_1 * #Heval_expr1 #Hvalue_eq
2029	whd in match (eval_expr ???????); whd in match (proj2 ???); whd in match (proj2 ???);
2030	>Heval_expr1 normalize nodelta >(value_eq_int_inversion … Hvalue_eq)
2031	whd in match (eval_bool_of_val ?);
2032	<Heq_bv
2033	whd in match (m_bind ?????);
2034	[ %{(Vint sz (zero (bitsize_of_intsize sz)))}
2035	>zero_ext_zero @conj try %2
2036	whd in match E0; whd in match (Eapp ??); >append_nil @refl ]
2037	normalize nodelta
2038	lapply (Hind2 … Hyp_present_e2 … Hexec_e2)
2039	-Hind2 * #cm_val_2 * #Heval_expr2 #Hvalue_eq2
2040	whd in match (eval_expr ???????); >Heval_expr2
2041	normalize nodelta
2042	cases (exec_bool_of_val_inversion … Hexec_bool_of_val_e2)
2043	[ 2: * #ptr2 * #ty2' * * #Hcl_val_e2 #Htypeof_e2 #Hb2_eq
2044	destruct cases (value_eq_ptr_inversion … Hvalue_eq2)
2045	#cm_ptr2 * #Hcm_ptr2 >Hcm_ptr2 #Hembed2
2046	whd in match (eval_bool_of_val ?);
2047	whd in match (m_bind ?????); normalize nodelta
2048	>zero_ext_one
2049	%{(Vint sz (repr sz 1))} @conj try %2
2050	whd in match (Eapp ? E0); whd in match E0; >append_nil @refl ]
2051	*
2052	[ 2: * #ty2' * * #Hcl_val_e2 #Htypeof_e2 #Hb2_eq destruct
2053	>(value_eq_null_inversion … Hvalue_eq2)
2054	whd in match (eval_bool_of_val ?);
2055	whd in match (m_bind ?????);
2056	normalize nodelta
2057	%{(Vint sz (zero (bitsize_of_intsize sz)))}
2058	>zero_ext_zero @conj try %2
2059	whd in match (Eapp ? E0); whd in match E0; >append_nil @refl ]
2060	* #sz2 * #sg2 * #i2 * * #Hcl_val_e2 #Htypeof_e2 #Heq_bv
2061	destruct (Hcl_val_e2)
2062	>(value_eq_int_inversion … Hvalue_eq2)
2063	whd in match (eval_bool_of_val ?); <Heq_bv
2064	cases b2 in Heq_bv; #Heq_bv
2065	whd in match (m_bind ?????); normalize nodelta
2066	[ %{(Vint sz (repr sz 1))} whd in match E0; whd in match (Eapp ? []);
2067	>append_nil @conj try @refl >zero_ext_one %2
2068	\| %{(Vint sz (zero (bitsize_of_intsize sz)))} whd in match E0; whd in match (Eapp ? []);
2069	>append_nil @conj try @refl >zero_ext_zero %2 ]
2070	\| 11: (* orbool, similar to andbool *)
2071	#ty
2072	#e1 #e2 #Hind1 #Hind2 whd in match (typeof ?);
2073	cases ty
2074	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
2075	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
2076	#cm_expr #Hexpr_vars #Htranslate #cl_final_val #trace #Hyp_present #Hexec_expr
2077	(* decompose first slice of clight execution *)
2078	cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2079	* #cl_val_e1 #cm_trace_e1 * #Hexec_e1 #Hexec_expr
2080	cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2081	* * normalize nodelta #Hexec_bool_of_val
2082	[ 1,3,5,7,9,11,13,15:
2083	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2084	\| *:
2085	#Hexec_expr
2086	cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2087	* #cl_val_e2 #cm_trace_e2 * #Hexec_e2 #Hexec_expr
2088	cases (bind_inversion ????? Hexec_expr) -Hexec_expr
2089	#b2 * #Hexec_bool_of_val_e2
2090	whd in ⊢ ((???%) → ?); #Heq
2091	destruct (Heq) ]
2092	cases (bind_inversion ????? Htranslate) -Htranslate normalize nodelta
2093	* #cm_expr_e1 #Hexpr_vars_e1 * #Htranslate_e1 #Htranslate
2094	cases (bind_inversion ????? Htranslate) -Htranslate
2095	* #cm_expr_e2 #Hexpr_vars_e2 * #Htranslate_e2 #Htranslate
2096	cases (bind_inversion ????? Htranslate) -Htranslate
2097	* #cm_expr_e2_welltyped #Hexpr_vars_wt * #Htype_coercion
2098	lapply (type_should_eq_inversion (typeof e2) (Tint sz sg) … Htype_coercion) -Htype_coercion
2099	* #Htypeof_e2_eq_ty
2100	(* cleanup the type coercion *)
2101	lapply (Hind2 cm_expr_e2 Hexpr_vars_e2 Htranslate_e2) -Hind2
2102	lapply Hexpr_vars_wt -Hexpr_vars_wt
2103	lapply cm_expr_e2_welltyped -cm_expr_e2_welltyped whd in match (typ_of_type ?);
2104	lapply Hexpr_vars_e2 -Hexpr_vars_e2
2105	lapply cm_expr_e2 -cm_expr_e2
2106	>Htypeof_e2_eq_ty normalize nodelta -Htypeof_e2_eq_ty
2107	#cm_expr_e2 #Hexpr_vars_e2 #cm_expr_e2_welltyped #Hexpr_vars_e2_wt #Hind2
2108	#Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
2109	lapply (Hind1 cm_expr_e1 … Hexpr_vars_e1 Htranslate_e1) -Hind1
2110	lapply Hexpr_vars_e1 -Hexpr_vars_e1
2111	lapply cm_expr_e1 -cm_expr_e1
2112	cases (exec_bool_of_val_inversion … Hexec_bool_of_val)
2113	[ 2,4: * #ptr1 * #ptr_ty1 * * #Hcl_val_e1 #Htypeof_e1 #Habsurd destruct (Habsurd)
2114	destruct >(Htypeof_e1) whd in match (typ_of_type ?);
2115	#cm_expr_e1 #Hexpr_vars_e1 #Hind1 normalize nodelta
2116	whd in ⊢ ((???%) → ?); #Habsurd destruct (Habsurd) ]
2117	*
2118	[ 2,4: * #ptr_ty * * #Hcl_val_e1 #Htypeof_e1 #Habsurd destruct (Habsurd)
2119	destruct >Htypeof_e1 whd in match (typ_of_type ?); normalize nodelta
2120	#cm_expr #Hexpr_vars #Hind whd in ⊢ ((???%) → ?);
2121	#Habsurd destruct (Habsurd) ]
2122	* #sz1 * #sg1 * #i1 * * #Hcl_val_e1 #Htypeof_e1 -Hexec_bool_of_val
2123	destruct >Htypeof_e1 #Heq_bv
2124	whd in match (typ_of_type ?) in ⊢ (% → % → % → % → ?);
2125	#cm_expr_e1 #Hexpr_vars_e1 #Hind1 normalize nodelta
2126	whd in ⊢ ((???%) → ?); #Heq
2127	destruct (Heq) cases Hyp_present -Hyp_present
2128	* #Hyp_present_e1 * * * #Hyp_present_e2 * *
2129	lapply (Hind1 … Hyp_present_e1 Hexec_e1)
2130	* #cm_val_1 * #Heval_expr1 #Hvalue_eq
2131	whd in match (eval_expr ???????);
2132	>Heval_expr1 normalize nodelta >(value_eq_int_inversion … Hvalue_eq)
2133	whd in match (eval_bool_of_val ?);
2134	<Heq_bv
2135	whd in match (m_bind ?????);
2136	[ %{(Vint sz (repr sz 1))}
2137	>zero_ext_one @conj try %2
2138	whd in match E0; whd in match (Eapp ??); >append_nil @refl ]
2139	normalize nodelta
2140	lapply (Hind2 … Hyp_present_e2 … Hexec_e2)
2141	-Hind2 * #cm_val_2 * #Heval_expr2 #Hvalue_eq2
2142	whd in match (eval_expr ???????); >Heval_expr2
2143	normalize nodelta
2144	cases (exec_bool_of_val_inversion … Hexec_bool_of_val_e2)
2145	[ 2: * #ptr2 * #ty2' * * #Hcl_val_e2 #Htypeof_e2 #Hb2_eq
2146	destruct cases (value_eq_ptr_inversion … Hvalue_eq2)
2147	#cm_ptr2 * #Hcm_ptr2 >Hcm_ptr2 #Hembed2
2148	whd in match (eval_bool_of_val ?);
2149	whd in match (m_bind ?????); normalize nodelta
2150	>zero_ext_one
2151	%{(Vint sz (repr sz 1))} @conj try %2
2152	whd in match (Eapp ? E0); whd in match E0; >append_nil @refl ]
2153	*
2154	[ 2: * #ty2' * * #Hcl_val_e2 #Htypeof_e2 #Hb2_eq destruct
2155	>(value_eq_null_inversion … Hvalue_eq2)
2156	whd in match (eval_bool_of_val ?);
2157	whd in match (m_bind ?????);
2158	normalize nodelta
2159	%{(Vint sz (zero (bitsize_of_intsize sz)))}
2160	>zero_ext_zero @conj try %2
2161	whd in match (Eapp ? E0); whd in match E0; >append_nil @refl ]
2162	* #sz2 * #sg2 * #i2 * * #Hcl_val_e2 #Htypeof_e2 #Heq_bv
2163	destruct (Hcl_val_e2)
2164	>(value_eq_int_inversion … Hvalue_eq2)
2165	whd in match (eval_bool_of_val ?); <Heq_bv
2166	cases b2 in Heq_bv; #Heq_bv
2167	whd in match (m_bind ?????); normalize nodelta
2168	[ %{(Vint sz (repr sz 1))} whd in match E0; whd in match (Eapp ? []);
2169	>append_nil @conj try @refl >zero_ext_one %2
2170	\| %{(Vint sz (zero (bitsize_of_intsize sz)))} whd in match E0; whd in match (Eapp ? []);
2171	>append_nil @conj try @refl >zero_ext_zero %2 ]
2172	\| 12: (* sizeof *)
2173	#ty cases ty
2174	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
2175	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
2176	#ty' #e #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
2177	whd in Hexec_expr:(??%?); destruct (Hexec_expr)
2178	normalize in match (typ_of_type ?);
2179	whd in Htranslate:(??%?); destruct (Htranslate)
2180	whd in match (eval_expr ???????);
2181	%{(Vint sz (repr sz (sizeof ty')))} @conj try @refl %2
2182	\| 13:
2183	#ty #ed #ty' cases ty'
2184	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
2185	\| #structname #fieldspec \| #unionname #fieldspec \| #id ]
2186	#i #Hind #e #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
2187	#Hexec_lvalue
2188	whd in Hexec_lvalue:(??%?); destruct
2189	[ whd in Htranslate_addr:(??%?);
2190	cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
2191	* #fieldexpr #Hexpr_vars_field * #Htranslate_field #Htranslate_addr
2192	cases (bind_inversion ????? Htranslate_addr) -Htranslate_addr
2193	#field_off * #Hfield_off whd in ⊢ ((???%) → ?);
2194	#Heq destruct (Heq)
2195	cases Hyp_present -Hyp_present #Hyp_present_fieldexpr #Hyp_present_cst
2196	]
2197	cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue
2198	* * #bl #off #tr * #Hexec_lvalue_ind #Hexec_lvalue
2199	[ 1: cases (bind_inversion ????? Hexec_lvalue) -Hexec_lvalue #field_off' *
2200	#Hfield_off' whd in ⊢ ((???%) → ?); #H destruct (H)
2201	cases (Hind … Hexpr_vars_field Htranslate_field … Hyp_present_fieldexpr Hexec_lvalue_ind)
2202	#cm_val_field * #Heval_cm #Hvalue_eq
2203	whd in match (eval_expr ???????);
2204	>Heval_cm normalize nodelta
2205	whd in match (eval_expr ???????); whd in match (m_bind ?????);
2206	whd in match (eval_binop ???????); normalize nodelta
2207	cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Heq_cm_ptr >Heq_cm_ptr
2208	normalize nodelta #Hptr_translate
2209	%{(Vptr (shift_pointer (bitsize_of_intsize I16) cm_ptr (repr I16 field_off)))}
2210	@conj whd in match (Eapp ??); >(append_nil ? trace) try @refl
2211	%4 whd in Hptr_translate:(??%?) ⊢ (??%?);
2212	cases (E cl_blo) in Hptr_translate; normalize nodelta
2213	[ #H destruct (H) ]
2214	* #BL #OFF normalize nodelta #Heq destruct (Heq)
2215	>Hfield_off' in Hfield_off; normalize in ⊢ ((??%%) → ?);
2216	#H destruct (H)
2217	whd in match (shift_pointer ???);
2218	whd in match (shift_offset ???) in ⊢ (???%);
2219	>sign_ext_same_size
2220	whd in match (offset_plus ??) in ⊢ (??%%);
2221	<(associative_addition_n ? (offv off))
2222	>(commutative_addition_n … (repr I16 field_off) (offv OFF))
2223	>(associative_addition_n ? (offv off))
2224	@refl
2225	\| 2: normalize in Hexec_lvalue:(???%); destruct (Hexec_lvalue)
2226	cases (Hind … Hexpr_vars Htranslate_addr ??? Hyp_present Hexec_lvalue_ind)
2227	#cm_val * #Heval_expr >Heval_expr #Hvalue_eq
2228	cases (value_eq_ptr_inversion … Hvalue_eq) #cm_ptr * #Hcm_ptr_eq >Hcm_ptr_eq
2229	#Hpointer_translation
2230	%{cm_val} @conj try assumption
2231	destruct @refl
2232	]
2233	\| 14: (* cost label *)
2234	#ty (* cases ty
2235	[ \| #sz #sg \| #ptr_ty \| #array_ty #array_sz \| #domain #codomain
2236	\| #structname #fieldspec \| #unionname #fieldspec \| #id ] *)
2237	#l * #ed #ety
2238	whd in match (typeof ?); whd in match (typeof ?);
2239	#Hind #e' #Hexpr_vars #Htranslate #cl_val #trace #Hyp_present #Hexec_expr
2240	cases (bind_inversion ????? Htranslate) -Htranslate * #cm_expr
2241	#Hexpr_vars * #Htranslate_ind #Htranslate
2242	cases (bind_inversion ????? Htranslate) -Htranslate * #cm_costexpr #Hexpr_vars_costexpr
2243	* whd in ⊢ ((???%) → ?); #H destruct (H) #Htyp_should_eq
2244	whd in match (typeof ?) in Htyp_should_eq:(??%?);
2245	cases (typ_should_eq_inversion (typ_of_type ety) (typ_of_type ty) ??? Htyp_should_eq)
2246	#Htyp_eq
2247	lapply Htranslate_ind -Htranslate_ind
2248	lapply Hexpr_vars_costexpr -Hexpr_vars_costexpr
2249	lapply Hexec_expr -Hexec_expr lapply Hyp_present -Hyp_present
2250	lapply Hexpr_vars -Hexpr_vars lapply e' -e'
2251	lapply Hind -Hind lapply cm_expr -cm_expr whd in match (typeof ?);
2252	<Htyp_eq
2253	#cm_expr #Hind #e' #Hexpr_vars #Hyp_present #Hexec_expr #Hexpr_vars_costexpr
2254	#Htranslate_ind #Heq lapply (jmeq_to_eq ??? Heq) -Heq #Heq destruct (Heq)
2255	whd in match (eval_expr ???????);
2256	cases (bind_inversion ????? Hexec_expr) * #cm_val #cm_trace * #Hexec_expr_ind
2257	whd in ⊢ ((???%) → ?); #Heq destruct (Heq)
2258	cases (Hind cm_expr Hexpr_vars Htranslate_ind … Hyp_present Hexec_expr_ind)
2259	#cm_val' * #Heval_expr' #Hvalue_eq
2260	>Heval_expr' normalize nodelta %{cm_val'} @conj try assumption
2261	>cons_to_append >(nil_append … cm_trace) @refl
2262	\| 15: *
2263	[ #sz #i \| #var_id \| #e1 \| #e1 \| #op #e1 \| #op #e1 #e2 \| #cast_ty #e1
2264	\| #cond #iftrue #iffalse \| #e1 #e2 \| #e1 #e2 \| #sizeofty \| #e1 #field \| #cost #e1 ]
2265	#ty normalize in ⊢ (% → ?);
2266	[ 2,3,12: @False_ind
2267	\| *: #_ #e' #Hexpr_vars #Htranslate_addr #cl_blo #cl_off #trace #Hyp_present
2268	normalize #Habsurd destruct (Habsurd) ]
2269	] qed.

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

Download in other formats:

Original Format