source: src/Clight/toCminorCorrectnessExpr.ma @ 2591

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

Moved simulation proof for expressions in toCminorCorrectnessExpr.ma, for separate typechecking.

File size: 109.8 KB
Line 
1include "Clight/toCminor.ma".
2include "Clight/CexecInd.ma".
3include "common/Globalenvs.ma".
4include "Clight/toCminorOps.ma".
5include "Clight/memoryInjections.ma".
6include "Clight/abstract.ma".
7include "Cminor/abstract.ma".
8
9record 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'] *)
23definition 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
56lemma 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
61whd 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
88lemma 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
113lemma 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
122lapply (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 *)
139lapply (exec_alloc_fail_antimonotonic … Hexec_alloc … Hlookup_fail)
140* #Hlookup' #Hnot_exists
141lapply (characterise_vars_all … Hcharacterise var_id t ?)
142[ 1,3: whd destruct (Halloc) >Hlookup_type_ok // ]
143#Hexists @False_ind
144cut (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
150qed.
151
152(* avoid a case analysis on type inside of a big proof *)
153lemma 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 ]
174whd in match (typ_of_type Tvoid);
175#e #f normalize nodelta #Heq destruct
176%{sz} %{sg} % try @refl >Heq %
177qed.
178
179
180(* The two following lemmas are just noise. *)
181
182lemma 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 //
198qed.
199
200lemma 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
220qed.
221
222lemma sign_ext_sign_ext_reduce :
223  ∀i. sign_ext 32 16 (sign_ext 16 32 i) = i.
224#i @refl
225qed. 
226
227lemma sign_ext_zero_ext_reduce :
228  ∀i. sign_ext 32 16 (zero_ext 16 32 i) = i.
229#i @refl
230qed.
231
232(* There are two zero_ext, and this causes the "disambiguator" to fail. So we do
233 * the cleanup ourselves. *)
234
235definition zero_ext_bv : ∀n1,n2. ∀bv:BitVector n1. BitVector n2 ≝ zero_ext.
236definition 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. *)
241lemma 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
248lemma 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
255lemma 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
261cases v in Hexec;
262[ | #vsz #i | | #p ]
263cases 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 ]
268whd 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*)
285lemma 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
319qed.
320
321lemma 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
338lemma 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
347normalize in match (access_mode ?);
348[ 1,4,5,6,7: #Habsurd destruct ]
349#_
350#H @H
351qed.
352
353lemma 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
360elim 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
375lemma 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
383cases (lookup_exec_alloc … Hlookup Hexec)
384[ normalize in ⊢ (% → ?); #Heq destruct
385| @(characterise_vars_localid … Hchar) ]
386qed.
387
388
389(* -------------------------------------------------------------------- *)
390(* Simulation proof for expression evaluation between Clight and Cminor *)
391
392lemma 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+1*8); *)
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.