include "Clight/Csyntax.ma".
include "Clight/TypeComparison.ma".

(* IG: used to prove preservation of the semantics. *)
include "Clight/Cexec.ma".
include "Clight/casts.ma".
include "Clight/CexecSound.ma".


(* include "ASM/AssemblyProof.ma". *) (* I had to manually copy some of the lemmas in this file, including an axiom ... *)

(* Attempt to remove unnecessary integer casts in Clight programs.

   This differs from the OCaml prototype by attempting to recursively determine
   whether subexpressions can be changed rather than using a fixed size pattern.
   As a result more complex expressions such as (char)((int)x + (int)y + (int)z)
   where x,y and z are chars can be simplified.
   
   A possible improvement that doesn't quite fit into this scheme would be to
   spot that casts can be removed in expressions like (int)x == (int)y where
   x and y have some smaller integer type.
 *)

(* Attempt to squeeze integer constant into a given type.

   This might be too conservative --- if we're going to cast it anyway, can't
   I just ignore the fact that the integer doesn't fit?
*)

(* [reduce_bits n m exp v] takes avector of size n + m + 1 and returns (if all goes well) a vector of size
 *  m+1 (an empty vector of bits makes no sense). It proceeds by removing /all/ the [n] leading bits equal
 * to [exp]. If it fails, it returns None. *)
let rec reduce_bits (n,m:nat) (exp:bool) (v:BitVector (plus n (S m))) on n : option (BitVector (S m)) ≝
match n return λn. BitVector (n+S m) → option (BitVector (S m)) with
[ O ⇒ λv. Some ? v
| S n' ⇒ λv. if eq_b (head' ?? v) exp then reduce_bits ?? exp (tail ?? v) else None ?
] v.

lemma reduce_bits_ok : ∀n,m.∀exp.∀v,v'. reduce_bits (S n) m exp v = Some ? v'→ reduce_bits n m exp (tail ?? v) = Some ? v'.
#n #m #exp #v #v' #H whd in H:(??%?); lapply H -H
cases (eq_b ? exp)
[ 1: #H whd in H:(??%?); //
| 2: #H normalize in H; destruct ] qed.

lemma reduce_bits_trunc : ∀n,m.∀exp.∀v:(BitVector (plus n (S m))).∀v'. 
  reduce_bits n m exp v = Some ? v' → v' = truncate n (S m) v.
#n #m elim n
[ 1: #exp #v #v' #H normalize in v v' H; destruct normalize >vsplit_O_n //
| 2: #n' #Hind #exp #v #v' #H >truncate_tail
 > (Hind ??? (reduce_bits_ok ?? exp v v' H)) // ] qed.
 
lemma reduce_bits_dec : ∀n,m.∀exp.∀v. (∃v'.reduce_bits n m exp v = Some ? v') ∨ reduce_bits n m exp v = None ?.
#n #m #exp #v elim (reduce_bits n m exp v)
[ 1: %2 //
| 2: #v' %1 @(ex_intro … v') // ] qed.

(* pred_bitsize_of_intsize I32 = 31, … *)
definition pred_bitsize_of_intsize : intsize → nat ≝
λsz. pred (bitsize_of_intsize sz).

definition signed : signedness → bool ≝
λsg. match sg with [ Unsigned ⇒ false | Signed ⇒ true ].

(* [simplify_int sz sz' sg sg' i] tries to convert an integer [i] of width [sz] and signedness [sg] 
 * into an integer of size [sz'] of signedness [sg'].
 * - It first proceeds by comparing the source and target width: if the target width is strictly superior
 *   to the source width, the conversion fails. 
 * - If the size is equal, the argument is returned as-is.
 * - If the target type is strictly smaller than the source, it tries to squeeze the integer to
 *   the desired size. 
*)
let rec simplify_int (sz,sz':intsize) (sg,sg':signedness) (i:bvint sz) : option (bvint sz') ≝
  let bit ≝ signed sg ∧ head' … i in
  (* [nat_compare] does more than an innocent post-doc might think. It also computes the difference between the two args.
   * if x < y, nat_compare x y = lt(x, y-(x+1))  
   * if x = y, nat_compare x y = eq x
   * if x > y, nat_compare x y = gt(x-(y+1), y) *)
  match nat_compare (pred_bitsize_of_intsize sz) (pred_bitsize_of_intsize sz')
      return λn,m,x.BitVector (S n) → option (BitVector (S m)) with
  [ nat_lt _ _ ⇒ λi. None ?   (* refuse to make constants larger *)
  | nat_eq _ ⇒ λi. Some ? i
  | nat_gt x y ⇒ λi. 
      (* 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.
       * 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),
       * we deduce that the actual arguments of [reduce_bits] are (S x) and (S y), which is consistent.
       * If [i] is of signed type and if it is negative, then it tries to remove the (S x) first "1" bits.
       * Otherwise, it tries to remove the (S x) first "0" bits.
       *)
      match reduce_bits ?? bit (i⌈BitVector (S (y+S x))↦BitVector ((S x) + (S y))⌉) with
      [ Some i' ⇒ 
        if signed sg' then 
          if eq_b bit (head' … i') then 
            Some ? i' 
          else None ? 
        else Some ? i'
      | None ⇒ None ?
      ]
  ] i.
>(commutative_plus_faster (S x)) @refl
qed.


lemma eq_intsize_identity : ∀id. eq_intsize id id = true.
* normalize //
qed.

lemma sz_eq_identity : ∀s. sz_eq_dec s s = inl ?? (refl ? s).
* normalize // 
qed.

lemma type_eq_identity : ∀t. type_eq t t = true.
#t normalize elim (type_eq_dec t t)
[ 1: #Heq normalize //
| 2: #H destruct elim H #Hcontr elim (Hcontr (refl ? t)) ] qed.

lemma type_neq_not_identity : ∀t1, t2. t1 ≠ t2 → type_eq t1 t2 = false.
#t1 #t2 #Hneq normalize elim (type_eq_dec t1 t2)
[ 1: #Heq destruct elim Hneq #Hcontr elim (Hcontr (refl ? t2))
| 2: #Hneq' normalize // ] qed.

definition size_le ≝ λsz1,sz2.
match sz1 with
[ I8 ⇒ True
| I16 ⇒ 
  match sz2 with
  [ I16 ⇒ True | I32 ⇒ True | _ ⇒ False ]
| I32 ⇒
  match sz2 with
  [ I32 ⇒ True | _ ⇒ False ]
].

definition size_lt ≝ λsz1,sz2.
match sz1 with
[ I8 ⇒
  match sz2 with
  [ I16 ⇒ True | I32 ⇒ True | _ ⇒ False ]
| I16 ⇒ 
  match sz2 with
  [ I32 ⇒ True | _ ⇒ False ]
| I32 ⇒ False
].

lemma size_lt_to_le : ∀sz1,sz2. size_lt sz1 sz2 → size_le sz1 sz2.
#sz1 #sz2 elim sz1 elim sz2 normalize // qed.

lemma size_lt_dec : ∀sz1,sz2. size_lt sz1 sz2 + (¬ (size_lt sz1 sz2)).
* * normalize /2/ /3/
qed.

lemma size_not_lt_to_ge : ∀sz1,sz2. ¬(size_lt sz1 sz2) → (sz1 = sz2) + (size_lt sz2 sz1).
* * normalize /2/ /3/
qed.

(* This function already exists in prop, we want it in type. *)
definition sign_eq_dect : ∀sg1,sg2:signedness. (sg1 = sg2) + (sg1 ≠ sg2).
* * normalize // qed.

lemma size_absurd : ∀a,b. size_le a b → size_lt b a → False.
* * normalize
#H1 #H2 try (@(False_ind … H1)) try (@(False_ind … H2)) qed. 
  
(* This defines necessary conditions for [src_expr] to be coerced to "target_ty".
 * Again, these are /not/ sufficient conditions. See [simplify_inv] for the rest. *)
definition necessary_conditions ≝ λsrc_sz.λsrc_sg.λtarget_sz.λtarget_sg.
match size_lt_dec target_sz src_sz with
[ inl Hlt ⇒ true
| inr Hnlt ⇒
  match sz_eq_dec target_sz src_sz with
  [ inl Hsz_eq ⇒
    match sign_eq_dect src_sg target_sg with
    [ inl Hsg_eq ⇒ false
    | inr Hsg_neq ⇒ true
    ]            
  | inr Hsz_neq ⇒ false
  ]
].

(* Inversion on necessary_conditions *)
lemma necessary_conditions_spec : 
  ∀src_sz,src_sg,target_sz, target_sg. (necessary_conditions src_sz src_sg target_sz target_sg = true) → 
      ((size_lt target_sz src_sz) ∨ (src_sz = target_sz ∧ src_sg ≠ target_sg)).
#src_sz #src_sg #target_sz #target_sg 
whd in match (necessary_conditions ????);
cases (size_lt_dec target_sz src_sz) normalize nodelta
[ 1: #Hlt #_ %1 //
| 2: #Hnlt 
     cases (sz_eq_dec target_sz src_sz) normalize nodelta
     [ 2: #_ #Hcontr destruct
     | 1: #Heq cases (sign_eq_dect src_sg target_sg) normalize nodelta
       [ 1: #_ #Hcontr destruct
       | 2: #Hsg_neq #_ %2 destruct /2/ ]
     ]
] qed.

(* Compare the results [r1,r2] of the evaluation of two expressions. If [r1] is an
 * integer value smaller but containing the same stuff than [r2] then all is well.
 * If the first evaluation is erroneous, we don't care about anything else. *)
definition smaller_integer_val ≝ λsrc_sz,dst_sz,sg. λr1,r2:res(val×trace).
match r1 with
[ OK res1 ⇒
  let 〈val1, tr1〉 ≝ res1 in
  ∀v1. val1 = Vint src_sz v1 →  
  match r2 with
  [ OK res2 ⇒ 
    let 〈val2, tr2〉 ≝ res2 in
    ∃v2. (val2 = Vint dst_sz v2 ∧
          v2 = cast_int_int src_sz sg dst_sz v1 ∧ tr1 = tr2 ∧ size_le dst_sz src_sz)    
  | _ ⇒ False ]
| Error errmsg1 ⇒ True
].

(* Simulation relation used for expression evaluation. *)
inductive res_sim (A : Type[0]) (r1 : res A) (r2 : res A) : Prop ≝
| SimOk   :  (∀a:A. r1 = OK ? a → r2 = OK ? a) → res_sim A r1 r2
| SimFail : (∃err. r1 = Error ? err) → res_sim A r1 r2.

(* Invariant of simplify_expr *)
inductive simplify_inv (ge : genv) (en : env) (m : mem) (e1 : expr) (e2 : expr) (target_sz : intsize) (target_sg : signedness) : bool → Prop ≝
(* Inv_eq states a standard simulation result. We enforce some needed equations on types to prove the cast cases. *)
| Inv_eq : ∀result_flag.
     result_flag = false →
     typeof e1 = typeof e2 →
     res_sim ? (exec_expr ge en m e1) (exec_expr ge en m e2) →
     res_sim ? (exec_lvalue ge en m e1) (exec_lvalue ge en m e2) →     
     simplify_inv ge en m e1 e2 target_sz target_sg result_flag
(* Inv_coerce_ok states that we successfuly squeezed the source expression to [target_sz]. The details are hidden in [smaller_integer_val]. *)
| Inv_coerce_ok : ∀src_sz,src_sg.
     (typeof e1) = (Tint src_sz src_sg) →
     (typeof e2) = (Tint target_sz target_sg) →     
     (smaller_integer_val src_sz target_sz src_sg (exec_expr ge en m e1) (exec_expr ge en m e2)) →
     simplify_inv ge en m e1 e2 target_sz target_sg true.
     
(* Invariant of simplify_inside *)     
definition conservation ≝ λe,result:expr.
∀ge,en,m. res_sim ? (exec_expr ge en m e) (exec_expr ge en m result)
                                                    ∧ res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge en m result)
                                                    ∧ typeof e = typeof result.

(* This lemma proves that simplify_int actually implements an integer cast. *)
(* The case 4 can be merged with cases 7 and 8. *)

lemma simplify_int_implements_cast : ∀sz,sz'.∀sg,sg'.∀i,i'. simplify_int sz sz' sg sg' i = Some ? i' → i' = cast_int_int sz sg sz' i.
* * 
[ 1: #sg #sg' #i #i' #Hsimp normalize in Hsimp ⊢ %; elim sg normalize destruct //
| 2,3,6: #sg #sg' #i #i' #Hsimp normalize in Hsimp; destruct (* ⊢ %; destruct destruct  whd in Hsimp:(??%?); destruct *)
| 4: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); normalize nodelta in Hsimp; normalize in i i' ⊢ %;
    normalize in match (signed ?) in Hsimp;
    normalize in match (S (plus ??)) in Hsimp;
    normalize in match (plus 7 8) in Hsimp;
    lapply Hsimp -Hsimp
    cases (head' bool 15 i)
    normalize in match (andb ??);
    [ 1,3: elim (reduce_bits_dec 8 7 true i) 
      [ 1,3: * #v' #Heq >Heq letin Heq_trunc ≝ (reduce_bits_trunc … Heq) normalize nodelta
        [ 1: cases (eq_b true ?) normalize #H destruct normalize @refl
        | 2: #H destruct normalize @refl ]
      | 2,4: #Heq >Heq normalize nodelta #H destruct ]
    | 2,4,5,6,7,8:
      elim (reduce_bits_dec 8 7 false i) 
      [ 1,3,5,7,9,11: * #v' #Heq >Heq normalize nodelta letin Heq_trunc ≝ (reduce_bits_trunc … Heq)
        [ 1,3,4: cases (eq_b false ?) normalize nodelta
         #H destruct normalize @refl
        | 2,5,6: #H destruct normalize @refl ]
      | 2,4,6,8,10,12: #Heq >Heq normalize nodelta #H destruct
      ]
    ]
| 5,9: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); destruct @refl
| 7, 8: * * #i #i' #Hsimp whd in Hsimp:(??%?) ⊢ (??%?); normalize nodelta in Hsimp; normalize in i i' ⊢ %;
    normalize in match (signed ?) in Hsimp;
    normalize in match (S (plus ??)) in Hsimp;    
    normalize in match (plus 7 24) in Hsimp;
    lapply Hsimp -Hsimp
    cases (head' bool ? i)   
    normalize in match (andb ??);
    [ 1,3,9,11:
      [ 1,2: (elim (reduce_bits_dec 24 7 true i)) | 3,4: (elim (reduce_bits_dec 16 15 true i)) ]
      [ 1,3,5,7: * #v' #Heq >Heq letin Heq_trunc ≝ (reduce_bits_trunc … Heq) normalize nodelta
        [ 1,3: cases (eq_b true ?) normalize #H destruct normalize @refl
        | 2,4: #H destruct normalize @refl ]
      | 2,4,6,8: #Heq >Heq normalize nodelta #H destruct ]
    | 2,4,5,6,7,8,10,12,13,14,15,16: 
      [ 1,2,3,4,5,6: elim (reduce_bits_dec 24 7 false i)
      | 6,7,8,9,10,11,12: elim (reduce_bits_dec 16 15 false i) ]
      [ 1,3,5,7,9,11,13,15,17,19,21,23: 
        * #v' #Heq >Heq normalize nodelta letin Heq_trunc ≝ (reduce_bits_trunc … Heq)
        [ 1,3,4,7,9,10: 
          cases (eq_b false ?) normalize nodelta #H destruct normalize @refl
        | 2,5,6,8,11,12: #H destruct normalize @refl ]
      | 2,4,6,8,10,12,14,16,18,20,22,24: #Heq >Heq normalize nodelta #H destruct
      ]
    ]
] qed.

(* Facts about cast_int_int *)

(* copied from AssemblyProof *)
lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A.
 #A #v generalize in match (refl … 0); cases v in ⊢ (??%? → ?%%??); //
 #n #hd #tl #abs @⊥ destruct (abs)
qed.

lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n).
 ∃hd.∃tl.v ≃ VCons A n hd tl.
 #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)));
 [ #abs @⊥ destruct (abs)
 | #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]
qed.

lemma vector_append_zero:
  ∀A,m.
  ∀v: Vector A m.
  ∀q: Vector A 0.
    v = q@@v.
  #A #m #v #q
  >(Vector_O A q) %
qed.

corollary prod_vector_zero_eq_left:
  ∀A, n.
  ∀q: Vector A O.
  ∀r: Vector A n.
    〈q, r〉 = 〈[[ ]], r〉.
  #A #n #q #r
  generalize in match (Vector_O A q …);
  #hyp
  >hyp in ⊢ (??%?);
  %
qed.
 
lemma vsplit_eq : ∀A. ∀m,n. ∀v : Vector A ((S m) + n).  ∃v1:Vector A (S m). ∃v2:Vector A n. v = v1 @@ v2.
# A #m #n elim m
[ 1: normalize #v
  elim (Vector_Sn ?? v) #hd * #tl #Eq
  @(ex_intro … (hd ::: [[]])) @(ex_intro … tl)
  >Eq normalize //
| 2: #n' #Hind #v
  elim (Vector_Sn ?? v) #hd * #tl #Eq
  elim (Hind tl)
  #tl1 * #tl2 #Eq_tl
  @(ex_intro … (hd ::: tl1))
  @(ex_intro … tl2)  
  destruct normalize //
] qed.

lemma vsplit_eq2 : ∀A. ∀m,n : nat. ∀v : Vector A (m + n).  ∃v1:Vector A m. ∃v2:Vector A n. v = v1 @@ v2.
# A #m #n elim m
[ 1: normalize #v @(ex_intro … (VEmpty ?)) @(ex_intro … v) normalize //
| 2: #n' #Hind #v
  elim (Vector_Sn ?? v) #hd * #tl #Eq
  elim (Hind tl)
  #tl1 * #tl2 #Eq_tl
  @(ex_intro … (hd ::: tl1))
  @(ex_intro … tl2)  
  destruct normalize //
] qed.

lemma vsplit_zero:
  ∀A,m.
  ∀v: Vector A m.
    〈[[]], v〉 = vsplit A 0 m v.
  #A #m #v
  elim v
  [ %
  | #n #hd #tl #ih
    normalize in ⊢ (???%); %
  ]
qed.


lemma vsplit_zero2:
  ∀A,m.
  ∀v: Vector A m.
    〈[[]], v〉 = vsplit' A 0 m v.
  #A #m #v
  elim v
  [ %
  | #n #hd #tl #ih
    normalize in ⊢ (???%); %
  ]
qed.

(* This is not very nice. Note that this axiom was copied verbatim from ASM/AssemblyProof.ma.
 * TODO sync with AssemblyProof.ma, in a better world we shouldn't have to copy all of this. *)
axiom vsplit_succ:
  ∀A, m, n.
  ∀l: Vector A m.
  ∀r: Vector A n.
  ∀v: Vector A (m + n).
  ∀hd.
    v = l@@r → (〈l, r〉 = vsplit ? m n v → 〈hd:::l, r〉 = vsplit ? (S m) n (hd:::v)).

axiom vsplit_succ2:
  ∀A, m, n.
  ∀l: Vector A m.
  ∀r: Vector A n.
  ∀v: Vector A (m + n).
  ∀hd.
    v = l@@r → (〈l, r〉 = vsplit' ? m n v → 〈hd:::l, r〉 = vsplit' ? (S m) n (hd:::v)).
     
lemma vsplit_prod2:
  ∀A,m,n.
  ∀p: Vector A (m + n).
  ∀v: Vector A m.
  ∀q: Vector A n.
    p = v@@q → 〈v, q〉 = vsplit' A m n p.
  #A #m
  elim m
  [ #n #p #v #q #hyp
    >hyp <(vector_append_zero A n q v)
    >(prod_vector_zero_eq_left A …)
    @vsplit_zero2
  | #r #ih #n #p #v #q #hyp
    >hyp
    cases (Vector_Sn A r v)
    #hd #exists
    cases exists
    #tl #jmeq >jmeq
    @vsplit_succ2 [1: % |2: @ih % ] 
  ]
qed.

lemma vsplit_prod:
  ∀A,m,n.
  ∀p: Vector A (m + n).
  ∀v: Vector A m.
  ∀q: Vector A n.
    p = v@@q → 〈v, q〉 = vsplit A m n p.
  #A #m
  elim m
  [ #n #p #v #q #hyp
    >hyp <(vector_append_zero A n q v)
    >(prod_vector_zero_eq_left A …)
    @vsplit_zero
  | #r #ih #n #p #v #q #hyp
    >hyp
    cases (Vector_Sn A r v)
    #hd #exists
    cases exists
    #tl #jmeq >jmeq
    @vsplit_succ [1: % |2: @ih % ] 
  ]
qed.

lemma cast_decompose : ∀s1, v. cast_int_int I32 s1 I8 v = (cast_int_int I16 s1 I8 (cast_int_int I32 s1 I16 v)).
#s1 #v normalize elim s1 normalize nodelta 
normalize in v;
elim (vsplit_eq ??? (v⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉))
[ 2,4: //
| 1,3: #l * #r normalize nodelta #Eq1
       <(vsplit_prod bool 16 16 … Eq1)
       elim (vsplit_eq ??? (r⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉))
       [ 2,4: //
       | 1,3: #lr * #rr normalize nodelta #Eq2
              <(vsplit_prod bool 8 8 … Eq2)
              cut (v = (l @@ lr) @@ rr)
              [ 1,3 : destruct >(vector_associative_append ? 16 8) //
              | 2,4: #Hrewrite destruct
                     <(vsplit_prod bool 24 8 … Hrewrite) @refl
              ]
       ]
] qed.

lemma cast_idempotent : ∀s1,s2,sz1,sz2,v. size_lt sz1 sz2 → cast_int_int sz2 s1 sz1 (cast_int_int sz1 s2 sz2 v) = v.
#s1 #s2 * * #v elim s1 elim s2
normalize #H try @refl
@(False_ind … H)
qed.

lemma cast_identity : ∀sz,sg,v. cast_int_int sz sg sz v = v.
* * #v normalize // qed.

lemma cast_collapse : ∀s1,s2,v. cast_int_int I32 s1 I8 (cast_int_int I16 s2 I32 v) = (cast_int_int I16 s1 I8 v).
#s1 #s2 #v >cast_decompose >cast_idempotent 
[ 1: @refl | 2: // ]
qed.

lemma cast_composition_lt : ∀a_sz,a_sg, b_sz, b_sg, c_sz, val.
   size_lt c_sz a_sz → size_lt c_sz b_sz →
   (cast_int_int a_sz a_sg c_sz val = 
        cast_int_int b_sz b_sg c_sz (cast_int_int a_sz a_sg b_sz val)).       
* #a_sg * #b_sg * #val whd in match (size_lt ??); whd in match (size_lt ??);
#Hlt1 #Hlt2
[ 1,2,3,4,5,6,7,8,9,10,11,12,14,15,17,18,19,20,21,23,24,27:
  @(False_ind … Hlt1) @(False_ind … Hlt2)
| 13,25,26: >cast_identity elim a_sg elim b_sg normalize //
| 22: normalize elim b_sg elim a_sg normalize
      normalize in val;
      elim (vsplit_eq ??? (val⌈Vector bool 32 ↦ Vector bool (16 + 16)⌉))
      [ 2,4,6,8: normalize //
      | 1,3,5,7: #left * #right normalize #Eq1
                 <(vsplit_prod bool 16 16 … Eq1)
                 elim (vsplit_eq ??? (right⌈Vector bool 16 ↦ Vector bool (8 + 8)⌉))
                 [ 2,4,6,8: //
                 | 1,3,5,7: #rightleft * #rightright normalize #Eq2
                            <(vsplit_prod bool 8 8 … Eq2)
                            cut (val = (left @@ rightleft) @@ rightright)
                            [ 1,3,5,7: destruct >(vector_associative_append ? 16 8) //
                            | 2,4,6,8: #Hrewrite destruct
                                       <(vsplit_prod bool 24 8 … Hrewrite) @refl
                            ]
                 ]
     ]
| 16: elim b_sg elim a_sg >cast_collapse @refl
] qed.

lemma cast_composition : ∀a_sz,a_sg, b_sz, b_sg, c_sz, val.
   size_le c_sz a_sz → size_le c_sz b_sz →
   (cast_int_int a_sz a_sg c_sz val = 
        cast_int_int b_sz b_sg c_sz (cast_int_int a_sz a_sg b_sz val)).
#a_sz #a_sg #b_sz #b_sg #c_sz #val #Hle_c_a #Hle_c_b
cases (size_lt_dec c_sz a_sz)
cases (size_lt_dec c_sz b_sz)
[ 1: #Hltb #Hlta @(cast_composition_lt … Hlta Hltb)
| 2: #Hnltb #Hlta 
  cases (size_not_lt_to_ge  … Hnltb)
  [ 1: #Heq destruct >cast_identity //
  | 2: #Hltb @(False_ind … (size_absurd ?? Hle_c_b Hltb))
  ]
| 3: #Hltb #Hnlta  
  cases (size_not_lt_to_ge  … Hnlta)
  [ 1: #Heq destruct >cast_idempotent //
  | 2: #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta))
  ]
| 4: #Hnltb #Hnlta
  cases (size_not_lt_to_ge  … Hnlta)  
  cases (size_not_lt_to_ge  … Hnltb)
  [ 1: #Heq_b #Heq_a destruct >cast_identity >cast_identity //
  | 2: #Hltb #Heq @(False_ind … (size_absurd ?? Hle_c_b Hltb))
  | 3: #Eq #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta))
  | 4: #Hltb #Hlta @(False_ind … (size_absurd ?? Hle_c_a Hlta))
  ]
] qed. 

let rec assert_int_value (v : option val) (expected_size : intsize) : option (BitVector (bitsize_of_intsize expected_size)) ≝
match v with
[ None ⇒ None ?
| Some v ⇒
  match v with
  [ Vint sz i ⇒
    match sz_eq_dec sz expected_size with
    [ inl Heq ⇒ Some ??
    | inr _ ⇒ None ?
    ]
  | _ ⇒ None ?
  ]
].
>Heq in i; #i @i qed.

(* cast_int_int behaves as truncate (≃ vsplit) when downsizing *)
(* ∀src_sz,target_sz,sg. ∀i. size_le target_sz src_sz → cast_int_int src_sz sg target_sz i = truncate *)

lemma vsplit_to_truncate : ∀m,n,i. (\snd  (vsplit bool m n i)) = truncate  m n i.
#m #n #i normalize // qed.

(* Somme lemmas on how "simplifiable" operations behave under cast_int_int. *)

lemma integer_add_cast_lt : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_lt target_sz src_sz →
                               (addition_n (bitsize_of_intsize target_sz)
                                    (cast_int_int src_sz sg target_sz lhs_int)
                                    (cast_int_int src_sz sg target_sz rhs_int)
                             = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)).
#src_sz #target_sz #sg #lhs_int #rhs_int #Hlt                             
elim src_sz in Hlt lhs_int rhs_int; elim target_sz
[ 1,2,3,5,6,9: normalize #H @(False_ind … H)
| *: elim sg #_
  normalize in match (bitsize_of_intsize ?);
  normalize in match (bitsize_of_intsize ?);
  #lint #rint
  normalize in match (cast_int_int ????);
  normalize in match (cast_int_int ????);
  whd in match (addition_n ???);
  whd in match (addition_n ???) in ⊢ (???%);
  >vsplit_to_truncate >vsplit_to_truncate
  <truncate_add_with_carries
  [ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint rint false);
  | 3,4: normalize in match (plus 24 8); generalize in match (add_with_carries ? lint rint false);
  | 5,6: normalize in match (plus 16 16); generalize in match (add_with_carries ? lint rint false);
  ]
  * #result #carry
  normalize nodelta //
qed.

lemma integer_add_cast_eq : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. target_sz = src_sz →
                               (addition_n (bitsize_of_intsize target_sz)
                                    (cast_int_int src_sz sg target_sz lhs_int)
                                    (cast_int_int src_sz sg target_sz rhs_int)
                             = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)).
#src_sz #target_sz #sg #lhs_int #rhs_int #Heq destruct
>cast_identity >cast_identity >cast_identity // qed.

lemma integer_add_cast_le : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_le target_sz src_sz →
                               (addition_n (bitsize_of_intsize target_sz)
                                    (cast_int_int src_sz sg target_sz lhs_int)
                                    (cast_int_int src_sz sg target_sz rhs_int)
                             = cast_int_int src_sz sg target_sz (addition_n (bitsize_of_intsize src_sz) lhs_int rhs_int)).
#src_sz #target_sz #sg #lhs_int #rhs_int #Hle
cases (sz_eq_dec target_sz src_sz)
[ 1: #Heq @(integer_add_cast_eq … Heq)
| 2: #Hneq cut (size_lt target_sz src_sz)
     [ 1: elim target_sz in Hle Hneq; elim src_sz normalize //
           #_ * #H @(H … (refl ??))
     | 2: #Hlt @(integer_add_cast_lt … Hlt)
     ]
] qed.

lemma truncate_eat : ∀l,n,m,v. l = n → ∃tl. truncate (S n) m v = truncate l m tl.
#l #n #m #v #len elim (Vector_Sn … v) #hd * #tl #Heq >len
@(ex_intro … tl)
>Heq >Heq 
elim (vsplit_eq2 … tl) #l * #r #Eq
normalize
 <(vsplit_prod bool n m tl l r Eq)
 <(vsplit_prod2 bool n m tl l r Eq)
 normalize //
qed.


lemma integer_neg_trunc : ∀m,n. ∀i: BitVector (m+n). two_complement_negation n (truncate m n i) = truncate m n (two_complement_negation (m+n) i).
#m elim m
[ 1: #n #i normalize in i; 
     whd in match (truncate ???);
     whd in match (truncate ???) in ⊢ (???%);
     <vsplit_zero <vsplit_zero //
| 2: #m' #Hind #n #i normalize in i;
     elim (Vector_Sn … i) #hd * #tl #Heq     
     whd in match (two_complement_negation (S ?) ?);      
     >Heq in ⊢ (??%?); >truncate_tail whd in match (tail ???) in ⊢ (??%?);
     whd in match (two_complement_negation ??) in ⊢ (??%?);
     lapply (Hind ? tl) #H
     whd in match (two_complement_negation ??) in H;
     (* trying to reduce add_with_carries *)     
     normalize in match (S m'+n);
     whd in match (zero ?) in ⊢ (???%);
     >Heq in match (negation_bv ??) in ⊢ (???%); 
     whd in match (negation_bv ??) in ⊢ (???%);
     >add_with_carries_unfold in ⊢ (???%);
     normalize in ⊢ (???%); 
     cases hd normalize nodelta
     [ 1,2: <add_with_carries_unfold  in ⊢ (???%); (* Good. Some progress. *)
          (* try to transform the rhs of H into what we need. *)     
          whd in match (two_complement_negation ??) in H:(???%);
          lapply H -H
          generalize in match (add_with_carries (m'+n) (negation_bv (m'+n) tl) (zero (m'+n)) true);
          * #Left #Right normalize nodelta
          #H generalize in ⊢ (???(???(????(???(match % with [ _ ⇒ ? | _ ⇒  ?])))));
          #b >(vsplit_to_truncate (S m')) >truncate_tail 
          cases b
          normalize nodelta 
          normalize in match (tail ???); @H
     ]
] qed. (* This was painful. *)
     
lemma integer_sub_cast_lt : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_lt target_sz src_sz →
                               (subtraction (bitsize_of_intsize target_sz)
                                    (cast_int_int src_sz sg target_sz lhs_int)
                                    (cast_int_int src_sz sg target_sz rhs_int)
                             = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)).
#src_sz #target_sz #sg #lhs_int #rhs_int #Hlt                             
elim src_sz in Hlt lhs_int rhs_int; elim target_sz
[ 1,2,3,5,6,9: normalize #H @(False_ind … H)
| *: elim sg #_
  normalize in match (bitsize_of_intsize ?);
  normalize in match (bitsize_of_intsize ?);
  #lint #rint
  normalize in match (cast_int_int ????);
  normalize in match (cast_int_int ????);
  whd in match (subtraction ???);
  whd in match (subtraction ???) in ⊢ (???%);
  >vsplit_to_truncate >vsplit_to_truncate
  >integer_neg_trunc <truncate_add_with_carries
  [ 1,2: normalize in match (plus 8 8); generalize in match (add_with_carries ? lint ? false);
  | 3,4: normalize in match (plus 24 8); generalize in match (add_with_carries ? lint ? false);
  | 5,6: normalize in match (plus 16 16); generalize in match (add_with_carries ? lint ? false);
  ]
  * #result #carry
  normalize nodelta //
qed.

lemma integer_sub_cast_eq : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. target_sz = src_sz →
                               (subtraction (bitsize_of_intsize target_sz)
                                    (cast_int_int src_sz sg target_sz lhs_int)
                                    (cast_int_int src_sz sg target_sz rhs_int)
                             = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)).
#src_sz #target_sz #sg #lhs_int #rhs_int #Heq destruct
>cast_identity >cast_identity >cast_identity //
qed.

lemma integer_sub_cast_le : ∀src_sz,target_sz,sg. ∀lhs_int,rhs_int. size_le target_sz src_sz →
                               (subtraction (bitsize_of_intsize target_sz)
                                    (cast_int_int src_sz sg target_sz lhs_int)
                                    (cast_int_int src_sz sg target_sz rhs_int)
                             = cast_int_int src_sz sg target_sz (subtraction (bitsize_of_intsize src_sz) lhs_int rhs_int)).
#src_sz #target_sz #sg #lhs_int #rhs_int #Hle
cases (sz_eq_dec target_sz src_sz)
[ 1: #Heq @(integer_sub_cast_eq … Heq)
| 2: #Hneq cut (size_lt target_sz src_sz)
     [ 1: elim target_sz in Hle Hneq; elim src_sz normalize //
           #_ * #H @(H … (refl ??))
     | 2: #Hlt @(integer_sub_cast_lt … Hlt)
     ]
] qed.

lemma simplify_int_success_lt : ∀sz,sg,sz',sg',i,i'. (simplify_int sz sz' sg sg' i=Some (bvint sz') i') → size_le  sz' sz.
* #sg * #sg' #i #i' #H whd in H:(??%?); try destruct normalize // qed.

lemma smaller_integer_val_identity : ∀sz,sg,x.
     smaller_integer_val sz sz sg x x.
#sz #sg *
[ 2: #error //
| 1: * #val #trace whd in match (smaller_integer_val ?????);
     #v1 #Hval %{v1} @conj try @conj try @conj //
     elim sz //
] qed.     

(* Inversion on exec_cast *)
lemma exec_cast_inv : ∀castee_val,src_sz,src_sg,cast_sz,cast_sg,m,result.
                         exec_cast m castee_val (Tint src_sz src_sg) (Tint cast_sz cast_sg) = OK ? result →
                         ∃i. castee_val = Vint src_sz i ∧ result = Vint cast_sz (cast_int_int src_sz src_sg cast_sz i).
#castee_val #src_sz #src_sg #cast_sz #cast_sg #m #result
elim castee_val 
[ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ]
[ 2: | *: whd in ⊢ ((??%?) → ?); #Habsurd destruct ]
whd in ⊢ ((??%?) → ?);
cases (sz_eq_dec sz' src_sz)
[ 1: #Heq destruct >intsize_eq_elim_true normalize nodelta #Heq destruct
     %{i}  /2/
| 2: #Hneq >intsize_eq_elim_false; try assumption #H destruct ]
qed.


(* Lemmas related to the Ebinop case *) 

lemma classify_add_int : ∀sz,sg. classify_add (Tint sz sg) (Tint sz sg) = add_case_ii sz sg.
* * // qed.

lemma classify_sub_int : ∀sz,sg. classify_sub (Tint sz sg) (Tint sz sg) = sub_case_ii sz sg.
* * // qed. 

lemma bool_conj_inv : ∀a,b : bool. (a ∧ b) = true → a = true ∧ b = true.
* * normalize #H @conj // qed.

(* Operations where it is safe to use a smaller integer type on the assumption
   that we would cast it down afterwards anyway. *)
definition binop_simplifiable ≝
λop. match op with [ Oadd ⇒ true | Osub ⇒ true | _ ⇒ false ].

(* Inversion principle for integer addition *)
lemma iadd_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r →
                                    ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (addition_n (bitsize_of_intsize dsz) i1 i2)).
#sz #sg #v1 #v2 #m #r
elim v1
[ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ]
whd in ⊢ ((??%?) → ?); normalize nodelta
>classify_add_int normalize nodelta #H destruct 
elim v2 in H;
[ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ]
whd in ⊢ ((??%?) → ?); #H destruct
elim (sz_eq_dec sz' sz'')
[ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/
| 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct
] qed. 

(* Inversion principle for integer subtraction. *)
lemma isub_inv : ∀sz,sg,v1,v2,m,r. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = Some ? r →
                                    ∃dsz,i1,i2. v1 = Vint dsz i1 ∧ v2 = Vint dsz i2 ∧ r = (Vint dsz (subtraction ? i1 i2)).
#sz #sg #v1 #v2 #m #r
elim v1
[ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ]
whd in ⊢ ((??%?) → ?); normalize nodelta
>classify_sub_int normalize nodelta #H destruct 
elim v2 in H;
[ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ]
whd in ⊢ ((??%?) → ?); #H destruct
elim (sz_eq_dec sz' sz'')
[ 1: #Heq destruct >intsize_eq_elim_true in H; #Heq destruct %{sz''} %{i} %{i'} /3/
| 2: #Hneq >intsize_eq_elim_false in H; try assumption #H destruct
] qed.

definition is_int : val → Prop ≝
λv.
match v with
[ Vint _ _ ⇒ True
| _ ⇒ False ].

(* "negative" (in the sense of ¬ Some) inversion principle for integer addition *)
lemma neg_iadd_inv : ∀sz,sg,v1,v2,m. sem_binary_operation Oadd v1 (Tint sz sg) v2 (Tint sz sg) m = None ? →
                                        ¬ (is_int v1) ∨ ¬ (is_int v2) ∨
                                        ∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2.
#sz #sg #v1 #v2 #m
elim v1
[ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ]
[ 2: | *: #_ %1 %1 % #H @H ]
elim v2
[ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ]
[ 2: | *: #_ %1 %2 % #H @H ]
whd in ⊢ ((??%?) → ?); normalize nodelta
>classify_add_int normalize nodelta
elim (sz_eq_dec sz' sz'')
[ 1: #Heq destruct >intsize_eq_elim_true #Habsurd destruct (Habsurd)
| 2: #Hneq >intsize_eq_elim_false try assumption #_ 
     %2 %{sz'} %{sz''} %{i} %{i'} try @conj try @conj //
] qed. 

(* "negative" inversion principle for integer subtraction *)
lemma neg_isub_inv : ∀sz,sg,v1,v2,m. sem_binary_operation Osub v1 (Tint sz sg) v2 (Tint sz sg) m = None ? →
                                        ¬ (is_int v1) ∨ ¬ (is_int v2) ∨
                                        ∃dsz1,dsz2,i1,i2. v1 = Vint dsz1 i1 ∧ v2 = Vint dsz2 i2 ∧ dsz1 ≠ dsz2.
#sz #sg #v1 #v2 #m
elim v1
[ 1: | 2: #sz' #i | 3: #f | 4: #r | 5: #ptr ]
[ 2: | *: #_ %1 %1 % #H @H ]
elim v2
[ 1: | 2: #sz'' #i' | 3: #f' | 4: #r' | 5: #ptr' ]
[ 2: | *: #_ %1 %2 % #H @H ]
whd in ⊢ ((??%?) → ?); normalize nodelta
>classify_sub_int normalize nodelta
elim (sz_eq_dec sz' sz'')
[ 1: #Heq destruct >intsize_eq_elim_true #Habsurd destruct (Habsurd)
| 2: #Hneq >intsize_eq_elim_false try assumption #_ 
     %2 %{sz'} %{sz''} %{i} %{i'} try @conj try @conj //
] qed.


lemma simplifiable_op_inconsistent : ∀op,sz,sg,v1,v2,m. 
   ¬ (is_int v1) → binop_simplifiable op = true → sem_binary_operation op v1 (Tint sz sg) v2 (Tint sz sg) m = None ?.
#op #sz #sg #v1 #v2 #m #H
elim op normalize in match (binop_simplifiable ?); #H destruct
elim v1 in H;
[ 1,6: | 2,7: #sz' #i normalize in ⊢ (% → ?); * #H @(False_ind … (H I)) | 3,8: #f | 4,9: #r | 5,10: #ptr ]
#_
whd in match (sem_binary_operation ??????); normalize nodelta
>classify_add_int normalize nodelta //
>classify_sub_int normalize nodelta //
qed.

notation > "hvbox('let' «ident x,ident y» 'as' ident E ≝ t 'in' s)"
 with precedence 10
for @{ match $t return λx.x = $t → ? with [ mk_Sig ${ident x} ${ident y} ⇒ λ${ident E}.$s ] (refl ? $t) }.

notation > "hvbox('let' « 〈ident x1,ident x2〉, ident y» 'as' ident E, ident F ≝ t 'in' s)"
 with precedence 10
for @{ match $t return λx.x = $t → ? with 
       [ mk_Sig ${fresh a} ${ident y} ⇒ λ${ident E}.
         match ${fresh a} return λx.x = ${fresh a} → ? with
         [ mk_Prod ${ident x1} ${ident x2} ⇒ λ${ident F}. $s ] (refl ? ${fresh a})
       ] (refl ? $t)
      }.

(* This function will make your eyes bleed. You've been warned.
 * Implements a correct-by-construction version of Brian's original cast-removal code. Does so by
 * threading an invariant defined in [simplify_inv], which says roughly "simplification yields either
   what you hoped for, i.e. an integer value of the right size, OR something equivalent to the original
   expression". [simplify_expr] is not to be called directly: simplify inside is the proper wrapper.
 * TODO: proper doc. Some cases are simplifiable. Some type equality tests are maybe dispensable.
 * This function is slightly more conservative than the original one, but this should be incrementally
 * modifiable (replacing calls to simplify_inside by calls to simplify_expr, + proving correction).
 * Also, I think that the proofs are factorizable to a great deal, but I'd rather have something
 * more or less "modular", case-by-case wise.
 *)
let rec simplify_expr (e:expr) (target_sz:intsize) (target_sg:signedness) 
  : Σresult:bool×expr. ∀ge,en,m. simplify_inv ge en m e (\snd result) target_sz target_sg (\fst result) ≝ 
match e return λx. x = e → ? with
[ Expr ed ty ⇒ λHexpr_eq.
  match ed return λx. ed = x → ? with
  [ Econst_int cst_sz i ⇒ λHdesc_eq.
    match ty return λx. x=ty → ? with
    [ Tint ty_sz sg ⇒ λHexprtype_eq.
      (* Ensure that the displayed type size [cst_sz] and actual size [sz] are equal ... *)
      match sz_eq_dec cst_sz ty_sz with
      [ inl Hsz_eq ⇒       
        match type_eq_dec ty (Tint target_sz target_sg) with
        [ inl Hdonothing   ⇒ «〈true, e〉, ?»
        | inr Hdosomething ⇒
          (* Do the actual useful work *)
          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
          [ Some i' ⇒ λHsimpl_eq. 
            «〈true, Expr (Econst_int target_sz i') (Tint target_sz target_sg)〉, ?»
          | None    ⇒ λ_. 
            «〈false, e〉, ?»
          ] (refl ? (simplify_int cst_sz target_sz sg target_sg i))
        ]
      | inr _ ⇒ (* The expression is ill-typed. *)
        «〈false, e〉, ?»
      ]
    | _ ⇒ λ_. 
      «〈false, e〉, ?» 
    ] (refl ? ty)    
  | Ederef e1 ⇒ λHdesc_eq.
      let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in  
      «〈false, Expr (Ederef e2) ty〉, ?»            
  | Eaddrof e1 ⇒ λHdesc_eq.
      let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in
      «〈false, Expr (Eaddrof e2) ty〉, ?»
  | Eunop op e1 ⇒ λHdesc_eq.
     let «e2,Hequiv» as Hsimplify ≝ simplify_inside e1 in
      «〈false, Expr (Eunop op e2) ty〉, ?»
  | Ebinop op lhs rhs ⇒ λHdesc_eq.
      (* Type equality is enforced to prove the equalities needed in return by the invariant. *)
      match binop_simplifiable op 
      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)))
      with
      [ true ⇒ λHop_simplifiable_eq.
        match assert_type_eq ty (typeof lhs) with
        [ OK Hty_eq_lhs ⇒
            match assert_type_eq (typeof lhs) (typeof rhs) with
            [ OK Htylhs_eq_tyrhs ⇒
                let «〈desired_type_lhs, lhs1〉, Hinv_lhs» as Hsimplify_lhs, Hpair_lhs ≝ simplify_expr lhs target_sz target_sg in
                let «〈desired_type_rhs, rhs1〉, Hinv_rhs» as Hsimplify_rhs, Hpair_rhs ≝ simplify_expr rhs target_sz target_sg in
                match desired_type_lhs ∧ desired_type_rhs
                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)))
                with
                [ true ⇒ λHdesired_eq.
                  «〈true, Expr (Ebinop op lhs1 rhs1) (Tint target_sz target_sg)〉, ?»
                | false ⇒ λHdesired_eq.
                  let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in
                  let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in
                  «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?»
                ] (refl ? (desired_type_lhs ∧ desired_type_rhs))
            | Error _ ⇒
                let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in
                let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in
                «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?»  
            ]                   
        | Error _ ⇒
            let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in
            let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in
             «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?»          
        ]
      | false ⇒ λHop_simplifiable_eq.
        let «lhs1, Hequiv_lhs» as Hsimplify_lhs ≝ simplify_inside lhs in
        let «rhs1, Hequiv_rhs» as Hsimplify_rhs ≝ simplify_inside rhs in
          «〈false, Expr (Ebinop op lhs1 rhs1) ty〉, ?»
      ] (refl ? (binop_simplifiable op))
  | Ecast cast_ty castee ⇒ λHdesc_eq.
      match cast_ty return λx. x = cast_ty → ? with
      [ Tint cast_sz cast_sg ⇒ λHcast_ty_eq.
        match type_eq_dec ty cast_ty with
        [ inl Hcast_eq ⇒
          match necessary_conditions cast_sz cast_sg target_sz target_sg
          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)))
          with
          [ true ⇒ λHconditions.
              let «〈desired_type, castee1〉, Hcastee_inv» as Hsimplify1, Hpair1 ≝ simplify_expr castee target_sz target_sg in
              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)) 
              with
              [ true ⇒ λHdesired_eq.
                «〈true, castee1〉, ?»
              | false ⇒ λHdesired_eq.
                let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr castee cast_sz cast_sg in
                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))
                with
                [ true ⇒ λHdesired2_eq.
                  «〈false, castee2〉, ?»
                | false ⇒ λHdesired2_eq.
                  «〈false, Expr (Ecast ty castee2) cast_ty〉, ?»
                ] (refl ? desired_type2)
              ] (refl ? desired_type)
          | false ⇒ λHconditions.
              let «〈desired_type2, castee2〉, Hcast2» as Hsimplify2, Hpair2 ≝ simplify_expr castee cast_sz cast_sg in
              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))
              with
              [ true ⇒ λHdesired2_eq.
                «〈false, castee2〉, ?»
              | false ⇒ λHdesired2_eq.
                «〈false, Expr (Ecast ty castee2) cast_ty〉, ?»
              ] (refl ? desired_type2)
          ] (refl ? (necessary_conditions cast_sz cast_sg target_sz target_sg))
        | inr Hcast_neq ⇒
          (* inconsistent types ... *)
          let «castee1, Hcastee_equiv» as Hsimplify ≝ simplify_inside castee in
          «〈false, Expr (Ecast cast_ty castee1) ty〉, ?»
        ] 
      | _ ⇒ λHcast_ty_eq.
        let «castee1, Hcastee_equiv» as Hsimplify ≝ simplify_inside castee in
        «〈false, Expr (Ecast cast_ty castee1) ty〉, ?»
      ] (refl ? cast_ty)      
  | Econdition cond iftrue iffalse ⇒ λHdesc_eq.
      let «cond1, Hcond_equiv» as Hsimplify ≝ simplify_inside cond in
      match assert_type_eq ty (typeof iftrue) with
      [ OK Hty_eq_iftrue ⇒
          match assert_type_eq (typeof iftrue) (typeof iffalse) with
          [ OK Hiftrue_eq_iffalse ⇒
              let «〈desired_true, iftrue1〉, Htrue_inv» as Hsimplify_iftrue, Hpair_iftrue      ≝ simplify_expr iftrue target_sz target_sg in
              let «〈desired_false, iffalse1〉, Hfalse_inv» as Hsimplify_iffalse, Hpair_iffalse ≝ simplify_expr iffalse target_sz target_sg in         
              match desired_true ∧ desired_false
              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)))
              with
              [ true ⇒ λHdesired_eq.
                «〈true, Expr (Econdition cond1 iftrue1 iffalse1) (Tint target_sz target_sg)〉, ?»
              | false ⇒ λHdesired_eq.
                let «iftrue1, Htrue_equiv» as Hsimplify_iftrue    ≝ simplify_inside iftrue in
                let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in
                «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?»      
              ] (refl ? (desired_true ∧ desired_false))
          | _ ⇒
            let «iftrue1, Htrue_equiv» as Hsimplify_iftrue    ≝ simplify_inside iftrue in
            let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in
            «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?»           
          ]
      | _ ⇒
        let «iftrue1, Htrue_equiv» as Hsimplify_iftrue    ≝ simplify_inside iftrue in
        let «iffalse1, Hfalse_equiv» as Hsimplify_iffalse ≝ simplify_inside iffalse in
        «〈false, Expr (Econdition cond1 iftrue1 iffalse1) ty〉, ?»      
      ]
    (* Could probably do better with these, too. *)
  | Eandbool lhs rhs ⇒ λHdesc_eq.
      let «lhs1, Hlhs_equiv» as Eq1 ≝ simplify_inside lhs in
      let «rhs1, Hrhs_equiv» as Eq2 ≝ simplify_inside rhs in
      «〈false, Expr (Eandbool lhs1 rhs1) ty〉, ?»
  | Eorbool lhs rhs ⇒ λHdesc_eq.
      let «lhs1, Hlhs_equiv» as Eq1 ≝ simplify_inside lhs in
      let «rhs1, Hrhs_equiv» as Eq2 ≝ simplify_inside rhs in
      «〈false, Expr (Eorbool lhs1 rhs1) ty〉,?»
  (* Could also improve Esizeof *)
  | Efield rec_expr f ⇒ λHdesc_eq.
      let «rec_expr1, Hrec_expr_equiv» as Hsimplify ≝ simplify_inside rec_expr in
      «〈false,Expr (Efield rec_expr1 f) ty〉, ?»
  | Ecost l e1 ⇒ λHdesc_eq.
      (* The invariant requires that the toplevel [ty] type matches the type of [e1]. *)
      (* /!\ XXX /!\ We assume that the type of a cost-labelled expr is the type of the underlying expr. *)
      match type_eq_dec ty (typeof e1) with
      [ inl Heq ⇒
        let «〈desired_type, e2〉, Hinv» as Hsimplify, Hpair ≝ simplify_expr e1 target_sz target_sg in
        «〈desired_type, Expr (Ecost l e2) (typeof e2)〉, ?»
      | inr Hneq ⇒
        let «e2, Hexpr_equiv» as Eq ≝ simplify_inside e1 in
        «〈false, Expr (Ecost l e2) ty〉, ?»
      ]                
  | Econst_float f ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?»
(* | Evar id ⇒ λHdesc_eq. «〈false, Expr ed ty〉, ?» *)
  (* In order for the simplification function to be less dymp, we would have to use this line, which would in fact
     require to alter the semantics of [load_value_of_type].  *)
  | Evar id        ⇒ λHdesc_eq. «〈type_eq ty (Tint target_sz target_sg), Expr ed ty〉, ?» 
  | Esizeof t      ⇒ λHdesc_eq. «〈type_eq ty (Tint target_sz target_sg), Expr ed ty〉, ?» 
  ] (refl ? ed)
] (refl ? e)

and simplify_inside (e:expr) : Σresult:expr. conservation e result ≝
match e return λx. x = e → ? with
[ Expr ed ty ⇒ λHexpr_eq.
  match ed return λx. x = ed → ? with
  [ Ederef e1 ⇒ λHdesc_eq.
    let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in
    «Expr (Ederef e2) ty, ?»
  | Eaddrof e1 ⇒ λHdesc_eq.
    let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in
    «Expr (Eaddrof e2) ty, ?»
  | Eunop op e1 ⇒ λHdesc_eq.
    let «e2, Hequiv» as Hsimplify ≝ simplify_inside e1 in
    «Expr (Eunop op e2) ty, ?»
  | Ebinop op lhs rhs ⇒ λHdesc_eq.
    let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in
    let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in
    «Expr (Ebinop op lhs1 rhs1) ty, ?»
  | Ecast cast_ty castee ⇒ λHdesc_eq.
    match type_eq_dec ty cast_ty with
    [ inl Hcast_eq ⇒
       match cast_ty return λx. x = cast_ty → Σresult:expr. conservation e result
       with
       [ Tint cast_sz cast_sg ⇒ λHcast_ty_eq.
          let «〈success, castee1〉, Htrans_inv» as Hsimplify, Hpair ≝ simplify_expr castee cast_sz cast_sg in
          match success return λx. x = success → Σresult:expr. conservation e result
         with
         [ true ⇒ λHsuccess_eq.
           «castee1, ?»
         | false ⇒ λHsuccess_eq.
           «Expr (Ecast cast_ty castee1) ty, ?»
          ] (refl ? success)
       | _ ⇒ λHcast_ty_eq.
          «e, ?»
       ] (refl ? cast_ty)
    | inr Hcast_neq ⇒
       «e, ?»    
    ]    
  | Econdition cond iftrue iffalse ⇒ λHdesc_eq.
    let «cond1, Hequiv_cond» as Eq_cond ≝ simplify_inside cond in
    let «iftrue1, Hequiv_iftrue» as Eq_iftrue ≝ simplify_inside iftrue in
    let «iffalse1, Hequiv_iffalse» as Eq_iffalse ≝ simplify_inside iffalse in
    «Expr (Econdition cond1 iftrue1 iffalse1) ty, ?»    
  | Eandbool lhs rhs ⇒ λHdesc_eq.
    let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in
    let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in
    «Expr (Eandbool lhs1 rhs1) ty, ?»      
  | Eorbool lhs rhs ⇒ λHdesc_eq.
    let «lhs1, Hequiv_lhs» as Eq_lhs ≝ simplify_inside lhs in
    let «rhs1, Hequiv_rhs» as Eq_rhs ≝ simplify_inside rhs in
    «Expr (Eorbool lhs1 rhs1) ty, ?»
  | Efield rec_expr f ⇒ λHdesc_eq.
    let «rec_expr1, Hequiv_rec» as Eq_rec ≝ simplify_inside rec_expr in
    «Expr (Efield rec_expr1 f) ty, ?»    
  | Ecost l e1 ⇒ λHdesc_eq.
    let «e2, Hequiv» as Eq ≝ simplify_inside e1 in
    «Expr (Ecost l e2) ty, ?»       
  | _ ⇒ λHdesc_eq.
    «e, ?»
  ] (refl ? ed)
] (refl ? e).
#ge #en #m
[ 1,3,5,6,7,8,9,10,11,12: %1 try @refl
     cases (exec_expr ge en m e) #res
     try (@(SimOk ???) //)
| 2: @(Inv_coerce_ok ge en m … target_sz target_sg target_sz target_sg) destruct /by refl/
(*
     whd in match (exec_expr ????); >eq_intsize_identity whd
     >sz_eq_identity normalize % [ 1: @conj // | 2: elim target_sz in i; normalize #i @I ]
*)     
| 4: destruct @(Inv_coerce_ok ge en m ???? ty_sz sg) / by refl/
     whd in match (exec_expr ????);
     whd in match (exec_expr ????);
     >eq_intsize_identity >eq_intsize_identity whd
     #v1 #Heq destruct (Heq) %{i'} try @conj try @conj try @conj //
     [ 1: @(simplify_int_implements_cast … Hsimpl_eq)
     | 2: @(simplify_int_success_lt … Hsimpl_eq) ]
| 13: %1 // >Hexpr_eq cases (exec_expr ge en m e) #res
      try (@(SimOk ???) //)
| 14: elim (type_eq_dec ty (Tint target_sz target_sg))
      [ 1: #Heq >Heq >type_eq_identity @(Inv_coerce_ok ??????? target_sz target_sg)
           destruct
           [ 1,2: //
           | 3: @smaller_integer_val_identity ]
      | 2: #Hneq >(type_neq_not_identity … Hneq) %1 // destruct
           @(SimOk ???) //
      ]
| 15: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
    [ 1: (* Proving preservation of the semantics for expressions. *)
      cases Hexpr_sim
      [ 2: (* Case where the evaluation of e1 as an expression fails *)      
        normalize * #err #Hfail >Hfail normalize nodelta @(SimFail ???) /2 by ex_intro/
      | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
        #Hsim %1 * #val #trace normalize #Hstep
        cut (∃ptr. (exec_expr ge en m e1 = OK ? 〈Vptr ptr, trace〉) ∧
                   (load_value_of_type ty m (pblock ptr) (poff ptr) = Some ? val))
        [ 1: lapply Hstep -Hstep
             cases (exec_expr ge en m e1)
             [ 1: * #val' #trace' normalize nodelta
                  cases val' normalize nodelta
                  [ 1,2,3,4: #H1 destruct #H2 destruct #H3 destruct
                  | 5: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *)
                       cases (load_value_of_type ty m (pblock pointer) (poff pointer)) in Heq;
                       normalize nodelta
                       [ 1: #Heq destruct | 2: #val2 #Heq destruct @conj // ]
                  ]
             | 2: normalize nodelta #errmesg #Hcontr destruct
             ]
        | 2: * #e1_ptr * #He1_eq_ptr #Hloadptr
             cut (∃ptr1. (exec_expr ge en m e2 = OK ? 〈Vptr ptr1, trace〉) 
                       ∧ (load_value_of_type ty m (pblock ptr1) (poff ptr1) = Some ? val))
             [ 1: @(ex_intro … e1_ptr) @conj
                  [ 1: @Hsim // | 2: // ]
             | 2: * #e2_ptr * #He2_exec #Hload_e2_ptr
                normalize >He2_exec normalize nodelta >Hload_e2_ptr normalize nodelta @refl
             ]
        ]
     ]
   | 2: (* Proving the preservation of the semantics for lvalues. *)
      cases Hexpr_sim
      [ 2: (* Case where the evaluation of e1 as an lvalue fails *)
        normalize * #err #Hfail >Hfail normalize nodelta @(SimFail ???) /2 by ex_intro/
      | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
        #Hsim %1 * * #block #offset #trace normalize #Hstep        
        cut (∃ptr. (exec_expr ge en m e1 = OK ? 〈Vptr ptr, trace〉) ∧ pblock ptr = block ∧ poff ptr = offset)
        [ 1: lapply Hstep -Hstep
             cases (exec_expr ge en m e1)
             [ 1: * #val' #trace' normalize nodelta
                  cases val' normalize nodelta
                  [ 1,2,3,4: #H1 destruct #H2 destruct #H3 destruct
                  | 5: #pointer #Heq @(ex_intro … pointer) (* @(ex_intro … trace') *)
                       destruct try @conj try @conj //
                  ]
             | 2: normalize nodelta #errmesg #Hcontr destruct
             ] 
        | 2: * #e1_ptr * * #He1_eq_ptr #Hblock #Hoffset
             cut (∃ptr1. (exec_expr ge en m e2 = OK ? 〈Vptr ptr1, trace〉)  ∧ pblock ptr1 = block ∧ poff ptr1 = offset) 
             [ 1: @(ex_intro … e1_ptr) @conj try @conj // @Hsim //
             | 2: * #e2_ptr * * #He2_exec #Hblock #Hoffset
                normalize >He2_exec normalize nodelta //
             ]
        ]
     ]
   ]
| 16: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
    [ 1: (* Proving preservation of the semantics for expressions. *)
      cases Hlvalue_sim
      [ 2: (* Case where the evaluation of e1 as an expression fails *)      
        * #err #Hfail @SimFail whd in match (exec_expr ????); >Hfail normalize nodelta /2 by ex_intro/
      | 1: (* Case where the evaluation of e1 as an expression succeeds (maybe) *)
        #Hsim %1 * #val #trace whd in match (exec_expr ????); #Hstep
        cut (∃block,offset,r,ptype,pc. (exec_lvalue ge en m e1 = OK ? 〈block, offset, trace〉) ∧
                                 (pointer_compat_dec block r = inl ?? pc) ∧
                                 (ty = Tpointer r ptype) ∧
                                  val = Vptr (mk_pointer r block pc offset))
        [ 1: lapply Hstep -Hstep
             cases (exec_lvalue ge en m e1)
             [ 1: * * #block #offset #trace' normalize nodelta
                  cases ty
                  [ 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
                  | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
                  normalize nodelta try (#Heq destruct)
                  @(ex_intro … block) @(ex_intro … offset) @(ex_intro … rg) @(ex_intro … ptr_ty)
                  cases (pointer_compat_dec block rg) in Heq; normalize
                  [ 2: #Hnotcompat #Hcontr destruct
                  | 1: #compat #Heq @(ex_intro … compat) try @conj try @conj try @conj destruct // ]
             | 2: normalize nodelta #errmesg #Hcontr destruct
             ]
        | 2: * #block * #offset * #region * #ptype * #pc * * * #Hexec_lvalue #Hptr_compat #Hty_eq #Hval_eq 
             whd in match (exec_expr ????); >(Hsim … Hexec_lvalue) normalize nodelta destruct normalize nodelta
             >Hptr_compat //
        ]
     ]
    | 2: (* Proving preservation of the semantics of lvalues. *)
         @SimFail /2 by ex_intro/
    ]
| 17: destruct %1 try @refl elim (Hequiv ge en m) * #Hexpr_sim #Hlvalue_sim #Htype_eq
      [ 1: whd in match (exec_expr ge en m (Expr ??));
           whd in match (exec_expr ge en m (Expr ??));
           cases Hexpr_sim           
           [ 2: * #error #Hexec >Hexec normalize nodelta @SimFail /2 by ex_intro/
           | 1: cases (exec_expr ge en m e1)
                [ 2: #error #Hexec normalize nodelta @SimFail /2 by ex_intro/
                | 1: * #val #trace #Hexec
                     >(Hexec ? (refl ? (OK ? 〈val,trace〉)))
                     normalize nodelta @SimOk #a >Htype_eq #H @H
                ]
           ]
      | 2: @SimFail /2 by ex_intro/
      ]
| 18: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_lhs #Hdesired_rhs -Hdesired_eq
      inversion (Hinv_lhs ge en m)
      [ 1: #result_flag_lhs #Hresult_lhs #Htype_lhs #Hsim_expr_lhs #Hsim_lvalue_lhs #Hresult_flag_lhs_eq_true
           #Hinv <Hresult_flag_lhs_eq_true in Hresult_lhs; >Hdesired_lhs #Habsurd destruct
      | 2: #lhs_src_sz #lhs_src_sg #Htype_lhs #Htype_lhs1 #Hsmaller_lhs #Hdesired_type_lhs #_
           inversion (Hinv_rhs ge en m)
           [ 1: #result_flag_rhs #Hresult_rhs #Htype_rhs #Hsim_expr_rhs #Hsim_lvalue_rhs #Hdesired_type_rhs_eq #_
                <Hdesired_type_rhs_eq in Hresult_rhs; >Hdesired_rhs #Habsurd destruct
           | 2: #rhs_src_sz #rhs_src_sg #Htype_rhs #Htype_rhs1 #Hsmaller_rhs #Hdesired_type_rhs #_
                @(Inv_coerce_ok  ge en m … target_sz target_sg lhs_src_sz lhs_src_sg)
                [ 1: >Htype_lhs //
                | 2: //
                | 3: whd in match (exec_expr ??? (Expr ??));
                     whd in match (exec_expr ??? (Expr ??));
                     (* Tidy up the type equations *)
                     >Htype_lhs in Htylhs_eq_tyrhs; >Htype_rhs #Heq destruct
                     lapply Hsmaller_rhs lapply Hsmaller_lhs
                     generalize in match rhs_src_sz; #src_sz 
                     generalize in match rhs_src_sg; #src_sg
                     -Hsmaller_lhs -Hsmaller_rhs -Htype_lhs -Htype_rhs -Hinv_lhs -Hinv_rhs
                     >Htype_lhs1 >Htype_rhs1 -Htype_lhs1 -Htype_rhs1
                     (* Enumerate all the cases for the evaluation of the source expressions ... *)
                     cases (exec_expr ge en m lhs);
                     try // * #val_lhs #trace_lhs normalize nodelta
                     cases (exec_expr ge en m rhs);
                     try // * #val_rhs #trace_rhs normalize nodelta
                     whd in match (m_bind ?????);
                     (* specialize to the actual simplifiable operations. *)
                     cases op in Hop_simplifiable_eq;                     
                     [ 1,2: | *: normalize in ⊢ (% → ?); #H destruct (H) ] #_                     
                     [ 1: lapply (iadd_inv src_sz src_sg val_lhs val_rhs m)
                     | 2: lapply (isub_inv src_sz src_sg val_lhs val_rhs m) ]
                     cases (sem_binary_operation ? val_lhs (Tint src_sz src_sg) val_rhs (Tint src_sz src_sg) m)
                     [ 1,3: #_ #_ #_ normalize @I ]
                     #src_result #Hinversion_src elim (Hinversion_src src_result (refl ? (Some ? src_result)))
                     #src_result_sz * #i1 * #i2 * * #Hval_lhs_eq #Hval_rhs_eq #Hsrc_result_eq
                     whd in match (opt_to_res ???); whd in match (m_bind ?????); normalize nodelta
                     >Hval_lhs_eq >Hval_rhs_eq #Hsmaller_rhs #Hsmaller_lhs
                     whd
                     #result_int #Hsrc_result >Hsrc_result in Hsrc_result_eq; #Hsrc_result_eq             
                     lapply (sym_eq ??? Hsrc_result_eq) -Hsrc_result_eq #Hsrc_result_eq                     
                     cut (src_result_sz = src_sz) [ 1,3: destruct // ] #Hsz_eq
                     lapply Hsmaller_lhs lapply Hsmaller_rhs
                     cases (exec_expr ge en m lhs1) normalize nodelta
                     [ 2,4: destruct #error normalize in ⊢ (% → ?); #H @(False_ind … (H i1 (refl ? (Vint src_sz i1)))) ]
                     * #val_lhs1 #trace_lhs1
                     cases (exec_expr ge en m rhs1)
                     [ 2,4: destruct #error #_ normalize in ⊢ (% → ?); #H @(False_ind … (H i2 (refl ? (Vint src_sz i2)))) ]
                     * #val_rhs1 #trace_rhs1
                     whd in match (m_bind ?????); normalize nodelta
                     [ 1: lapply (neg_iadd_inv target_sz target_sg val_lhs1 val_rhs1 m)
                          lapply (iadd_inv target_sz target_sg val_lhs1 val_rhs1 m)
                     | 2: lapply (neg_isub_inv target_sz target_sg val_lhs1 val_rhs1 m)
                          lapply (isub_inv target_sz target_sg val_lhs1 val_rhs1 m) ]
                     cases (sem_binary_operation ? val_lhs1 (Tint target_sz target_sg) val_rhs1 (Tint target_sz target_sg) m)
                     [ 1,3: destruct #_ #Hneg_inversion elim (Hneg_inversion (refl ? (None ?)))
                            (* Proceed by case analysis on Hneg_inversion to prove the absurdity of this branch *)
                            *
                            [ 1,4: whd in ⊢ (? → % → ?); normalize nodelta
                                   #Habsurd #Hcounterexample elim (Hcounterexample i1 (refl ? (Vint src_sz i1)))
                                   #i * * * #Hlhs1_is_int >Hlhs1_is_int in Habsurd; * #Habsurd
                                   @(False_ind … (Habsurd I))
                            | 2,5: whd in ⊢ (? → ? → % → ?); normalize nodelta
                                   #Habsurd #_ #Hcounterexample elim (Hcounterexample i2 (refl ? (Vint src_sz i2)))
                                   #i * * * #Hlhs1_is_int >Hlhs1_is_int in Habsurd; * #Habsurd
                                   @(False_ind … (Habsurd I))
                            | 3,6: #dsz1 * #dsz2 * #j1 * #j2 * * #Hval_lhs1 #Hval_rhs1 #Hsz_neq
                                   whd in ⊢ (% → % → ?); normalize nodelta
                                   #Hsmaller_lhs #Hsmaller_rhs 
                                   elim (Hsmaller_lhs … i1 (refl ? (Vint src_sz i1))) 
                                   #li * * * #Hval_lhs1_alt #H_lhs_cast_eq #Htrace_eq_lhs #Hsize_le
                                   elim (Hsmaller_rhs … i2 (refl ? (Vint src_sz i2)))
                                   #ri * * * #Hval_rhs1_alt #H_rhs_cast_eq #Htrace_eq_rhs #_
                                   destruct elim Hsz_neq #Habsurd @(Habsurd (refl ? target_sz))
                           ]
                     | 2,4: destruct #result #Hinversion #_ #Hsmaller_lhs #Hsmaller_rhs normalize nodelta
                            elim (Hinversion result (refl ? (Some ? result)))
                            #result_sz * #lhs_int * #rhs_int * * #Hlhs1_eq #Hrhs1_eq #Hop_eq
                            elim (Hsmaller_lhs … i1 (refl ? (Vint src_sz i1))) 
                            #li * * * #Hval_lhs1_alt #H_lhs_cast_eq #Htrace_eq_lhs #Hsize_le
                            elim (Hsmaller_rhs … i2 (refl ? (Vint src_sz i2)))
                            #ri * * * #Hval_rhs1_alt #H_rhs_cast_eq #Htrace_eq_rhs #_
                            destruct
                            [ 1: %{(addition_n (bitsize_of_intsize target_sz)
                                     (cast_int_int src_sz src_sg target_sz i1)
                                     (cast_int_int src_sz src_sg target_sz i2))}
                                 try @conj try @conj try @conj //
                                 >integer_add_cast_le try //
                            | 2: %{(subtraction (bitsize_of_intsize target_sz)
                                    (cast_int_int src_sz src_sg target_sz i1)
                                    (cast_int_int src_sz src_sg target_sz i2))}
                                 try @conj try @conj try @conj //
                                 >integer_sub_cast_le try //
                            ]
                     ] ] ] ]
| 19,20,21,22: destruct %1 try @refl
   elim (Hequiv_lhs ge en m) * #Hexpr_sim_lhs #Hlvalue_sim_lhs #Htype_eq_lhs
   elim (Hequiv_rhs ge en m) * #Hexpr_sim_rhs #Hlvalue_sim_rhs #Htype_eq_rhs
   [ 1,3,5,7: 
      whd in match (exec_expr ????); whd in match (exec_expr ????);
      cases Hexpr_sim_lhs
      [ 2,4,6,8: * #error #Herror >Herror @SimFail /2 by refl, ex_intro/
      | *: cases (exec_expr ge en m lhs)
           [ 2,4,6,8: #error #_ @SimFail /2 by refl, ex_intro/
           | *: * #lval #ltrace #Hsim_lhs normalize nodelta         
                cases Hexpr_sim_rhs
                [ 2,4,6,8: * #error #Herror >Herror @SimFail /2 by refl, ex_intro/
                | *: cases (exec_expr ge en m rhs)
                     [ 2,4,6,8: #error #_  @SimFail /2 by refl, ex_intro/
                     | *: * #rval #rtrace #Hsim_rhs
                          whd in match (exec_expr ??? (Expr (Ebinop ???) ?));
                          >(Hsim_lhs 〈lval,ltrace〉 (refl ? (OK ? 〈lval,ltrace〉)))
                          >(Hsim_rhs 〈rval,rtrace〉 (refl ? (OK ? 〈rval,rtrace〉)))
                          normalize nodelta
                          >Htype_eq_lhs >Htype_eq_rhs
                          @SimOk * #val #trace #H @H
                     ]
                ]
           ]
      ]
   | *: @SimFail /2 by refl, ex_intro/  
   ]
(* Jump to the cast cases *)   
| 23,30,31,32,33,34,35,36: %1 try @refl
  [ 1,4,7,10,13,16,19,22: destruct // ]
  elim (Hcastee_equiv ge en m) * #Hexec_sim #Hlvalue_sim #Htype_eq
  (* exec_expr simulation *)
  [ 1,3,5,7,9,11,13,15: cases Hexec_sim
       [ 2,4,6,8,10,12,14,16: destruct * #error #Hexec_fail @SimFail whd in match (exec_expr ge en m ?);
            >Hexec_fail /2 by refl, ex_intro/
       | 1,3,5,7,9,11,13,15: #Hsim @SimOk * #val #trace <Hexpr_eq >Hdesc_eq
            whd in match (exec_expr ge en m ?); #Hstep
            cut (∃v1. exec_expr ge en m castee = OK ? 〈v1,trace〉
                    ∧ exec_cast m v1 (typeof castee) cast_ty = OK ? val)
            [ 1,3,5,7,9,11,13,15: 
                 lapply Hstep -Hstep cases (exec_expr ge en m castee)
                 [ 2,4,6,8,10,12,14,16: #error1 normalize nodelta #Hcontr destruct
                 | 1,3,5,7,9,11,13,15: * #val1 #trace1 normalize nodelta
                      #Hstep @(ex_intro … val1)
                      cases (exec_cast m val1 (typeof castee) cast_ty) in Hstep;
                      [ 2,4,6,8,10,12,14,16: #error #Hstep normalize in Hstep; destruct
                      | 1,3,5,7,9,11,13,15: #result #Hstep normalize in Hstep; destruct
                           @conj @refl
                      ]
                 ]
            | 2,4,6,8,10,12,14,16: * #v1 * #Hexec_expr #Hexec_cast
                 whd in match (exec_expr ge en m ?);
                 >(Hsim … Hexec_expr ) normalize nodelta
                 <Htype_eq >Hexec_cast //
            ]   
      ]
  | 2,4,6,8,10,12,14,16: destruct  @SimFail /2 by refl, ex_intro/
  ]
| 24: destruct inversion (Hcastee_inv ge en m)
  [ 1: #result_flag #Hresult_flag #Htype_eq #Hexpr_sim #Hlvalue_sim #Hresult_flag_2 
       <Hresult_flag_2 in Hresult_flag; #Hcontr destruct
  | 2: #src_sz #src_sg #Htype_castee #Htype_castee1 #Hsmaller_eval #_ #Hinv_eq
       @(Inv_coerce_ok ??????? cast_sz cast_sg)
       [ 1: // | 2: <Htype_castee1 //
       | 3: whd in match (exec_expr ??? (Expr ??));
            >Htype_castee
            (* Simplify the goal by culling impossible cases, using Hsmaller_val *)
            cases (exec_expr ge en m castee) in Hsmaller_eval;
            [ 2: #error //
            | 1: * #castee_val #castee_trace #Hsmaller normalize nodelta
              lapply (exec_cast_inv castee_val src_sz src_sg cast_sz cast_sg m)
              cases (exec_cast m castee_val (Tint src_sz src_sg) (Tint cast_sz cast_sg))
              [ 2: #error #_ @I
              | 1: #result #Hinversion elim (Hinversion result (refl ? (OK ? result))) 
                   #castee_int * #Hcastee_val_eq #Hresult_eq
                   whd in match (m_bind ?????);
                   #result_int #Hresult_eq2
                   cases (exec_expr ge en m castee1) in Hsmaller;
                   [ 2: #error normalize in ⊢ (% → ?); #Habsurd 
                        @(False_ind … (Habsurd castee_int Hcastee_val_eq))
                   | 1: * #val1 #trace1 whd in ⊢ (% → ?); normalize nodelta
                        #Hsmaller elim (Hsmaller castee_int Hcastee_val_eq)
                        #val1_int * * * #Hval1_eq #Hval1_int_eq #Hcastee_trace_eq 
                        destruct #Hle %{(cast_int_int src_sz src_sg target_sz castee_int)}
                        try @conj try @conj try @conj try //                                                
                        [ 1: @cast_composition ] try assumption
                        elim (necessary_conditions_spec … (sym_eq … Hconditions))
                        [ 2,4: * #Heq >Heq #_ elim target_sz //
                        | 1,3: #Hlt @(size_lt_to_le ?? Hlt) ]
 ] ] ] ] ]
| 25,27: destruct
      inversion (Hcast2 ge en m)
      [ 1,3: (* Impossible case.  *)
           #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #Hresult_contr <Hresult_contr in Hresult;
           #Hcontr destruct
      | 2,4: (* We successfuly cast the expression to the desired type. We can thus get rid of the "cast" itself.
              We did not successfuly cast the subexpression to target_sz, though. *)
           #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #_ #Hinv_eq
           @(Inv_eq ???????) //
           [ 1,4: >Htype_castee2 //
           | 2,5: (* Prove simulation for exec_expr *)
               whd in match (exec_expr ??? (Expr ??));
               cases (exec_expr ge en m castee) in Hsmaller_eval;
               [ 2,4: (* erroneous evaluation of the original expression *)
                     #error #Hsmaller_eval @SimFail @(ex_intro … error) //
               | 1,3: * #val #trace normalize nodelta >Htype_castee
                      lapply (exec_cast_inv val src_sz src_sg cast_sz cast_sg m)
                      cases (exec_cast m val (Tint src_sz src_sg) (Tint cast_sz cast_sg))
                      [ 2,4: #error #_ #_ @SimFail /2 by ex_intro/
                      | 1,3: #result #Hinversion elim (Hinversion result (refl ??))
                             #val_int * #Hval_eq #Hresult_eq
                             cases (exec_expr ge en m castee2)
                             [ 2,4: #error #Hsmaller_eval normalize in Hsmaller_eval; @(False_ind … (Hsmaller_eval val_int Hval_eq))
                             | 1,3: * #val1 #trace1 #Hsmaller elim (Hsmaller val_int Hval_eq)
                                    #val1_int * * * #Hval1_eq #Hcast_eq #Htrace_eq #Hle
                                    destruct @SimOk normalize #a #H @H ]
                ] ]
           | 3,6: @SimFail /2 by refl, ex_intro/
      ] ]
| 26,28: destruct
      inversion (Hcast2 ge en m)
      [ 2,4: (* Impossible case. *)
            #src_sz #src_sg #Htype_castee #Htype_castee2 #Hsmaller_eval #Habsurd #Hinv_eq
            (* Do some gymnastic to transform the Habsurd jmeq into a proper, 'destruct'able eq *)
            letin Habsurd_eq ≝ (jmeq_to_eq ??? Habsurd) lapply Habsurd_eq
            -Habsurd_eq -Habsurd #Habsurd destruct
      | 1,3: (* All our attempts at casting down the expression have failed. We still use the
               resulting expression, as we may have discovered and simplified unrelated casts. *)
            #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #_ #Hinv
            @(Inv_eq ???????) //
            [ 1,3: (* Simulation for exec_expr *)
                 whd in match (exec_expr ??? (Expr ??));
                 whd in match (exec_expr ??? (Expr ??));
                 cases Hsim_expr
                 [ 2,4: * #error #Hexec_err >Hexec_err @SimFail @(ex_intro … error) //
                 | 1,3: #Hexec_ok
                      cases (exec_expr ge en m castee) in Hexec_ok;
                      [ 2,4: #error #Hsim @SimFail normalize nodelta /2/
                      | 1,3: * #val #trace #Hsim normalize nodelta
                           >Htype_eq >(Hsim 〈val,trace〉 (refl ? (OK ? 〈val,trace〉))) normalize nodelta
                           @SimOk #a #H @H
                      ]
                 ]
            | 2,4: @SimFail /2 by refl, ex_intro/
            ]
      ]
| 29: destruct elim (Hcastee_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
      @(Inv_eq ???????) //
      whd in match (exec_expr ??? (Expr ??));
      whd in match (exec_expr ??? (Expr ??));
      [ 1: cases Hsim_expr
           [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by refl, ex_intro/
           | 1: #Hexec_ok @SimOk * #val #trace
                cases (exec_expr ge en m castee) in Hexec_ok;
                [ 2: #error #Habsurd normalize in Habsurd; normalize nodelta #H destruct
                | 1: * #val #trace #Hexec_ok normalize nodelta
                     >(Hexec_ok … 〈val, trace〉 (refl ? (OK ? 〈val, trace〉)))
                     >Htype_eq
                     normalize nodelta #H @H
                ]
           ]
      | 2: @SimFail /2 by refl, ex_intro/
      ]
| 37: destruct elim (bool_conj_inv … Hdesired_eq) #Hdesired_true #Hdesired_false -Hdesired_eq
      inversion (Htrue_inv ge en m)
      [ 1: #result_flag_true #Hresult_true #Htype_true #Hsim_expr_true #Hsim_lvalue_true #Hresult_flag_true_eq_false
           #Hinv <Hresult_flag_true_eq_false in Hresult_true; >Hdesired_true #Habsurd destruct
      | 2: #true_src_sz #true_src_sg #Htype_eq_true #Htype_eq_true1 #Hsmaller_true #_ #Hinv_true 
           inversion (Hfalse_inv ge en m)
           [ 1: #result_flag_false #Hresult_false #Htype_false #Hsim_expr_false #Hsim_lvalue_false #Hresult_flag_false_eq_false
                #Hinv <Hresult_flag_false_eq_false in Hresult_false; >Hdesired_false #Habsurd destruct
           | 2: #false_src_sz #false_src_sg #Htype_eq_false #Htype_eq_false1 #Hsmaller_false #_ #Hinv_false
                >Htype_eq_true @(Inv_coerce_ok ??????? true_src_sz true_src_sg)
                [ 1,2: //
                | 3: whd in match (exec_expr ????); whd in match (exec_expr ??? (Expr ??));
                     elim (Hcond_equiv ge en m) * #Hexec_cond_sim #_ #Htype_cond_eq
                     cases Hexec_cond_sim
                     [ 2: * #error #Herror >Herror normalize @I
                     | 1: cases (exec_expr ge en m cond)
                          [ 2: #error #_ normalize @I
                          | 1: * #cond_val #cond_trace #Hcond_sim 
                               >(Hcond_sim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉)))                               
                               normalize nodelta
                               >Htype_cond_eq
                               cases (exec_bool_of_val cond_val (typeof cond1)) *
                               [ 3,4: normalize //
                               | 1,2: normalize in match (m_bind ?????);
                                      normalize in match (m_bind ?????);
                                      -Hexec_cond_sim -Hcond_sim -cond_val
                                      [ 1: (* true branch taken *)
                                           cases (exec_expr ge en m iftrue) in Hsmaller_true;
                                           [ 2: #error #_ @I
                                           | 1: * #val_true_branch #trace_true_branch #Hsmaller
                                                #val_true_branch #Hval_true_branch lapply Hsmaller -Hsmaller                                                
                                                cases (exec_expr ge en m iftrue1)
                                                [ 2: #error normalize in ⊢ (% → ?); #Hsmaller 
                                                     @(False_ind … (Hsmaller val_true_branch Hval_true_branch))
                                                | 1: * #val_true1_branch #trace_true1_branch #Hsmaller normalize nodelta
                                                     elim (Hsmaller val_true_branch Hval_true_branch)
                                                     #val_true1_int * * * #val_true1_branch #Hval_cast_eq #Htrace_eq #Hle
                                                     %{val_true1_int} try @conj try @conj try @conj //
                                           ] ]
                                     | 2: (* false branch taken. Same proof as above, different arguments ... *) 
                                           cut (false_src_sz = true_src_sz ∧ false_src_sg = true_src_sg)
                                           [ 1: >Htype_eq_true in Hiftrue_eq_iffalse; >Htype_eq_false #Htype_eq
                                                destruct (Htype_eq) @conj @refl ] * #Hsz_eq #Hsg_eq destruct
                                           cases (exec_expr ge en m iffalse) in Hsmaller_false;
                                           [ 2: #error #_ @I
                                           | 1: destruct * #val_false_branch #trace_false_branch #Hsmaller
                                                #val_false_branch #Hval_false_branch lapply Hsmaller -Hsmaller
                                                cases (exec_expr ge en m iffalse1)
                                                [ 2: #error normalize in ⊢ (% → ?); #Hsmaller 
                                                     @(False_ind … (Hsmaller val_false_branch Hval_false_branch))
                                                | 1: * #val_false1_branch #trace_false1_branch #Hsmaller normalize nodelta
                                                     elim (Hsmaller val_false_branch Hval_false_branch)
                                                     #val_false1_int * * * #val_false1_branch #Hval_cast_eq #Htrace_eq #Hle
                                                     %{val_false1_int} try @conj try @conj try @conj //
                                           ] ]
      ] ] ] ] ] ] ]
| 38,39,40: destruct
   elim (Hcond_equiv ge en m) * #Hsim_expr_cond #Hsim_vlalue_cond #Htype_cond_eq
   elim (Htrue_equiv ge en m) * #Hsim_expr_true #Hsim_vlalue_true #Htype_true_eq
   elim (Hfalse_equiv ge en m) * #Hsim_expr_false #Hsim_vlalue_false #Htype_false_eq
   %1 try @refl
   [ 1,3,5: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
            cases (exec_expr ge en m cond) in Hsim_expr_cond;
            [ 2,4,6: #error #_ @SimFail /2 by ex_intro/
            | 1,3,5: * #cond_val #cond_trace normalize nodelta 
                cases (exec_expr ge en m cond1)
                [ 2,4,6: #error *
                         [ 1,3,5: #Hsim lapply (Hsim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉))) 
                                  #Habsurd destruct
                         | *: * #error #Habsurd destruct ]
                | 1,3,5: * #cond_val1 #cond_trace1 *
                         [ 2,4,6: * #error #Habsurd destruct
                         | 1,3,5: #Hsim lapply (Hsim 〈cond_val,cond_trace〉 (refl ? (OK ? 〈cond_val,cond_trace〉)))
                             #Hcond_eq normalize nodelta destruct (Hcond_eq)
                             >Htype_cond_eq cases (exec_bool_of_val cond_val (typeof cond1))
                             [ 2,4,6: #error @SimFail normalize /2 by refl, ex_intro /
                             | 1,3,5: * (* true branch *)
                                [ 1,3,5:
                                 normalize in match (m_bind ?????);
                                 normalize in match (m_bind ?????);
                                 cases Hsim_expr_true
                                 [ 2,4,6: * #error #Hexec_fail >Hexec_fail @SimFail /2 by refl, ex_intro/
                                 | 1,3,5: cases (exec_expr ge en m iftrue)
                                     [ 2,4,6: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/
                                     | 1,3,5: * #val_true #trace_true normalize nodelta #Hsim
                                              >(Hsim 〈val_true,trace_true〉 (refl ? (OK ? 〈val_true,trace_true〉)))
                                              normalize nodelta @SimOk #a #H @H
                                     ]
                                 ]
                             | 2,4,6:
                                 normalize in match (m_bind ?????);
                                 normalize in match (m_bind ?????);                             
                                 cases Hsim_expr_false
                                 [ 2,4,6: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFail /2 by refl, ex_intro/
                                 | 1,3,5: cases (exec_expr ge en m iffalse)
                                     [ 2,4,6: #error #_ normalize nodelta @SimFail /2 by refl, ex_intro/
                                     | 1,3,5: * #val_false #trace_false normalize nodelta #Hsim
                                              >(Hsim 〈val_false,trace_false〉 (refl ? (OK ? 〈val_false,trace_false〉)))
                                              normalize nodelta @SimOk #a #H @H
                                     ]
                                 ]
                               ]
                             ]
                          ]
                ]
            ]
   | 2,4,6: @SimFail /2 by ex_intro/            
   ]
| 41,42: destruct
    elim (Hlhs_equiv ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs
    elim (Hrhs_equiv ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs
    %1 try @refl
    [ 1,3: whd in match (exec_expr ??? (Expr ??));
           whd in match (exec_expr ??? (Expr ??));
           cases Hsim_expr_lhs
           [ 2,4: * #error #Hexec_fail >Hexec_fail normalize nodelta @SimFail /2 by refl, ex_intro/
           | 1,3: cases (exec_expr ge en m lhs) 
              [ 2,4: #error #_ @SimFail /2 by refl, ex_intro/
              | 1,3: * #lhs_val #lhs_trace #Hsim normalize nodelta
                     >(Hsim 〈lhs_val,lhs_trace〉 (refl ? (OK ? 〈lhs_val,lhs_trace〉)))
                     normalize nodelta >Htype_eq_lhs
                     cases (exec_bool_of_val lhs_val (typeof lhs1))
                       [ 2,4: #error normalize @SimFail /2 by refl, ex_intro/
                     | 1,3: * 
                         whd in match (m_bind ?????);
                         whd in match (m_bind ?????);                    
                         [ 2,3: (* lhs evaluates to true *)
                            @SimOk #a #H @H
                         | 1,4: cases Hsim_expr_rhs
                            [ 2,4: * #error #Hexec >Hexec @SimFail /2 by refl, ex_intro/
                            | 1,3: cases (exec_expr ge en m rhs) 
                                [ 2,4: #error #_ @SimFail /2 by refl, ex_intro/
                                | 1,3: * #rhs_val #rhs_trace -Hsim #Hsim
                                       >(Hsim 〈rhs_val,rhs_trace〉 (refl ? (OK ? 〈rhs_val,rhs_trace〉)))
                                       normalize nodelta >Htype_eq_rhs
                                       @SimOk #a #H @H
                                ]
                            ]
                         ]
                      ]
              ]
          ]
   | 2,4:  @SimFail /2 by ex_intro/
   ]
| 43: destruct
      cases (type_eq_dec ty (Tint target_sz target_sg))
      [ 1: #Htype_eq >Htype_eq >type_eq_identity
           @(Inv_coerce_ok ??????? target_sz target_sg)
           [ 1,2: //
           | 3: @smaller_integer_val_identity ]
      | 2: #Hneq >(type_neq_not_identity … Hneq)
           %1 // @SimOk #a #H @H
      ]
| 44: destruct elim (Hrec_expr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
      %1 try @refl
      [ 1: whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
           whd in match (exec_lvalue ????) in Hsim_lvalue;
           whd in match (exec_lvalue' ?????);
           whd in match (exec_lvalue' ?????);
           >Htype_eq
           cases (typeof rec_expr1) normalize nodelta
           [ 2: #sz #sg | 3: #fl | 4: #rg #ty | 5: #rg #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #rg #ty ]
           [ 1,2,3,4,5,8,9: @SimFail /2 by refl, ex_intro/
           | 6,7: cases Hsim_lvalue
              [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/
              | 1,3: cases (exec_lvalue ge en m rec_expr)
                 [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/
                 | 1,3: #a #Hsim >(Hsim a (refl ? (OK ? a)))
                         whd in match (m_bind ?????);
                         @SimOk #a #H @H
                 ]
              ]
           ]
      | 2: whd in match (exec_lvalue ??? (Expr ??)); whd in match (exec_lvalue ??? (Expr ??));
           >Htype_eq
           cases (typeof rec_expr1) normalize nodelta
           [ 2: #sz #sg | 3: #fl | 4: #rg #ty | 5: #rg #ty #n | 6: #tl #ty | 7: #id #fl | 8: #id #fl | 9: #rg #ty ]
           [ 1,2,3,4,5,8,9: @SimFail /2 by refl, ex_intro/
           | 6,7: cases Hsim_lvalue
              [ 2,4: * #error #Herror >Herror normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/
              | 1,3: cases (exec_lvalue ge en m rec_expr)
                 [ 2,4: #error #_ normalize in ⊢ (??%?); @SimFail /2 by refl, ex_intro/
                 | 1,3: #a #Hsim >(Hsim a (refl ? (OK ? a)))
                         whd in match (m_bind ?????);
                         @SimOk #a #H @H
                 ]
              ]
           ]
     ]
| 45: destruct 
   inversion (Hinv ge en m)
   [ 2: #src_sz #src_sg #Htypeof_e1 #Htypeof_e2 #Hsmaller #Hdesired_eq #_
         @(Inv_coerce_ok ??????? src_sz src_sg)
         [ 1: >Htypeof_e1 //
         | 2: >Htypeof_e2 //
         | 3: whd in match (exec_expr ??? (Expr ??));
              whd in match (exec_expr ??? (Expr ??));
              cases (exec_expr ge en m e1) in Hsmaller;
              [ 2: #error normalize //
              | 1: * #val1 #trace1 #Hsmaller #val1_int #Hval1_eq                   
                   cases (exec_expr ge en m e2) in Hsmaller;
                   [ 2: #error normalize in ⊢ (% → ?); #Habsurd @(False_ind … (Habsurd val1_int Hval1_eq))
                   | 1: * #val2 #trace #Hsmaller elim (Hsmaller val1_int Hval1_eq)
                        #val2_int * * * #Hval2_eq #Hcast #Htrace #Hle normalize nodelta
                        %{val2_int} try @conj try @conj try @conj //
                   ]
               ]
         ]
   | 1: #result_flag #Hresult #Htype_eq #Hsim_expr #Hsim_lvalue #Hdesired_typ #_
        >Hresult %1 try @refl
        [ 1: >Htype_eq //
        | 2: whd in match (exec_expr ??? (Expr ??));
             whd in match (exec_expr ??? (Expr ??));
             cases Hsim_expr
             [ 2: * #error #Hexec_error >Hexec_error @SimFail /2 by ex_intro/
             | 1: cases (exec_expr ge en m e1)
                  [ 2: #error #_ @SimFail /2 by ex_intro/
                  | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #He2_exec >He2_exec
                        @SimOk #a #H @H
                  ]
             ]
        | 3: @SimFail /2 by ex_intro/
        ]
   ]
| 46: destruct elim (Hexpr_equiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
      %1 try @refl
      [ 1: whd in match (exec_expr ??? (Expr ??));
           whd in match (exec_expr ??? (Expr ??));
           cases Hsim_expr
           [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
           | 1: cases (exec_expr ge en m e1)
                [ 2: #error #_ @SimFail /2 by ex_intro/
                | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hsim2 >Hsim2 @SimOk #a #H @H ]
           ]
      | 2: @SimFail /2 by ex_intro/ ]
(* simplify_inside cases. Amounts to propagate a simulation result, except for the /cast/ case which actually calls
 * simplify_expr *)      
| 47, 48, 49: (* trivial const_int, const_float and var cases *)
  try @conj try @conj try @refl
  @SimOk #a #H @H
| 50: (* Deref case *) destruct
  elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
  try @conj try @conj
  [ 1: 
    whd in match (exec_expr ??? (Expr ??));
    whd in match (exec_expr ??? (Expr ??));
    whd in match (exec_lvalue' ?????);
    whd in match (exec_lvalue' ?????);  
  | 2:
    whd in match (exec_lvalue ??? (Expr ??));
    whd in match (exec_lvalue ??? (Expr ??));
  ]
  [ 1,2:  
    cases Hsim_expr
    [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
    | 1,3: cases (exec_expr ge en m e1)
         [ 2,4: #error #_ @SimFail /2 by ex_intro/
         | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ]
  | 3: // ]
| 51: (* Addrof *) destruct
  elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
  try @conj try @conj   
  [ 1: 
    whd in match (exec_expr ??? (Expr ??));
    whd in match (exec_expr ??? (Expr ??));
    cases Hsim_lvalue
    [ 2: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/
    | 1: cases (exec_lvalue ge en m e1)
       [ 2: #error #_ @SimFail /2 by ex_intro/
       | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk #a #H @H ] ]
  | 2: @SimFail /2 by ex_intro/
  | 3: // ]
| 52: (* Unop *) destruct
  elim (Hequiv ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
  try @conj try @conj
  [ 1: 
    whd in match (exec_expr ??? (Expr ??));
    whd in match (exec_expr ??? (Expr ??));
    cases Hsim_expr
    [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
    | 1: cases (exec_expr ge en m e1)
         [ 2: #error #_ @SimFail /2 by ex_intro/
         | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H @SimOk
              >Htype_eq #a #H @H ] ]
  | 2: @SimFail /2 by ex_intro/              
  | 3: // ]
| 53: (* Binop *) destruct
  elim (Hequiv_lhs ge en m) * #Hsim_expr_lhs #Hsim_lvalue_lhs #Htype_eq_lhs
  elim (Hequiv_rhs ge en m) * #Hsim_expr_rhs #Hsim_lvalue_rhs #Htype_eq_rhs
  try @conj try @conj
  [ 1: 
    whd in match (exec_expr ??? (Expr ??));
    whd in match (exec_expr ??? (Expr ??));
    cases Hsim_expr_lhs
    [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
    | 1: cases (exec_expr ge en m lhs)
         [ 2: #error #_ @SimFail /2 by ex_intro/
         | 1: #lhs_value #Hsim_lhs cases Hsim_expr_rhs
              [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
              | 1: cases (exec_expr ge en m rhs)
                   [ 2: #error #_ @SimFail /2 by ex_intro/
                   | 1: #rhs_value #Hsim_rhs 
                        lapply (Hsim_lhs lhs_value (refl ? (OK ? lhs_value)))
                        lapply (Hsim_rhs rhs_value (refl ? (OK ? rhs_value)))
                        #Hrhs >Hrhs #Hlhs >Hlhs >Htype_eq_rhs >Htype_eq_lhs
                        @SimOk #a #H @H
                   ]
              ]
         ]
    ]
  | 2: @SimFail /2 by ex_intro/
  | 3: //
  ]
| 54: (* Cast, fallback case *)
  try @conj try @conj try @refl
  @SimOk #a #H @H
| 55: (* Cast, success case *) destruct
  inversion (Htrans_inv ge en m)
  [ 1: (* contradiction *)
       #result_flag #Hresult_flag #Htype_eq #Hsim_epr #Hsim_lvalue #Hresult_flag_true
       <Hresult_flag_true in Hresult_flag; #Habsurd destruct
  | 2: #src_sz #src_sg #Hsrc_type_eq #Htarget_type_eq #Hsmaller #_ #_
       try @conj try @conj try @conj
       [ 1: whd in match (exec_expr ??? (Expr ??));
            cases (exec_expr ge en m castee) in Hsmaller;
            [ 2: #error #_ @SimFail /2 by ex_intro/
            | 1: * #val #trace normalize nodelta >Hsrc_type_eq
                 lapply (exec_cast_inv val src_sz src_sg cast_sz cast_sg m)
                 cases (exec_cast m val ??)
                 [ 2: #error #_ #_ @SimFail /2 by ex_intro/
                 | 1: #result #Hinversion elim (Hinversion result (refl ??)) 
                      #val_int * #Hval_eq #Hcast
                      cases (exec_expr ge en m castee1)
                      [ 2: #error #Habsurd normalize in Habsurd; @(False_ind … (Habsurd val_int Hval_eq))
                      | 1: * #val1 #trace1 #Hsmaller elim (Hsmaller val_int Hval_eq)
                           #val1_int * * * #Hval1_int #Hval18int #Htrace #Hle
                           @SimOk destruct normalize // ]
                      ]
             ]
      | 2: @SimFail /2 by ex_intro/
      | 3: >Htarget_type_eq //
      ]
  ]
| 56: (* Cast, "failure" case *) destruct
  inversion (Htrans_inv ge en m)
  [ 2: (* contradiction *)
       #src_sz #src_sg #Htype_castee #Htype_castee1 #Hsmaller #Habsurd
       lapply (jmeq_to_eq ??? Habsurd) -Habsurd #Herror destruct
  | 1: #result_flag #Hresult_flag #Htype_eq #Hsim_expr #Hsim_lvalue #_ #_
       try @conj try @conj try @conj
       [ 1: whd in match (exec_expr ????);
            whd in match (exec_expr ??? (Expr ??));
            cases Hsim_expr
            [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
            | 1: cases (exec_expr ??? castee)
                 [ 2: #error #_ @SimFail /2 by ex_intro/
                 | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec_ok >Hexec_ok
                       @SimOk >Htype_eq #a #H @H ]
            ]
       | 2: @SimFail /2 by ex_intro/
       | 3: //
       ]
  ]
| 57,58,59,60,61,62,63,64,68:       
  try @conj try @conj try @refl
  @SimOk #a #H @H
| 65: destruct
  elim (Hequiv_cond ge en m) * #Hsim_exec_cond #Hsim_lvalue_cond #Htype_eq_cond
  elim (Hequiv_iftrue ge en m) * #Hsim_exec_true #Hsim_lvalue_true #Htype_eq_true
  elim (Hequiv_iffalse ge en m) * #Hsim_exec_false #Hsim_lvalue_false #Htype_eq_false
  try @conj try @conj
  [ 1: whd in match (exec_expr ??? (Expr ??));
       whd in match (exec_expr ??? (Expr ??));
       cases Hsim_exec_cond
       [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
       | 1: cases (exec_expr ??? cond)
            [ 2: #error #_ @SimFail /2 by ex_intro/
            | 1: * #condb #condtrace #Hcond_sim lapply (Hcond_sim 〈condb, condtrace〉 (refl ? (OK ? 〈condb, condtrace〉)))
                 #Hcond_ok >Hcond_ok >Htype_eq_cond
                 normalize nodelta
                 cases (exec_bool_of_val condb (typeof cond1))
                 [ 2: #error @SimFail /2 by ex_intro/
                 | 1: * whd in match (m_bind ?????); whd in match (m_bind ?????);
                      normalize nodelta
                      [ 1: (* true branch taken *)
                           cases Hsim_exec_true
                           [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
                           | 1: cases (exec_expr ??? iftrue)
                                [ 2: #error #_ @SimFail /2 by ex_intro/
                                | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H
                                     @SimOk #a #H @H
                                ]
                           ]
                      | 2: (* false branch taken *)
                           cases Hsim_exec_false
                           [ 2: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
                           | 1: cases (exec_expr ??? iffalse)
                                [ 2: #error #_ @SimFail /2 by ex_intro/
                                | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H
                                     @SimOk #a #H @H
                                ]
                           ]
                      ]
                ]
           ]
      ]
  | 2: @SimFail /2 by ex_intro/
  | 3: //
  ]
| 66,67: destruct
  elim (Hequiv_lhs ge en m) * #Hsim_exec_lhs #Hsim_lvalue_lhs #Htype_eq_lhs
  elim (Hequiv_rhs ge en m) * #Hsim_exec_rhs #Hsim_lvalue_rhs #Htype_eq_rhs
  try @conj try @conj
  whd in match (exec_expr ??? (Expr ??));
  whd in match (exec_expr ??? (Expr ??));
  [ 1,4: cases Hsim_exec_lhs 
       [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
       | 1,3: cases (exec_expr ??? lhs)
            [ 2,4: #error #_ @SimFail /2 by ex_intro/
            | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hlhs >Hlhs >Htype_eq_lhs
                   normalize nodelta elim a #lhs_val #lhs_trace
                   cases (exec_bool_of_val lhs_val (typeof lhs1))
                   [ 2,4: #error @SimFail /2 by ex_intro/
                   | 1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????);
                        [ 2,3: @SimOk //
                        | 1,4: cases Hsim_exec_rhs
                            [ 2,4: * #error #Hexec_fail >Hexec_fail @SimFail /2 by ex_intro/
                            | 1,3: cases (exec_expr ??? rhs)
                               [ 2,4: #error #_ @SimFail /2 by ex_intro/
                               | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrhs >Hrhs >Htype_eq_rhs
                                    @SimOk #a #H @H
                               ]
                            ]
                        ]
                   ]
             ]
        ]
  | 2,5: @SimFail /2 by ex_intro/
  | 3,6: //
  ]
| 69: (* record field *) destruct
   elim (Hequiv_rec ge en m) * #Hsim_expr #Hsim_lvalue #Htype_eq
   try @conj try @conj   
   whd in match (exec_expr ??? (Expr ??));
   whd in match (exec_expr ??? (Expr ??)); 
   whd in match (exec_lvalue' ??? (Efield rec_expr f) ty);
   whd in match (exec_lvalue' ??? (Efield rec_expr1 f) ty);  
   [ 1: >Htype_eq cases (typeof rec_expr1) normalize nodelta
       [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty'
       | 7: #id #fl | 8: #id #fl | 9: #rg #id ]
       try (@SimFail /2 by ex_intro/)
       cases Hsim_lvalue
       [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/
       | 1,3: cases (exec_lvalue ge en m rec_expr)
            [ 2,4: #error #_ @SimFail /2 by ex_intro/
            | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec >Hexec
                   @SimOk #a #H @H ]
       ]
   | 2: (* Note: identical to previous case. Too lazy to merge and manually shift indices. *)
       >Htype_eq cases (typeof rec_expr1) normalize nodelta
       [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty'
       | 7: #id #fl | 8: #id #fl | 9: #rg #id ]
       try (@SimFail /2 by ex_intro/)
       cases Hsim_lvalue
       [ 2,4: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/
       | 1,3: cases (exec_lvalue ge en m rec_expr)
            [ 2,4: #error #_ @SimFail /2 by ex_intro/
            | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hexec >Hexec
                   @SimOk #a #H @H ]
       ]
   | 3: // ]
| 70: (* cost label *) destruct
   elim (Hequiv ge en m) *  #Hsim_expr #Hsim_lvalue #Htype_eq
   try @conj try @conj
   whd in match (exec_expr ??? (Expr ??));
   whd in match (exec_expr ??? (Expr ??));
   [ 1:
     cases Hsim_expr
     [ 2: * #error #Hexec >Hexec @SimFail /2 by ex_intro/
     | 1: cases (exec_expr ??? e1)
          [ 2: #error #_ @SimFail /2 by ex_intro/
          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #H >H
               @SimOk #a #H @H ]
     ]
   | 2: @SimFail /2 by ex_intro/
   | 3: //
   ]
] qed.

(* Propagate cast simplification through statements and programs. *)

definition simplify_e ≝ λe. pi1 … (simplify_inside e).

let rec simplify_statement (s:statement) : statement ≝
match s with
[ Sskip ⇒ Sskip
| Sassign e1 e2 ⇒ Sassign (simplify_e e1) (simplify_e e2)
| Scall eo e es ⇒ Scall (option_map ?? simplify_e eo) (simplify_e e) (map ?? simplify_e es)
| Ssequence s1 s2 ⇒ Ssequence (simplify_statement s1) (simplify_statement s2)
| Sifthenelse e s1 s2 ⇒ Sifthenelse (simplify_e e) (simplify_statement s1) (simplify_statement s2) (* TODO: try to reduce size of e *)
| Swhile e s1 ⇒ Swhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *)
| Sdowhile e s1 ⇒ Sdowhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *)
| Sfor s1 e s2 s3 ⇒ Sfor (simplify_statement s1) (simplify_e e) (simplify_statement s2) (simplify_statement s3) (* TODO: reduce size of e *)
| Sbreak ⇒ Sbreak
| Scontinue ⇒ Scontinue
| Sreturn eo ⇒ Sreturn (option_map ?? simplify_e eo)
| Sswitch e ls ⇒ Sswitch (simplify_e e) (simplify_ls ls)
| Slabel l s1 ⇒ Slabel l (simplify_statement s1)
| Sgoto l ⇒ Sgoto l
| Scost l s1 ⇒ Scost l (simplify_statement s1)
]
and simplify_ls ls ≝
match ls with
[ LSdefault s ⇒ LSdefault (simplify_statement s)
| LScase sz i s ls' ⇒ LScase sz i (simplify_statement s) (simplify_ls ls')
].

definition simplify_function : function → function ≝
λf. mk_function (fn_return f) (fn_params f) (fn_vars f) (simplify_statement (fn_body f)).

definition simplify_fundef : clight_fundef → clight_fundef ≝
λf. match f with
  [ CL_Internal f ⇒ CL_Internal (simplify_function f)
  | _ ⇒ f
  ].

definition simplify_program : clight_program → clight_program ≝
λp. transform_program … p (λ_.simplify_fundef).

(* Simulation on statement continuations. Stolen from labelSimulation and adapted to our setting. *)
inductive cont_cast : cont → cont → Prop ≝
| cc_stop : cont_cast Kstop Kstop
| cc_seq : ∀s,k,k'. cont_cast k k' → cont_cast (Kseq s k) (Kseq (simplify_statement s) k')
| cc_while : ∀e,s,k,k'.
    cont_cast k k' →
    cont_cast (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k')
| cc_dowhile : ∀e,s,k,k'.
    cont_cast k k' →
    cont_cast (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k')
| cc_for1 : ∀e,s1,s2,k,k'.
    cont_cast k k' →
    cont_cast (Kseq (Sfor Sskip e s1 s2) k) (Kseq (Sfor Sskip (simplify_e e) (simplify_statement s1) (simplify_statement s2)) k')
| cc_for2 : ∀e,s1,s2,k,k'. 
    cont_cast k k' →
    cont_cast (Kfor2 e s1 s2 k) (Kfor2 (simplify_e e) (simplify_statement s1) (simplify_statement s2) k')
| cc_for3 : ∀e,s1,s2,k,k'. 
    cont_cast k k' → 
    cont_cast (Kfor3 e s1 s2 k) (Kfor3 (simplify_e e) (simplify_statement s1) (simplify_statement s2) k')
| cc_switch : ∀k,k'. 
    cont_cast k k' → cont_cast (Kswitch k) (Kswitch k')
| cc_call : ∀r,f,en,k,k'. 
    cont_cast k k' → 
    cont_cast (Kcall r f en k) (Kcall r (simplify_function f) en k').

lemma call_cont_cast : ∀k,k'.
  cont_cast k k' →
  cont_cast (call_cont k) (call_cont k').
#k0 #k0' #K elim K /2/
qed.

inductive state_cast : state → state → Prop ≝
| swc_state : ∀f,s,k,k',e,m. 
  cont_cast k k' →
  state_cast (State f s k e m) (State (simplify_function f) (simplify_statement s ) k' e m)
| swc_callstate : ∀fd,args,k,k',m. 
  cont_cast k k' → state_cast (Callstate fd args k m) (Callstate (simplify_fundef fd) args k' m)
| swc_returnstate : ∀res,k,k',m. 
  cont_cast k k' → state_cast (Returnstate res k m) (Returnstate res k' m)
| swc_finalstate : ∀r. 
  state_cast (Finalstate r) (Finalstate r)
.

record related_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
  rg_find_symbol: ∀s.
    find_symbol ? ge s = find_symbol ? ge' s;
  rg_find_funct: ∀v,f.
    find_funct ? ge v = Some ? f →
    find_funct ? ge' v = Some ? (t f);
  rg_find_funct_ptr: ∀b,f.
    find_funct_ptr ? ge b = Some ? f →
    find_funct_ptr ? ge' b = Some ? (t f)
}.

(* The return type of any function is invariant under cast simplification *)
lemma fn_return_simplify : ∀f. fn_return (simplify_function f) = fn_return f.
// qed.


definition expr_lvalue_ind_combined ≝
λP,Q,ci,cf,lv,vr,dr,ao,uo,bo,ca,cd,ab,ob,sz,fl,co,xx.
conj ??
 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx)
 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx).
 
lemma simulation_transitive : ∀A,r0,r1,r2. res_sim A r0 r1 → res_sim A r1 r2 → res_sim A r0 r2.
#A #r0 #r1 #r2 *
[ 2: * #error #H >H #_ @SimFail /2 by ex_intro/
| 1: cases r0
     [ 2: #error #_ #_ @SimFail /2 by ex_intro/
     | 1: #elt #Hsim lapply (Hsim elt (refl ? (OK ? elt))) #H >H // ]
] qed.

lemma sim_related_globals : ∀ge,ge',en,m. related_globals ? simplify_fundef ge ge' → 
  (∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m e)) ∧
  (∀ed, ty. res_sim ? (exec_lvalue' ge en m ed ty) (exec_lvalue' ge' en m ed ty)).
#ge #ge' #en #m #Hrelated @expr_lvalue_ind_combined
[ 1: #sz #ty #i @SimOk #a normalize //
| 2: #ty #f @SimOk #a normalize //
| 3: * 
    [ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
    | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
    #ty #Hsim_lvalue try //
    whd in match (Plvalue ???);
    whd in match (exec_expr ????);
    whd in match (exec_expr ????);
    cases Hsim_lvalue
    [ 2,4,6: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/
    | *: cases (exec_lvalue' ge en m ? ty)
         [ 2,4,6: #error #_ @SimFail /2 by ex_intro/
         | *: #a #Hsim_lvalue lapply (Hsim_lvalue a (refl ? (OK ? a))) #Hrewrite >Hrewrite
              @SimOk // ]
    ]
| 4: #v #ty whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????);
     cases (lookup SymbolTag block en v) normalize nodelta
     [ 2: #block @SimOk //
     | 1: elim Hrelated #Hsymbol #_ #_ >(Hsymbol v) @SimOk //
     ]
| 5: #e #ty #Hsim_expr whd in match (exec_lvalue' ?????); whd in match (exec_lvalue' ?????);
     cases Hsim_expr
     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     | 1: cases (exec_expr ge en m e)
          [ 2: #error #_ @SimFail /2 by ex_intro/
          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
                @SimOk // ]
     ]
| 6: #ty #ed #ty' #Hsim_lvalue 
     whd in match (exec_expr ????); whd in match (exec_expr ????);
     whd in match (exec_lvalue ????); whd in match (exec_lvalue ????);
     cases Hsim_lvalue
     [ 2: * #error #Hlvalue_fail >Hlvalue_fail @SimFail /2 by ex_intro/
     | 1: cases (exec_lvalue' ge en m ed ty')
         [ 2: #error #_ @SimFail /2 by ex_intro/
         | *: #a #Hsim_lvalue lapply (Hsim_lvalue a (refl ? (OK ? a))) #Hrewrite >Hrewrite
              @SimOk // ]
    ]
| 7: #ty #op #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     cases Hsim
     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     | 1: cases (exec_expr ge en m e)
          [ 2: #error #_ @SimFail /2 by ex_intro/
          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
               @SimOk // ]
     ]
| 8: #ty #op #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     cases Hsim1
     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     | 1: cases (exec_expr ge en m e1)
          [ 2: #error #_ @SimFail /2 by ex_intro/
          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
               cases Hsim2
               [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
               | 1: cases (exec_expr ge en m e2)
                    [ 2: #error #_ @SimFail /2 by ex_intro/
                    | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
                         @SimOk // ]
               ]
          ]
     ]
| 9: #ty #cast_ty #e #Hsim whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     cases Hsim
     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     | 1: cases (exec_expr ge en m e)
          [ 2: #error #_ @SimFail /2 by ex_intro/
          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
               @SimOk // ]
     ] (* mergeable with 7 modulo intros *)
| 10: #ty #e1 #e2 #e3 #Hsim1 #Hsim2 #Hsim3 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     cases Hsim1
     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     | 1: cases (exec_expr ge en m e1)
          [ 2: #error #_ @SimFail /2 by ex_intro/
          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite normalize nodelta
               cases (exec_bool_of_val (\fst a) (typeof e1))
               [ 2: #error @SimFail /2 by ex_intro/
               | 1: *
                    [ 1: (* true branch *) cases Hsim2
                    | 2: (* false branch *) cases Hsim3 ]
                    [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
                    | 1: cases (exec_expr ge en m e2) | 3: cases (exec_expr ge en m e3) ]
                    [ 2,4: #error #_ @SimFail /2 by ex_intro/ 
                    | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite @SimOk // ]
              ]
          ]
     ]
| 11,12: #ty #e1 #e2 #Hsim1 #Hsim2 whd in match (exec_expr ??? (Expr ??)); whd in match (exec_expr ??? (Expr ??));
     cases Hsim1
     [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     | 1,3: cases (exec_expr ge en m e1)
          [ 2,4: #error #_ @SimFail /2 by ex_intro/
          | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite normalize nodelta
                 cases (exec_bool_of_val ??)
                 [ 2,4: #erro @SimFail /2 by ex_intro/
                 | 1,3: * whd in match (m_bind ?????); whd in match (m_bind ?????); 
                        [ 2,3: @SimOk //
                        | 1,4: cases Hsim2
                               [ 2,4: * #error #Hfail >Hfail normalize nodelta @SimFail /2 by ex_intro/
                               | 1,3: cases (exec_expr ge en m e2)
                                      [ 2,4: #error #_ @SimFail /2 by ex_intro/
                                      | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
                                           @SimOk // ]
                               ]
                        ]
                ]
          ]
     ]
| 13: #ty #sizeof_ty @SimOk normalize //
| 14: #ty #e #ty' #field #Hsim_lvalue 
      whd in match (exec_lvalue' ? en m (Efield ??) ty); 
      whd in match (exec_lvalue' ge' en m (Efield ??) ty);
      normalize in match (typeof (Expr ??));
      cases ty' in Hsim_lvalue; normalize nodelta
      [ 2: #sz #sg | 3: #fsz | 4: #rg #ptr_ty | 5: #rg #array_ty #array_sz | 6: #domain #codomain
      | 7: #structname #fieldspec | 8: #unionname #fieldspec | 9: #rg #id ]
      #Hsim_lvalue
      try (@SimFail /2 by ex_intro/)
      normalize in match (exec_lvalue ge en m ?);
      normalize in match (exec_lvalue ge' en m ?);
      cases Hsim_lvalue
      [ 2,4: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
      | 1,3: cases (exec_lvalue' ge en m e ?)
             [ 2,4: #error #_ @SimFail /2 by ex_intro/
             | 1,3: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
                    @SimOk /2 by ex_intro/ ]
      ]
| 15: #ty #lab #e #Hsim 
      whd in match (exec_expr ??? (Expr ??));
      whd in match (exec_expr ??? (Expr ??));
      cases Hsim
     [ 2: * #error #Hfail >Hfail @SimFail /2 by ex_intro/
     | 1: cases (exec_expr ge en m e)
          [ 2: #error #_ @SimFail /2 by ex_intro/
          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
               @SimOk // ]
     ] (* cf case 7, again *)
| 16: *
      [ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
      | 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
      #ty normalize in match (is_not_lvalue ?);
      [ 3,4,13: #Habsurd @(False_ind … Habsurd) ] #_
      @SimFail /2 by ex_intro/
] qed.

lemma related_globals_expr_simulation : ∀ge,ge',en,m. 
  related_globals ? simplify_fundef ge ge' →
  ∀e. res_sim ? (exec_expr ge en m e) (exec_expr ge' en m (simplify_e e)) ∧
      typeof e = typeof (simplify_e e).
#ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?);
cases e #ed #ty cases ed
[ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
| 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
elim (simplify_inside (Expr ??)) #e' #Hconservation whd in Hconservation; @conj lapply (Hconservation ge en m)
* * try //
cases (exec_expr ge en m (Expr ??))
try (#error #_ #_ #_ @SimFail /2 by ex_intro/)
* #val #trace #Hsim_expr #Hsim_lvalue #Htype_eq
try @(simulation_transitive ???? Hsim_expr (proj1 ?? (sim_related_globals ge ge' en m Hrelated) ?))
qed.

lemma related_globals_lvalue_simulation : ∀ge,ge',en,m. 
  related_globals ? simplify_fundef ge ge' →
  ∀e. res_sim ? (exec_lvalue ge en m e) (exec_lvalue ge' en m (simplify_e e)) ∧
      typeof e = typeof (simplify_e e).
#ge #ge' #en #m #Hrelated #e whd in match (simplify_e ?);
cases e #ed #ty cases ed
[ 1: #sz #i | 2: #fl | 3: #id | 4: #e1 | 5: #e1 | 6: #op #e1 | 7: #op #e1 #e2 | 8: #cast_ty #e1
| 9: #cond #iftrue #iffalse | 10: #e1 #e2 | 11: #e1 #e2 | 12: #sizeofty | 13: #e1 #field | 14: #cost #e1 ]
elim (simplify_inside (Expr ??)) #e' #Hconservation whd in Hconservation; @conj lapply (Hconservation ge en m)
* * try //
cases (exec_lvalue ge en m (Expr ??))
try (#error #_ #_ #_ @SimFail /2 by ex_intro/)
* #val #trace #Hsim_expr #Hsim_lvalue #Htype_eq
(* Having to distinguish between exec_lvalue' and exec_lvalue is /ugly/. *)
cases e' in Hsim_lvalue ⊢ %; #ed' #ty' whd in match (exec_lvalue ????); whd in match (exec_lvalue ????);
lapply (proj2 ?? (sim_related_globals ge ge' en m Hrelated) ed' ty') #Hsim_lvalue2 #Hsim_lvalue1
try @(simulation_transitive ???? Hsim_lvalue1 Hsim_lvalue2)
qed.

lemma related_globals_exprlist_simulation : ∀ge,ge',en,m.
related_globals ? simplify_fundef ge ge' →
∀args. res_sim ? (exec_exprlist ge en m args ) (exec_exprlist ge' en m (map expr expr simplify_e args)).
#ge #ge' #en #m #Hrelated #args
elim args
[ 1: /3/
| 2: #hd #tl #Hind normalize
     elim (related_globals_expr_simulation ge ge' en m Hrelated hd)
     *
     [ 2: * #error #Hfail >Hfail #_ @SimFail /2 by refl, ex_intro/
     | 1: cases (exec_expr ge en m hd)
          [ 2: #error #_ #_ @SimFail /2 by refl, ex_intro/
          | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Heq >Heq #Htype_eq >Htype_eq
               cases Hind normalize
               [ 2: * #error #Hfail >Hfail @SimFail /2 by refl, ex_intro/
               | 1: cases (exec_exprlist ??? tl)
                    [ 2: #error #_ @SimFail /2 by refl, ex_intro/
                    | 1: * #values #trace #Hsim lapply (Hsim 〈values, trace〉 (refl ? (OK ? 〈values, trace〉)))
                         #Heq >Heq @SimOk // ]
               ]
          ]
     ]
] qed.

lemma simplify_type_of_fundef_eq : ∀clfd. (type_of_fundef (simplify_fundef clfd)) = (type_of_fundef clfd).
* // qed.

lemma simplify_typeof_eq : ∀ge:genv.∀en:env.∀m:mem. ∀func. typeof (simplify_e func) = typeof func.
#ge #en #m #func whd in match (simplify_e func); elim (simplify_inside func)
#func' #H lapply (H ge en m) * * #_ #_ //
qed.

lemma simplify_fun_typeof_eq : ∀ge:genv.∀en:env.∀m:mem. ∀func. fun_typeof (simplify_e func) = fun_typeof func.
#ge #en #m #func whd in match (simplify_e func); whd in match (fun_typeof ?) in ⊢ (??%%);
>simplify_typeof_eq whd in match (simplify_e func); // qed.

lemma simplify_is_not_skip: ∀s.s ≠ Sskip → ∃pf. is_Sskip (simplify_statement s) = inr … pf.
*
[ 1: * #Habsurd elim (Habsurd (refl ? Sskip))
| *: #a try #b try #c try #d try #e
     whd in match (simplify_statement ?);
     whd in match (is_Sskip ?);
     try /2 by refl, ex_intro/
] qed.

lemma call_cont_simplify : ∀k,k'.
  cont_cast k k' →
  cont_cast (call_cont k) (call_cont k').
#k0 #k0' #K elim K /2/
qed.

lemma simplify_ls_commute : ∀l. (simplify_statement (seq_of_labeled_statement l)) = (seq_of_labeled_statement (simplify_ls l)).
#l @(labeled_statements_ind … l)
[ 1: #default_statement //
| 2: #sz #i #s #tl #Hind
     whd in match (seq_of_labeled_statement ?) in ⊢ (??%?);
     whd in match (simplify_ls ?) in ⊢ (???%);
     whd in match (seq_of_labeled_statement ?) in ⊢ (???%);
     whd in match (simplify_statement ?) in ⊢ (??%?);
     >Hind //
] qed.

lemma select_switch_commute : ∀sz,i,l.
 select_switch sz i (simplify_ls l) = simplify_ls (select_switch sz i l).
#sz #i #l @(labeled_statements_ind … l)
[ 1: #default_statement //
| 2: #sz' #i' #s #tl #Hind
     whd in match (simplify_ls ?) in ⊢ (??%?);
     whd in match (select_switch ???) in ⊢ (??%%);
     cases (sz_eq_dec sz sz')
     [ 1: #Hsz_eq destruct >intsize_eq_elim_true >intsize_eq_elim_true
           cases (eq_bv (bitsize_of_intsize sz') i' i) normalize nodelta
           whd in match (simplify_ls ?) in ⊢ (???%);
           [ 1: // | 2: @Hind ]
     | 2: #Hneq >(intsize_eq_elim_false ? sz sz' ???? Hneq) >(intsize_eq_elim_false ? sz sz' ???? Hneq)
          @Hind
     ]
] qed.

lemma elim_IH_aux :
  ∀lab. ∀s:statement.∀k,k'. cont_cast k k' →
  ∀Hind:(∀k:cont.∀k':cont.
          cont_cast k k' → 
          match find_label lab s k with 
          [ None ⇒ find_label lab (simplify_statement s) k'=None (statement×cont)
          | Some (r:(statement×cont))⇒
            let 〈s',ks〉 ≝r in 
            ∃ks':cont. find_label lab (simplify_statement s) k' = Some (statement×cont) 〈simplify_statement s',ks'〉
                        ∧ cont_cast ks ks']).
  (find_label lab s k = None ? ∧ find_label lab (simplify_statement s) k' = None ?) ∨
  (∃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').
#lab #s #k #k' #Hcont_cast #Hind
lapply (Hind k k' Hcont_cast)
cases (find_label lab s k)
[ 1: normalize nodelta #Heq >Heq /3/
| 2: * #st #kst normalize nodelta * #kst' * #Heq #Hcont_cast' >Heq %2
     %{st} %{kst} %{kst'} @conj try @conj //
] qed.


lemma cast_find_label : ∀lab,s,k,k'.
  cont_cast k k' →
  match find_label lab s k with
  [ Some r ⇒
    let 〈s',ks〉 ≝ r in
    ∃ks'. find_label lab (simplify_statement s) k' = Some ? 〈simplify_statement s', ks'〉
    ∧ cont_cast ks ks'
  | None ⇒
    find_label lab (simplify_statement s) k' = None ?
  ].
#lab #s @(statement_ind2 ? (λls.
    ∀k:cont
    .∀k':cont
     .cont_cast k k'
      →match find_label_ls lab ls k with 
       [None⇒ 
        find_label_ls lab (simplify_ls ls) k' = None ?
       |Some r ⇒
        let 〈s',ks〉 ≝r in 
        ∃ks':cont
        .find_label_ls lab (simplify_ls ls) k'
         =Some (statement×cont) 〈simplify_statement s',ks'〉
         ∧cont_cast ks ks']
) … s)
[ 1: #k #k' #Hcont_cast
     whd in match (find_label ? Sskip ?); normalize nodelta @refl
| 2: #e1 #e2 #k #k' #Hcont_cast
     whd in match (find_label ? (Sassign e1 e2) ?); normalize nodelta @refl
| 3: #e0 #e #args #k #k' #Hcont_cast
     whd in match (find_label ? (Scall e0 e args) ?); normalize nodelta @refl
| 4: #s1 #s2 #Hind_s1 #Hind_s2 #k #k' #Hcont_cast
     whd in match (find_label ? (Ssequence s1 s2) ?); 
     whd in match (find_label ? (simplify_statement (Ssequence s1 s2)) ?); 
     elim (elim_IH_aux lab s1 (Kseq s2 k) (Kseq (simplify_statement s2) k') ? Hind_s1)
     [ 3: try ( @cc_seq // )
     | 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
          normalize nodelta %{kst'} /2/ 
     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
          elim (elim_IH_aux lab s2 k k' Hcont_cast Hind_s2)
          [ 2: * #st * #kst * #kst' * * #Hrewrite2 >Hrewrite2 #Hrewrite3 >Hrewrite3 #Hcont_cast'
               normalize nodelta %{kst'} /2/
          | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
     ] ]  
| 5: #e #s1 #s2 #Hind_s1 #Hind_s2 #k #k' #Hcont_cast
     whd in match (find_label ???);
     whd in match (find_label ? (simplify_statement ?) ?);
     elim (elim_IH_aux lab s1 k k' Hcont_cast Hind_s1)
     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
          normalize nodelta %{kst'} /2/
     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
          elim (elim_IH_aux lab s2 k k' Hcont_cast Hind_s2)
          [ 2: * #st * #kst * #kst' * * #Hrewrite2 >Hrewrite2 #Hrewrite3 >Hrewrite3 #Hcont_cast'
               normalize nodelta %{kst'} /2/
          | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
     ] ]
| 6: #e #s #Hind_s #k #k' #Hcont_cast
     whd in match (find_label ???);
     whd in match (find_label ? (simplify_statement ?) ?);
     elim (elim_IH_aux lab s (Kwhile e s k) (Kwhile (simplify_e e) (simplify_statement s) k') ? Hind_s)
     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
          normalize nodelta %{kst'} /2/
     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
     | 3: @cc_while // ]
| 7: #e #s #Hind_s #k #k' #Hcont_cast
     whd in match (find_label ???);
     whd in match (find_label ? (simplify_statement ?) ?);
     elim (elim_IH_aux lab s (Kdowhile e s k) (Kdowhile (simplify_e e) (simplify_statement s) k') ? Hind_s)
     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
          normalize nodelta %{kst'} /2/
     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
     | 3: @cc_dowhile // ]
| 8: #s1 #cond #s2 #s3 #Hind_s1 #Hind_s2 #Hind_s3 #k #k' #Hcont_cast     
     whd in match (find_label ???);
     whd in match (find_label ? (simplify_statement ?) ?);
     elim (elim_IH_aux lab s1
               (Kseq (Sfor Sskip cond s2 s3) k)
               (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement s2) (simplify_statement s3)) k')
               ? Hind_s1)
     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
          normalize nodelta %{kst'} /2/
     | 3: @cc_for1 //
     | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
          elim (elim_IH_aux lab s3
                    (Kfor2 cond s2 s3 k)
                    (Kfor2 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k')
                      ? Hind_s3)
          [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
                normalize nodelta %{kst'} /2/
          | 3: @cc_for2 //
          | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta
               elim (elim_IH_aux lab s2
                         (Kfor3 cond s2 s3 k)
                         (Kfor3 (simplify_e cond) (simplify_statement s2) (simplify_statement s3) k')
                           ? Hind_s2)
               [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
                    normalize nodelta %{kst'} /2/
               | 3: @cc_for3 //
               | 1: * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 normalize nodelta //
    ] ] ]
| 9,10: #k #k' #Hcont_cast normalize in match (find_label ???); normalize nodelta //
| 11: #e #k #k' #Hcont_cast normalize in match (find_label ???); normalize nodelta //
| 12: #e #ls #Hind #k #k' #Hcont_cast
     whd in match (find_label ???);
     whd in match (find_label ? (simplify_statement ?) ?);
     (* We can't elim the Hind on a list of labeled statements. We must proceed more manually. *)
     lapply (Hind (Kswitch k) (Kswitch k') ?)
     [ 1: @cc_switch //
     | 2: cases (find_label_ls lab ls (Kswitch k)) normalize nodelta
          [ 1: //
          | 2: * #st #kst normalize nodelta // ] ]
| 13: #lab' #s0 #Hind #k #k' #Hcont_cast
     whd in match (find_label ???);
     whd in match (find_label ? (simplify_statement ?) ?);
     cases (ident_eq lab lab') normalize nodelta
     [ 1: #_ %{k'} /2/
     | 2: #_ elim (elim_IH_aux lab s0 k k' Hcont_cast Hind)
          [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
                normalize nodelta %{kst'} /2/
          | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ] 
     ]
| 14: #l #k #k' #Hcont_cast //
| 15: #l #s0 #Hind #k #k' #Hcont_cast
     whd in match (find_label ???);
     whd in match (find_label ? (simplify_statement ?) ?);
     elim (elim_IH_aux lab s0 k k' Hcont_cast Hind)
     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
          normalize nodelta %{kst'} /2/
     | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ]
| 16: #s0 #Hind #k #k' #Hcont_cast
     whd in match (find_label ???);
     whd in match (find_label ? (simplify_statement ?) ?);
     elim (elim_IH_aux lab s0 k k' Hcont_cast Hind)
     [ 2: * #st * #kst * #kst' * * #Hrewrite >Hrewrite #Hrewrite1 >Hrewrite1 #Hcont_cast'
          normalize nodelta %{kst'} /2/
     | 1: * #Heq >Heq #Heq1 >Heq1 normalize nodelta // ]
| 17: #sz #i #s0 #t #Hind_s0 #Hind_ls #k #k' #Hcont_cast
     whd in match (simplify_ls ?);
     whd in match (find_label_ls ???);
     lapply Hind_ls
     @(labeled_statements_ind … t)
     [ 1: #default_case #Hind_ls whd in match (seq_of_labeled_statement ?);
          elim (elim_IH_aux lab s0 
                  (Kseq default_case k) 
                  (Kseq (simplify_statement default_case) k') ? Hind_s0)
         [ 2: * #st * #kst * #kst' * * #Hrewrite #Hrewrite1 #Hcont_cast'
              >Hrewrite >Hrewrite1         
              normalize nodelta whd in match (find_label_ls ???);
              >Hrewrite >Hrewrite1 normalize nodelta
              %{kst'} /2/
         | 3: @cc_seq //
         | 1: * #Hrewrite #Hrewrite1 >Hrewrite normalize nodelta
              lapply (Hind_ls k k' Hcont_cast)
              cases (find_label_ls lab (LSdefault default_case) k)
              [ 1: normalize nodelta #Heq1 
                   whd in match (simplify_ls ?);
                   whd in match (find_label_ls lab ??);
                   whd in match (seq_of_labeled_statement ?);
                   whd in match (find_label_ls lab ??);
                   >Hrewrite1 normalize nodelta @Heq1
              | 2: * #st #kst normalize nodelta #H
                   whd in match (find_label_ls lab ??);
                   whd in match (simplify_ls ?);
                   whd in match (seq_of_labeled_statement ?);
                   >Hrewrite1 normalize nodelta @H
              ]
         ]
     | 2: #sz' #i' #s' #tl' #Hind #A
     
          whd in match (seq_of_labeled_statement ?);
          elim (elim_IH_aux lab s0
                   (Kseq (Ssequence s' (seq_of_labeled_statement tl')) k)
                   (Kseq (simplify_statement (Ssequence s' (seq_of_labeled_statement tl'))) k')
                   ?
                   Hind_s0)
          [ 3: @cc_seq //
          | 1: * #Heq #Heq2 >Heq >Heq2 normalize nodelta
               lapply (A k k' Hcont_cast)
               cases (find_label_ls lab (LScase sz' i' s' tl') k) normalize nodelta
               [ 1: #H whd in match (find_label_ls ???);
                    <simplify_ls_commute
                    whd in match (seq_of_labeled_statement ?);
                    >Heq2 normalize nodelta
                    assumption
               | 2: * #st #kst normalize nodelta #H
                    whd in match (find_label_ls ???);
                    <simplify_ls_commute >Heq2 normalize nodelta @H
               ]
          | 2: * #st * #kst * #kst' * * #Hrewrite #Hrewrite1 #Hcont_cast'
               >Hrewrite normalize nodelta
               %{kst'} @conj try //
               whd in match (find_label_ls ???);
               <simplify_ls_commute >Hrewrite1 //
          ]
    ]
] qed.    
                   
lemma cast_find_label_fn : ∀lab,f,k,k',s,ks.
  cont_cast k k' →
  find_label lab (fn_body f) k = Some ? 〈s,ks〉 →
  ∃ks'. find_label lab (fn_body (simplify_function f)) k' = Some ? 〈simplify_statement s,ks'〉
        ∧ cont_cast ks ks'.
#lab * #rettype #args #vars #body #k #k' #s #ks #Hcont_cast #Hfind_lab
whd in match (simplify_function ?);
lapply (cast_find_label lab body ?? Hcont_cast)
>Hfind_lab normalize nodelta //
qed.

theorem cast_correction : ∀ge, ge'.
  related_globals ? simplify_fundef ge ge' →
  ∀s1, s1', tr, s2. 
  state_cast s1 s1' →
  exec_step ge s1 = Value … 〈tr,s2〉 →
  ∃s2'. exec_step ge' s1' = Value … 〈tr,s2'〉 ∧
        state_cast s2 s2'.
#ge #ge' #Hrelated #s1 #s1' #tr #s2 #Hs1_sim_s1' #Houtcome
inversion Hs1_sim_s1'
[ 1: (* regular state *) 
     #f #stm #k #k' #en #m #Hcont_cast
     lapply (related_globals_expr_simulation ge ge' en m Hrelated) #Hsim_related
     lapply (related_globals_lvalue_simulation ge ge' en m Hrelated) #Hsim_lvalue_related
     cases stm
     (* Perform the intros for the statements*)
     [ 1: | 2: #lhs #rhs | 3: #ret #func #args | 4: #stm1 #stm2 | 5: #cond #iftrue #iffalse | 6: #cond #body
     | 7: #cond #body | 8: #init #cond #step #body | 9,10: | 11: #retval | 12: #cond #switchcases | 13: #lab #body
     | 14: #lab | 15: #cost #body ]
     [ 1: (* Skip *)
          #Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1
          whd in match (exec_step ??); whd in match (exec_step ??);
          inversion Hcont_cast
          [ 1: (* Kstop *)
               #Hk #Hk' #_ >fn_return_simplify cases (fn_return f) normalize nodelta
               [ 1: >Heq_s1 in Hs1_sim_s1'; >Heq_s1' #Hsim inversion Hsim
                    [ 1: #f0 #s #k0 #k0' #e #m0 #Hcont_cast0 #Hstate_eq #Hstate_eq' #_
                         #Eq whd in match (ret ??) in Eq; destruct (Eq) 
                         %{(Returnstate Vundef Kstop (free_list m (blocks_of_env en)))} @conj
                         [ 1: // | 2: %3 %1 ]
                    | 2: #fd #args #k0 #k0' #m0 #Hcont_cast0 #Habsurd destruct (Habsurd)
                    | 3: #res #k0 #k0' #m0 #Hcont_cast #Habsurd destruct (Habsurd)
                    | 4: #r #Habsurd destruct (Habsurd) ]                    
               | 3: #irrelevant #Habsurd destruct
               | 5: #irrelevant1 #irrelevant2 #irrelevant3 #Habsurd destruct
               | *: #irrelevant1 #irrelevant2 #Habsurd destruct ]
          | 2: (* Kseq stm' k' *)
               #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
               whd in match (ret ??) in Eq; destruct (Eq)
               %{(State (simplify_function f) (simplify_statement stm') k0' en m)} @conj
               [ 1: // | 2: %1 // ]               
          | 3: (* Kwhile *)
               #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
               whd in match (ret ??) in Eq; destruct (Eq)               
               %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)} @conj
               [ 1: // | 2: %1 // ]
          | 4: (* Kdowhile *)
               #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
               elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq cases Hsim_cond
               [ 2: * #error #Hfail >Hfail in Eq; #Habsurd normalize in Habsurd; destruct
               | 1: cases (exec_expr ge en m cond) in Eq;
                    [ 2: #error whd in match (m_bind ?????) in ⊢ (% → ?); #Habsurd destruct
                    | 1: * #val #trace whd in match (m_bind ?????) in ⊢ (% → ?); <Htype_cond_eq
                         #Eq #Hsim_cond lapply (Hsim_cond 〈val,trace〉 (refl ? (OK ? 〈val,trace〉))) 
                         #Hrewrite_cond >Hrewrite_cond whd in match (m_bind ?????);
                         (* case analysis on the outcome of the conditional *)
                         cases (exec_bool_of_val val (typeof cond)) in Eq ⊢ %;
                         [ 2: (* evaluation of the conditional fails *)
                              #error normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd)
                         | 1: * whd in match (bindIO ??????); 
                                whd in match (bindIO ??????);
                                #Eq destruct (Eq)
                              [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) (simplify_statement body)) k0' en m)}
                                   @conj [ 1: // | 2: %1 // ]
                              | 2: %{(State (simplify_function f) Sskip k0' en m)}
                                   @conj [ 1: // | 2: %1 // ]
                              ]
                         ]
                    ]
               ]
           | 5,6,7:
                #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
                whd in match (ret ??) in Eq ⊢ %; destruct (Eq)
                [ 1: %{(State (simplify_function f) 
                              (Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body)) 
                               k0' en m)} @conj
                     [ 1: // | 2: %1 // ]
                | 2: %{(State (simplify_function f) 
                              (simplify_statement step) 
                              (Kfor3 (simplify_e cond) (simplify_statement step) (simplify_statement body) k0')
                              en m)} @conj
                     [ 1: // | 2: %1 @cc_for3 // ]
                | 3: %{(State (simplify_function f)
                              (Sfor Sskip (simplify_e cond) (simplify_statement step)
                              (simplify_statement body)) 
                              k0' en m)} @conj
                     [ 1: // | 2: %1 // ]
                ]
           | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ normalize nodelta #Eq
                whd in match (ret ??) in Eq ⊢ %; destruct (Eq)
                %{(State (simplify_function f) Sskip k0' en m)} @conj
                [ 1: // | 2: %1 // ]
           | 9: (* Call *)
                #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ #Eq
                >fn_return_simplify cases (fn_return f) in Eq; normalize nodelta
               [ 1: #Eq whd in match (ret ??) in Eq ⊢ %; destruct (Eq)
                    %{(Returnstate Vundef (Kcall r (simplify_function f0) en0 k0')
                                  (free_list m (blocks_of_env en)))} @conj
                    [ 1: // | 2: %3 @cc_call // ]                                  
               | 3: #irrelevant #Habsurd destruct (Habsurd)
               | 5: #irrelevant1 #irrelevant2 #irrelevant3 #Habsurd destruct (Habsurd)
               | *: #irrelevant1 #irrelevant2 #Habsurd destruct (Habsurd) ]
           ]
     | 2: (* Assign *)
          #Heq_s1 #Heq_s1' #_ lapply Houtcome >Heq_s1
          whd in match (simplify_statement ?); #Heq
          whd in match (exec_step ??) in Heq ⊢ %;
          (* Begin by making the simplify_e disappear using Hsim_related *)
          elim (Hsim_lvalue_related lhs) *
          [ 2: * #error #Hfail >Hfail in Heq; #Habsurd normalize in Habsurd; destruct (Habsurd)
          | 1: cases (exec_lvalue ge en m lhs) in Heq;
               [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
               | 1: * * #block #offset #trace
                    whd in match (bindIO ??????); #Heq #Hsim #Htype_eq_lhs
                    lapply (Hsim 〈block, offset, trace〉 (refl ? (OK ? 〈block, offset, trace〉)))
                    #Hrewrite >Hrewrite -Hrewrite whd in match (bindIO ??????);
                    (* After [lhs], treat [rhs] *)
                    elim (Hsim_related rhs) *
                    [ 2: * #error #Hfail >Hfail in Heq; #Habsurd normalize in Habsurd; destruct (Habsurd)
                    | 1: cases (exec_expr ge en m rhs) in Heq;
                         [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
                         | 1: * #val #trace
                              whd in match (bindIO ??????); #Heq #Hsim #Htype_eq_rhs
                              lapply (Hsim 〈val, trace〉 (refl ? (OK ? 〈val, trace〉)))
                              #Hrewrite >Hrewrite -Hrewrite whd in match (bindIO ??????);
                              <Htype_eq_lhs <Htype_eq_rhs
                              cases (opt_to_io ?????) in Heq;
                              [ 1: #o #resumption whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
                              | 3: #error whd in match (bindIO ??????); #Habsurd destruct (Habsurd)
                              | 2: #mem whd in match (bindIO ??????); #Heq destruct (Heq)
                                   %{(State (simplify_function f) Sskip k' en mem)} @conj
                                   [ 1: // | 2: %1 // ]
                              ]
                         ]
                    ]
               ]
         ]
    | 3: (* Call *)
         #Heq_s1 #Heq_s1' #_  lapply Houtcome >Heq_s1
         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
         whd in match (exec_step ??) in Heq ⊢ %;
         elim (Hsim_related func) in Heq; *
         [ 2: * #error #Hfail >Hfail #Htype_eq #Habsurd normalize in Habsurd; destruct (Habsurd)
         | 1: cases (exec_expr ??? func)
              [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
              | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Heq >Heq #Htype_eq >Htype_eq
                   whd in match (bindIO ??????) in ⊢ (% → %);
                   elim (related_globals_exprlist_simulation ge ge' en m Hrelated args)
                   [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
                   | 1: cases (exec_exprlist ge en m args)
                        [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
                        | 1: #l -Hsim #Hsim lapply (Hsim l (refl ? (OK ? l))) #Heq >Heq
                             whd in match (bindIO ??????) in ⊢ (% → %);
                             elim Hrelated #_ #Hfunct #_ lapply (Hfunct (\fst a))
                             cases (find_funct clight_fundef ge (\fst a));
                             [ 1: #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
                             | 2: #clfd -Hsim #Hsim lapply (Hsim clfd (refl ? (Some ? clfd))) #Heq >Heq
                                  whd in match (bindIO ??????) in ⊢ (% → %);
                                  >simplify_type_of_fundef_eq >(simplify_fun_typeof_eq ge en m)
                                  cases (assert_type_eq (type_of_fundef clfd) (fun_typeof func))
                                  [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
                                  | 1: #Htype_eq cases ret                                     
                                       [ 1: whd in match (bindIO ??????) in ⊢ (% → %);
                                            #Eq destruct (Eq)
                                            %{(Callstate (simplify_fundef clfd) (\fst  l) 
                                                         (Kcall (None (block×offset×type)) (simplify_function f) en k') m)}
                                            @conj
                                            [ 1: // | 2: %2 @cc_call // ]
                                       | 2: #fptr whd in match (bindIO ??????) in ⊢ (% → %); 
                                            elim (Hsim_lvalue_related fptr) *
                                            [ 2: * #error #Hfail >Hfail #_
                                                 #Habsurd normalize in Habsurd; destruct (Habsurd)
                                            | 1: cases (exec_lvalue ge en m fptr)
                                                 [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
                                                 | 1: #a #Hsim #Htype_eq_fptr >(Hsim a (refl ? (OK ? a)))
                                                      whd in match (bindIO ??????) in ⊢ (% → %);
                                                      #Heq destruct (Heq)
                                                      %{(Callstate (simplify_fundef clfd) (\fst  l)
                                                                   (Kcall (Some (block×offset×type) 〈\fst  a,typeof (simplify_e fptr)〉)
                                                                   (simplify_function f) en k') m)}
                                                      @conj [ 1: // | 2: >(simplify_typeof_eq ge en m) %2 @cc_call // ]
        ] ] ] ] ] ] ] ] ]
    | 4: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
         whd in match (exec_step ??) in Heq ⊢ %;
         destruct (Heq)
         %{(State (simplify_function f) (simplify_statement stm1) (Kseq (simplify_statement stm2) k') en m)}
         @conj
         [ 1: // | 2: %1 @cc_seq // ]
    | 5: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
         whd in match (exec_step ??) in Heq ⊢ %;
         elim (Hsim_related cond) in Heq; *
         [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
         | 1: cases (exec_expr ge en m cond)
              [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
              | 1: * #condval #condtrace #Hsim lapply (Hsim 〈condval, condtrace〉 (refl ? (OK ? 〈condval, condtrace〉))) #Heq >Heq
                   #Htype_eq_cond
                   whd in match (bindIO ??????) in ⊢ (% → %);
                   >(simplify_typeof_eq ge en m)
                   cases (exec_bool_of_val condval (typeof cond))
                   [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
                   | 1: * whd in match (bindIO ??????) in ⊢ (% → %); #Heq normalize nodelta in Heq ⊢ %;
                        [ 1: destruct skip (condtrace)
                             %{(State (simplify_function f) (simplify_statement iftrue) k' en m)} @conj
                             [ 1: // | 2: <e0 %1 // ]
                        | 2: destruct skip (condtrace)
                             %{(State (simplify_function f) (simplify_statement iffalse) k' en m)} @conj
                             [ 1: // | 2: <e0 %1 // ]
                        ] ] ] ]
    | 6: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 
         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
         whd in match (exec_step ??) in Heq ⊢ %;
         elim (Hsim_related cond) in Heq; *
         [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
         | 1: cases (exec_expr ge en m cond)
              [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
              | 1: * #condval #condtrace #Hsim lapply (Hsim 〈condval, condtrace〉 (refl ? (OK ? 〈condval, condtrace〉))) #Heq >Heq
                   #Htype_eq_cond
                   whd in match (bindIO ??????) in ⊢ (% → %);
                   >(simplify_typeof_eq ge en m)
                   cases (exec_bool_of_val condval (typeof cond))
                   [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
                   | 1: * whd in match (bindIO ??????) in ⊢ (% → %); #Heq normalize nodelta in Heq ⊢ %;
                        [ 1: destruct skip (condtrace)
                             %{(State (simplify_function f) (simplify_statement body) (Kwhile (simplify_e cond) (simplify_statement body) k') en m)}
                             @conj
                             [ 1: // | 2: <e0 %1 @cc_while // ]
                        | 2: destruct skip (condtrace)
                             %{(State (simplify_function f) Sskip k' en m)} @conj
                             [ 1: // | 2: <e0 %1 // ]
                        ] ] ] ]
    | 7: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
         whd in match (exec_step ??) in Heq ⊢ %;
         destruct (Heq)
         %{(State (simplify_function f) (simplify_statement body)
                  (Kdowhile (simplify_e cond) (simplify_statement body) k') en m)} @conj
         [ 1: // | 2: %1 @cc_dowhile // ]
    | 8: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
         whd in match (exec_step ??) in Heq ⊢ %;
         cases (is_Sskip init) in Heq;
         [ 2: #Hinit_neq_Sskip elim (simplify_is_not_skip init Hinit_neq_Sskip) #pf #Hrewrite >Hrewrite
              normalize nodelta
              whd in match (ret ??) in ⊢ (% → %);
              #Eq destruct (Eq)
              %{(State (simplify_function f) (simplify_statement init)
                       (Kseq (Sfor Sskip (simplify_e cond) (simplify_statement step) (simplify_statement body)) k') en m)} @conj
              [ 1: // | 2: %1 @cc_for1 // ]   
         | 1: #Hinit_eq_Sskip >Hinit_eq_Sskip 
              whd in match (simplify_statement ?);
              whd in match (is_Sskip ?);
              normalize nodelta
              elim (Hsim_related cond) *
              [ 2: * #error #Hfail #_ >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
              | 1: cases (exec_expr ge en m cond)
                   [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
                   | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite #Htype_eq_cond >Hrewrite
                        whd in match (m_bind ?????); whd in match (m_bind ?????);
                        <Htype_eq_cond
                        cases (exec_bool_of_val ? (typeof cond))
                        [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
                        | 1: * whd in match (bindIO ??????); whd in match (bindIO ??????);
                             normalize nodelta #Heq destruct (Heq)
                             [ 1: %{(State (simplify_function f) (simplify_statement body)
                                           (Kfor2 (simplify_e cond) (simplify_statement step) (simplify_statement body) k') en m)}
                                   @conj [ 1: // | 2: %1 @cc_for2 // ]
                             | 2: %{(State (simplify_function f) Sskip k' en m)} @conj
                                  [ 1: // | 2: %1 // ]
         ] ] ] ] ]
    | 9: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
         whd in match (exec_step ??) in Heq ⊢ %;
         inversion Hcont_cast in Heq; normalize nodelta
         [ 1: #Hk #Hk' #_
         | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 
         | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
         | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
         | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 
         | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
         | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ]
         #H whd in match (ret ??) in H ⊢ %;
         destruct (H)
         [ 1,4: %{(State (simplify_function f) Sbreak k0' en m)} @conj [ 1,3: // | 2,4: %1 // ]
         | 2,3,5,6: %{(State (simplify_function f) Sskip k0' en m)} @conj try // %1 // ]
    | 10: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
         whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
         whd in match (exec_step ??) in Heq ⊢ %;
         inversion Hcont_cast in Heq; normalize nodelta
         [ 1: #Hk #Hk' #_
         | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 
         | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
         | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
         | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 
         | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
         | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ]
         #H whd in match (ret ??) in H ⊢ %;
         destruct (H)
         [ 1,4,6: %{(State (simplify_function f) Scontinue k0' en m)} @conj try // %1 //
         | 2: %{(State (simplify_function f) (Swhile (simplify_e cond) (simplify_statement body)) k0' en m)} 
              @conj try // %1 //
         | 3: elim (Hsim_related cond) #Hsim_cond #Htype_cond_eq elim Hsim_cond in H;
              [ 2: * #error #Hfail >Hfail #Habsurd normalize in Habsurd; destruct (Habsurd)
              | 1: cases (exec_expr ??? cond)
                   [ 2: #error #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
                   | 1: #a #Hsim lapply (Hsim a (refl ? (OK ? a))) #Hrewrite >Hrewrite
                        whd in match (m_bind ?????) in ⊢ (% → %);
                        <Htype_cond_eq
                        cases (exec_bool_of_val ? (typeof cond))
                        [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
                        | 1: * whd in match (bindIO ??????); whd in match (bindIO ??????);
                             normalize nodelta #Heq destruct (Heq)
                             [ 1: %{(State (simplify_function f) (Sdowhile (simplify_e cond) (simplify_statement body)) k0' en m)}
                                  @conj [ 1: // | 2: %1 // ]
                             | 2: %{(State (simplify_function f) Sskip k0' en m)}
                                  @conj [ 1: // | 2: %1 // ]
             ] ] ] ]
         | 5: %{(State (simplify_function f) (simplify_statement step)
                       (Kfor3 (simplify_e cond) (simplify_statement step) (simplify_statement body) k0') en m)} @conj
              [ 1: // | 2: %1 @cc_for3 // ]
         ]
    | 11: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
          whd in match (exec_step ??) in Heq ⊢ %;
          cases retval in Heq; normalize nodelta
          [ 1: >fn_return_simplify cases (fn_return f) normalize nodelta
               whd in match (ret ??) in ⊢ (% → %);
               [ 2: #sz #sg | 3: #fl | 4: #rg #ty' | 5: #rg #ty #n | 6: #tl #ty'
               | 7: #id #fl | 8: #id #fl | 9: #rg #id ]
               #H destruct (H)
               %{(Returnstate Vundef (call_cont k') (free_list m (blocks_of_env en)))}
               @conj [ 1: // | 2: %3 @call_cont_simplify // ]
          | 2: #e >fn_return_simplify cases (type_eq_dec (fn_return f) Tvoid) normalize nodelta
               [ 1: #_ #Habsurd destruct (Habsurd)
               | 2: #_ elim (Hsim_related e) *
                    [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
                    | 1: cases (exec_expr ??? e)
                         [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
                         | 1: #a #Hsim #Htype_eq_e lapply (Hsim a (refl ? (OK ? a)))
                              #Hrewrite >Hrewrite
                              whd in match (m_bind ?????); whd in match (m_bind ?????); 
                              #Heq destruct (Heq)
                              %{(Returnstate (\fst  a) (call_cont k') (free_list m (blocks_of_env en)))}
                              @conj [ 1: // | 2: %3 @call_cont_simplify // ]
         ] ] ] ]
    | 12: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
          whd in match (exec_step ??) in Heq ⊢ %;
          elim (Hsim_related cond) in Heq; *
          [ 2: * #error #Hfail >Hfail #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
          | 1: cases (exec_expr ??? cond)
               [ 2: #error #_ #_ #Habsurd normalize in Habsurd; destruct (Habsurd)
               | 1: #a #Hsim #Htype_eq_cond lapply (Hsim a (refl ? (OK ? a)))
                    #Hrewrite >Hrewrite
                    whd in match (bindIO ??????); whd in match (bindIO ??????);
                    cases (\fst a) normalize nodelta
                    [ 1,3,4,5: #a destruct (a) #b destruct (b)
                    | 2: #sz #i whd in match (ret ??) in ⊢ (% → %); #Heq destruct (Heq)
                         %{(State (simplify_function f)
                                  (seq_of_labeled_statement (select_switch sz i (simplify_ls switchcases)))
                                  (Kswitch k') en m)} @conj
                         [ 1: //
                         | 2: @(labeled_statements_ind … switchcases)
                              [ 1: #default_s
                                   whd in match (simplify_ls ?);
                                   whd in match (select_switch sz i ?) in ⊢ (?%%);
                                   whd in match (seq_of_labeled_statement ?) in ⊢ (?%%);
                                   %1 @cc_switch //
                              | 2: #sz' #i' #top_case #tail #Hind
                                   cut ((seq_of_labeled_statement (select_switch sz i (simplify_ls (LScase sz' i' top_case tail))))
                                         = (simplify_statement (seq_of_labeled_statement (select_switch sz i (LScase sz' i' top_case tail)))))
                                   [ 1: >select_switch_commute >simplify_ls_commute @refl
                                   | 2: #Hrewrite >Hrewrite
                                        %1 @cc_switch //
         ] ] ] ] ] ]
    | 13: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
          whd in match (exec_step ??) in Heq ⊢ %;
          destruct (Heq)
          %{(State (simplify_function f) (simplify_statement body) k' en m)}
          @conj %1 //
   | 14: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
          whd in match (exec_step ??) in Heq ⊢ %;
          lapply (cast_find_label_fn lab f (call_cont k) (call_cont k'))
          cases (find_label lab (fn_body f) (call_cont k)) in Heq;
          normalize nodelta
          [ 1: #Habsurd destruct (Habsurd)
          | 2: * #st #kst normalize nodelta
               #Heq whd in match (ret ??) in Heq;
               #H lapply (H st kst (call_cont_simplify ???) (refl ? (Some ? 〈st,kst〉))) try //
               * #kst' * #Heq2 #Hcont_cast' >Heq2 normalize nodelta
               destruct (Heq)
               %{(State (simplify_function f) (simplify_statement st) kst' en m)} @conj
               [ 1: // | 2: %1 // ]
          ]
   | 15: #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
          whd in match (simplify_statement ?) in Heq ⊢ %; #Heq
          whd in match (exec_step ??) in Heq ⊢ %;
          destruct (Heq)                    
          %{(State (simplify_function f) (simplify_statement body) k' en m)}
          @conj
          [ 1: // | 2: %1 // ]
   ]
| 2: (* Call state *)
     #fd #args #k #k' #m #Hcont_cast #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     whd in match (exec_step ??) in ⊢ (% → %);
     elim fd in Heq_s1'; normalize nodelta
     [ 1: * #rettype #args #vars #body #Heq_s1'
          whd in match (simplify_function ?);
          cases (exec_alloc_variables empty_env ??)
          #local_env #new_mem normalize nodelta
          cases (exec_bind_parameters ????)
          [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
          | 1: #new_mem_init
               whd in match (m_bind ?????); whd in match (m_bind ?????);
                #Heq destruct (Heq)               
                %{(State (mk_function rettype args vars (simplify_statement body))
                         (simplify_statement body) k' local_env new_mem_init)} @conj
                [ 1: // | 2: %1 // ]
          ]
     | 2: #id #argtypes #rettype #Heq_s1'
          cases (check_eventval_list args ?)
          [ 2: #error #Habsurd normalize in Habsurd; destruct (Habsurd)
          | 1: #l whd in match (m_bind ?????); whd in match (m_bind ?????);
          #Habsurd destruct (Habsurd) ]
     ]
| 3: (* Return state *)              
     #res #k #k' #m #Hcont_cast #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome;
     whd in match (exec_step ??) in ⊢ (% → %);
     inversion Hcont_cast 
     [ 1: #Hk #Hk' #_
     | 2: #stm' #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_ 
     | 3: #cond #body #k0 #k0' #Hconst_cast0 #Hind #Hk #Hk' #_
     | 4: #cond #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     | 5,6,7: #cond #step #body #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_ 
     | 8: #k0 #k0' #Hcont_cast0 #Hind #Hk #Hk' #_
     | 9: #r #f0 #en0 #k0 #k0' #Hcont_cast #Hind #Hk #Hk' #_ ]
     normalize nodelta
     [ 1: cases res normalize nodelta
          [ 2: * normalize nodelta #i 
               [ 3: #Heq whd in match (ret ??) in Heq; destruct (Heq)
                    %{(Finalstate i)} @conj [ 1: // | 2: // ]
               | * : #Habsurd destruct (Habsurd) ]
          | *: #a try #b destruct ]
     | 9: elim r normalize nodelta
          [ 2: * * #block #offset #typ normalize nodelta
               cases (opt_to_io io_out io_in mem ? (store_value_of_type' ????))
               [ 2: #mem whd in match (m_bind ?????); whd in match (m_bind ?????);
                    #Heq destruct (Heq)
                    %{(State (simplify_function f0) Sskip k0' en0 mem)} @conj
                    [ 1: // | 2: %1 // ]
               | 1: #output #resumption
                    whd in match (m_bind ?????); #Habsurd destruct (Habsurd)
               | 3: #eror #Habsurd normalize in Habsurd; destruct (Habsurd) ]
          | 1: #Heq whd in match (ret ??) in Heq; destruct (Heq)
               %{(State (simplify_function f0) Sskip k0' en0 m)} @conj
               [ 1: // | 2: %1 // ]
          ]
     | *: #Habsurd destruct (Habsurd) ]
| 4: (* Final state *)
     #r #Heq_s1 #Heq_s1' #_ >Heq_s1 in Houtcome; 
     whd in match (exec_step ??) in ⊢ (% → %);
     #Habsurd destruct (Habsurd)
]