source: src/Clight/toCminorCorrectnessExpr.ma @ 2608

Last change on this file since 2608 was 2608, checked in by garnier, 8 years ago

Regions are no more stored in blocks. block_region now tests the id, it being below 0 implying Code region, XData otherwise.
Changes propagated through the front-end and common. Some more work might be required in the back-end, but it should be
trivial to fix related problems.

Motivation: no way to /elegantly/ prove that two blocks with the same id but different regions are non-sensical.
Prevented some proofs to go through in memory injections.

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