source: src/Clight/SimplifyCasts.ma @ 2103

Last change on this file since 2103 was 2103, checked in by campbell, 6 years ago

Make transform_*program take a more general transformation to make
properties easier to state.

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